Theorem Provers to Protect Democracy: Formally Verified Vote-Counting-Software

Add to your list(s) Download to your calendar using vCal

• Mukesh Tiwari, University of Cambridge
• Friday 21 January 2022, 14:00-15:00
• tba.

If you have a question about this talk, please contact Jamie Vicary.

THIS SEMINAR WILL BE IN ROOM SS03

Paper ballots are widely used around the world to record the preferences of eligible voters. Paper ballots provide three important ingredients: (i) correctness, (ii) verifiability, and (iii) privacy. However, a paper ballot election brings various other challenges, e.g., it is slow for large democracies like India, error prone for complex voting methods like single transferable vote, and poses operational challenges for large countries like Australia. In order to mitigate these problems, and various others, many countries are adopting electronic voting. However, electronic voting introduces a new set of problems. In most cases, the software programs—written in unsound languages like C, Java and used to conduct elections— have numerous problems, including, but not limited to, counting bugs, ballot identification, etc. Moreover, these software programs are proprietary artifacts and are not allowed to be inspected by members of the public. As a consequence, the result produced by these software programs can not be substantiated.

In this talk, I will address three main concerns of electronic voting: (i) correctness, (ii) verifiability, and (iii) privacy. More specifically, I will demonstrate the correctness by implementing the vote counting algorithm (Schulze Method) in Coq theorem prover, the verifiability by generating an independently checkable scrutiny sheet, and the privacy by using cryptography. This work was done as a part of my PhD [1] at the Australian National University, Canberra, Australia and you can check the Coq formalisation [2, 3].

[1] https://github.com/mukeshtiwari/Thesis/blob/master/thesisTemplate/thesis.pdf [2] https://github.com/mukeshtiwari/formalized-voting/tree/master/schulze-modified [3] https://github.com/mukeshtiwari/EncryptionSchulze/tree/master/code/Workingcode

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tba
• yk373's list

Note that ex-directory lists are not shown.