SPOOC: Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Véronique Cortier, Benedikt Schmidt, Constantin Catalin Dragan, Pierre-Yves Strub, Francois Dupressoir, and Bogdan Warinschi. Machine-Checked Proofs of Privacy for Electronic Voting Protocols. In Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P'17), pp. 993–1008, IEEE Computer Society Press, San Francisco, CA, USA, May 2017.
doi:10.1109/SP.2017.28

Download

[PDF] [HTML]

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.

BibTeX

@InProceedings{easycrypt-SP17,
  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.  \par 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.
                  },
  author =	 {V\'eronique Cortier and Benedikt Schmidt and
                  Constantin Catalin Dragan and Pierre-Yves Strub and
                  Francois Dupressoir and Bogdan Warinschi},
  title =	 {Machine-Checked Proofs of Privacy for Electronic
                  Voting Protocols},
  booktitle =	 {{P}roceedings of the 37th IEEE Symposium on Security
                  and Privacy (S\&P'17)},
  year =	 2017,
  address =	 {San Francisco, CA, USA},
  month =	 may,
  pages =	 {993--1008},
  publisher =	 {{IEEE} Computer Society Press},
  doi =		 {10.1109/SP.2017.28},
  acronym =	 {{S\&P}'17},
  nmonth =	 5,
                  ={https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7958621},
}