University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Theorem Provers to Protect Democracy: Formally Verified Vote-Counting-Software

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

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

  • UserMukesh Tiwari, University of Cambridge
  • ClockFriday 21 January 2022, 14:00-15:00
  • Housetba.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity