ABSTRACT. We present a machine-checked security analysis of Belenios-- a deployed voting protocol which has already been used 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, e.g. how to deal with revote policies.

Together, our results yield the first machine-checked analysis of both privacy and verifiability properties for a deployed electronic voting protocol. Last, but not least, 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 a need for the development of less specific security notions for electronic voting protocols with registration authorities.