Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
Véronique Cortier, Constantin Catalin Dragan, Pierre-Yves Strub, Francois Dupressoir, and Bogdan Warinschi. Machine-checked proofs for electronic voting: privacy and verifiability for Belenios. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pp. 298–312, IEEE Computer Society Press, July 2018.
doi:10.1109/CSF.2018.00029
Download
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.
BibTeX
@InProceedings{Belenios-Easycrypt-CSF18,
author = {V\'eronique Cortier and Constantin Catalin Dragan
and Pierre-Yves Strub and Francois Dupressoir and
Bogdan Warinschi},
title = {Machine-checked proofs for electronic voting:
privacy and verifiability for Belenios},
booktitle = {{P}roceedings of the 31st {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'18)},
year = 2018,
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. \par 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. \par 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. },
month = jul,
pages = {298--312},
publisher = {{IEEE} Computer Society Press},
year = 2018,
acronym = {{CSF}'18},
nmonth = 7,
={https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8429313},
doi = {10.1109/CSF.2018.00029}
}