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.
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.
Original language | English |
---|---|
Title of host publication | 2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017) |
Subtitle of host publication | Proceedings of a meeting held 22-26 May 2017, San Jose, California, USA |
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
Pages | 993-1008 |
Number of pages | 17 |
ISBN (Electronic) | 9781509055333 |
ISBN (Print) | 9781509055340 |
DOIs | |
Publication status | Published - Jul 2017 |
Publication series
Name | |
---|---|
ISSN (Print) | 2375-1207 |
Fingerprint
Dive into the research topics of 'Machine-Checked Proofs of Privacy for Electronic Voting Protocols'. Together they form a unique fingerprint.Profiles
-
Dr François Dupressoir
- School of Computer Science - Associate Professor in Cryptography
Person: Academic
-
Bogdan Warinschi
- School of Computer Science - Professor of Computer Science
- Cryptography and Information Security
Person: Academic , Member