skip to content

Department of Computer Science and Technology

Friday, 21 January, 2022 - 14:00 to 15:00
Mukesh Tiwari, University of Cambridge

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].


Seminar series: 
Logic and Semantics Seminar

Upcoming seminars