Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1) , (2) , (3) , (4) , (5) , (3) , (6) , (4)
1
2
3
4
5
6

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.
Fichier principal
Vignette du fichier
main.pdf (428.36 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03913573 , version 1 (27-12-2022)

Identifiers

Cite

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. pp.335-347, ⟨10.1109/CSF54842.2022.9919663⟩. ⟨hal-03913573⟩
0 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More