Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Abstract : We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme. In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.
Type de document :
Communication dans un congrès
38th IEEE Symposium on Security and Privacy (S&P'17), May 2017, San Jose, United States. pp.993 - 1008, 2017, 〈10.1109/SP.2017.28〉
Liste complète des métadonnées

Littérature citée [40 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01624270
Contributeur : Véronique Cortier <>
Soumis le : jeudi 26 octobre 2017 - 10:39:59
Dernière modification le : jeudi 10 mai 2018 - 02:06:01
Document(s) archivé(s) le : samedi 27 janvier 2018 - 13:38:24

Fichier

SP17(1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Véronique Cortier, Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, et al.. Machine-Checked Proofs of Privacy for Electronic Voting Protocols. 38th IEEE Symposium on Security and Privacy (S&P'17), May 2017, San Jose, United States. pp.993 - 1008, 2017, 〈10.1109/SP.2017.28〉. 〈hal-01624270〉

Partager

Métriques

Consultations de la notice

398

Téléchargements de fichiers

97