Skip to content

Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publication2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017)
Subtitle of host publicationProceedings of a meeting held 22-26 May 2017, San Jose, California, USA
Publisher or commissioning bodyInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages17
ISBN (Electronic)9781509055333
ISBN (Print)9781509055340
DateAccepted/In press - 9 Feb 2017
DateE-pub ahead of print - 26 Jun 2017
DatePublished (current) - Jul 2017

Publication series

ISSN (Print)2375-1207


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.

Download statistics

No data available



  • Full-text PDF (accepted author manuscript)

    Rights statement: This is the author accepted manuscript (AAM). The final published version (version of record) is available online via IEEE at Please refer to any applicable terms of use of the publisher.

    Accepted author manuscript, 447 KB, PDF document


View research connections

Related faculties, schools or groups