Paper 2018/225

A foundation for secret, verifiable elections

Ben Smyth

Abstract

Many voting systems rely on art, rather than science, to ensure that votes are freely made, with equal influence. Such systems build upon creativity and skill, rather than scientific foundations. These systems are routinely broken in ways that compromise free-choice or permit undue influence. Breaks can be avoided by proving that voting systems satisfy formal notions of voters voting freely and of detecting undue influence. This manuscript provides a detailed technical introduction to a definition of ballot secrecy by Smyth that formalises the former notion and a definition of verifiability by Smyth, Frink & Clarkson that formalises the latter. The definitions are presented in the computational model of cryptography: Ballot secrecy is expressed as the inability to distinguish between an instance of the voting system in which voters cast some votes, from another instance in which the voters cast a permutation of those votes. Verifiability decomposes into individual verifiability, which is expressed as the inability to cause a collision between ballots, and universal verifiability, which is expressed as the inability to cause an incorrect election outcome to be accepted. The definitions are complimented with simple examples that demonstrate the essence of these properties and detailed proofs are constructed to show how secrecy and verifiability can be formally proved. Finally, the Helios and Helios Mixnet voting systems are presented as case studies to provide an understanding of state-of-the-art systems that are being used for binding elections.