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
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}, }