BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Theorem Provers to Protect Democracy: Formally Verified Vote-Count
 ing-Software - Mukesh Tiwari\, University of Cambridge
DTSTART:20220121T140000Z
DTEND:20220121T150000Z
UID:TALK163306@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:THIS SEMINAR WILL BE IN ROOM SS03\n\nPaper ballots are widely 
 used around the world to record\nthe preferences of eligible voters. Paper
  ballots provide three important ingredients: (i) correctness\, (ii) verif
 iability\, and (iii) privacy.\nHowever\, a paper ballot election brings va
 rious other challenges\, e.g.\, it is slow for large democracies like Indi
 a\, error prone for\ncomplex voting methods like single transferable vote\
 , and poses operational challenges for large countries like Australia. In 
 order to\nmitigate these problems\, and various others\, many countries ar
 e adopting electronic voting. However\, electronic voting introduces a new
 \nset of problems. In most cases\, the software programs --written in unso
 und languages like C\, Java and used to conduct elections--\nhave numerous
  problems\, including\, but not limited to\, counting bugs\, ballot identi
 fication\, etc. Moreover\, these software programs  are\nproprietary artif
 acts and are not allowed to be inspected by members of the public. As a co
 nsequence\, the result\nproduced by these software programs can not be sub
 stantiated.\n\nIn this talk\, I will address three main concerns of electr
 onic voting:  (i) correctness\, (ii) verifiability\, and (iii) privacy.  M
 ore specifically\,\nI will demonstrate the correctness by implementing the
  vote counting algorithm (Schulze Method) in Coq theorem prover\,\nthe ver
 ifiability by generating an independently checkable scrutiny sheet\, and t
 he privacy by using cryptography. This work\nwas done as a part of my PhD 
 [1] at the Australian National University\, Canberra\, Australia and  you 
 can check the Coq formalisation [2\, 3].\n\n[1] https://github.com/mukesht
 iwari/Thesis/blob/master/thesisTemplate/thesis.pdf\n[2] https://github.com
 /mukeshtiwari/formalized-voting/tree/master/schulze-modified\n[3] https://
 github.com/mukeshtiwari/EncryptionSchulze/tree/master/code/Workingcode
LOCATION:tba
END:VEVENT
END:VCALENDAR