Affiliations: [a] Surrey Centre for Cyber Security, University of Surrey, Guildford, United Kingdom | [b] Department of Computer Science, University of Bristol, Bristol, United Kingdom | [c] Department of Computer Science & SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg | [d] Department of Mathematical Sciences, NTNU, Trondheim, Norway | [e] School of Computing, Australian National University, Canberra, Australia | [f] Department of Computer Science & SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg | [g] LORIA, CNRS & Univ Lorraine, France | [h] University of Luxembourg, Esch-sur-Alzette, Luxembourg | [i] Department of Mathematical Sciences, NTNU, Trondheim, Norway
Note: [1] This paper is an extended and revised version of a paper presented at CSF’22.
Abstract: Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the state of the art by taking into account that verification in many schemes will happen or must happen after the tally has been published, not before as in previous definitions. As a case study we give a machine-checked proof of privacy for Selene, which is a remote electronic voting scheme which offers an attractive mix of security properties and usability. Prior to our work, the computational privacy of Selene has never been formally verified. Finally, we also prove that MiniVoting and Belenios satisfies our definition.
