University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Machine-checked proofs for electronic voting: privacy and verifiability for Belenios

Cortier, Véronique, Dragan, Constantin Cătălin, Dupressoir, Francois and Warinschi, Bogdan (2018) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios In: 31st IEEE Computer Security Foundations Symposium, 09-12 Jul 2018, Oxford, UK.

[img]
Preview
Text
Machine-checked proofs for electronic voting.pdf - Accepted version Manuscript

Download (412kB) | Preview

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.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
NameEmailORCID
Cortier, Véronique
Dragan, Constantin Cătălinc.dragan@surrey.ac.uk
Dupressoir, Francoisf.dupressoir@surrey.ac.uk
Warinschi, Bogdan
Date : 9 August 2018
Funders : Engineering and Physical Sciences Research Council (EPSRC)
DOI : 10.1109/CSF.2018.00029
Copyright Disclaimer : © 2018 the Author(s).
Related URLs :
Depositing User : Clive Harris
Date Deposited : 01 May 2018 07:58
Last Modified : 11 Dec 2018 11:24
URI: http://epubs.surrey.ac.uk/id/eprint/846330

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800