Paper 2022/1182

Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co

Constantin Cătălin Drăgan, University of Surrey
François Dupressoir, University of Bristol
Ehsan Estaji, University of Luxembourg
Kristian Gjøsteen, Norwegian University of Science and Technology
Thomas Haines, Australian National University
Peter Y. A. Ryan, University of Luxembourg
Peter B. Rønne, University of Lorraine, University of Luxembourg
Morten Rotvold Solberg, Norwegian University of Science and Technology

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.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. 2022 IEEE 35th Computer Security Foundations Symposium (CSF)
Formal verification e-voting Selene privacy
Contact author(s)
c dragan @ surrey ac uk
f dupressoir @ bristol ac uk
ehsan estaji @ uni lu
kristian gjosteen @ ntnu no
thomas haines @ anu edu au
peter roenne @ gmail com
mosolb @ ntnu no
2022-09-09: approved
2022-09-09: received
See all versions
Short URL
Creative Commons Attribution


      author = {Constantin Cătălin Drăgan and François Dupressoir and Ehsan Estaji and Kristian Gjøsteen and Thomas Haines and Peter Y. A. Ryan and Peter B. Rønne and Morten Rotvold Solberg},
      title = {Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1182},
      year = {2022},
      doi = {10.1109/CSF54842.2022.00021},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.