A formal analysis of the Norwegian E-voting protocol

A formal analysis of the Norwegian E-voting protocol. Véronique Cortier and Cyrille Wiedling. Journal of Computer Security, 25(15777):21–57, 2017.

Download

[PDF] [HTML]

Abstract

Norway used e-voting in its last political election both in September 2011 and September 2013, with more than 28,000 voters using the e-voting option in 2011, and 70,000 in 2013. While some other countries use a black-box, proprietary voting solution, Norway has made its system publicly available. The underlying protocol, designed by Scytl, involves several authorities (a ballot box, a receipt generator, a decryption service, and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. ballot secrecy, considering several corruption scenarios. We use a state-of-the-art definition of ballot secrecy, based on equivalence properties and stated in the applied pi-calculus.

BibTeX

@Article{JCS2016,
  author = 	 {V\'eronique Cortier and Cyrille Wiedling},
  title = 	 {A formal analysis of the Norwegian E-voting protocol},
  journal = 	 {Journal of Computer Security},
  year = 	 {2017},
  OPTkey = 	 {},
  volume = 	 {25},
  number = 	 {15777},
  pages = 	 {21--57},
  OPTmonth = 	 {},
  OPTannote = 	 {},
  abstract = {Norway used e-voting in its last political election both in September
2011 and September 2013, with more than 28,000 voters using the
e-voting option in 2011, and 70,000 in 2013. While some other
countries use a black-box, proprietary voting solution, Norway has
made its system publicly available. The underlying protocol, designed by Scytl, involves several authorities (a ballot box, a receipt generator, a decryption service,  and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. ballot secrecy, considering several corruption scenarios. We use a state-of-the-art definition of ballot secrecy, based on equivalence properties and stated in the applied pi-calculus. 
},
doi ={10.3233/JCS-15777},
}