Machine-checked proofs for electronic voting: Privacy and verifiability for belenios

Veronique Cortier*, Constantin Catalin Dragan, Francois Dupressoir, Bogdan Warinschi

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

4 Citations (Scopus)

Abstract

We present a machine-checked security analysis of Belenios - a deployed voting protocol used already in more than 200 elections. Belenios extends Helios with an explicit registration authority to obtain eligibility guarantees. We offer two main results. First, we build upon a recent framework for proving ballot privacy in EasyCrypt. Inspired by our application to Belenios, we adapt and extend the privacy security notions to account for protocols that include a registration phase. Our analysis identifies a trust assumption which is missing in the existing (pen and paper) analysis of Belenios: Ballot privacy does not hold if the registrar misbehaves, even if the role of the registrar is seemingly to provide eligibility guarantees. Second, we develop a novel framework for proving strong verifiability in EasyCrypt and apply it to Belenios. In the process, we clarify several aspects of the pen-and-paper proof, such as how to deal with revote policies. Together, our results yield the first machine-checked analysis of both ballot privacy and verifiability properties for a deployed electronic voting protocol. Perhaps more importantly, we identify several issues regarding the applicability of existing definitions of privacy and verifiability to systems other than Helios. While we show how to adapt the definitions to the particular case of Belenios, our findings indicate the need for more general security notions for electronic voting protocols with registration authorities.

Original languageEnglish
Title of host publication2018 IEEE 31st Computer Security Foundations Symposium (CSF 2018)
Subtitle of host publicationProceedings of a meeting held 9-12 July 2018, Oxford, United Kingdom
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages298-312
Number of pages15
ISBN (Electronic)9781538666807
ISBN (Print)9781538666814
DOIs
Publication statusPublished - Sep 2018
Event31st IEEE Computer Security Foundations Symposium, CSF 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

Name
ISSN (Print)2374-8303

Conference

Conference31st IEEE Computer Security Foundations Symposium, CSF 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Keywords

  • Easycrypt
  • electronic-voting
  • machine-checked-proofs
  • privacy
  • verifiability

Fingerprint Dive into the research topics of 'Machine-checked proofs for electronic voting: Privacy and verifiability for belenios'. Together they form a unique fingerprint.

  • Cite this

    Cortier, V., Dragan, C. C., Dupressoir, F., & Warinschi, B. (2018). Machine-checked proofs for electronic voting: Privacy and verifiability for belenios. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF 2018): Proceedings of a meeting held 9-12 July 2018, Oxford, United Kingdom (pp. 298-312). [8429313] Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/CSF.2018.00029