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

Véronique Cortier, David Galindo, and Mathieu Turuani. A formal analysis of the Neuchâtel e-voting protocol. In 3rd IEEE European Symposium on Security and Privacy (EuroSP'18), London, UK, April 2018.
doi:10.1109/EuroSP.2018.00037

Download

[PDF] [HTML] 

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 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.

BibTeX

@InProceedings{Neufchatel-EuroSP18,
  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.  \par 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.},
  author =	 {V\'eronique Cortier and David Galindo and Mathieu
                  Turuani},
  title =	 {A formal analysis of the Neuch\^atel e-voting
                  protocol},
  booktitle =	 {3rd IEEE European Symposium on Security and Privacy
                  (EuroSP'18)},
  year =	 2018,
  month =	 {April},
  address =	 {London, UK},
  doi =		 {10.1109/EuroSP.2018.00037},
                  ={https://members.loria.fr/VCortier/files/Papers/EuroSP18.pdf},
}