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

Veronique Cortier, David Galindo, Mathieu Turuani

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)
221 Downloads (Pure)


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 verifiability properties. Our analysis mostly confirms 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 verifiability, even if the voter’s device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically binding elections has been realized.
Original languageEnglish
Title of host publicationProceedings of 3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages13
Publication statusE-pub ahead of print - Jul 2018
Event3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P) - London, United Kingdom
Duration: 24 Apr 201826 Apr 2018


Conference3rd IEEE European Symposium on Security and Privacy 2018 (EuroS&P)
Country/TerritoryUnited Kingdom


Dive into the research topics of 'A formal analysis of the Neuchâtel e-voting protocol'. Together they form a unique fingerprint.

Cite this