A formal analysis of the Norwegian e-voting protocol

A formal analysis of the Norwegian e-voting protocol. Véronique Cortier and Cyrille Wiedling. Rapport de recherche RR-7781, INRIA, 2011.

Download

[PDF] [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, consid- ering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model.

BibTeX

@techreport{CORTIER:2011:INRIA-00636115:1,
    hal_id = {inria-00636115},
    title = {{A formal analysis of the Norwegian e-voting protocol}},
    author = {Cortier, V{\'e}ronique and Wiedling, Cyrille},
    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, consid- ering several corruption scenarios. Part of this study has conducted using the ProVerif tool, on a simplified model.}},
    keywords = {e-voting, privacy, formal methods},
    language = {Anglais},
    affiliation = {CASSIS - INRIA Lorraine - LORIA / LIFC},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-7781},
    year = {2011},
    month = Nov,
}