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

Constantin Cătălin Drăgan; François Dupressoir; Ehsan Estaji; Kristian Gjøsteen; Thomas Haines; Peter Y. A. Ryan; Peter B. Rønne; Morten Rotvold Solberg

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

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.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. 2022 IEEE 35th Computer Security Foundations Symposium (CSF)
DOI: 10.1109/CSF54842.2022.00021
Keywords: 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
History: 2022-09-09: approved; 2022-09-09: received; See all versions
Short URL: https://ia.cr/2022/1182
License: CC BY

BibTeX

@misc{cryptoeprint:2022/1182,
      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{https://eprint.iacr.org/2022/1182}},
      url = {https://eprint.iacr.org/2022/1182}
}