A formal analysis of the Neuchâtel e-voting protocol

Veronique Cortier; David Galindo; Mathieu  Turuani

doi:10.1109/EuroSP.2018.00037

A formal analysis of the Neuchâtel e-voting protocol

Veronique Cortier, David Galindo, Mathieu Turuani

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

8 Citations (Scopus)

241 Downloads (Pure)

Abstract

Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and veriﬁability properties. Our analysis mostly conﬁrms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast veriﬁability, even if the voter’s device is compromised. To our knowledge, this is the ﬁrst time a full-ﬂedged automatic symbolic analysis of an e-voting system used for politically binding elections has been realized.

Original language	English
Title of host publication	Proceedings of 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Number of pages	13
DOIs	https://doi.org/10.1109/EuroSP.2018.00037
Publication status	E-pub ahead of print - Jul 2018
Event	3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P) - London, United Kingdom Duration: 24 Apr 2018 → 26 Apr 2018

Conference

Conference	3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)
Country/Territory	United Kingdom
City	London
Period	24/04/18 → 26/04/18

Access to Document

10.1109/EuroSP.2018.00037

Cortier_et_al_A_formal_analysis_IEEE_Conference_publication
(c) IEEE 2018. Publication in Proceedings of 3rd IEEE European Symposium on Security and Privacy 2018: 10.1109/EuroSP.2018.00037
Accepted author manuscript, 372 KBLicence: None: All rights reserved

Cite this

@inproceedings{67dd6ac979344ab39a0f41e62af7a6cf,

title = "A formal analysis of the Neuch{\^a}tel e-voting protocol",

abstract = "Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuch{\^a}tel. We design a detailed model of the protocol in ProVerif for both privacy and veriﬁability properties. Our analysis mostly conﬁrms the security of the underlying protocol: we show that the Neuch{\^a}tel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast veriﬁability, even if the voter{\textquoteright}s device is compromised. To our knowledge, this is the ﬁrst time a full-ﬂedged automatic symbolic analysis of an e-voting system used for politically binding elections has been realized.",

author = "Veronique Cortier and David Galindo and Mathieu Turuani",

year = "2018",

month = jul,

doi = "10.1109/EuroSP.2018.00037",

language = "English",

booktitle = "Proceedings of 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

note = "3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P) ; Conference date: 24-04-2018 Through 26-04-2018",

}

Cortier, V, Galindo, D & Turuani, M 2018, A formal analysis of the Neuchâtel e-voting protocol. in Proceedings of 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P). Institute of Electrical and Electronics Engineers (IEEE), 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P), London, United Kingdom, 24/04/18. https://doi.org/10.1109/EuroSP.2018.00037

TY - GEN

T1 - A formal analysis of the Neuchâtel e-voting protocol

AU - Cortier, Veronique

AU - Galindo, David

AU - Turuani, Mathieu

PY - 2018/7

Y1 - 2018/7

N2 - Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and veriﬁability properties. Our analysis mostly conﬁrms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast veriﬁability, even if the voter’s device is compromised. To our knowledge, this is the ﬁrst time a full-ﬂedged automatic symbolic analysis of an e-voting system used for politically binding elections has been realized.

AB - Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and veriﬁability properties. Our analysis mostly conﬁrms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast veriﬁability, even if the voter’s device is compromised. To our knowledge, this is the ﬁrst time a full-ﬂedged automatic symbolic analysis of an e-voting system used for politically binding elections has been realized.

U2 - 10.1109/EuroSP.2018.00037

DO - 10.1109/EuroSP.2018.00037

M3 - Conference contribution

BT - Proceedings of 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)

Y2 - 24 April 2018 through 26 April 2018

ER -

A formal analysis of the Neuchâtel e-voting protocol

Abstract

Conference

Access to Document

Fingerprint

Cite this