A formal analysis of the Norwegian E-voting protocol

A formal analysis of the Norwegian E-voting protocol. Véronique Cortier and Cyrille Wiedling. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), pp. 109–128, Lecture Notes in Computer Science 7215, Springer, Tallinn, Estonia, March 2012.

Download

[PDF] [long version] [HTML]

Abstract

Norway has used e-voting in its last political election in September 2011, with more than 25 000 voters using the e-voting option. The underlying protocol is a new protocol designed by the ERGO group, involving several actors (a bulletin box but also 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. Formal definitions of properties such as privacy, coercion-resistance or verifiability have been recently proposed, based on equivalence properties.
In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. privacy, considering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model.

BibTeX

@inproceedings{post12-vote,
doi = {10.1007/978-3-642-28641-4_7},
   address = {Tallinn, Estonia}, 
   author = {Cortier, V{\'e}ronique and Wiedling, Cyrille}, 
   booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, 
   month = mar, 
   publisher = {Springer}, 
   series = {Lecture Notes in Computer Science}, 
   title = {A formal analysis of the Norwegian E-voting protocol}, 
   volume    = {7215},
   year      = {2012},
   pages     = {109--128},
   abstract = {Norway has used e-voting in its last political election in September 2011, with more than 25 000 voters using the e-voting option. The underlying protocol is a new protocol designed by the ERGO group, involving several actors (a bulletin box but also 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. Formal definitions of properties such as privacy, coercion-resistance or verifiability have been recently proposed, based on equivalence properties.
\par 
In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. privacy, considering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model.},
}