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. In Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P'17), pp. 993–1008, IEEE Computer Society Press, 2017.

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,
  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},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {{P}roceedings of the 37th IEEE Symposium on Security and Privacy (S\&P'17)},
  year = 	 {2017},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  pages = 	 {993--1008},
  OPTmonth = 	 {},
  OPTaddress = 	 {},
  OPTorganization = {},
  publisher = {{IEEE} Computer Society Press},
  OPTannote = 	 {},
  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.
},
doi = {10.1109/SP.2017.28},
}