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

Constantin Catalin Dragan (1) , Francois Dupressoir (2) , Ehsan Estaji (3) , Kristian Gjøsteen (4) , Thomas Haines (5) , Peter Y.A. Ryan (3) , Peter Rønne (6) , Morten Rotvold Solberg (4)

1 UNIS - University of Surrey
2 University of Bristol [Bristol]
3 University of Luxembourg [Luxembourg]
4 NTNU Samfunnsforskning AS / NTNU Social Research
5 ANU - Australian National University
6 PESTO - Proof techniques for security protocols

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.

Domains: Cryptography and Security [cs.CR]

Constantin Catalin Dragan, Francois Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, et al.. Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co. 2022 IEEE 35th Computer Security Foundations Symposium (CSF), Aug 2022, Haifa, Israel. ⟨10.1109/CSF54842.2022.9919663⟩. ⟨hal-03913573v2⟩