A formal analysis of the Norwegian e-voting protocol

Véronique Cortier 1 Cyrille Wiedling 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Reports
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00636115
Contributor : Cyrille Wiedling <>
Submitted on : Wednesday, October 26, 2011 - 5:33:25 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Thursday, March 30, 2017 - 6:11:39 PM

File

RR-7781.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00636115, version 1

Citation

Véronique Cortier, Cyrille Wiedling. A formal analysis of the Norwegian e-voting protocol. [Research Report] RR-7781, INRIA. 2011. ⟨inria-00636115⟩

Share

Metrics

Record views

524

Files downloads

478