0 00:00:00,000 --> 00:00:30,000 Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/2095 Thanks! 1 00:00:00,620 --> 00:00:02,089 Hello, and welcome back to the 2 00:00:02,090 --> 00:00:03,019 functional. 3 00:00:03,020 --> 00:00:05,479 Our next speaker will be Rajeev Cary. 4 00:00:05,480 --> 00:00:07,429 Until last year, he was a professor at 5 00:00:07,430 --> 00:00:09,619 the Australian National University, and 6 00:00:09,620 --> 00:00:11,569 his talk will be about how the counting 7 00:00:11,570 --> 00:00:14,269 of elections with complex voting schemes. 8 00:00:14,270 --> 00:00:16,909 If that happens electronically and 9 00:00:16,910 --> 00:00:19,099 and verifiably 10 00:00:19,100 --> 00:00:21,199 after the talk, there will be a Q&A 11 00:00:21,200 --> 00:00:23,479 session, a live session here 12 00:00:23,480 --> 00:00:25,849 to ask questions, post them in 13 00:00:25,850 --> 00:00:27,949 the eye, see and channel 14 00:00:27,950 --> 00:00:30,049 a hashtag RC three 15 00:00:30,050 --> 00:00:32,989 Dash fan in the rocket chat at 16 00:00:32,990 --> 00:00:35,249 Hashtag FEMM and in the 17 00:00:35,250 --> 00:00:37,399 videos and Twitter with the 18 00:00:37,400 --> 00:00:39,619 hashtag. Are you three fam without 19 00:00:39,620 --> 00:00:40,529 the dash? 20 00:00:40,530 --> 00:00:42,199 If you're in the rotation for a shower, 21 00:00:42,200 --> 00:00:44,629 give this animal that song on missed 22 00:00:44,630 --> 00:00:46,729 in that play out and also 23 00:00:46,730 --> 00:00:48,829 fun translated of F, a native 24 00:00:48,830 --> 00:00:51,169 of translated tombstone or I'm content. 25 00:00:51,170 --> 00:00:52,309 Then we're talking about that talent to 26 00:00:52,310 --> 00:00:54,380 hunt and now enjoy the talk. 27 00:00:55,580 --> 00:00:56,599 Hello, everybody. 28 00:00:56,600 --> 00:00:57,740 My name is Rajeev. 29 00:00:59,420 --> 00:01:01,729 I used to be a full professor at the 30 00:01:01,730 --> 00:01:03,889 Australian National University and now 31 00:01:03,890 --> 00:01:06,049 emeritus, and this 32 00:01:06,050 --> 00:01:08,269 is joint work with Millard 33 00:01:08,270 --> 00:01:10,459 Galli, who was a PhD student 34 00:01:10,460 --> 00:01:13,009 with us until a couple of years ago 35 00:01:13,010 --> 00:01:15,439 and patents and who is an associate 36 00:01:15,440 --> 00:01:16,759 professor at the end. 37 00:01:16,760 --> 00:01:18,859 You just 38 00:01:18,860 --> 00:01:21,139 before I go ahead, all of the 39 00:01:21,140 --> 00:01:23,209 stuff that I'm talking about, the code 40 00:01:23,210 --> 00:01:25,339 and the verification and the proofs 41 00:01:25,340 --> 00:01:27,499 are available here if you want 42 00:01:27,500 --> 00:01:28,500 them. 43 00:01:29,300 --> 00:01:31,639 Okay, so what 44 00:01:31,640 --> 00:01:32,599 am I going to talk about? 45 00:01:32,600 --> 00:01:35,299 I'm going to talk about a way 46 00:01:35,300 --> 00:01:37,010 that we can. 47 00:01:38,080 --> 00:01:39,080 Count. 48 00:01:39,920 --> 00:01:42,739 Complex voting schemes, 49 00:01:42,740 --> 00:01:44,839 for example, the single transferable 50 00:01:44,840 --> 00:01:47,509 voting scheme by computer, 51 00:01:47,510 --> 00:01:49,340 but in a way so that 52 00:01:50,390 --> 00:01:53,029 the results are both formally 53 00:01:53,030 --> 00:01:55,279 and publicly verifiable 54 00:01:55,280 --> 00:01:57,519 by pretty much anybody. 55 00:01:57,520 --> 00:02:00,139 Okay, so 56 00:02:00,140 --> 00:02:01,900 this is the overview. 57 00:02:03,110 --> 00:02:04,519 First of all, I'm going to talk a little 58 00:02:04,520 --> 00:02:06,699 bit about what in doing verifiable into 59 00:02:06,700 --> 00:02:08,419 and verify abilities in 60 00:02:09,530 --> 00:02:12,259 electronic voting as it's known. 61 00:02:12,260 --> 00:02:13,549 Then I'll explain what single 62 00:02:13,550 --> 00:02:15,799 transferable voting is. 63 00:02:15,800 --> 00:02:17,899 Then I'll explain the parlous 64 00:02:17,900 --> 00:02:19,759 situation of computer counting in 65 00:02:19,760 --> 00:02:21,169 Australia. 66 00:02:21,170 --> 00:02:22,939 Then I'll explain a little bit about how 67 00:02:22,940 --> 00:02:25,139 interactive theorem proving works and 68 00:02:25,140 --> 00:02:28,009 then the work that we did in more detail. 69 00:02:28,010 --> 00:02:30,259 Now there's a lot of stuff here. 70 00:02:30,260 --> 00:02:32,419 And so I'm I need to 71 00:02:32,420 --> 00:02:34,729 give a flavor of 72 00:02:34,730 --> 00:02:36,949 everything rather than going 73 00:02:36,950 --> 00:02:39,049 to the depth of the details. 74 00:02:39,050 --> 00:02:40,909 So I hope you'll bear with me, and I'm 75 00:02:40,910 --> 00:02:42,829 more than happy to answer any questions 76 00:02:42,830 --> 00:02:45,679 you have in the chat session afterwards. 77 00:02:45,680 --> 00:02:46,680 So let's get going. 78 00:02:48,650 --> 00:02:51,139 So in electronic voting, 79 00:02:51,140 --> 00:02:53,479 the gold standard is 80 00:02:53,480 --> 00:02:55,699 known as end in 81 00:02:55,700 --> 00:02:58,279 verifiability, and 82 00:02:58,280 --> 00:03:00,529 the way that they achieve it 83 00:03:00,530 --> 00:03:02,689 is by three 84 00:03:02,690 --> 00:03:04,789 steps which sort of feed into 85 00:03:04,790 --> 00:03:05,989 each other. 86 00:03:05,990 --> 00:03:08,239 So the first one is called cast 87 00:03:08,240 --> 00:03:10,459 as intended, and the idea 88 00:03:10,460 --> 00:03:12,649 is that a voter should 89 00:03:12,650 --> 00:03:14,839 be able to verify in some 90 00:03:14,840 --> 00:03:17,209 way that the electronic ballot 91 00:03:17,210 --> 00:03:19,339 that he or she is casting 92 00:03:19,340 --> 00:03:21,739 is actually what they intended. 93 00:03:21,740 --> 00:03:24,319 Right. So the idea here is to mimic 94 00:03:24,320 --> 00:03:26,719 a paper ballot, you know, because 95 00:03:26,720 --> 00:03:28,489 when you put a paper ballot in the box, 96 00:03:28,490 --> 00:03:29,929 you know exactly what you're putting in 97 00:03:29,930 --> 00:03:30,919 the box. 98 00:03:30,920 --> 00:03:33,439 But when you do electronic 99 00:03:33,440 --> 00:03:35,149 voting via some sort of computer 100 00:03:35,150 --> 00:03:37,369 terminal, you don't necessarily 101 00:03:37,370 --> 00:03:39,139 know what the computer is actually 102 00:03:39,140 --> 00:03:40,610 casting on your behalf. 103 00:03:41,810 --> 00:03:43,879 And so as intended is 104 00:03:43,880 --> 00:03:46,459 to make sure that your 105 00:03:46,460 --> 00:03:48,499 the electronic ballot really is what you 106 00:03:48,500 --> 00:03:49,549 meant it to be. 107 00:03:49,550 --> 00:03:51,529 And there are cryptographic ways to 108 00:03:51,530 --> 00:03:52,879 achieve that. 109 00:03:52,880 --> 00:03:55,159 Recorded as cost says 110 00:03:55,160 --> 00:03:57,289 that you must be able to provide 111 00:03:57,290 --> 00:03:59,359 public evidence that the ballot was not 112 00:03:59,360 --> 00:04:01,309 tampered with in transit. 113 00:04:01,310 --> 00:04:02,719 Right. So it's all great. 114 00:04:02,720 --> 00:04:04,879 The electronic ballot is what you 115 00:04:04,880 --> 00:04:06,859 intended, but if there's a man in the 116 00:04:06,860 --> 00:04:09,169 middle attack, then the man in the middle 117 00:04:09,170 --> 00:04:11,330 can change the ballot in transit. 118 00:04:12,340 --> 00:04:14,659 And finally, there's the tally 119 00:04:14,660 --> 00:04:15,879 was recorded. 120 00:04:15,880 --> 00:04:18,789 So the idea is that a voter can verify 121 00:04:18,790 --> 00:04:20,889 that the ballot was telling, right, 122 00:04:20,890 --> 00:04:23,589 in other words, that the tallying 123 00:04:23,590 --> 00:04:25,329 program didn't just throw the ballot 124 00:04:25,330 --> 00:04:26,379 away. 125 00:04:26,380 --> 00:04:28,839 Right now, these three things naturally 126 00:04:28,840 --> 00:04:31,149 form, you know, a cascade 127 00:04:31,150 --> 00:04:34,029 so that if you have cast as intended 128 00:04:34,030 --> 00:04:36,309 and then recorded as cast and 129 00:04:36,310 --> 00:04:38,709 tallied is recorded, you have 130 00:04:38,710 --> 00:04:40,869 in verifiability and there 131 00:04:40,870 --> 00:04:43,330 are, you know, publicly available 132 00:04:44,440 --> 00:04:46,629 electronic voting systems that try 133 00:04:46,630 --> 00:04:48,669 to guarantee these things. 134 00:04:48,670 --> 00:04:51,130 Now, most of these 135 00:04:52,600 --> 00:04:54,909 solutions for the first two 136 00:04:54,910 --> 00:04:57,039 are cryptographic in some sense, you 137 00:04:57,040 --> 00:04:58,899 know, some sort of hashing, some sort of 138 00:04:58,900 --> 00:05:01,959 mixing. I won't go into the details 139 00:05:01,960 --> 00:05:03,459 now, tally this record. 140 00:05:03,460 --> 00:05:04,869 It is all well and good. 141 00:05:04,870 --> 00:05:06,969 You know that you know that your vote was 142 00:05:06,970 --> 00:05:08,019 tallied. 143 00:05:08,020 --> 00:05:10,539 But what is the vote counting program 144 00:05:10,540 --> 00:05:11,919 contains a bug. 145 00:05:11,920 --> 00:05:14,379 So what you really want to know 146 00:05:14,380 --> 00:05:16,989 is that it was tallied correctly, 147 00:05:16,990 --> 00:05:18,999 and that's what we're trying to address 148 00:05:19,000 --> 00:05:20,050 in this work here. 149 00:05:21,400 --> 00:05:24,489 And the idea is called 150 00:05:24,490 --> 00:05:26,709 software independence, and it goes 151 00:05:26,710 --> 00:05:28,389 back to Ron reversed one of the 152 00:05:28,390 --> 00:05:30,819 co-inventors of RSA. 153 00:05:30,820 --> 00:05:32,919 So the idea is that a vote 154 00:05:32,920 --> 00:05:35,079 counting program has to produce 155 00:05:35,080 --> 00:05:37,209 a telling script, write some sort of 156 00:05:37,210 --> 00:05:38,980 evidence of what it was doing. 157 00:05:40,000 --> 00:05:42,159 And then what we do is 158 00:05:42,160 --> 00:05:44,679 we try and guarantee that 159 00:05:44,680 --> 00:05:47,079 if the tallying script is correct 160 00:05:47,080 --> 00:05:49,899 with some notion of correctness, 161 00:05:49,900 --> 00:05:52,119 then the result is correct with 162 00:05:52,120 --> 00:05:54,589 the appropriate notion of correctness. 163 00:05:54,590 --> 00:05:55,959 OK, so there are two notions of 164 00:05:55,960 --> 00:05:57,939 correctness here. One is the correctness 165 00:05:57,940 --> 00:06:00,009 of the telling script and the other is 166 00:06:00,010 --> 00:06:01,749 the correctness of the count. 167 00:06:01,750 --> 00:06:03,819 And what we do is we formally 168 00:06:03,820 --> 00:06:06,099 tie them together with this 169 00:06:06,100 --> 00:06:08,559 implication in line 170 00:06:08,560 --> 00:06:09,999 in Idea two. 171 00:06:10,000 --> 00:06:11,889 Right. So that's a formal implication 172 00:06:11,890 --> 00:06:14,049 which has to hold in logic. 173 00:06:14,050 --> 00:06:16,119 And then our claim is that it's trivial 174 00:06:16,120 --> 00:06:17,949 to write a program to check the telling 175 00:06:17,950 --> 00:06:19,929 script, and I'm hoping to demonstrate 176 00:06:19,930 --> 00:06:21,130 that in the rest of my talk. 177 00:06:22,900 --> 00:06:24,129 OK. 178 00:06:24,130 --> 00:06:26,199 So the idea 179 00:06:26,200 --> 00:06:27,999 is rather than. 180 00:06:29,170 --> 00:06:31,659 Verifying that every 181 00:06:31,660 --> 00:06:33,579 run of the vote counting program is 182 00:06:33,580 --> 00:06:34,569 correct. 183 00:06:34,570 --> 00:06:36,879 What we verify is that this 184 00:06:36,880 --> 00:06:39,009 particular run of the vote counting 185 00:06:39,010 --> 00:06:40,299 program is correct. 186 00:06:40,300 --> 00:06:42,519 Right? The one that counted your ballots 187 00:06:42,520 --> 00:06:45,129 or the one that counted this election. 188 00:06:45,130 --> 00:06:47,589 And so this idea of this 189 00:06:47,590 --> 00:06:49,719 one is correct will come up 190 00:06:49,720 --> 00:06:51,469 through my slides a little bit. 191 00:06:51,470 --> 00:06:53,169 OK, it's a new take on formal 192 00:06:53,170 --> 00:06:54,170 verification. 193 00:06:55,280 --> 00:06:56,209 All right. 194 00:06:56,210 --> 00:06:58,459 So what do we mean by a voting scheme? 195 00:06:58,460 --> 00:07:00,589 So the example that I 196 00:07:00,590 --> 00:07:02,509 want to deal with is single transferable 197 00:07:02,510 --> 00:07:04,429 voting. So it's basically a method for 198 00:07:04,430 --> 00:07:06,709 sitting out, filling in and counting 199 00:07:06,710 --> 00:07:08,669 paper ballots, right? 200 00:07:08,670 --> 00:07:10,609 Yeah, of course. If you make it 201 00:07:10,610 --> 00:07:12,529 electronic, you still have to have an 202 00:07:12,530 --> 00:07:13,999 electronic voting scheme. 203 00:07:14,000 --> 00:07:15,550 But now we're out of the 204 00:07:17,150 --> 00:07:19,759 the scope of what we've done. 205 00:07:19,760 --> 00:07:21,829 So we have a paper ballot 206 00:07:21,830 --> 00:07:24,019 and for example, like this 207 00:07:24,020 --> 00:07:26,269 one here, it says that, you know, 208 00:07:26,270 --> 00:07:28,489 there are four candidates and I 209 00:07:28,490 --> 00:07:30,739 vote Charlie one, Dave 210 00:07:30,740 --> 00:07:32,869 to Alice, three, and I don't 211 00:07:32,870 --> 00:07:35,329 really care about Bob now, depending 212 00:07:35,330 --> 00:07:37,129 on the voting scheme, this can either be 213 00:07:37,130 --> 00:07:38,929 a legal ballot or not. 214 00:07:38,930 --> 00:07:41,029 So, for example, do you 215 00:07:41,030 --> 00:07:42,859 have to fill out all the numbers? 216 00:07:42,860 --> 00:07:45,019 So in some jurisdictions, this would 217 00:07:45,020 --> 00:07:47,119 be an illegal ballot because I haven't 218 00:07:47,120 --> 00:07:48,499 put a floor here. 219 00:07:48,500 --> 00:07:50,329 But in other jurisdictions, this is 220 00:07:50,330 --> 00:07:51,330 allowed 221 00:07:52,460 --> 00:07:54,679 in in the Australian 222 00:07:54,680 --> 00:07:56,629 capital territory in Canberra, where I 223 00:07:56,630 --> 00:07:58,729 am. What we do is we also do 224 00:07:58,730 --> 00:08:00,949 something called Robson rotation, 225 00:08:00,950 --> 00:08:03,229 and the idea is that if you just 226 00:08:03,230 --> 00:08:05,719 have a fixed order of the candidates, 227 00:08:05,720 --> 00:08:07,759 then the donkey vote, right? 228 00:08:07,760 --> 00:08:09,149 The voter that doesn't care. 229 00:08:09,150 --> 00:08:11,269 We'll just go one two three four 230 00:08:11,270 --> 00:08:13,639 vertically and that those donkey 231 00:08:13,640 --> 00:08:15,829 votes will all go to Alice. 232 00:08:15,830 --> 00:08:17,629 And unfortunately, we have a lot of 233 00:08:17,630 --> 00:08:19,699 donkeys in Canberra, and so there are 234 00:08:19,700 --> 00:08:21,949 lots of votes that are donkey votes. 235 00:08:21,950 --> 00:08:24,469 So what they do is they 236 00:08:24,470 --> 00:08:26,599 produce reordered versions 237 00:08:26,600 --> 00:08:28,939 of these ballots in all the possible 238 00:08:28,940 --> 00:08:31,549 permutations and distribute them 239 00:08:31,550 --> 00:08:33,319 to the physical locations in equal 240 00:08:33,320 --> 00:08:34,219 numbers. 241 00:08:34,220 --> 00:08:36,529 So the idea is that, you know, 242 00:08:36,530 --> 00:08:38,779 the donkeys get equally distributed 243 00:08:38,780 --> 00:08:41,359 through all of the candidates. 244 00:08:41,360 --> 00:08:43,279 The main thing that we need to do, of 245 00:08:43,280 --> 00:08:45,559 course, in counting, is detect 246 00:08:45,560 --> 00:08:47,869 when a quota is 247 00:08:47,870 --> 00:08:50,539 when a candidate reaches a quota. 248 00:08:50,540 --> 00:08:52,489 If someone doesn't reach a quota, then 249 00:08:52,490 --> 00:08:54,289 detect who the weakest candidate is 250 00:08:54,290 --> 00:08:55,290 because that's who we're going to 251 00:08:56,420 --> 00:08:57,559 eliminate. 252 00:08:57,560 --> 00:08:59,629 And how do we break ties? 253 00:08:59,630 --> 00:09:01,609 And how do we transfer a vote and when to 254 00:09:01,610 --> 00:09:02,569 stop counting? 255 00:09:02,570 --> 00:09:04,099 So as you can see, this has got nothing 256 00:09:04,100 --> 00:09:06,409 to do with the cyber security aspects 257 00:09:06,410 --> 00:09:08,869 of electronic voting rights about formal 258 00:09:08,870 --> 00:09:11,149 verification of an algorithm. 259 00:09:11,150 --> 00:09:12,749 And I'm going to go into the details of 260 00:09:12,750 --> 00:09:14,869 STV counting now 261 00:09:14,870 --> 00:09:17,239 to explain why it's hard. 262 00:09:17,240 --> 00:09:19,279 So these are all the details or the 263 00:09:19,280 --> 00:09:21,379 technical terms that I might use, 264 00:09:21,380 --> 00:09:23,809 and I'm just going to talk about 265 00:09:23,810 --> 00:09:26,059 how we count the ballots 266 00:09:26,060 --> 00:09:27,499 and refer to these things. 267 00:09:27,500 --> 00:09:29,539 So I'm going to let you read this. 268 00:09:29,540 --> 00:09:32,119 Just note here that the transfer 269 00:09:32,120 --> 00:09:34,189 value of a ballot can be less than or 270 00:09:34,190 --> 00:09:35,869 equal to one. That's the main thing that 271 00:09:35,870 --> 00:09:37,279 I want to get across. 272 00:09:37,280 --> 00:09:39,379 Okay, so here is here 273 00:09:39,380 --> 00:09:41,599 is a pile of ballots and 274 00:09:41,600 --> 00:09:43,609 what do we do? We do the following. 275 00:09:43,610 --> 00:09:45,739 We tally all the highest prefer 276 00:09:45,740 --> 00:09:46,819 preferences. 277 00:09:46,820 --> 00:09:48,139 So what does that mean? 278 00:09:48,140 --> 00:09:50,209 That means that we create a 279 00:09:50,210 --> 00:09:52,459 pile of ballots for Charlie, 280 00:09:52,460 --> 00:09:55,279 and this ballot goes into Charlie's pile 281 00:09:55,280 --> 00:09:56,329 and that's it. 282 00:09:56,330 --> 00:09:58,489 Then we take the next ballot of 283 00:09:58,490 --> 00:10:00,559 the pile and put it into wherever the 284 00:10:00,560 --> 00:10:03,139 one candidate is. 285 00:10:03,140 --> 00:10:05,209 So at the end of that, what we're going 286 00:10:05,210 --> 00:10:07,369 to get is we're going to get in this case 287 00:10:07,370 --> 00:10:09,439 for piles, one for Alice, one 288 00:10:09,440 --> 00:10:11,089 football, one for Charlie and one for 289 00:10:11,090 --> 00:10:13,669 Dave, and every pile 290 00:10:13,670 --> 00:10:15,829 in, every ballot in 291 00:10:15,830 --> 00:10:17,089 Charlie's pile. 292 00:10:17,090 --> 00:10:19,519 We'll have a one here and every 293 00:10:19,520 --> 00:10:21,919 ballot in David's pile 294 00:10:21,920 --> 00:10:24,319 will have a one here, 295 00:10:24,320 --> 00:10:26,389 and every ballot in 296 00:10:26,390 --> 00:10:28,579 Alice's pile will have a one here and 297 00:10:28,580 --> 00:10:30,979 so on. So the idea is that we've counted 298 00:10:30,980 --> 00:10:32,899 the first preferences. 299 00:10:32,900 --> 00:10:35,959 Now, if anyone meets the quota, if 300 00:10:35,960 --> 00:10:37,819 whatever we fixed the quota debate, then 301 00:10:37,820 --> 00:10:39,589 they're elected, I'll explain how that's 302 00:10:39,590 --> 00:10:41,119 done in the moment. 303 00:10:41,120 --> 00:10:43,309 But if nobody's elected, then 304 00:10:43,310 --> 00:10:46,249 we have to choose a weakest candidate 305 00:10:46,250 --> 00:10:47,750 and eliminate that candidate. 306 00:10:49,100 --> 00:10:51,259 And either way, whether 307 00:10:51,260 --> 00:10:53,569 we elect a candidate or we eliminate 308 00:10:53,570 --> 00:10:55,490 a candidate, we have to transfer their 309 00:10:56,690 --> 00:10:57,619 ballots. 310 00:10:57,620 --> 00:11:00,259 So let me explain what transfering means. 311 00:11:00,260 --> 00:11:02,149 So suppose that in the first count, 312 00:11:02,150 --> 00:11:03,709 Charlie is elected. 313 00:11:03,710 --> 00:11:06,019 So what we want to do now is we want this 314 00:11:06,020 --> 00:11:08,689 ballot to go into Dave's pile. 315 00:11:08,690 --> 00:11:10,999 But typically we don't 316 00:11:11,000 --> 00:11:13,339 let it go in today's pile with a full 317 00:11:13,340 --> 00:11:15,589 value because Charlie is 318 00:11:15,590 --> 00:11:17,719 this voter has already got his or 319 00:11:17,720 --> 00:11:20,419 her preference. By having Charlie elected 320 00:11:20,420 --> 00:11:22,699 and now allowing them to have 321 00:11:22,700 --> 00:11:25,009 a full vote to elect Dave 322 00:11:25,010 --> 00:11:27,019 is sort of giving them more power. 323 00:11:27,020 --> 00:11:29,089 So the idea is that we attenuate 324 00:11:29,090 --> 00:11:31,999 the value of this ballot in some way 325 00:11:32,000 --> 00:11:34,249 and the ballot value becomes less than 326 00:11:34,250 --> 00:11:36,589 one and explain more 327 00:11:36,590 --> 00:11:37,590 in a moment. 328 00:11:38,210 --> 00:11:40,549 Of course, if the number of candidates 329 00:11:40,550 --> 00:11:43,369 that are remaining is 330 00:11:43,370 --> 00:11:45,499 is less than 331 00:11:45,500 --> 00:11:47,119 the number of seats that we need to 332 00:11:47,120 --> 00:11:49,849 elect, then you can just elect everybody. 333 00:11:49,850 --> 00:11:52,039 OK, so that's also done in 334 00:11:52,040 --> 00:11:54,259 the ACTU where I live. 335 00:11:54,260 --> 00:11:56,479 Let me go into the details a bit more, 336 00:11:56,480 --> 00:11:58,249 so here's an example. 337 00:11:58,250 --> 00:12:00,379 So we have four candidates A, B, 338 00:12:00,380 --> 00:12:02,869 C and D, we have to run an election 339 00:12:02,870 --> 00:12:05,269 where we have to elect two of them. 340 00:12:05,270 --> 00:12:07,189 And here are the five ballots in the 341 00:12:07,190 --> 00:12:09,319 election. So a one 342 00:12:09,320 --> 00:12:11,629 b to d three. 343 00:12:11,630 --> 00:12:13,819 Similarly, D one 344 00:12:13,820 --> 00:12:16,009 C to see one 345 00:12:16,010 --> 00:12:16,939 d two. 346 00:12:16,940 --> 00:12:19,159 That's what these ballots represent. 347 00:12:19,160 --> 00:12:21,019 Let's assume that there are no fractional 348 00:12:21,020 --> 00:12:23,539 transfers for the moment, so we don't 349 00:12:23,540 --> 00:12:25,579 attenuate the value just to keep things 350 00:12:25,580 --> 00:12:26,599 simple. 351 00:12:26,600 --> 00:12:28,939 And let's not do this autofill thing 352 00:12:28,940 --> 00:12:31,429 right where we elect 353 00:12:31,430 --> 00:12:33,589 all of the candidates if 354 00:12:33,590 --> 00:12:35,479 there are less candidates than the seats. 355 00:12:35,480 --> 00:12:37,339 It just keeps things simple, for my 356 00:12:37,340 --> 00:12:38,719 example. 357 00:12:38,720 --> 00:12:40,879 Now in Canberra, 358 00:12:40,880 --> 00:12:42,859 what we use is something called a drip 359 00:12:42,860 --> 00:12:45,139 quota named after a person, 360 00:12:45,140 --> 00:12:46,969 and it's defined to be this. 361 00:12:46,970 --> 00:12:48,859 It's the total number of ballots, which 362 00:12:48,860 --> 00:12:51,049 is five divided by 363 00:12:51,050 --> 00:12:53,209 the number of seats, plus one, which 364 00:12:53,210 --> 00:12:54,379 is three. 365 00:12:54,380 --> 00:12:56,239 And it's the floor function, right? 366 00:12:56,240 --> 00:12:58,009 So it's the greatest integer that's less 367 00:12:58,010 --> 00:13:00,289 than that plus one. 368 00:13:00,290 --> 00:13:01,969 So what does that mean? 369 00:13:01,970 --> 00:13:02,899 It's five. 370 00:13:02,900 --> 00:13:05,389 Divided by three is one point something 371 00:13:05,390 --> 00:13:08,089 the floor is one plus one is two. 372 00:13:08,090 --> 00:13:10,339 So as soon as someone gets to 373 00:13:12,200 --> 00:13:14,299 vote in this election, 374 00:13:14,300 --> 00:13:15,889 they get elected. 375 00:13:15,890 --> 00:13:17,179 So what am I going to do now? 376 00:13:17,180 --> 00:13:18,409 I'm going to count all the first 377 00:13:18,410 --> 00:13:20,749 preferences, so I'm going to go down here 378 00:13:20,750 --> 00:13:22,369 and count all the first preferences. 379 00:13:22,370 --> 00:13:24,829 So as you expect, we should get a three 380 00:13:24,830 --> 00:13:27,439 for a A, one for D 381 00:13:27,440 --> 00:13:28,879 and a one for C. 382 00:13:28,880 --> 00:13:30,349 So here they are. 383 00:13:30,350 --> 00:13:32,569 Right is a three four, eight 384 00:13:32,570 --> 00:13:34,669 one four D and one for C. 385 00:13:35,970 --> 00:13:38,189 Now what now what we have to do is see 386 00:13:38,190 --> 00:13:40,009 whether anybody meets the quota. 387 00:13:40,010 --> 00:13:43,019 Well, it does meet the quota, 388 00:13:43,020 --> 00:13:45,089 right? He has three ballots 389 00:13:45,090 --> 00:13:46,769 and the quota is two ballots. 390 00:13:46,770 --> 00:13:48,929 So he actually has one ballot more than 391 00:13:48,930 --> 00:13:50,729 the quota. So let's elect a. 392 00:13:51,990 --> 00:13:54,419 Now what we have to do is decide 393 00:13:54,420 --> 00:13:57,299 what are we going to do with a surplus? 394 00:13:57,300 --> 00:13:58,919 So what was the surplus? 395 00:13:58,920 --> 00:14:01,979 Well, the surplus is one because 396 00:14:01,980 --> 00:14:04,349 I only needed two of these ballots 397 00:14:04,350 --> 00:14:06,479 to get across the line, but 398 00:14:06,480 --> 00:14:08,369 a has got three. 399 00:14:08,370 --> 00:14:10,319 So the surplus is one. 400 00:14:10,320 --> 00:14:13,049 We have to decide how to 401 00:14:13,050 --> 00:14:15,089 transfer the surplus. 402 00:14:15,090 --> 00:14:17,039 There are various ways which I'll come 403 00:14:17,040 --> 00:14:19,439 back to a bit later, but 404 00:14:19,440 --> 00:14:21,329 right now I just want to keep things 405 00:14:21,330 --> 00:14:23,219 simple. What I'm going to do is I'm going 406 00:14:23,220 --> 00:14:24,719 to say, Look, all these ballots are 407 00:14:24,720 --> 00:14:25,739 identical. 408 00:14:25,740 --> 00:14:27,689 So let's just delete two of them and 409 00:14:27,690 --> 00:14:29,039 transfer the third. 410 00:14:29,040 --> 00:14:31,109 So let's just delete the first two 411 00:14:31,110 --> 00:14:32,879 and transfer the third. 412 00:14:32,880 --> 00:14:35,069 So what's going to happen is this ballot 413 00:14:35,070 --> 00:14:37,349 is now going to move from this pile 414 00:14:37,350 --> 00:14:38,789 to BS pile. 415 00:14:38,790 --> 00:14:41,339 So bees count should go up by one. 416 00:14:41,340 --> 00:14:43,689 And that's exactly what happens. 417 00:14:43,690 --> 00:14:46,149 Now we have a three way tie. 418 00:14:46,150 --> 00:14:48,549 Nobody is elected because nobody 419 00:14:48,550 --> 00:14:51,699 meets the quota, so we have to 420 00:14:51,700 --> 00:14:54,399 eliminate the weakest candidate. 421 00:14:54,400 --> 00:14:55,839 How are we going to choose the weakest 422 00:14:55,840 --> 00:14:57,609 candidate? We're again, there are various 423 00:14:57,610 --> 00:14:59,469 ways and it makes a difference. 424 00:14:59,470 --> 00:15:01,599 But for simplicity, let's 425 00:15:01,600 --> 00:15:03,759 just pretend that this ballot, 426 00:15:03,760 --> 00:15:05,709 because it's transferred, is somehow 427 00:15:05,710 --> 00:15:07,839 worth less than these ballots, which 428 00:15:07,840 --> 00:15:09,389 are not transferred, right? 429 00:15:09,390 --> 00:15:11,019 I'm just making something up. 430 00:15:11,020 --> 00:15:12,759 But there are much better ways, of 431 00:15:12,760 --> 00:15:14,289 course, right? 432 00:15:14,290 --> 00:15:16,359 So what I'm going to do is 433 00:15:16,360 --> 00:15:17,739 I'm going to now transfer. 434 00:15:17,740 --> 00:15:19,380 I'm going to eliminate or 435 00:15:20,500 --> 00:15:22,629 eliminate a sorry, I'm going 436 00:15:22,630 --> 00:15:24,969 to eliminate B and transfer 437 00:15:24,970 --> 00:15:26,439 the ballot, right? 438 00:15:26,440 --> 00:15:28,659 So I've eliminated B 439 00:15:28,660 --> 00:15:30,939 and transferred the ballot to D. 440 00:15:30,940 --> 00:15:33,169 But D now gets two votes 441 00:15:33,170 --> 00:15:35,589 right. So we had because one 442 00:15:35,590 --> 00:15:38,529 day equals one, we eliminated B. 443 00:15:38,530 --> 00:15:40,719 The vote went to D, so D's count 444 00:15:40,720 --> 00:15:42,249 goes to two. 445 00:15:42,250 --> 00:15:44,259 He means he or she meets the quota. 446 00:15:44,260 --> 00:15:46,299 And so D's elected. 447 00:15:46,300 --> 00:15:47,559 And that's it. That's the end of the 448 00:15:47,560 --> 00:15:49,509 election because we were tasked with 449 00:15:49,510 --> 00:15:50,949 electing two people. 450 00:15:50,950 --> 00:15:53,379 We elected two people, we eliminated 451 00:15:53,380 --> 00:15:55,570 B and C's just left hanging. 452 00:15:57,530 --> 00:16:00,049 As well, neither elected 453 00:16:00,050 --> 00:16:01,190 nor eliminated, but 454 00:16:02,540 --> 00:16:03,889 the winners are Andy. 455 00:16:05,090 --> 00:16:07,399 Okay, so 456 00:16:07,400 --> 00:16:09,169 what I'd like to do now is tell you a 457 00:16:09,170 --> 00:16:11,359 little bit about the sad state 458 00:16:11,360 --> 00:16:13,639 of affairs of electronic vote 459 00:16:13,640 --> 00:16:14,779 counting in Australia. 460 00:16:16,670 --> 00:16:19,009 We don't have any official electronic 461 00:16:19,010 --> 00:16:21,379 voting. As such, we have 462 00:16:21,380 --> 00:16:24,349 booths spaced voting in the act. 463 00:16:24,350 --> 00:16:25,909 But I just want to talk about vote 464 00:16:25,910 --> 00:16:27,169 counting. 465 00:16:27,170 --> 00:16:29,329 So at the highest level, we have 466 00:16:29,330 --> 00:16:31,699 the Australian Election Commission, which 467 00:16:31,700 --> 00:16:34,249 counts the federal elections, 468 00:16:34,250 --> 00:16:36,379 the national elections and as 469 00:16:36,380 --> 00:16:38,299 you can see here, the code is hidden. 470 00:16:38,300 --> 00:16:39,199 It's proprietary. 471 00:16:39,200 --> 00:16:41,509 It's not available for scrutiny 472 00:16:41,510 --> 00:16:43,999 when a lawyer in Tasmania 473 00:16:44,000 --> 00:16:46,549 put in a Freedom of Information request 474 00:16:46,550 --> 00:16:48,979 that the code be published. 475 00:16:48,980 --> 00:16:51,169 He was denied by the Australian 476 00:16:51,170 --> 00:16:52,849 Electoral Commission on the grounds of 477 00:16:52,850 --> 00:16:55,609 security and commercial in confidence. 478 00:16:55,610 --> 00:16:57,589 He appealed the decision to something 479 00:16:57,590 --> 00:17:00,499 called the Arbitration Commission, 480 00:17:00,500 --> 00:17:03,019 and the Arbitration Commission 481 00:17:03,020 --> 00:17:05,689 threw out the defense of security 482 00:17:05,690 --> 00:17:07,909 because the code is just run in 483 00:17:07,910 --> 00:17:09,499 house, right? It's not connected to the 484 00:17:09,500 --> 00:17:11,299 internet in any way. 485 00:17:11,300 --> 00:17:12,300 But they 486 00:17:13,430 --> 00:17:15,979 maintained the commercial in confidence 487 00:17:15,980 --> 00:17:18,289 argument and denied the Freedom 488 00:17:18,290 --> 00:17:19,430 of Information request. 489 00:17:20,810 --> 00:17:22,969 Now what you should be asking yourself is 490 00:17:22,970 --> 00:17:25,519 why would the highest electronic 491 00:17:25,520 --> 00:17:27,739 authority sorry, election authority 492 00:17:27,740 --> 00:17:29,719 in Australia have commercial in 493 00:17:29,720 --> 00:17:31,639 confidence reasons for keeping their code 494 00:17:31,640 --> 00:17:32,569 secret? 495 00:17:32,570 --> 00:17:34,939 And it's because they make roughly 496 00:17:34,940 --> 00:17:37,249 $19 million a year 497 00:17:37,250 --> 00:17:40,069 by running elections privately 498 00:17:40,070 --> 00:17:42,949 for electing the directors of companies, 499 00:17:42,950 --> 00:17:44,629 and they don't want to endanger that 500 00:17:44,630 --> 00:17:45,649 business. 501 00:17:45,650 --> 00:17:47,899 So what they're choosing to do is they're 502 00:17:47,900 --> 00:17:49,969 choosing to deny the public 503 00:17:49,970 --> 00:17:52,579 the right to see the code, 504 00:17:52,580 --> 00:17:54,529 which is used to elect their 505 00:17:54,530 --> 00:17:56,089 representatives in the national 506 00:17:56,090 --> 00:17:58,069 government because they want to make a 507 00:17:58,070 --> 00:17:59,780 profit on the side. 508 00:18:01,220 --> 00:18:03,349 The Victorian Electoral Commission also 509 00:18:03,350 --> 00:18:04,639 has some proprietary code. 510 00:18:04,640 --> 00:18:06,769 Victoria is the state where Melbourne is 511 00:18:06,770 --> 00:18:08,869 also has some proprietary code code. 512 00:18:08,870 --> 00:18:10,489 As far as I know, it's available for 513 00:18:10,490 --> 00:18:12,859 scrutiny. But as far as I know, nobody 514 00:18:12,860 --> 00:18:14,059 has done any scrutiny. 515 00:18:15,560 --> 00:18:17,779 The situation that I'm most familiar 516 00:18:17,780 --> 00:18:20,299 with is the Australian Capital Territory, 517 00:18:20,300 --> 00:18:22,369 where the code was developed by a company 518 00:18:22,370 --> 00:18:25,399 called Software Improvements using C++. 519 00:18:25,400 --> 00:18:28,099 It's been used four times since the 2001 520 00:18:28,100 --> 00:18:30,199 election and up until 521 00:18:30,200 --> 00:18:32,179 recently the counting code, not the 522 00:18:32,180 --> 00:18:34,309 casting code, but the counting code was 523 00:18:34,310 --> 00:18:36,169 available from the website. 524 00:18:36,170 --> 00:18:38,539 But in the last election, which happened 525 00:18:38,540 --> 00:18:40,729 in 2019, they decided to keep 526 00:18:40,730 --> 00:18:42,559 that secret as well. 527 00:18:42,560 --> 00:18:44,809 Of course, the full code is available 528 00:18:44,810 --> 00:18:45,859 if you're willing to sign a 529 00:18:45,860 --> 00:18:48,109 non-disclosure agreement, which says you 530 00:18:48,110 --> 00:18:49,939 shall not publish until we give you 531 00:18:49,940 --> 00:18:51,379 permission to publish. 532 00:18:51,380 --> 00:18:53,509 But being, you know, good 533 00:18:53,510 --> 00:18:55,490 academics, we're not willing to do that. 534 00:18:56,960 --> 00:18:59,059 The other province that I know of 535 00:18:59,060 --> 00:19:00,589 is the New South Wales Electoral 536 00:19:00,590 --> 00:19:02,209 Commission. New South Wales is the 537 00:19:02,210 --> 00:19:04,309 province where Sydney's so 538 00:19:04,310 --> 00:19:06,439 they make on their or at least 539 00:19:06,440 --> 00:19:08,689 a couple of years ago, online 540 00:19:08,690 --> 00:19:10,760 on their website, you could get detailed 541 00:19:11,960 --> 00:19:13,909 functional requirements. 542 00:19:13,910 --> 00:19:16,489 There was a letter from 543 00:19:16,490 --> 00:19:18,439 a legal expert at the Queensland 544 00:19:18,440 --> 00:19:20,959 University of Technology to say that 545 00:19:20,960 --> 00:19:23,149 he or she thinks that the 546 00:19:23,150 --> 00:19:25,219 functional requirements meet 547 00:19:25,220 --> 00:19:26,929 the legislation. 548 00:19:26,930 --> 00:19:29,749 Then the code was certified 549 00:19:29,750 --> 00:19:31,939 by a company called Beardless Soft, which 550 00:19:31,940 --> 00:19:33,949 I'm assuming is an Indian company because 551 00:19:33,950 --> 00:19:35,929 I know that Burleigh is a big company in 552 00:19:35,930 --> 00:19:38,119 India as 553 00:19:38,120 --> 00:19:39,709 passing old tests. 554 00:19:39,710 --> 00:19:41,689 But when you look at their certificate, 555 00:19:41,690 --> 00:19:43,999 the very first line says we 556 00:19:44,000 --> 00:19:46,159 give no guarantees that the code does 557 00:19:46,160 --> 00:19:47,959 what it's supposed to do. 558 00:19:47,960 --> 00:19:49,999 We just check this, this, this and this. 559 00:19:50,000 --> 00:19:52,759 And you know, it's all okay. 560 00:19:52,760 --> 00:19:53,989 It's proprietary code. 561 00:19:53,990 --> 00:19:55,219 When we ask for 562 00:19:56,450 --> 00:19:58,879 the code, they denied us the code, 563 00:19:58,880 --> 00:20:01,459 and it's not available for scrutiny. 564 00:20:01,460 --> 00:20:04,039 Okay, so what? 565 00:20:04,040 --> 00:20:06,649 How can we sort of abstract 566 00:20:06,650 --> 00:20:08,749 the approaches because I want to try and 567 00:20:08,750 --> 00:20:10,159 keep things in the abstract? 568 00:20:10,160 --> 00:20:12,289 So the idea here is that let's 569 00:20:12,290 --> 00:20:14,479 look at three aspects. 570 00:20:14,480 --> 00:20:16,369 So let's look at the artifacts that 571 00:20:16,370 --> 00:20:18,469 exist, the scrutiny 572 00:20:18,470 --> 00:20:20,839 that we can place them under and 573 00:20:20,840 --> 00:20:22,139 lacking the scrutiny. 574 00:20:22,140 --> 00:20:24,319 Where is the trust, the blind trust that 575 00:20:24,320 --> 00:20:25,909 we have to place? 576 00:20:25,910 --> 00:20:28,249 So we have, you know, a 14 577 00:20:28,250 --> 00:20:30,319 page document which outlines 578 00:20:30,320 --> 00:20:32,779 what the Hair Clock Act is 579 00:20:32,780 --> 00:20:34,909 in Austria, in Canberra for 580 00:20:34,910 --> 00:20:36,739 how to count votes, according to single 581 00:20:36,740 --> 00:20:39,349 transferable voting and 582 00:20:39,350 --> 00:20:41,509 the Australia, the Australian Capital 583 00:20:41,510 --> 00:20:43,609 Territory Electoral Commission and 584 00:20:43,610 --> 00:20:44,629 software improvements. 585 00:20:44,630 --> 00:20:46,159 The company have come up with these 586 00:20:46,160 --> 00:20:48,709 functional specifications in UML. 587 00:20:48,710 --> 00:20:50,989 They're not published, but presumably 588 00:20:50,990 --> 00:20:52,669 I could get them if I was willing to sign 589 00:20:52,670 --> 00:20:54,589 a non-disclosure agreement. 590 00:20:54,590 --> 00:20:56,659 So here we have to trust so. 591 00:20:56,660 --> 00:20:57,919 Are improvements in the election 592 00:20:57,920 --> 00:21:00,199 commission, then software 593 00:21:00,200 --> 00:21:01,939 improvements have produced the computer 594 00:21:01,940 --> 00:21:03,529 code in C++. 595 00:21:03,530 --> 00:21:05,509 They're not willing to publish the code 596 00:21:05,510 --> 00:21:07,489 well. They used to publish the counting 597 00:21:07,490 --> 00:21:09,019 code, but they're not even doing that 598 00:21:09,020 --> 00:21:11,119 now. And so what we have to 599 00:21:11,120 --> 00:21:13,249 do is we have to trust this auditing by 600 00:21:13,250 --> 00:21:15,289 some company called B.M.. 601 00:21:15,290 --> 00:21:17,449 So in 602 00:21:17,450 --> 00:21:19,549 Canberra, the company that 603 00:21:21,020 --> 00:21:23,479 certified the code or audited, the code 604 00:21:23,480 --> 00:21:25,159 is called BMP. 605 00:21:25,160 --> 00:21:26,779 Now, why on earth should you trust this 606 00:21:26,780 --> 00:21:27,679 PMPM company? 607 00:21:27,680 --> 00:21:28,909 What do they do? 608 00:21:28,910 --> 00:21:31,369 Well, VM is a company that actually 609 00:21:31,370 --> 00:21:33,529 audits gaming machines, 610 00:21:33,530 --> 00:21:35,599 so I'm assuming you have them 611 00:21:35,600 --> 00:21:36,559 in Germany as well. 612 00:21:36,560 --> 00:21:38,449 But we have these things which we call 613 00:21:38,450 --> 00:21:40,219 one of them and it's, you know, these 614 00:21:40,220 --> 00:21:42,199 machines that you put money into and they 615 00:21:42,200 --> 00:21:44,299 tell you they roll the dice and tell you 616 00:21:44,300 --> 00:21:46,819 whether you've won the jackpot or not. 617 00:21:46,820 --> 00:21:48,889 Now in Australia, the legislation says 618 00:21:48,890 --> 00:21:51,049 that they have to return 619 00:21:51,050 --> 00:21:53,689 some percentage of their takings. 620 00:21:53,690 --> 00:21:55,609 Eighty five per cent has to be returned 621 00:21:55,610 --> 00:21:56,610 to the players. 622 00:21:57,590 --> 00:21:59,749 So this company actually audits 623 00:21:59,750 --> 00:22:01,849 gaming machines and certifies them 624 00:22:01,850 --> 00:22:04,279 to be correct in the sense 625 00:22:04,280 --> 00:22:06,169 of returning 85 per cent of their 626 00:22:06,170 --> 00:22:08,599 takings. So at some stage they decided 627 00:22:08,600 --> 00:22:10,849 that, well, if we ordered 628 00:22:10,850 --> 00:22:12,379 gaming machines, why don't we audit 629 00:22:12,380 --> 00:22:13,429 software as well? 630 00:22:13,430 --> 00:22:15,709 And so they audit software 631 00:22:15,710 --> 00:22:18,379 again. The very first 632 00:22:18,380 --> 00:22:20,569 page of their certificate says We do 633 00:22:20,570 --> 00:22:23,209 not give any guarantees that this 634 00:22:23,210 --> 00:22:24,709 code actually counts the ballots 635 00:22:24,710 --> 00:22:25,710 properly. 636 00:22:26,660 --> 00:22:28,579 A New South Wales, I have a similar 637 00:22:28,580 --> 00:22:30,659 approach. So again, legal texts that 638 00:22:30,660 --> 00:22:32,899 have forty seven pages of specs, but 639 00:22:32,900 --> 00:22:34,099 they're actually published. 640 00:22:35,660 --> 00:22:37,459 There was a vendor we don't know who 641 00:22:37,460 --> 00:22:39,199 produced a computer code. 642 00:22:39,200 --> 00:22:40,879 The computer code is proprietary. 643 00:22:40,880 --> 00:22:42,199 You can't look at it. 644 00:22:42,200 --> 00:22:44,269 But now we have to trust this company 645 00:22:44,270 --> 00:22:45,349 called MuleSoft. 646 00:22:45,350 --> 00:22:47,929 And again, the very first pages. 647 00:22:47,930 --> 00:22:50,179 We don't guarantee that the code does 648 00:22:50,180 --> 00:22:51,200 what it was supposed to do. 649 00:22:52,850 --> 00:22:55,279 Now what's the situation? 650 00:22:55,280 --> 00:22:57,619 So over the past two years, we've found 651 00:22:57,620 --> 00:23:00,049 many bugs in the system, 652 00:23:00,050 --> 00:23:01,909 and some of my colleagues have recently 653 00:23:01,910 --> 00:23:04,159 found bugs in the New South 654 00:23:04,160 --> 00:23:05,779 Wales system. So I'd like to tell you a 655 00:23:05,780 --> 00:23:07,639 little bit about the bugs. 656 00:23:07,640 --> 00:23:09,679 So the very first bug that we found was a 657 00:23:09,680 --> 00:23:11,299 simple four loop error. 658 00:23:11,300 --> 00:23:13,159 You know, what you want is a full and 659 00:23:13,160 --> 00:23:14,899 outermost full loop that says something 660 00:23:14,900 --> 00:23:16,969 like, you know, for 661 00:23:16,970 --> 00:23:19,669 I equals one to the number of candidates 662 00:23:19,670 --> 00:23:21,769 do blah blah blah. 663 00:23:21,770 --> 00:23:23,989 Now that had a slight bug in that, so 664 00:23:23,990 --> 00:23:26,119 they either had n minus one or plus 665 00:23:26,120 --> 00:23:28,669 one. I can't quite remember which, but 666 00:23:28,670 --> 00:23:30,739 one of the these students who 667 00:23:30,740 --> 00:23:33,439 now works for Google Zurich found 668 00:23:33,440 --> 00:23:35,569 that the code 669 00:23:35,570 --> 00:23:37,669 would run perfectly fine if there was an 670 00:23:37,670 --> 00:23:39,889 even number of candidates, but would 671 00:23:39,890 --> 00:23:41,899 just crash and burn if there was an odd 672 00:23:41,900 --> 00:23:42,889 number of candidates. 673 00:23:42,890 --> 00:23:44,869 I can't remember which way it would have 674 00:23:44,870 --> 00:23:46,129 actually happened. 675 00:23:46,130 --> 00:23:48,229 We found the bug three days 676 00:23:48,230 --> 00:23:50,569 before these people were going to count 677 00:23:50,570 --> 00:23:52,999 the Act 2001 election 678 00:23:53,000 --> 00:23:55,249 live on television on 679 00:23:55,250 --> 00:23:58,429 the day of the election. 680 00:23:58,430 --> 00:23:59,989 They admitted the error. 681 00:23:59,990 --> 00:24:02,059 They fixed it, but we got this nice 682 00:24:02,060 --> 00:24:03,649 letter back from the Election Commission 683 00:24:03,650 --> 00:24:05,809 saying thank you for notifying 684 00:24:05,810 --> 00:24:07,039 us of the simple error. 685 00:24:07,040 --> 00:24:08,989 It was easy to fix and everything's fine 686 00:24:08,990 --> 00:24:09,949 now. 687 00:24:09,950 --> 00:24:11,929 So we asked them, Well, if there was this 688 00:24:11,930 --> 00:24:13,369 simple error, how do you know there are 689 00:24:13,370 --> 00:24:14,749 not other errors? 690 00:24:14,750 --> 00:24:16,789 And they said, No, no, no, we're sure 691 00:24:16,790 --> 00:24:18,739 everything's fine. 692 00:24:18,740 --> 00:24:20,389 Of course, a little bit later, one of my 693 00:24:20,390 --> 00:24:22,789 colleagues all went to found another 694 00:24:22,790 --> 00:24:23,790 bug. 695 00:24:24,530 --> 00:24:26,779 That's this one. Here he had it. 696 00:24:26,780 --> 00:24:28,879 There was an unknown initialized Boolean, 697 00:24:28,880 --> 00:24:30,379 and different compilers could give 698 00:24:30,380 --> 00:24:32,209 different results. 699 00:24:32,210 --> 00:24:33,799 Another one of my colleagues, Jeremy 700 00:24:33,800 --> 00:24:35,390 Dawson, rewrote 701 00:24:36,410 --> 00:24:38,569 the implementation or 702 00:24:38,570 --> 00:24:40,729 rewrote his own implementation using 703 00:24:40,730 --> 00:24:42,799 a functional programing language. 704 00:24:42,800 --> 00:24:44,569 And when we checked the results of the 705 00:24:44,570 --> 00:24:46,729 2001 election, we found 706 00:24:46,730 --> 00:24:48,379 that three ballots were going in a 707 00:24:48,380 --> 00:24:50,359 slightly different way at a certain 708 00:24:50,360 --> 00:24:52,459 point. And we tripped when we traced 709 00:24:52,460 --> 00:24:54,529 it. What we found is that there was a 710 00:24:54,530 --> 00:24:56,629 three way tie right for 711 00:24:56,630 --> 00:24:57,659 the weakest candidate. 712 00:24:57,660 --> 00:24:59,779 So in a real election, there was a three 713 00:24:59,780 --> 00:25:02,209 way tie where there were three 714 00:25:02,210 --> 00:25:04,609 candidates always equal number of 715 00:25:04,610 --> 00:25:06,769 votes and one none of them who met 716 00:25:06,770 --> 00:25:08,839 the quota. And one of them had to be 717 00:25:08,840 --> 00:25:10,339 chosen as the weakest candidate. 718 00:25:11,720 --> 00:25:14,059 Now the the legislation 719 00:25:14,060 --> 00:25:15,949 says that when you're in the situation, 720 00:25:15,950 --> 00:25:17,509 you've got a three way tie. 721 00:25:17,510 --> 00:25:19,639 You go back and go 722 00:25:19,640 --> 00:25:22,039 back to the previous rounds until 723 00:25:22,040 --> 00:25:24,199 all candidates have an unequal number 724 00:25:24,200 --> 00:25:25,279 of votes. 725 00:25:25,280 --> 00:25:27,409 Now, Jeremy's a mathematician, so what he 726 00:25:27,410 --> 00:25:29,029 said is what does that mean? 727 00:25:29,030 --> 00:25:31,099 Well, all candidates have an 728 00:25:31,100 --> 00:25:33,709 unequal number of votes means 729 00:25:33,710 --> 00:25:35,929 no two candidates have 730 00:25:35,930 --> 00:25:37,739 the same number of votes. 731 00:25:37,740 --> 00:25:39,799 Right. So what this English text actually 732 00:25:39,800 --> 00:25:42,049 means is that all the ballots 733 00:25:42,050 --> 00:25:43,969 have to be counts have to be pairwise 734 00:25:43,970 --> 00:25:45,259 distinct, right? 735 00:25:45,260 --> 00:25:46,609 So they are equal. 736 00:25:46,610 --> 00:25:48,619 We have to go back until this one is not 737 00:25:48,620 --> 00:25:50,389 equal to this one. This one is not equal 738 00:25:50,390 --> 00:25:52,519 to this one and this one is not equal 739 00:25:52,520 --> 00:25:54,919 to this one pairwise distinct 740 00:25:54,920 --> 00:25:56,609 but the way the index code. 741 00:25:56,610 --> 00:25:58,369 Wasn't doing that, what it was doing is 742 00:25:58,370 --> 00:25:59,809 going back until one of them was 743 00:25:59,810 --> 00:26:00,859 different. 744 00:26:00,860 --> 00:26:03,049 So we wrote to the election commissioner 745 00:26:03,050 --> 00:26:04,609 and said, Look, we think we found a 746 00:26:04,610 --> 00:26:06,709 problem. Your code doesn't meet 747 00:26:06,710 --> 00:26:08,059 the legislation. 748 00:26:08,060 --> 00:26:09,649 And he wrote, It's a very nice letter 749 00:26:09,650 --> 00:26:11,179 saying, thank you very much. 750 00:26:11,180 --> 00:26:13,609 But we've defined 751 00:26:13,610 --> 00:26:15,649 the meaning of this English text to be 752 00:26:15,650 --> 00:26:17,779 exactly what the code our current 753 00:26:17,780 --> 00:26:19,179 code does. 754 00:26:19,180 --> 00:26:20,929 Right? Well, we can't argue with that. 755 00:26:20,930 --> 00:26:22,190 He was the election commissioner. 756 00:26:24,140 --> 00:26:25,369 How bad were these things? 757 00:26:25,370 --> 00:26:27,769 Well, for every bug, we could generate 758 00:26:27,770 --> 00:26:29,809 a very small election, which we could 759 00:26:29,810 --> 00:26:31,879 demonstrably show 760 00:26:31,880 --> 00:26:33,709 gave the wrong result. 761 00:26:33,710 --> 00:26:36,289 But I just said we have full confidence 762 00:26:36,290 --> 00:26:38,089 in our code. 763 00:26:38,090 --> 00:26:40,699 The University of Melbourne group found 764 00:26:40,700 --> 00:26:42,859 a bug in the New South quote in 765 00:26:42,860 --> 00:26:45,439 the New South Wales code recently, 766 00:26:45,440 --> 00:26:47,599 which actually reduce the chances of 767 00:26:47,600 --> 00:26:49,669 a candidate winning from 90 per cent to 768 00:26:49,670 --> 00:26:51,019 10 per cent. 769 00:26:51,020 --> 00:26:52,699 The first question you should be asking 770 00:26:52,700 --> 00:26:55,159 is why are we talking about probabilities 771 00:26:55,160 --> 00:26:56,809 here when we're talking about an 772 00:26:56,810 --> 00:26:58,999 election? And this is worth 773 00:26:59,000 --> 00:27:00,019 discussing. 774 00:27:00,020 --> 00:27:02,359 So let me go back to here where 775 00:27:02,360 --> 00:27:05,179 I had to transfer 776 00:27:05,180 --> 00:27:06,619 one of these ballots. 777 00:27:06,620 --> 00:27:09,559 Okay, so remember that 778 00:27:09,560 --> 00:27:11,689 as being elected and he's got 779 00:27:11,690 --> 00:27:14,299 a surplus of one, and I need to transfer 780 00:27:14,300 --> 00:27:16,579 these one of these three ballots. 781 00:27:16,580 --> 00:27:18,949 So what we did was we just transferred 782 00:27:18,950 --> 00:27:21,529 one of them because they are all equal. 783 00:27:21,530 --> 00:27:23,839 What New South Wales does is something 784 00:27:23,840 --> 00:27:24,739 really clever. 785 00:27:24,740 --> 00:27:26,839 They randomly select one 786 00:27:26,840 --> 00:27:28,909 of these ballots to transfer 787 00:27:28,910 --> 00:27:31,069 and transfer that randomly selected 788 00:27:31,070 --> 00:27:33,559 ballot, which is all fine in this case 789 00:27:33,560 --> 00:27:34,819 because they're all equal. 790 00:27:34,820 --> 00:27:37,549 But if these things were different, then 791 00:27:37,550 --> 00:27:39,919 we would basically be flipping a coin 792 00:27:39,920 --> 00:27:42,859 to see who gets elected. 793 00:27:42,860 --> 00:27:44,959 And more importantly, what it means 794 00:27:44,960 --> 00:27:47,779 is that you can't rerun the count 795 00:27:47,780 --> 00:27:49,669 because your random number generator may 796 00:27:49,670 --> 00:27:51,469 do different things at the same position 797 00:27:51,470 --> 00:27:53,149 in the second count. 798 00:27:53,150 --> 00:27:54,589 So what did my colleagues do? 799 00:27:54,590 --> 00:27:56,329 What they did is they ran the election 800 00:27:56,330 --> 00:27:58,429 100 times, and what 801 00:27:58,430 --> 00:28:00,529 they found is that one 802 00:28:00,530 --> 00:28:02,719 particular candidate was winning in 803 00:28:02,720 --> 00:28:05,329 ninety nine per cent of their runs. 804 00:28:05,330 --> 00:28:07,459 But in the real election, there was 805 00:28:07,460 --> 00:28:09,889 a bug and it reduced the chances 806 00:28:09,890 --> 00:28:12,319 of that person winning to 10 per cent. 807 00:28:12,320 --> 00:28:14,449 But the person couldn't challenge 808 00:28:14,450 --> 00:28:16,669 the result because the 809 00:28:16,670 --> 00:28:18,659 three month period for a legal challenge 810 00:28:18,660 --> 00:28:19,699 had passed. 811 00:28:19,700 --> 00:28:21,589 So, you know, this poor person 812 00:28:21,590 --> 00:28:23,539 potentially lost the election because of 813 00:28:23,540 --> 00:28:25,550 a bug, but she couldn't challenge. 814 00:28:28,340 --> 00:28:30,409 Now I want to talk about a better way 815 00:28:30,410 --> 00:28:31,399 of doing things. 816 00:28:31,400 --> 00:28:33,239 So I'm switching now, right? 817 00:28:33,240 --> 00:28:34,999 So this is the parlous state of 818 00:28:35,000 --> 00:28:37,609 electronic voting counting in Australia. 819 00:28:37,610 --> 00:28:39,379 I want to try and talk about how to do it 820 00:28:39,380 --> 00:28:41,449 properly, but in order 821 00:28:41,450 --> 00:28:43,119 to do it properly, we need something 822 00:28:43,120 --> 00:28:44,989 called a form of verification. 823 00:28:44,990 --> 00:28:46,519 And so what I want to do is tell you a 824 00:28:46,520 --> 00:28:48,469 little bit about formal verification and 825 00:28:48,470 --> 00:28:49,819 what that means. 826 00:28:49,820 --> 00:28:52,339 So formal verification started in the 60s 827 00:28:52,340 --> 00:28:54,769 with an eye during 828 00:28:54,770 --> 00:28:56,899 right, so artificial intelligence 829 00:28:56,900 --> 00:28:58,969 researchers were dreaming about 830 00:28:58,970 --> 00:29:00,619 automating mathematics. 831 00:29:00,620 --> 00:29:02,779 So the idea is that we can do 832 00:29:02,780 --> 00:29:04,879 mathematics fully, automatically on a 833 00:29:04,880 --> 00:29:06,979 computer, and you can read a really nice 834 00:29:06,980 --> 00:29:09,229 paper by a guy called 835 00:29:09,230 --> 00:29:10,490 one of the authors is 836 00:29:12,710 --> 00:29:14,959 John Harrison, who is 837 00:29:14,960 --> 00:29:17,089 an expert in this formal verification 838 00:29:18,710 --> 00:29:21,259 area, and he currently works for 839 00:29:21,260 --> 00:29:22,039 Amazon. 840 00:29:22,040 --> 00:29:23,749 Why? Because they want to do formal 841 00:29:23,750 --> 00:29:25,729 verification of their code eventually. 842 00:29:27,230 --> 00:29:29,029 Of course, what they found is that, you 843 00:29:29,030 --> 00:29:31,369 know, automating mathematics 844 00:29:31,370 --> 00:29:32,759 is the ultimate. 845 00:29:34,010 --> 00:29:35,780 That's just give me a second. 846 00:29:39,720 --> 00:29:41,879 Automating mathematics is the ultimate 847 00:29:41,880 --> 00:29:43,529 undesirable problem. 848 00:29:43,530 --> 00:29:45,929 And so human 849 00:29:45,930 --> 00:29:48,269 guidance was indispensable. 850 00:29:48,270 --> 00:29:50,339 Right. So they tried for 10 years 851 00:29:50,340 --> 00:29:52,649 and basically realized that we needed 852 00:29:52,650 --> 00:29:53,849 to be interactive. 853 00:29:53,850 --> 00:29:54,899 It couldn't be automatic. 854 00:29:56,160 --> 00:29:58,229 Now the reasons why 855 00:29:58,230 --> 00:30:00,989 you might want to automate mathematics 856 00:30:00,990 --> 00:30:03,069 began to get more and more serious. 857 00:30:03,070 --> 00:30:05,339 So the first example was the Apple 858 00:30:05,340 --> 00:30:07,260 hack and proof of the full color theorem. 859 00:30:08,400 --> 00:30:10,139 This is the famous theorem that says you 860 00:30:10,140 --> 00:30:12,480 take any Mac in three days 861 00:30:13,530 --> 00:30:15,929 of countries and you can color 862 00:30:15,930 --> 00:30:18,149 it in for 863 00:30:18,150 --> 00:30:20,429 it at most four colors 864 00:30:20,430 --> 00:30:22,499 so that no two countries have the 865 00:30:22,500 --> 00:30:24,839 same adjacent, no 866 00:30:24,840 --> 00:30:26,579 two adjacent countries have the same 867 00:30:26,580 --> 00:30:27,659 color. 868 00:30:27,660 --> 00:30:29,489 So Apple and Hopkin came up with a proof 869 00:30:29,490 --> 00:30:31,709 in 1976, and there were some 870 00:30:31,710 --> 00:30:34,289 1500 lines of code. 871 00:30:34,290 --> 00:30:36,059 And people are asking, Is the code 872 00:30:36,060 --> 00:30:38,219 correct? And I said, Well, we think 873 00:30:38,220 --> 00:30:40,080 it is what we do. 874 00:30:41,400 --> 00:30:43,199 The best example that I know of is the 875 00:30:43,200 --> 00:30:45,539 Pentium bug in 1994, 876 00:30:45,540 --> 00:30:47,609 because it cost Intel half a half 877 00:30:47,610 --> 00:30:48,629 a billion dollars. 878 00:30:48,630 --> 00:30:49,890 So they then 879 00:30:51,480 --> 00:30:52,979 started hiring people in formal 880 00:30:52,980 --> 00:30:54,929 verification, and they had a team for 881 00:30:54,930 --> 00:30:56,939 many years. And John Harrison actually 882 00:30:56,940 --> 00:30:58,589 used to work for Intel for a number of 883 00:30:58,590 --> 00:31:00,030 years before he moved to Amazon. 884 00:31:01,650 --> 00:31:03,389 The next example is called the Kepler 885 00:31:03,390 --> 00:31:04,499 conjecture. 886 00:31:04,500 --> 00:31:07,409 This was approved by Thomas Hales 887 00:31:07,410 --> 00:31:10,049 that the best way of stacking oranges 888 00:31:10,050 --> 00:31:11,760 is the face centered cubic 889 00:31:13,050 --> 00:31:14,999 way. It's the way that your average 890 00:31:15,000 --> 00:31:17,579 greengrocer at your market 891 00:31:17,580 --> 00:31:18,479 stacks them. 892 00:31:18,480 --> 00:31:20,099 But there was no proof that this was the 893 00:31:20,100 --> 00:31:21,630 most space efficient way of 894 00:31:22,860 --> 00:31:24,089 stacking oranges. 895 00:31:24,090 --> 00:31:26,219 He came up with a proof, but it had 896 00:31:26,220 --> 00:31:28,529 200 pages of handwritten notes 897 00:31:28,530 --> 00:31:30,599 or typed notes and a three gigabyte 898 00:31:30,600 --> 00:31:32,999 computer disk of examples. 899 00:31:33,000 --> 00:31:35,279 So again, the journal said, 900 00:31:35,280 --> 00:31:37,489 Well, we're not sure about this, but 901 00:31:37,490 --> 00:31:38,880 you know, we think it's OK. 902 00:31:40,080 --> 00:31:42,029 So what's the idea of formal proof? 903 00:31:42,030 --> 00:31:44,099 The idea of formal proof is that we use 904 00:31:44,100 --> 00:31:46,619 computers to do logic 905 00:31:46,620 --> 00:31:48,899 based checking of 906 00:31:48,900 --> 00:31:51,509 proofs. So we enter the proof 907 00:31:51,510 --> 00:31:53,369 into a computer using a specially 908 00:31:53,370 --> 00:31:55,799 designed language and the computer checks 909 00:31:55,800 --> 00:31:57,669 whether the proof is correct or not. 910 00:31:57,670 --> 00:31:59,819 As you can see, this is a chicken or 911 00:31:59,820 --> 00:32:01,709 egg problem, because how do you know that 912 00:32:01,710 --> 00:32:03,449 the computer program is correct? 913 00:32:03,450 --> 00:32:04,679 And that's what I want to talk a little 914 00:32:04,680 --> 00:32:05,680 bit about now. 915 00:32:06,450 --> 00:32:08,589 This is actually a very 916 00:32:08,590 --> 00:32:11,489 well developed area of research. 917 00:32:11,490 --> 00:32:13,019 And the current goal, there are many 918 00:32:13,020 --> 00:32:14,879 proof assistance, but the current goal is 919 00:32:14,880 --> 00:32:16,319 actually to make them more human 920 00:32:16,320 --> 00:32:18,089 friendly. So let me talk a little bit 921 00:32:18,090 --> 00:32:19,090 about 922 00:32:20,280 --> 00:32:22,229 formal proof, and I'm going to do that 923 00:32:22,230 --> 00:32:23,999 using an example. 924 00:32:24,000 --> 00:32:26,309 So let's take the example 925 00:32:26,310 --> 00:32:28,049 of odd and even numbers. 926 00:32:28,050 --> 00:32:30,059 So what's the definition of an even 927 00:32:30,060 --> 00:32:32,159 number? Well, it's a number 928 00:32:32,160 --> 00:32:33,959 which can be divided by two. 929 00:32:33,960 --> 00:32:36,149 So it can be written and is even 930 00:32:36,150 --> 00:32:38,519 if it can be written as two times some 931 00:32:38,520 --> 00:32:41,279 other number right to, for example, 932 00:32:41,280 --> 00:32:43,619 zero times zero 933 00:32:43,620 --> 00:32:46,199 one times to two times 934 00:32:46,200 --> 00:32:47,939 to three times to. 935 00:32:47,940 --> 00:32:49,529 And so on. 936 00:32:49,530 --> 00:32:50,939 What's an odd number? 937 00:32:50,940 --> 00:32:53,249 Well, an odd number is just an even 938 00:32:53,250 --> 00:32:55,229 number +1 write. 939 00:32:55,230 --> 00:32:57,359 The odd numbers are sitting 940 00:32:57,360 --> 00:32:59,549 in here, so it's zero plus 941 00:32:59,550 --> 00:33:01,679 one two plus one four plus 942 00:33:01,680 --> 00:33:03,839 one, five plus one and so on. 943 00:33:05,360 --> 00:33:07,049 So now I want to prove a lemma. 944 00:33:07,050 --> 00:33:09,569 If the natural number N is even, 945 00:33:09,570 --> 00:33:11,759 then the natural number in +1 is 946 00:33:11,760 --> 00:33:13,979 odd. So how can I do that? 947 00:33:13,980 --> 00:33:15,329 Well, here's a simple proof. 948 00:33:16,530 --> 00:33:17,819 How does it proceed? 949 00:33:17,820 --> 00:33:20,189 So what we do is we say, OK, let's assume 950 00:33:20,190 --> 00:33:22,469 that n is even that means 951 00:33:22,470 --> 00:33:24,539 that there's some K 952 00:33:24,540 --> 00:33:26,759 such that N is equal to two times 953 00:33:26,760 --> 00:33:27,389 K. 954 00:33:27,390 --> 00:33:29,549 So we know that this holds for our 955 00:33:29,550 --> 00:33:31,499 even number N. 956 00:33:31,500 --> 00:33:33,209 Well, now what we'll do is just will add 957 00:33:33,210 --> 00:33:35,219 one to this and one to this. 958 00:33:35,220 --> 00:33:36,119 And what will we get? 959 00:33:36,120 --> 00:33:38,009 We'll get that in. Plus one is of the 960 00:33:38,010 --> 00:33:40,589 form two times K plus one. 961 00:33:40,590 --> 00:33:42,719 But what do we know about numbers 962 00:33:42,720 --> 00:33:44,909 of the form two times code plus one? 963 00:33:44,910 --> 00:33:47,309 Well, there are by definition, 964 00:33:47,310 --> 00:33:49,769 so in plus one must be order. 965 00:33:49,770 --> 00:33:50,789 All right. 966 00:33:50,790 --> 00:33:52,859 Now what I want to do next is to 967 00:33:52,860 --> 00:33:54,929 show you an example of a 968 00:33:54,930 --> 00:33:57,479 computer script where a computer 969 00:33:58,680 --> 00:34:00,779 program called Coque, which 970 00:34:00,780 --> 00:34:03,089 is a theorem Prouver, an automated 971 00:34:03,090 --> 00:34:05,549 proof assistant, has proven 972 00:34:05,550 --> 00:34:08,138 this has checked the proof. 973 00:34:08,139 --> 00:34:10,499 OK, so this is what it looks like 974 00:34:10,500 --> 00:34:12,029 now. I can't go into the details, of 975 00:34:12,030 --> 00:34:14,309 course, but the idea is this 976 00:34:14,310 --> 00:34:16,529 that we import some library called 977 00:34:16,530 --> 00:34:18,419 arithmetic because they've defined a 978 00:34:18,420 --> 00:34:19,769 library, which allows us to do 979 00:34:19,770 --> 00:34:20,789 arithmetic. 980 00:34:20,790 --> 00:34:22,979 We define that 981 00:34:22,980 --> 00:34:25,138 for the natural number N 982 00:34:25,139 --> 00:34:26,999 is even if what? 983 00:34:27,000 --> 00:34:29,099 Well, if there is a K sextet N 984 00:34:29,100 --> 00:34:31,198 equals two times K, the 985 00:34:31,199 --> 00:34:32,759 natural number N is odd. 986 00:34:32,760 --> 00:34:35,369 If what exists a K sex that 987 00:34:35,370 --> 00:34:37,559 N equals two times K plus one. 988 00:34:37,560 --> 00:34:39,009 And here is a. 989 00:34:39,010 --> 00:34:41,349 Encoding of dilemma for all natural 990 00:34:41,350 --> 00:34:44,259 numbers in, if any, even 991 00:34:44,260 --> 00:34:46,089 then in plus one is odd. 992 00:34:46,090 --> 00:34:47,738 And this is the proof. 993 00:34:47,739 --> 00:34:49,658 Again, I can't go into the details, but 994 00:34:49,659 --> 00:34:51,729 these are commands that I've given 995 00:34:51,730 --> 00:34:54,189 to the interactive zero prove. 996 00:34:54,190 --> 00:34:56,138 These are comments where I've tried to 997 00:34:56,139 --> 00:34:58,509 capture what line of the previous 998 00:34:58,510 --> 00:35:00,909 proof I'm capturing here. 999 00:35:00,910 --> 00:35:02,889 And the idea is that when I get down to 1000 00:35:02,890 --> 00:35:05,379 here, I type QED 1001 00:35:05,380 --> 00:35:07,899 and the computer program 1002 00:35:07,900 --> 00:35:09,819 is checking all these steps and it says, 1003 00:35:09,820 --> 00:35:11,469 yes, all the steps are correct. 1004 00:35:11,470 --> 00:35:12,519 Or it says no. 1005 00:35:12,520 --> 00:35:13,719 This step is wrong here. 1006 00:35:13,720 --> 00:35:14,829 Fix it up. 1007 00:35:14,830 --> 00:35:17,169 And so the idea is that we interactively 1008 00:35:17,170 --> 00:35:19,279 push the proof through Congress 1009 00:35:19,280 --> 00:35:20,280 through the details. 1010 00:35:21,410 --> 00:35:23,619 Okay, next question 1011 00:35:23,620 --> 00:35:25,149 you should be asking is why should we 1012 00:35:25,150 --> 00:35:26,949 trust machine check proof? 1013 00:35:26,950 --> 00:35:29,259 So what we do is machine check 1014 00:35:29,260 --> 00:35:31,479 proof is based on the Alonzo 1015 00:35:31,480 --> 00:35:34,029 Church's lambda calculus from the 1930s. 1016 00:35:34,030 --> 00:35:35,139 It's a published paper. 1017 00:35:35,140 --> 00:35:36,819 It's been reviewed for the last. 1018 00:35:36,820 --> 00:35:39,399 Goodness knows almost 90 years or so 1019 00:35:39,400 --> 00:35:41,409 by mathematicians. 1020 00:35:41,410 --> 00:35:43,479 The official 1021 00:35:43,480 --> 00:35:45,579 research laboratory in rail from 1022 00:35:45,580 --> 00:35:47,469 France has produced this COC the 1023 00:35:47,470 --> 00:35:49,479 improvement, which is about 50000 lines 1024 00:35:49,480 --> 00:35:51,459 of code. It's been in development since 1025 00:35:51,460 --> 00:35:52,569 1976. 1026 00:35:52,570 --> 00:35:55,329 It's been checked by lots of people 1027 00:35:55,330 --> 00:35:57,249 and everything is published. 1028 00:35:57,250 --> 00:35:59,259 And so yes, we do have to trust some of 1029 00:35:59,260 --> 00:36:00,189 these things. 1030 00:36:00,190 --> 00:36:02,289 But you can you can 1031 00:36:02,290 --> 00:36:04,480 actually check these things. 1032 00:36:06,100 --> 00:36:07,659 So the idea is that we're going to use 1033 00:36:07,660 --> 00:36:09,570 this framework to do 1034 00:36:10,750 --> 00:36:12,849 formally verified electronic 1035 00:36:12,850 --> 00:36:14,109 counting. 1036 00:36:14,110 --> 00:36:16,749 So here's a map of what we've done. 1037 00:36:16,750 --> 00:36:19,059 So what we did is we took 1038 00:36:19,060 --> 00:36:21,129 the legal text that's the English 1039 00:36:21,130 --> 00:36:23,649 for the pages of the Hare Clerk Act. 1040 00:36:23,650 --> 00:36:26,319 We manually transferred it into logic 1041 00:36:26,320 --> 00:36:28,539 as rules capturing the state 1042 00:36:28,540 --> 00:36:31,059 transitions of an automaton. 1043 00:36:31,060 --> 00:36:32,439 Right. So basically, the state 1044 00:36:32,440 --> 00:36:34,539 transitions where a computer moves 1045 00:36:34,540 --> 00:36:36,039 from this state to that state. 1046 00:36:36,040 --> 00:36:37,569 And we tried to keep the computer as 1047 00:36:37,570 --> 00:36:38,629 simple as possible. 1048 00:36:38,630 --> 00:36:40,329 Right. So we're not trying to mimic a 1049 00:36:40,330 --> 00:36:41,409 full computer. 1050 00:36:41,410 --> 00:36:42,609 We're trying to mimic some sort of 1051 00:36:42,610 --> 00:36:44,679 abstract machine capturing abstract 1052 00:36:44,680 --> 00:36:45,940 machine and logic. 1053 00:36:47,050 --> 00:36:49,029 Then we converted this legal text into 1054 00:36:49,030 --> 00:36:51,219 formulae of higher order into mystic 1055 00:36:51,220 --> 00:36:52,869 logic as our third functional 1056 00:36:52,870 --> 00:36:53,799 specification. 1057 00:36:53,800 --> 00:36:56,829 So this is logic and this is logic. 1058 00:36:56,830 --> 00:36:59,169 And what we proved in Cork is 1059 00:36:59,170 --> 00:37:01,749 that if this thing produces 1060 00:37:01,750 --> 00:37:04,059 a correct certificate with some 1061 00:37:04,060 --> 00:37:06,219 notion of correctness, then this 1062 00:37:06,220 --> 00:37:08,349 thing produces a correct count 1063 00:37:08,350 --> 00:37:10,479 with your partner notion of 1064 00:37:10,480 --> 00:37:11,769 correct count. 1065 00:37:11,770 --> 00:37:13,569 Again, I can't go into the details, but 1066 00:37:13,570 --> 00:37:14,979 I'll try to give you an example in a 1067 00:37:14,980 --> 00:37:15,980 minute. 1068 00:37:16,510 --> 00:37:18,639 Now these are the 1069 00:37:18,640 --> 00:37:20,469 cocking interactive zero gravity a so 1070 00:37:20,470 --> 00:37:22,569 well-developed that actually 1071 00:37:22,570 --> 00:37:24,429 we were able to extract the code 1072 00:37:24,430 --> 00:37:26,619 automatically, which I can't go into, 1073 00:37:26,620 --> 00:37:28,689 right? So the idea is that once you do a 1074 00:37:28,690 --> 00:37:31,059 proof in Cork and Cork accepts 1075 00:37:31,060 --> 00:37:33,069 the proof, you can generate the code 1076 00:37:33,070 --> 00:37:35,019 automatically. So we didn't write any 1077 00:37:35,020 --> 00:37:37,119 code, we just did a proof 1078 00:37:37,120 --> 00:37:38,120 and we press the button. 1079 00:37:39,410 --> 00:37:41,509 Why should you trust any of this, well, 1080 00:37:41,510 --> 00:37:43,669 everything's published right, you 1081 00:37:43,670 --> 00:37:45,859 can get your election expert to check 1082 00:37:45,860 --> 00:37:48,289 this. You can get your mathematical 1083 00:37:48,290 --> 00:37:50,569 logician from you, dodge that, say 1084 00:37:50,570 --> 00:37:52,309 to check this. 1085 00:37:52,310 --> 00:37:54,619 And the only thing you really need to 1086 00:37:54,620 --> 00:37:56,719 trust is the certificate, which 1087 00:37:56,720 --> 00:37:59,209 we're going to publish and you can check. 1088 00:37:59,210 --> 00:38:01,789 So that's what I want to go into now. 1089 00:38:01,790 --> 00:38:02,869 So what have we done? 1090 00:38:02,870 --> 00:38:05,059 We've completed STV vote counting 1091 00:38:05,060 --> 00:38:06,679 and also the Shultz's method. 1092 00:38:06,680 --> 00:38:08,719 The Shultz's method is used, for example, 1093 00:38:08,720 --> 00:38:10,909 by the Linux community when they 1094 00:38:10,910 --> 00:38:14,179 want to decide which way to 1095 00:38:14,180 --> 00:38:16,489 fork branches, our code 1096 00:38:16,490 --> 00:38:19,429 computes with extract fractions. 1097 00:38:19,430 --> 00:38:21,199 It's efficient. We can count up to 10 1098 00:38:21,200 --> 00:38:23,299 million votes with 40 candidates and 20 1099 00:38:23,300 --> 00:38:25,609 focuses in 20 minutes. 1100 00:38:25,610 --> 00:38:27,499 It produces a certificate. 1101 00:38:27,500 --> 00:38:29,569 It produces a paper 1102 00:38:29,570 --> 00:38:31,999 printout of the state machine 1103 00:38:32,000 --> 00:38:34,639 and what states it's going through. 1104 00:38:34,640 --> 00:38:36,649 And what we claim is that an average 1105 00:38:36,650 --> 00:38:38,509 third year computer science student can 1106 00:38:38,510 --> 00:38:40,549 write a program to check the certificate. 1107 00:38:40,550 --> 00:38:42,469 And that's what I want to go into 1108 00:38:43,550 --> 00:38:44,869 in a moment. 1109 00:38:44,870 --> 00:38:47,119 In in in reality, you don't even need 1110 00:38:47,120 --> 00:38:49,129 to trust the hardware, the software, 1111 00:38:49,130 --> 00:38:50,779 because all you need to do is check 1112 00:38:50,780 --> 00:38:52,549 whether the certificate is correct 1113 00:38:52,550 --> 00:38:54,619 because our proof guarantees you 1114 00:38:54,620 --> 00:38:56,389 that a correct certificate implies a 1115 00:38:56,390 --> 00:38:57,739 correct count. 1116 00:38:57,740 --> 00:39:00,169 Right. And the converse of this is that 1117 00:39:00,170 --> 00:39:02,209 incorrect count means incorrect 1118 00:39:02,210 --> 00:39:03,199 certificate. 1119 00:39:03,200 --> 00:39:05,269 So if you check the certificate, you can 1120 00:39:05,270 --> 00:39:06,769 check with the count. 1121 00:39:06,770 --> 00:39:08,329 So this is what I want to talk about now. 1122 00:39:09,740 --> 00:39:11,539 So what we actually did is we 1123 00:39:12,680 --> 00:39:14,779 encoded a minimal abstract machine, 1124 00:39:14,780 --> 00:39:16,289 which has three types of stakes. 1125 00:39:16,290 --> 00:39:17,899 There's an initial state where all the 1126 00:39:17,900 --> 00:39:19,409 ballots are uncounted. 1127 00:39:19,410 --> 00:39:21,919 There's a final state 1128 00:39:21,920 --> 00:39:23,269 where we declare winners. 1129 00:39:23,270 --> 00:39:24,319 And then there are a bunch of 1130 00:39:24,320 --> 00:39:25,669 intermediate states. 1131 00:39:25,670 --> 00:39:28,189 I can't go into the details, but the idea 1132 00:39:28,190 --> 00:39:30,499 is that these intermediate states 1133 00:39:30,500 --> 00:39:32,569 carry complicated data, which 1134 00:39:32,570 --> 00:39:34,849 are usually lists and ballots 1135 00:39:34,850 --> 00:39:36,499 are moving from one place to another 1136 00:39:36,500 --> 00:39:38,029 list, according to the state. 1137 00:39:38,030 --> 00:39:40,489 Transitions of this machine 1138 00:39:40,490 --> 00:39:42,529 and the state transitions correspond to 1139 00:39:42,530 --> 00:39:44,599 counting, eliminating, transferring, 1140 00:39:44,600 --> 00:39:47,539 electing and declaring winners as rules. 1141 00:39:47,540 --> 00:39:49,699 And so, you know, the machine moves 1142 00:39:49,700 --> 00:39:51,439 from this state to this state. 1143 00:39:51,440 --> 00:39:53,779 If you count, it moves from this state 1144 00:39:53,780 --> 00:39:55,909 to this state. If you eliminate 1145 00:39:55,910 --> 00:39:57,289 and that's captured in logic, 1146 00:39:58,730 --> 00:40:00,799 then what we did is we we actually 1147 00:40:00,800 --> 00:40:02,899 prove minimal conditions that 1148 00:40:02,900 --> 00:40:05,419 the rules need to satisfy for everything 1149 00:40:05,420 --> 00:40:06,420 to be correct. 1150 00:40:07,190 --> 00:40:09,559 Now I can't go into the details of this, 1151 00:40:09,560 --> 00:40:11,509 but what I want to do is give a simple 1152 00:40:11,510 --> 00:40:12,499 example. 1153 00:40:12,500 --> 00:40:14,599 So let's go back to that idea of the 1154 00:40:14,600 --> 00:40:16,759 actual numbers and what what I'll 1155 00:40:16,760 --> 00:40:19,129 do is I'll show you some coding, 1156 00:40:19,130 --> 00:40:21,289 which which includes the natural 1157 00:40:21,290 --> 00:40:22,369 numbers in the clock. 1158 00:40:22,370 --> 00:40:24,259 So this is actual copy code. 1159 00:40:24,260 --> 00:40:26,869 And it says to the clock theorem prove 1160 00:40:26,870 --> 00:40:29,029 that Capital Zero is my 1161 00:40:29,030 --> 00:40:30,209 type of natural number. 1162 00:40:30,210 --> 00:40:33,289 I'm defining my private type of natural 1163 00:40:33,290 --> 00:40:34,219 capital. 1164 00:40:34,220 --> 00:40:35,869 Capital is a my. 1165 00:40:35,870 --> 00:40:38,119 These are my type of natural number and 1166 00:40:38,120 --> 00:40:40,189 s is a function which takes 1167 00:40:40,190 --> 00:40:42,259 any natural nut mine that you give it 1168 00:40:42,260 --> 00:40:44,449 and gives back another natural number. 1169 00:40:44,450 --> 00:40:45,379 So what does that mean? 1170 00:40:45,380 --> 00:40:47,989 It means that zero is capital 1171 00:40:47,990 --> 00:40:48,949 O. 1172 00:40:48,950 --> 00:40:51,259 One is s of capital. 1173 00:40:51,260 --> 00:40:53,369 Two is s of S of capital, 1174 00:40:53,370 --> 00:40:55,699 so three is SL, s0 1175 00:40:55,700 --> 00:40:57,649 s of capital and so on. 1176 00:40:57,650 --> 00:40:59,779 So every natural number is represented as 1177 00:40:59,780 --> 00:41:01,909 a string, which ends 1178 00:41:01,910 --> 00:41:04,039 in capital O and has a number 1179 00:41:04,040 --> 00:41:05,269 of S's in front of it. 1180 00:41:06,490 --> 00:41:08,829 So what we did is the state 1181 00:41:08,830 --> 00:41:11,169 machine is encoded using this complicated 1182 00:41:11,170 --> 00:41:13,479 thing, and what you can see here is right 1183 00:41:13,480 --> 00:41:15,609 that there is this 1184 00:41:15,610 --> 00:41:17,129 initial list of ballots. 1185 00:41:17,130 --> 00:41:18,999 There is the final list of candidates 1186 00:41:19,000 --> 00:41:21,129 which are elected 1187 00:41:21,130 --> 00:41:22,989 and then there is a complicated structure 1188 00:41:22,990 --> 00:41:24,759 which captures these lists. 1189 00:41:24,760 --> 00:41:26,469 Again, I can't go into the details. 1190 00:41:28,660 --> 00:41:30,819 The minimal STV instance is then given 1191 00:41:30,820 --> 00:41:32,979 by the definitions of these rules 1192 00:41:32,980 --> 00:41:35,079 and the rules that satisfy the 1193 00:41:35,080 --> 00:41:36,429 respective conditions. 1194 00:41:36,430 --> 00:41:38,559 The conditions consist of two parts. 1195 00:41:38,560 --> 00:41:40,629 When is the rule applicable and how 1196 00:41:40,630 --> 00:41:42,159 does it change the state? 1197 00:41:42,160 --> 00:41:44,469 And then we in COC, we prove the three 1198 00:41:44,470 --> 00:41:45,669 theorems. 1199 00:41:45,670 --> 00:41:47,829 Every applicable transition reduces 1200 00:41:47,830 --> 00:41:48,729 complexity. 1201 00:41:48,730 --> 00:41:51,069 So whenever you do something, you're 1202 00:41:51,070 --> 00:41:53,469 reducing the complexity of what remains. 1203 00:41:53,470 --> 00:41:54,969 That means that eventually we have to 1204 00:41:54,970 --> 00:41:57,669 reduce the complexity to zero. 1205 00:41:57,670 --> 00:41:59,349 There's a notion called liveness, which 1206 00:41:59,350 --> 00:42:01,569 says from any state, you 1207 00:42:01,570 --> 00:42:02,829 can't be blocked. 1208 00:42:02,830 --> 00:42:05,359 There's always at least one exit, 1209 00:42:05,360 --> 00:42:07,689 right? And these do two things together 1210 00:42:07,690 --> 00:42:09,789 imply that whenever you give me a 1211 00:42:09,790 --> 00:42:11,829 set of ballots, my process will 1212 00:42:11,830 --> 00:42:13,389 terminate, right? 1213 00:42:13,390 --> 00:42:14,949 So I guarantee you that this is an 1214 00:42:14,950 --> 00:42:16,329 algorithm which terminates. 1215 00:42:17,390 --> 00:42:19,539 Okay, then what we did is we 1216 00:42:19,540 --> 00:42:21,819 use the code extraction for facilities 1217 00:42:21,820 --> 00:42:23,979 of got to actually extract the code, 1218 00:42:23,980 --> 00:42:26,169 which I can't go into. 1219 00:42:26,170 --> 00:42:28,359 And what we did 1220 00:42:28,360 --> 00:42:30,459 is produced a program that 1221 00:42:30,460 --> 00:42:32,859 actually produces a certificate 1222 00:42:32,860 --> 00:42:34,299 once the certificate. 1223 00:42:34,300 --> 00:42:36,009 It's a run of the state machine. 1224 00:42:36,010 --> 00:42:37,959 And what we claim is that it's easy to 1225 00:42:37,960 --> 00:42:40,149 write a program to check the certificate. 1226 00:42:40,150 --> 00:42:42,399 Again, I can't go into the details, but 1227 00:42:42,400 --> 00:42:43,989 I'll give you an example. 1228 00:42:43,990 --> 00:42:46,659 So going back to our 1229 00:42:46,660 --> 00:42:48,819 natural numbers, I claim that 1230 00:42:48,820 --> 00:42:50,889 this is a certificate of 1231 00:42:50,890 --> 00:42:53,319 correct edition, 1232 00:42:53,320 --> 00:42:55,599 right? So what is it? 1233 00:42:55,600 --> 00:42:58,269 It's just a stack of lines 1234 00:42:58,270 --> 00:42:59,949 of the form and something. 1235 00:42:59,950 --> 00:43:01,719 Something something. 1236 00:43:01,720 --> 00:43:04,119 OK. And in the same way, 1237 00:43:04,120 --> 00:43:06,339 this is a certificate produced 1238 00:43:06,340 --> 00:43:08,139 by our vote counting program. 1239 00:43:08,140 --> 00:43:09,909 And as you can see, it's a bunch of 1240 00:43:09,910 --> 00:43:12,249 lists. So this is a ballot which says 1241 00:43:12,250 --> 00:43:14,379 a preferred oversee, preferred 1242 00:43:14,380 --> 00:43:16,659 of a b, and it moves in some 1243 00:43:16,660 --> 00:43:18,939 way through the lists until we declare 1244 00:43:18,940 --> 00:43:20,289 a winner. 1245 00:43:20,290 --> 00:43:23,109 I can't go into the details, but 1246 00:43:23,110 --> 00:43:24,429 this is what's going on. 1247 00:43:24,430 --> 00:43:26,559 So the claim is that 1248 00:43:26,560 --> 00:43:28,509 to check the certificate, all you need to 1249 00:43:28,510 --> 00:43:30,669 do is simple pattern matching 1250 00:43:30,670 --> 00:43:32,649 and check that these actually are the 1251 00:43:32,650 --> 00:43:34,749 rules that are being used to go 1252 00:43:34,750 --> 00:43:36,729 from here to here, where these are the 1253 00:43:36,730 --> 00:43:37,869 rules at zero. 1254 00:43:37,870 --> 00:43:39,999 And that is in this 1255 00:43:40,000 --> 00:43:42,159 case, right. But in our case, it would be 1256 00:43:42,160 --> 00:43:43,869 to stop and count rules. 1257 00:43:43,870 --> 00:43:46,359 So now I want to go into 1258 00:43:46,360 --> 00:43:47,399 an example. 1259 00:43:47,400 --> 00:43:49,539 So keeping the example simple. 1260 00:43:49,540 --> 00:43:51,099 So what are we going to do is we're going 1261 00:43:51,100 --> 00:43:53,649 to define the natural numbers, as I said, 1262 00:43:53,650 --> 00:43:55,209 and we're going to say that a basic 1263 00:43:55,210 --> 00:43:57,429 derivation is any string of this 1264 00:43:57,430 --> 00:43:59,559 form that is a string 1265 00:43:59,560 --> 00:44:01,659 that starts with the word add 1266 00:44:01,660 --> 00:44:03,789 and has three things after it, all 1267 00:44:03,790 --> 00:44:05,559 of which are X, Y and Z. 1268 00:44:05,560 --> 00:44:07,659 But the first one has to be equal 1269 00:44:07,660 --> 00:44:08,829 to the third one. 1270 00:44:08,830 --> 00:44:11,549 And the middle one has to be bigger. 1271 00:44:11,550 --> 00:44:12,569 And why is that? 1272 00:44:12,570 --> 00:44:14,849 Well, because that just says that 1273 00:44:14,850 --> 00:44:17,279 adding zero to X is X, 1274 00:44:17,280 --> 00:44:19,619 and we know that adding zero leaves 1275 00:44:19,620 --> 00:44:20,620 x alone. 1276 00:44:21,750 --> 00:44:23,849 And then the step case is if 1277 00:44:23,850 --> 00:44:26,819 you know that adding extra y gives Z, 1278 00:44:26,820 --> 00:44:29,009 then you know that adding X to 1279 00:44:29,010 --> 00:44:31,079 Y plus one gives Z Plus 1280 00:44:31,080 --> 00:44:31,709 one. 1281 00:44:31,710 --> 00:44:33,779 And so all we're doing is we're inserting 1282 00:44:33,780 --> 00:44:36,179 s twice into this position 1283 00:44:36,180 --> 00:44:38,099 in this position to convert that to an 1284 00:44:38,100 --> 00:44:40,289 air supply and convert that to an s 1285 00:44:40,290 --> 00:44:41,429 of Z. 1286 00:44:41,430 --> 00:44:43,709 Right. So what's the derivation? 1287 00:44:43,710 --> 00:44:46,409 It's a stack of correct derivations 1288 00:44:46,410 --> 00:44:47,760 and the result is in the bottom. 1289 00:44:48,780 --> 00:44:50,759 And the theorem says a correct derivation 1290 00:44:50,760 --> 00:44:52,769 always contains a correct result. 1291 00:44:52,770 --> 00:44:54,239 How can you verify that? 1292 00:44:54,240 --> 00:44:56,399 Well, I claim that this is a correct 1293 00:44:56,400 --> 00:44:57,299 derivation. 1294 00:44:57,300 --> 00:44:59,309 So let's check, is this a correct 1295 00:44:59,310 --> 00:45:01,409 derivation? Yes, because 1296 00:45:01,410 --> 00:45:03,689 it's something and the same 1297 00:45:03,690 --> 00:45:06,089 thing with a big go in the middle. 1298 00:45:06,090 --> 00:45:07,679 That was a correct definition, and it 1299 00:45:07,680 --> 00:45:09,779 says that zero plus one equals 1300 00:45:09,780 --> 00:45:10,780 one. 1301 00:45:11,280 --> 00:45:13,349 This one is a correct definition, because 1302 00:45:13,350 --> 00:45:15,419 if this is a correct derivation, then all 1303 00:45:15,420 --> 00:45:17,729 we've done is added an s here and edit 1304 00:45:17,730 --> 00:45:20,219 it here, and this thing says 1305 00:45:20,220 --> 00:45:22,289 you can transform one correct derivation 1306 00:45:22,290 --> 00:45:24,059 into another correct derivation. 1307 00:45:24,060 --> 00:45:25,979 So this is a correct derivation. 1308 00:45:25,980 --> 00:45:27,209 What's the result? 1309 00:45:27,210 --> 00:45:28,979 One plus one is two. 1310 00:45:28,980 --> 00:45:31,409 And so what's the final result? 1311 00:45:31,410 --> 00:45:33,629 One plus three is four. 1312 00:45:33,630 --> 00:45:35,699 So all you need to do is you only need to 1313 00:45:35,700 --> 00:45:37,770 check are those rules that I took 1314 00:45:38,880 --> 00:45:40,469 that I specified up here. 1315 00:45:40,470 --> 00:45:42,000 And it's just a pattern matching problem. 1316 00:45:43,590 --> 00:45:45,599 So what? What's the election process? 1317 00:45:45,600 --> 00:45:48,059 So what we do is we publish our logical 1318 00:45:48,060 --> 00:45:50,339 encoding of the vote counting process. 1319 00:45:50,340 --> 00:45:52,169 We publish the specification of what 1320 00:45:52,170 --> 00:45:53,699 correct certificate means. 1321 00:45:53,700 --> 00:45:56,009 We published a mathematical proof 1322 00:45:56,010 --> 00:45:57,779 that a correct certificate implies a 1323 00:45:57,780 --> 00:45:58,780 correct result. 1324 00:46:00,080 --> 00:46:01,699 What does the software vendor do, the 1325 00:46:01,700 --> 00:46:04,129 software vendor to lose the program, 1326 00:46:04,130 --> 00:46:06,859 which is almost certainly buggy 1327 00:46:06,860 --> 00:46:09,259 for vote counting, but it has to produce 1328 00:46:09,260 --> 00:46:11,119 a correct certificate, it has to produce 1329 00:46:11,120 --> 00:46:13,219 a certificate according to what we mean 1330 00:46:13,220 --> 00:46:14,419 to be a certificate. 1331 00:46:14,420 --> 00:46:15,799 And what we mean to be a correct 1332 00:46:15,800 --> 00:46:16,949 certificate. 1333 00:46:16,950 --> 00:46:18,649 Now, of course, if the program is buggy, 1334 00:46:18,650 --> 00:46:20,299 it may not do that. 1335 00:46:20,300 --> 00:46:21,799 So the election authorities have to 1336 00:46:21,800 --> 00:46:24,349 publish all the ballots. 1337 00:46:24,350 --> 00:46:25,699 Now what can we do? 1338 00:46:25,700 --> 00:46:28,219 Well, now we can have very, very 1339 00:46:28,220 --> 00:46:30,679 widely available 1340 00:46:30,680 --> 00:46:33,139 scrutiny because look, the political 1341 00:46:33,140 --> 00:46:35,119 parties can each hire a third year 1342 00:46:35,120 --> 00:46:36,709 computer science student to write a 1343 00:46:36,710 --> 00:46:37,969 certificate checker. 1344 00:46:37,970 --> 00:46:39,949 What's a certificate check program? 1345 00:46:39,950 --> 00:46:41,149 They just look at what a correct 1346 00:46:41,150 --> 00:46:42,949 certificate means and what a certificate 1347 00:46:42,950 --> 00:46:45,229 means and encode 1348 00:46:45,230 --> 00:46:46,729 what it means for the certificate to be 1349 00:46:46,730 --> 00:46:48,889 correct, it's pattern matching. 1350 00:46:48,890 --> 00:46:50,599 Other academics could set a software 1351 00:46:50,600 --> 00:46:52,459 engineering project to sign a certificate 1352 00:46:52,460 --> 00:46:54,559 checker. So what we could have is 1353 00:46:54,560 --> 00:46:56,059 we could have lots and lots of 1354 00:46:56,060 --> 00:46:57,499 certificate checkers which have been 1355 00:46:57,500 --> 00:46:59,659 independently developed, 1356 00:46:59,660 --> 00:47:01,819 and it's highly unlikely that 1357 00:47:01,820 --> 00:47:03,229 all of them will contain the same 1358 00:47:04,230 --> 00:47:05,959 right? So what do we do? 1359 00:47:05,960 --> 00:47:08,239 Well, you run the election, 1360 00:47:08,240 --> 00:47:10,759 everybody checks and someone sets. 1361 00:47:10,760 --> 00:47:13,009 The public certificate is incorrect. 1362 00:47:13,010 --> 00:47:15,139 So what we say, OK, you claim that 1363 00:47:15,140 --> 00:47:16,999 the public certificate is incorrect. 1364 00:47:17,000 --> 00:47:18,499 Where does it break the correctness 1365 00:47:18,500 --> 00:47:19,499 criteria? 1366 00:47:19,500 --> 00:47:20,989 All right. We told you what it meant to 1367 00:47:20,990 --> 00:47:22,009 be correct. 1368 00:47:22,010 --> 00:47:24,349 You tell us where it's incorrect. 1369 00:47:24,350 --> 00:47:26,299 And if you tell us that it's incorrect in 1370 00:47:26,300 --> 00:47:28,489 line five thirty five. 1371 00:47:28,490 --> 00:47:30,829 So I know it's incorrect in going 1372 00:47:30,830 --> 00:47:32,149 from here to here. 1373 00:47:32,150 --> 00:47:34,609 Well, we can check that right. 1374 00:47:34,610 --> 00:47:36,679 So there's public checking of 1375 00:47:36,680 --> 00:47:38,089 that claim. 1376 00:47:38,090 --> 00:47:39,829 Then someone else says on your 1377 00:47:39,830 --> 00:47:41,839 mathematical proof is wrong. 1378 00:47:41,840 --> 00:47:43,639 So we'll say, All right, you claim the 1379 00:47:43,640 --> 00:47:44,989 mathematical proof is wrong. 1380 00:47:44,990 --> 00:47:46,549 Tell us where it breaks the rules of 1381 00:47:46,550 --> 00:47:48,649 logic. We've published our rules 1382 00:47:48,650 --> 00:47:50,179 and we published our proof. 1383 00:47:50,180 --> 00:47:52,429 So you could go to the people in Berlin 1384 00:47:52,430 --> 00:47:54,589 or Darmstadt or Karlsruhe 1385 00:47:54,590 --> 00:47:56,659 and get the academics there to check out 1386 00:47:56,660 --> 00:47:57,660 proofs. 1387 00:47:58,250 --> 00:48:00,559 Someone else might say the correctness 1388 00:48:00,560 --> 00:48:02,629 criteria or the mathematical mathematical 1389 00:48:02,630 --> 00:48:03,979 encoding is wrong. 1390 00:48:03,980 --> 00:48:05,599 Again, we say, All right, when you claim 1391 00:48:05,600 --> 00:48:07,999 something is wrong, give us an example 1392 00:48:08,000 --> 00:48:10,099 of where it does something wrong and we 1393 00:48:10,100 --> 00:48:12,289 can check. So the electoral experts can 1394 00:48:12,290 --> 00:48:13,290 check. 1395 00:48:14,030 --> 00:48:16,039 Finally, what if the vote counting 1396 00:48:16,040 --> 00:48:18,259 program is buggy or hacked, 1397 00:48:18,260 --> 00:48:20,389 right? We don't care, 1398 00:48:20,390 --> 00:48:22,519 because the theorem says 1399 00:48:22,520 --> 00:48:24,409 that the correct certificate implies the 1400 00:48:24,410 --> 00:48:25,669 correct result. 1401 00:48:25,670 --> 00:48:27,739 So the control positive says 1402 00:48:27,740 --> 00:48:30,229 incorrect result implies incorrect 1403 00:48:30,230 --> 00:48:31,249 certificate. 1404 00:48:31,250 --> 00:48:32,929 And we've got all these thousands of 1405 00:48:32,930 --> 00:48:34,999 people around Germany checking 1406 00:48:35,000 --> 00:48:36,719 the certificate. 1407 00:48:36,720 --> 00:48:38,999 Right. So what it says is that 1408 00:48:39,000 --> 00:48:41,219 the bug or even the hack 1409 00:48:41,220 --> 00:48:43,799 could not have manifested itself during 1410 00:48:43,800 --> 00:48:46,439 this run of the program. 1411 00:48:46,440 --> 00:48:48,449 Right. The hacker tried to do something 1412 00:48:48,450 --> 00:48:50,519 or the vendor had a bug in 1413 00:48:50,520 --> 00:48:52,619 their program, but that bug did 1414 00:48:52,620 --> 00:48:54,899 not manifest itself during this run. 1415 00:48:54,900 --> 00:48:56,100 So this one is correct. 1416 00:48:57,160 --> 00:48:58,160 That's the idea. 1417 00:48:59,260 --> 00:49:00,189 So what are we done? 1418 00:49:00,190 --> 00:49:02,259 We've completed STV counting, as 1419 00:49:02,260 --> 00:49:03,819 I said, we've completed that, Schultz 1420 00:49:03,820 --> 00:49:04,719 admitted. 1421 00:49:04,720 --> 00:49:06,879 Counts 10 million votes, blah 1422 00:49:06,880 --> 00:49:08,739 blah blah, right? 1423 00:49:08,740 --> 00:49:11,259 Certificate is a plaintext 1424 00:49:11,260 --> 00:49:13,539 certificate which vouched 1425 00:49:13,540 --> 00:49:15,339 for the correctness of the count. 1426 00:49:15,340 --> 00:49:16,869 And you don't even need to trust the 1427 00:49:16,870 --> 00:49:18,759 hardware or software because there are 1428 00:49:18,760 --> 00:49:20,799 all these certificate checkers written by 1429 00:49:20,800 --> 00:49:21,909 independent people 1430 00:49:23,230 --> 00:49:25,569 who will check the certificate. 1431 00:49:25,570 --> 00:49:27,669 Now, the only caveat the dangerous one 1432 00:49:27,670 --> 00:49:30,249 is that we have to publish your ballots. 1433 00:49:30,250 --> 00:49:32,529 And that's actually a problem because 1434 00:49:32,530 --> 00:49:34,659 what is known is that if you publish 1435 00:49:34,660 --> 00:49:37,119 ballots, then the election can be 1436 00:49:37,120 --> 00:49:39,219 vulnerable to something called a Sicilian 1437 00:49:39,220 --> 00:49:42,099 attack, which I won't go into for now. 1438 00:49:42,100 --> 00:49:44,379 What we've actually done is get 1439 00:49:44,380 --> 00:49:46,989 Millard has even verified 1440 00:49:46,990 --> 00:49:48,849 the certificate checker, so he has 1441 00:49:48,850 --> 00:49:51,279 produced us a verified 1442 00:49:51,280 --> 00:49:53,379 certificate checker, which is formally 1443 00:49:53,380 --> 00:49:55,149 correct with respect to the semantics of 1444 00:49:55,150 --> 00:49:57,339 C using a different theorem, 1445 00:49:57,340 --> 00:49:59,619 prouver interactive theorem or cake 1446 00:49:59,620 --> 00:50:01,749 eml we've had we can cover 1447 00:50:01,750 --> 00:50:04,509 all STV schemes used in Australia. 1448 00:50:04,510 --> 00:50:06,009 And the problem that we're really 1449 00:50:06,010 --> 00:50:08,319 interested in now is can we do 1450 00:50:08,320 --> 00:50:10,389 this to encrypted ballots 1451 00:50:10,390 --> 00:50:12,519 because that would remove this as 1452 00:50:12,520 --> 00:50:13,539 an attack. 1453 00:50:13,540 --> 00:50:15,219 So the message that I want to try and get 1454 00:50:15,220 --> 00:50:18,069 across to you in Germany is 1455 00:50:18,070 --> 00:50:20,259 verified and publicly verified 1456 00:50:20,260 --> 00:50:22,839 e counting is now possible. 1457 00:50:22,840 --> 00:50:23,949 Thank you for your attention. 1458 00:50:26,380 --> 00:50:28,269 Hello and welcome back and thank you for 1459 00:50:28,270 --> 00:50:30,399 the nice talk and someone in the chat 1460 00:50:30,400 --> 00:50:32,549 mentioned after hearing 1461 00:50:32,550 --> 00:50:34,629 a for the like 1462 00:50:34,630 --> 00:50:36,579 before hearing of Steve for the first 1463 00:50:36,580 --> 00:50:38,619 time, they thought the German electoral 1464 00:50:38,620 --> 00:50:40,299 system was complicated. 1465 00:50:40,300 --> 00:50:42,399 As a reminder, we have a Q&A session 1466 00:50:42,400 --> 00:50:44,289 now. If you want to ask questions, you 1467 00:50:44,290 --> 00:50:46,599 can ask in the IOC at 83 1468 00:50:46,600 --> 00:50:48,579 three minus them and the rockets at at 1469 00:50:48,580 --> 00:50:49,989 them and in the Twitter feed. 1470 00:50:49,990 --> 00:50:52,269 Diverse at eighty three. 1471 00:50:52,270 --> 00:50:54,549 And now welcome 1472 00:50:54,550 --> 00:50:56,319 to the Q&A session. 1473 00:50:56,320 --> 00:50:57,999 Rajeev should join us now. 1474 00:50:58,000 --> 00:50:58,989 Yes, he is here. 1475 00:50:58,990 --> 00:50:59,990 Hello and welcome. 1476 00:51:01,330 --> 00:51:02,330 Hi. 1477 00:51:03,430 --> 00:51:05,649 OK, we actually do have quite quite 1478 00:51:05,650 --> 00:51:07,809 a few questions. I'm positively surprised 1479 00:51:07,810 --> 00:51:08,810 about that. 1480 00:51:09,550 --> 00:51:12,009 And the first one is, 1481 00:51:12,010 --> 00:51:14,469 are there similar movements to public 1482 00:51:14,470 --> 00:51:17,799 money public vote in Australia? 1483 00:51:17,800 --> 00:51:19,899 And if that if 1484 00:51:19,900 --> 00:51:21,939 there is any international cooperation 1485 00:51:21,940 --> 00:51:23,019 between these movements? 1486 00:51:24,400 --> 00:51:25,689 And how do you do this? 1487 00:51:25,690 --> 00:51:27,489 Play into arguing against closed source 1488 00:51:27,490 --> 00:51:28,490 voting court. 1489 00:51:30,900 --> 00:51:33,479 So, so the first one is 1490 00:51:33,480 --> 00:51:35,849 about international 1491 00:51:35,850 --> 00:51:37,379 cooperation. 1492 00:51:37,380 --> 00:51:39,599 And as far as I know, there isn't any, 1493 00:51:39,600 --> 00:51:41,879 the only cooperation there is is between 1494 00:51:41,880 --> 00:51:43,679 academics like myself. 1495 00:51:43,680 --> 00:51:45,869 So there are groups in culture 1496 00:51:45,870 --> 00:51:49,319 where there are groups in France, 1497 00:51:49,320 --> 00:51:51,479 in India and there are various other 1498 00:51:51,480 --> 00:51:53,159 groups around the world that are trying 1499 00:51:53,160 --> 00:51:55,649 to push the election commissions 1500 00:51:55,650 --> 00:51:58,170 to take up our technology. 1501 00:51:59,520 --> 00:52:01,589 The biggest problem that we have is that 1502 00:52:01,590 --> 00:52:04,529 the election commissions 1503 00:52:04,530 --> 00:52:07,619 are not sophisticated. 1504 00:52:09,080 --> 00:52:11,899 Acquire, sorry, are not acquirers 1505 00:52:11,900 --> 00:52:14,329 of sophisticated software. 1506 00:52:14,330 --> 00:52:16,309 Right, so they're not like Nessa or 1507 00:52:16,310 --> 00:52:18,419 they're not like, you know, the space 1508 00:52:18,420 --> 00:52:20,539 commissions, they go 1509 00:52:20,540 --> 00:52:21,679 out to tender. 1510 00:52:21,680 --> 00:52:23,929 And you know, if a vendor says our code 1511 00:52:23,930 --> 00:52:26,179 is correct, then they just say, Well, 1512 00:52:26,180 --> 00:52:28,369 OK, yeah, the code is correct. 1513 00:52:28,370 --> 00:52:29,510 The vendor says so right. 1514 00:52:31,100 --> 00:52:32,539 And what was the second question? 1515 00:52:32,540 --> 00:52:34,609 Sorry, the how was 1516 00:52:34,610 --> 00:52:36,469 I going to argue? 1517 00:52:36,470 --> 00:52:38,719 How did this play into arguing against 1518 00:52:38,720 --> 00:52:40,399 closed source voting code? 1519 00:52:40,400 --> 00:52:42,679 So I think it was more about the push 1520 00:52:42,680 --> 00:52:44,749 to get the public to get 1521 00:52:44,750 --> 00:52:46,999 the voting code and the counting 1522 00:52:47,000 --> 00:52:48,000 code published. 1523 00:52:49,310 --> 00:52:51,829 Right. So so what's going on here 1524 00:52:51,830 --> 00:52:54,289 is it's a strange 1525 00:52:56,060 --> 00:52:58,579 confluence of interests. 1526 00:52:58,580 --> 00:53:01,939 So the election commissions 1527 00:53:01,940 --> 00:53:04,249 have built up a lot of trust over 1528 00:53:04,250 --> 00:53:06,589 the last 100 years, and the last 1529 00:53:06,590 --> 00:53:08,989 thing they want is to have their trust 1530 00:53:08,990 --> 00:53:09,990 undermined. 1531 00:53:10,760 --> 00:53:12,859 So what they don't want is I 1532 00:53:12,860 --> 00:53:15,259 don't want academics like jumping 1533 00:53:15,260 --> 00:53:17,449 up and down, saying there's a bug in your 1534 00:53:17,450 --> 00:53:19,639 code, there's another bug in your code. 1535 00:53:19,640 --> 00:53:21,769 And so what they prefer is to 1536 00:53:21,770 --> 00:53:24,019 say, our vendor guarantees us 1537 00:53:24,020 --> 00:53:25,429 that everything is fine. 1538 00:53:25,430 --> 00:53:28,579 Trust us, and 1539 00:53:28,580 --> 00:53:30,949 this is only going to change 1540 00:53:30,950 --> 00:53:34,099 when there actually is a disaster 1541 00:53:34,100 --> 00:53:36,199 and somebody's a losing 1542 00:53:36,200 --> 00:53:38,089 candidate challenges the result and it 1543 00:53:38,090 --> 00:53:39,409 goes to court. 1544 00:53:39,410 --> 00:53:41,509 And you know, the case is thrown out 1545 00:53:41,510 --> 00:53:42,979 and they have to run the election again, 1546 00:53:42,980 --> 00:53:44,599 and it's going to cost them in a couple 1547 00:53:44,600 --> 00:53:46,339 of million dollars and be very 1548 00:53:46,340 --> 00:53:47,359 embarrassing. 1549 00:53:47,360 --> 00:53:49,519 So the only time this will change 1550 00:53:49,520 --> 00:53:50,689 is when there's a disaster, 1551 00:53:50,690 --> 00:53:51,690 unfortunately. 1552 00:53:53,760 --> 00:53:56,399 And what we found around the world is 1553 00:53:56,400 --> 00:53:58,949 there are many academics like myself 1554 00:53:58,950 --> 00:54:00,809 jumping up and down saying, Look, we need 1555 00:54:00,810 --> 00:54:03,359 to do formal verification, and almost 1556 00:54:03,360 --> 00:54:05,249 all of them have been ignored by the 1557 00:54:05,250 --> 00:54:07,259 election commissions for the reasons that 1558 00:54:07,260 --> 00:54:08,760 I just explained. 1559 00:54:10,430 --> 00:54:12,139 Well, that sounds like the concept of 1560 00:54:12,140 --> 00:54:14,449 security, but security is still popular, 1561 00:54:14,450 --> 00:54:16,239 and so. Absolutely. 1562 00:54:16,240 --> 00:54:17,599 Absolutely. Yup. 1563 00:54:17,600 --> 00:54:18,600 Trust us. 1564 00:54:19,730 --> 00:54:21,709 OK, then maybe we get to the next 1565 00:54:21,710 --> 00:54:23,809 question regarding the Bucks in the 1566 00:54:23,810 --> 00:54:25,219 counting modules, whether any 1567 00:54:25,220 --> 00:54:27,319 requirements on the code quality to avoid 1568 00:54:27,320 --> 00:54:29,329 common mistakes, for example, by forcing 1569 00:54:29,330 --> 00:54:31,339 compiler warnings to be treated as errors 1570 00:54:31,340 --> 00:54:32,840 or using static analyzes. 1571 00:54:34,190 --> 00:54:35,469 I don't know. 1572 00:54:35,470 --> 00:54:36,649 They won't tell us. 1573 00:54:36,650 --> 00:54:38,989 All they tell us is that we've tested 1574 00:54:38,990 --> 00:54:41,029 the code extensively and it passes all 1575 00:54:41,030 --> 00:54:42,109 our tests. 1576 00:54:42,110 --> 00:54:44,119 Now you have to understand where the 1577 00:54:44,120 --> 00:54:46,249 election is coming from us here. 1578 00:54:46,250 --> 00:54:48,529 So in the old days, they used to count 1579 00:54:48,530 --> 00:54:49,879 ballots by hand. 1580 00:54:49,880 --> 00:54:51,739 Right now in Canberra, we have about 1581 00:54:51,740 --> 00:54:53,659 350000 voters. 1582 00:54:53,660 --> 00:54:55,819 And so, you know, they needed 1583 00:54:55,820 --> 00:54:58,069 to count these votes quickly by hand to 1584 00:54:58,070 --> 00:55:00,149 to declare the election. 1585 00:55:00,150 --> 00:55:02,749 And what happened is that in 1996, 1586 00:55:02,750 --> 00:55:04,909 there was actually a challenge and 1587 00:55:04,910 --> 00:55:07,069 it went down to some very small number 1588 00:55:07,070 --> 00:55:08,599 of votes, you know, three votes or 1589 00:55:08,600 --> 00:55:09,919 something like that. 1590 00:55:09,920 --> 00:55:12,019 And so Candidate A was declared the 1591 00:55:12,020 --> 00:55:14,239 winner candidate be challenged. 1592 00:55:14,240 --> 00:55:16,399 So they had to do a recount by hand, 1593 00:55:16,400 --> 00:55:17,869 which took a week. 1594 00:55:17,870 --> 00:55:19,429 Then the result went the other way. 1595 00:55:19,430 --> 00:55:21,649 Candidate B was the winner by five 1596 00:55:21,650 --> 00:55:24,079 votes, a challenge and Candidate 1597 00:55:24,080 --> 00:55:25,189 H challenged. 1598 00:55:25,190 --> 00:55:26,749 So then they had to do another recount, 1599 00:55:26,750 --> 00:55:28,249 which took another week. 1600 00:55:28,250 --> 00:55:29,929 And in the end, I can't remember the 1601 00:55:29,930 --> 00:55:31,759 result. But you know, it took three or 1602 00:55:31,760 --> 00:55:33,170 four weeks to 1603 00:55:35,960 --> 00:55:38,149 give the results the final results, which 1604 00:55:38,150 --> 00:55:39,709 were challenge free. 1605 00:55:39,710 --> 00:55:42,079 And so at that time, the Act electoral 1606 00:55:42,080 --> 00:55:43,929 commissioner said, Look, this is silly. 1607 00:55:43,930 --> 00:55:45,179 There's gotta be a better way. 1608 00:55:45,180 --> 00:55:48,109 Let's do it by computer counting. 1609 00:55:48,110 --> 00:55:50,359 But of course, what he or she doesn't 1610 00:55:50,360 --> 00:55:52,489 realize is that by doing it, 1611 00:55:52,490 --> 00:55:54,559 by computer counting, you're putting 1612 00:55:54,560 --> 00:55:56,449 all your eggs in one basket. 1613 00:55:56,450 --> 00:55:58,699 So you have a single point of failure 1614 00:55:58,700 --> 00:56:00,679 and you're putting a lot of trust on that 1615 00:56:00,680 --> 00:56:02,059 single point of failure. 1616 00:56:02,060 --> 00:56:03,529 And that's what we're not able to get 1617 00:56:03,530 --> 00:56:04,530 across to them. 1618 00:56:06,010 --> 00:56:07,210 OK, thank you. 1619 00:56:09,070 --> 00:56:11,559 OK, the next one is, have you proved 1620 00:56:11,560 --> 00:56:13,539 the cook to Husker compiler to be 1621 00:56:13,540 --> 00:56:15,279 correct? And are you certain that you 1622 00:56:15,280 --> 00:56:18,099 don't end up with the force as prediction 1623 00:56:18,100 --> 00:56:20,139 with force as a precondition anyway? 1624 00:56:21,640 --> 00:56:22,149 Right. 1625 00:56:22,150 --> 00:56:24,609 So this is the classic thing of 1626 00:56:24,610 --> 00:56:26,649 formal verification, which is garbage in, 1627 00:56:26,650 --> 00:56:28,149 garbage out. Right? 1628 00:56:28,150 --> 00:56:31,149 So if our formulas are inconsistent, 1629 00:56:31,150 --> 00:56:33,309 then we can prove anything we like. 1630 00:56:33,310 --> 00:56:35,709 And no, there is no proof 1631 00:56:35,710 --> 00:56:37,059 that coke is consistent. 1632 00:56:37,060 --> 00:56:39,129 There could well be some sort of serious 1633 00:56:39,130 --> 00:56:41,679 logical error. You know, in our 1634 00:56:41,680 --> 00:56:43,569 formal coding. 1635 00:56:43,570 --> 00:56:44,570 But. 1636 00:56:45,690 --> 00:56:47,939 At the end of the day, we have a proof 1637 00:56:47,940 --> 00:56:50,129 that a correct certificate implies 1638 00:56:50,130 --> 00:56:52,229 a correct count, right, which 1639 00:56:52,230 --> 00:56:53,369 you can check. 1640 00:56:53,370 --> 00:56:55,709 So even though 1641 00:56:55,710 --> 00:56:58,349 there may be a problem in clock, 1642 00:56:58,350 --> 00:57:00,779 we can tell you that that 1643 00:57:00,780 --> 00:57:03,239 bug in court didn't manifest itself 1644 00:57:03,240 --> 00:57:05,399 in our proof. If our proof is correct 1645 00:57:05,400 --> 00:57:06,510 and you can check the proof. 1646 00:57:08,060 --> 00:57:10,399 Right, so this is classic peer review, 1647 00:57:10,400 --> 00:57:11,659 scientific peer review. 1648 00:57:12,710 --> 00:57:14,509 You know, string theory might be wrong, 1649 00:57:14,510 --> 00:57:16,249 but it passes all the tests that we can 1650 00:57:16,250 --> 00:57:18,799 throw it at the moment because it 1651 00:57:18,800 --> 00:57:20,719 passes all the experiments that we can 1652 00:57:20,720 --> 00:57:21,720 do. 1653 00:57:22,680 --> 00:57:23,680 Yes. 1654 00:57:24,150 --> 00:57:26,699 OK. So I think the next question is 1655 00:57:26,700 --> 00:57:28,789 not completely serious, 1656 00:57:28,790 --> 00:57:30,929 it is does anyone trust a third year 1657 00:57:30,930 --> 00:57:32,100 computer science student? 1658 00:57:35,030 --> 00:57:37,369 Well, frankly, I would entrust 1659 00:57:37,370 --> 00:57:38,989 the third year computer science for the 1660 00:57:38,990 --> 00:57:41,269 Australian University, but I know 1661 00:57:41,270 --> 00:57:43,489 that in Germany, you teach them 1662 00:57:43,490 --> 00:57:45,559 properly and, you know, affordable over 1663 00:57:45,560 --> 00:57:47,519 their diplomas is not trivial. 1664 00:57:47,520 --> 00:57:49,579 So I trust Chairman Fuji computer 1665 00:57:49,580 --> 00:57:50,580 science students. 1666 00:57:51,720 --> 00:57:53,929 OK, I guess a lot of us would be happy 1667 00:57:53,930 --> 00:57:54,930 about that answer. 1668 00:57:56,040 --> 00:57:58,249 OK, the 1669 00:57:58,250 --> 00:58:01,189 next one is to what degree do voters 1670 00:58:01,190 --> 00:58:04,069 trust these voting machines? 1671 00:58:04,070 --> 00:58:05,629 And I'm not sure if if there were any 1672 00:58:05,630 --> 00:58:06,979 voting machines in the truck, but I guess 1673 00:58:06,980 --> 00:58:08,840 you have a better qualified to answer it. 1674 00:58:09,930 --> 00:58:12,109 Right. So in Canberra, 1675 00:58:12,110 --> 00:58:13,999 as I said, we don't have any electronic 1676 00:58:14,000 --> 00:58:16,129 voting, you know, by your 1677 00:58:16,130 --> 00:58:18,199 by your tap tablet or something 1678 00:58:18,200 --> 00:58:20,359 like that, right? What we have is you go 1679 00:58:20,360 --> 00:58:22,519 into a booth and the booth has 1680 00:58:22,520 --> 00:58:24,709 a computer with a screen and 1681 00:58:24,710 --> 00:58:26,269 you prepare, you know, you press the 1682 00:58:26,270 --> 00:58:26,719 buttons. 1683 00:58:26,720 --> 00:58:28,249 I think it's a touch screen. 1684 00:58:28,250 --> 00:58:29,989 You press the, you know, you touch the 1685 00:58:29,990 --> 00:58:31,969 screen to create your ballot and then you 1686 00:58:31,970 --> 00:58:34,039 say, you know, yes, this is the 1687 00:58:34,040 --> 00:58:36,139 ballot that I want to submit. 1688 00:58:36,140 --> 00:58:38,419 And then you get a nice friendly 1689 00:58:38,420 --> 00:58:40,069 screen that says, thank you very much. 1690 00:58:40,070 --> 00:58:42,229 Your your ballot has been cast 1691 00:58:42,230 --> 00:58:44,719 and you know, trust us right 1692 00:58:44,720 --> 00:58:46,939 now. What people should 1693 00:58:46,940 --> 00:58:49,819 be asking is, how do you know 1694 00:58:49,820 --> 00:58:51,919 that the ballot that you show 1695 00:58:51,920 --> 00:58:54,019 on the screen is the one that 1696 00:58:54,020 --> 00:58:55,489 you're actually casting? 1697 00:58:55,490 --> 00:58:57,199 How do you know that the machine isn't 1698 00:58:57,200 --> 00:58:59,599 making a mistake and casting, you know, 1699 00:58:59,600 --> 00:59:01,699 vote one Raj every 1700 00:59:01,700 --> 00:59:02,700 time? 1701 00:59:03,170 --> 00:59:05,389 And unfortunately, the 1702 00:59:05,390 --> 00:59:07,459 average voter is 1703 00:59:07,460 --> 00:59:09,529 not sophisticated enough to 1704 00:59:09,530 --> 00:59:11,539 ask these sorts of questions. 1705 00:59:11,540 --> 00:59:13,939 And so what they do is they say, Well, 1706 00:59:13,940 --> 00:59:16,219 you know, I can't check a pen and paper 1707 00:59:16,220 --> 00:59:17,569 election. 1708 00:59:17,570 --> 00:59:18,619 Who do I trust? 1709 00:59:18,620 --> 00:59:20,419 I trust the election authority. 1710 00:59:20,420 --> 00:59:22,279 And in this case, I do the same. 1711 00:59:22,280 --> 00:59:24,469 I don't know enough about 1712 00:59:24,470 --> 00:59:26,569 computer computers to know 1713 00:59:26,570 --> 00:59:28,909 that what's on the screen is what's 1714 00:59:28,910 --> 00:59:30,979 being cast, but I trust 1715 00:59:30,980 --> 00:59:32,269 the Election Commission to have done 1716 00:59:32,270 --> 00:59:33,270 their job. 1717 00:59:35,850 --> 00:59:36,850 OK. Yeah. 1718 00:59:38,000 --> 00:59:40,149 So another one 1719 00:59:40,150 --> 00:59:42,249 wants to know, how can you 1720 00:59:42,250 --> 00:59:44,529 clarify if you can clarify 1721 00:59:44,530 --> 00:59:46,089 whether and how you distinguish e 1722 00:59:46,090 --> 00:59:47,590 counting from e-voting? 1723 00:59:49,340 --> 00:59:51,499 Right. So if you remember, right 1724 00:59:51,500 --> 00:59:53,959 at the beginning, I gave you this idea 1725 00:59:53,960 --> 00:59:56,059 of end to end verifiable 1726 00:59:56,060 --> 00:59:57,139 voting. 1727 00:59:57,140 --> 00:59:58,489 Right, do you remember there was this 1728 00:59:58,490 --> 01:00:00,619 cascade? There was cast, 1729 01:00:00,620 --> 01:00:03,079 there was there was cast 1730 01:00:03,080 --> 01:00:05,060 as intended, there was 1731 01:00:06,110 --> 01:00:08,779 collected as cast and 1732 01:00:08,780 --> 01:00:10,399 counted as collected. 1733 01:00:10,400 --> 01:00:12,739 So the idea of electronic 1734 01:00:12,740 --> 01:00:15,289 voting is that you have all of these, 1735 01:00:15,290 --> 01:00:17,869 right? So you know, you cast your 1736 01:00:17,870 --> 01:00:19,519 ballot on your tablet. 1737 01:00:19,520 --> 01:00:21,589 Somehow, the tablet has 1738 01:00:21,590 --> 01:00:24,139 to give you evidence that 1739 01:00:24,140 --> 01:00:26,299 what you created on the 1740 01:00:26,300 --> 01:00:28,519 tablet was actually the electronic ballot 1741 01:00:28,520 --> 01:00:29,779 that was cast. 1742 01:00:29,780 --> 01:00:32,059 Then, you know, the the tablet 1743 01:00:32,060 --> 01:00:34,129 sends the ballot somehow 1744 01:00:34,130 --> 01:00:36,559 magically over the internet to 1745 01:00:36,560 --> 01:00:38,689 the election authority, and the election 1746 01:00:38,690 --> 01:00:40,759 authority has to produce some evidence 1747 01:00:40,760 --> 01:00:43,399 that you can verify that the 1748 01:00:43,400 --> 01:00:45,499 electronic ballot wasn't tampered with in 1749 01:00:45,500 --> 01:00:47,599 transit. And finally, 1750 01:00:47,600 --> 01:00:49,429 when the election authority publishes a 1751 01:00:49,430 --> 01:00:51,499 result, they have to provide some 1752 01:00:51,500 --> 01:00:54,049 evidence, publicly verifiable evidence 1753 01:00:54,050 --> 01:00:56,209 that you can 1754 01:00:56,210 --> 01:00:58,729 check to say that your ballot was 1755 01:00:58,730 --> 01:01:00,739 actually in the count right now. 1756 01:01:00,740 --> 01:01:03,109 So that's the traditional way of doing 1757 01:01:03,110 --> 01:01:04,699 electronic voting. 1758 01:01:04,700 --> 01:01:07,279 There are systems out there that do that. 1759 01:01:07,280 --> 01:01:09,709 As I said in Canberra, we have booth 1760 01:01:09,710 --> 01:01:10,819 based voting. 1761 01:01:10,820 --> 01:01:13,159 So you cast your ballot inside 1762 01:01:13,160 --> 01:01:16,129 a booth in privacy on a computer 1763 01:01:16,130 --> 01:01:18,619 that they say works properly. 1764 01:01:18,620 --> 01:01:21,319 Then the ballot is 1765 01:01:21,320 --> 01:01:23,779 somehow transferred to the election of 1766 01:01:23,780 --> 01:01:25,789 authority, which they say is secure and 1767 01:01:25,790 --> 01:01:27,139 everything is fine. 1768 01:01:27,140 --> 01:01:29,299 They count the ballots according to their 1769 01:01:29,300 --> 01:01:31,039 computer program, which they won't show 1770 01:01:31,040 --> 01:01:33,109 us, and they assure us that everything 1771 01:01:33,110 --> 01:01:35,689 is fine. So as you can see in Canberra, 1772 01:01:35,690 --> 01:01:37,189 we have nothing. 1773 01:01:37,190 --> 01:01:39,949 We have no end to end verifiability 1774 01:01:39,950 --> 01:01:41,419 because we have to trust the Election 1775 01:01:41,420 --> 01:01:44,329 Commission or the vendor at every stage. 1776 01:01:44,330 --> 01:01:45,469 Does that answer the question? 1777 01:01:47,750 --> 01:01:50,989 I guess so, so basically, you're 1778 01:01:50,990 --> 01:01:52,919 tackling this third of the three problems 1779 01:01:52,920 --> 01:01:55,009 without leaving the US to 1780 01:01:55,010 --> 01:01:56,010 out of scope. 1781 01:01:56,840 --> 01:01:57,919 Yeah, OK. 1782 01:01:57,920 --> 01:01:59,959 So another and there are cryptographic, 1783 01:01:59,960 --> 01:02:00,859 they're equipped. 1784 01:02:00,860 --> 01:02:02,299 There are incredibly intricate 1785 01:02:02,300 --> 01:02:04,099 cryptographic methods to solve the first 1786 01:02:04,100 --> 01:02:05,100 two. 1787 01:02:05,340 --> 01:02:07,509 And, OK, so another 1788 01:02:07,510 --> 01:02:09,729 one was in Germany, we have more, 1789 01:02:09,730 --> 01:02:11,529 more bizarre voting methods than a single 1790 01:02:11,530 --> 01:02:13,659 transferable votes and the idea of 1791 01:02:13,660 --> 01:02:15,969 if this would work with cumulative voting 1792 01:02:15,970 --> 01:02:19,179 or pan sorry, French 1793 01:02:19,180 --> 01:02:20,679 pan check or 1794 01:02:22,360 --> 01:02:23,859 it's red panacea. 1795 01:02:23,860 --> 01:02:25,809 Yes, I kind of think so. 1796 01:02:25,810 --> 01:02:28,239 Yeah. So in other words, is it a solution 1797 01:02:28,240 --> 01:02:30,130 for all situations? 1798 01:02:32,140 --> 01:02:34,749 The simple answer is, I don't know. 1799 01:02:34,750 --> 01:02:36,159 I haven't tried. 1800 01:02:36,160 --> 01:02:38,799 But as I said, my colleagues in culture 1801 01:02:38,800 --> 01:02:41,139 there's a there's a theoretical computer 1802 01:02:41,140 --> 01:02:42,779 science group and a verification, a 1803 01:02:42,780 --> 01:02:44,560 formal message group in Cultura. 1804 01:02:45,700 --> 01:02:48,249 They would be the people to understand 1805 01:02:48,250 --> 01:02:49,449 the German system. 1806 01:02:49,450 --> 01:02:51,309 I'm sorry, I just haven't. 1807 01:02:51,310 --> 01:02:52,719 I just haven't had a look. 1808 01:02:55,330 --> 01:02:56,330 OK. 1809 01:02:57,310 --> 01:02:59,529 But I have a I have a reverse question. 1810 01:02:59,530 --> 01:03:01,719 You said that the German system 1811 01:03:01,720 --> 01:03:04,029 is a bit bizarre, but I mean, 1812 01:03:04,030 --> 01:03:06,189 counting itself is pretty arcane as well, 1813 01:03:06,190 --> 01:03:08,469 right? So does it get any more 1814 01:03:08,470 --> 01:03:10,539 bizarre than STV 1815 01:03:10,540 --> 01:03:12,159 in Germany? 1816 01:03:12,160 --> 01:03:14,019 That's a good question. 1817 01:03:16,510 --> 01:03:18,789 I haven't looked into into the federal 1818 01:03:18,790 --> 01:03:21,429 election system lately, but it didn't 1819 01:03:21,430 --> 01:03:23,469 look so complicated to me. 1820 01:03:23,470 --> 01:03:25,449 But it could be in the local elections 1821 01:03:25,450 --> 01:03:27,339 that there are more complicated voting 1822 01:03:27,340 --> 01:03:28,340 systems. 1823 01:03:30,810 --> 01:03:32,879 But that's just my unqualified answer, 1824 01:03:32,880 --> 01:03:35,559 so that's probably a lot more, 1825 01:03:35,560 --> 01:03:37,919 lot more qualified people. 1826 01:03:37,920 --> 01:03:40,289 So so what's known is that Steve 1827 01:03:40,290 --> 01:03:42,809 is actually one of the hottest. 1828 01:03:42,810 --> 01:03:44,909 Okay, so there's an area called social 1829 01:03:44,910 --> 01:03:47,339 choice theory where, you know, people 1830 01:03:47,340 --> 01:03:49,019 typically mathematicians compare 1831 01:03:49,020 --> 01:03:50,729 different voting schemes. 1832 01:03:50,730 --> 01:03:52,799 And, you know, people have come 1833 01:03:52,800 --> 01:03:55,079 up with many other alternatives to STV 1834 01:03:55,080 --> 01:03:57,299 to try and make it fairer or better. 1835 01:03:57,300 --> 01:03:59,339 You know, there are at least 10 different 1836 01:03:59,340 --> 01:04:01,259 voting schemes that we could discuss. 1837 01:04:01,260 --> 01:04:03,179 But Steve is known to be one of the more 1838 01:04:03,180 --> 01:04:05,249 arcane ones because, you know, 1839 01:04:05,250 --> 01:04:07,619 everything depends on, for example, 1840 01:04:07,620 --> 01:04:09,419 how do you break ties? 1841 01:04:09,420 --> 01:04:11,609 How do you decide 1842 01:04:11,610 --> 01:04:13,319 who's the weakest candidate and this sort 1843 01:04:13,320 --> 01:04:15,689 of stuff? And for example, 1844 01:04:15,690 --> 01:04:16,690 in the 1845 01:04:18,030 --> 01:04:20,669 act system, the one in Canberra, 1846 01:04:20,670 --> 01:04:22,589 there's actually a clause which says if 1847 01:04:22,590 --> 01:04:24,749 everything is equal all the way up to 1848 01:04:24,750 --> 01:04:26,669 the beginning, then the election 1849 01:04:26,670 --> 01:04:28,799 commissioner can toss a coin, or he or 1850 01:04:28,800 --> 01:04:31,209 she could choose names out of a hat. 1851 01:04:31,210 --> 01:04:33,779 Right. So that's how, you know, 1852 01:04:33,780 --> 01:04:35,639 bizarre it gets. 1853 01:04:35,640 --> 01:04:36,779 Yeah. 1854 01:04:36,780 --> 01:04:39,269 OK, so someone noted that apparently 1855 01:04:39,270 --> 01:04:41,669 these more bizarre voting systems appear 1856 01:04:41,670 --> 01:04:44,009 in Bavaria like this one of the southern 1857 01:04:44,010 --> 01:04:45,869 states of Germany? 1858 01:04:45,870 --> 01:04:47,969 Yeah, actually, I knew that Bavaria was a 1859 01:04:47,970 --> 01:04:50,129 bit unusual. Yeah, yeah, 1860 01:04:50,130 --> 01:04:52,289 sure. OK, so the last of the 1861 01:04:52,290 --> 01:04:54,389 official questions, how is this 1862 01:04:54,390 --> 01:04:55,589 Typekit generated? 1863 01:04:55,590 --> 01:04:57,809 And the Oscar noted 1864 01:04:57,810 --> 01:04:59,279 that he or she might have missed it to 1865 01:04:59,280 --> 01:05:00,280 the during the talk. 1866 01:05:02,580 --> 01:05:05,039 The certificate is just a naive printout 1867 01:05:05,040 --> 01:05:07,139 of the run of the state machine. 1868 01:05:08,880 --> 01:05:11,219 Right, so I mean, 1869 01:05:11,220 --> 01:05:13,439 strictly speaking, you 1870 01:05:13,440 --> 01:05:15,809 know, we could be cheating, 1871 01:05:15,810 --> 01:05:17,639 what we could be doing is taking your 1872 01:05:17,640 --> 01:05:20,189 ballots and randomly generating 1873 01:05:20,190 --> 01:05:22,529 a certificate and claiming that 1874 01:05:22,530 --> 01:05:24,299 this certificate, correct, contains a 1875 01:05:24,300 --> 01:05:26,129 correct count. We might not even be 1876 01:05:26,130 --> 01:05:27,479 running a program. 1877 01:05:27,480 --> 01:05:29,609 Right? Literally, we could have 1878 01:05:29,610 --> 01:05:31,289 a thousand monkeys sitting on 1879 01:05:31,290 --> 01:05:33,419 typewriters, randomly generating 1880 01:05:33,420 --> 01:05:35,999 a certificate and then after, 1881 01:05:36,000 --> 01:05:38,489 I don't know, say an hour, we say 1882 01:05:38,490 --> 01:05:39,989 this is the certificate. 1883 01:05:39,990 --> 01:05:41,880 Right? And Raj wins. 1884 01:05:43,440 --> 01:05:45,989 But it doesn't matter because 1885 01:05:45,990 --> 01:05:48,389 the proof says that if you 1886 01:05:48,390 --> 01:05:50,789 can verify that the certificate 1887 01:05:50,790 --> 01:05:53,099 is correct, then the count 1888 01:05:53,100 --> 01:05:54,839 that it contains is correct. 1889 01:05:54,840 --> 01:05:56,669 So it doesn't matter if we generate it 1890 01:05:56,670 --> 01:05:58,799 using a random number generator. 1891 01:05:58,800 --> 01:06:01,259 I mean, we don't, of course, but strictly 1892 01:06:01,260 --> 01:06:02,260 speaking, we could. 1893 01:06:04,710 --> 01:06:06,719 OK, thank you. And one last question that 1894 01:06:06,720 --> 01:06:08,519 we had in the studio here. 1895 01:06:08,520 --> 01:06:10,619 And could you maybe elaborate a little 1896 01:06:10,620 --> 01:06:12,509 bit more about what was the problem with 1897 01:06:12,510 --> 01:06:13,619 publishing the vote? 1898 01:06:13,620 --> 01:06:15,389 You said there was this Sicilian attack, 1899 01:06:15,390 --> 01:06:16,859 but yeah, sure. 1900 01:06:16,860 --> 01:06:17,759 OK. 1901 01:06:17,760 --> 01:06:19,829 All right. So this goes back 1902 01:06:19,830 --> 01:06:22,529 to the mafia in Sicily, 1903 01:06:22,530 --> 01:06:24,029 and that's why it's called the Sicilian 1904 01:06:24,030 --> 01:06:25,139 attack. Right. 1905 01:06:25,140 --> 01:06:27,000 So what you want is, you know, 1906 01:06:28,320 --> 01:06:30,359 you're running, you have an election for 1907 01:06:30,360 --> 01:06:32,849 mayor and you want to make sure that Raj 1908 01:06:32,850 --> 01:06:35,039 gets elected because Raj is crooked and 1909 01:06:35,040 --> 01:06:37,079 you can bribe him and, you know, do what? 1910 01:06:37,080 --> 01:06:39,029 Get him to do whatever you want. 1911 01:06:39,030 --> 01:06:41,699 So what you do is you tell 1912 01:06:41,700 --> 01:06:43,769 the voter that I want you to 1913 01:06:43,770 --> 01:06:45,959 vote in a particularly arcane 1914 01:06:45,960 --> 01:06:47,129 way. Right. 1915 01:06:47,130 --> 01:06:49,589 So you vote Frederick 1916 01:06:49,590 --> 01:06:51,659 three and free to 1917 01:06:51,660 --> 01:06:54,809 one. And Raj, 17, 1918 01:06:54,810 --> 01:06:57,239 and you know, you're five 1919 01:06:57,240 --> 01:06:58,240 or something like that. 1920 01:06:59,520 --> 01:07:01,949 And then what you do is if you publish 1921 01:07:01,950 --> 01:07:04,379 the ballots, you can check whether 1922 01:07:04,380 --> 01:07:06,479 that ballot exists. 1923 01:07:06,480 --> 01:07:08,519 You know, is there a ballot that what was 1924 01:07:08,520 --> 01:07:10,889 it, three to 17 year old, five, Raj, 1925 01:07:10,890 --> 01:07:13,089 17, and Fred, one. 1926 01:07:13,090 --> 01:07:15,269 Whatever it was, if that ballot 1927 01:07:15,270 --> 01:07:17,459 is missing, then you know that 1928 01:07:17,460 --> 01:07:19,859 the voter didn't do as you asked. 1929 01:07:19,860 --> 01:07:22,319 And then you can, you know, either 1930 01:07:22,320 --> 01:07:24,569 burn down their house or, you know, 1931 01:07:24,570 --> 01:07:26,099 shoot their children or whatever you've 1932 01:07:26,100 --> 01:07:27,989 done to coerce them, right? 1933 01:07:27,990 --> 01:07:30,059 And so in 1934 01:07:30,060 --> 01:07:32,729 Australia, in STV, 1935 01:07:32,730 --> 01:07:35,429 it's actually very plausible because, 1936 01:07:35,430 --> 01:07:37,409 for example, you know, we have elections 1937 01:07:37,410 --> 01:07:39,569 where there are 43 candidates 1938 01:07:39,570 --> 01:07:42,299 and you can encode your ballot 1939 01:07:42,300 --> 01:07:45,599 in many, many different combinations 1940 01:07:45,600 --> 01:07:47,309 to be unique. 1941 01:07:47,310 --> 01:07:49,379 And so, you know, we ask you to 1942 01:07:49,380 --> 01:07:50,669 vote in this way. 1943 01:07:50,670 --> 01:07:52,529 And once the ballots are published, we 1944 01:07:52,530 --> 01:07:54,749 check whether that particular 1945 01:07:54,750 --> 01:07:56,849 perversely generated ballot 1946 01:07:56,850 --> 01:07:58,019 is in there. 1947 01:07:58,020 --> 01:07:59,789 And what we've done, of course, is made 1948 01:07:59,790 --> 01:08:01,559 sure that we're scattering all the 1949 01:08:01,560 --> 01:08:03,599 candidates except the one that we want to 1950 01:08:03,600 --> 01:08:06,839 win and making them win. 1951 01:08:06,840 --> 01:08:07,840 Does that help? 1952 01:08:08,970 --> 01:08:10,709 Yes. For me, it makes it makes it 1953 01:08:10,710 --> 01:08:12,209 understandable, it basically breaks the 1954 01:08:12,210 --> 01:08:14,159 basic assumption that any vote you would 1955 01:08:14,160 --> 01:08:15,809 like and the way you vote is really 1956 01:08:15,810 --> 01:08:16,810 actually secret. 1957 01:08:18,000 --> 01:08:19,799 That's right. So you can uniquely 1958 01:08:19,800 --> 01:08:22,019 identify a vote because of the complexity 1959 01:08:22,020 --> 01:08:23,639 of the system. 1960 01:08:23,640 --> 01:08:24,869 Yes. 1961 01:08:24,870 --> 01:08:25,858 OK. 1962 01:08:25,859 --> 01:08:28,349 Let me ask the tough questions. 1963 01:08:28,350 --> 01:08:29,938 Perfect. Thank you so much. 1964 01:08:29,939 --> 01:08:32,159 Rush for four for your talk 1965 01:08:32,160 --> 01:08:33,749 and also for for the very detailed 1966 01:08:33,750 --> 01:08:35,849 answers. And thank 1967 01:08:35,850 --> 01:08:36,850 you very much. 1968 01:08:37,680 --> 01:08:39,119 OK. 1969 01:08:39,120 --> 01:08:41,879 And now on the film channel, 1970 01:08:41,880 --> 01:08:42,778 the next. 1971 01:08:42,779 --> 01:08:44,818 The last thing for today happening is the 1972 01:08:44,819 --> 01:08:46,919 Herrod news show at midnight and 1973 01:08:46,920 --> 01:08:48,269 tomorrow it's continues. 1974 01:08:48,270 --> 01:08:50,579 Or we continue at 5:00 p.m. 1975 01:08:50,580 --> 01:08:52,589 with writing lecture notes directly in 1976 01:08:52,590 --> 01:08:54,839 Ludeke and then see you. 1977 01:08:54,840 --> 01:08:55,840 Bye bye.