Abstract

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