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

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 veri-fiability 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.
Type de document :
Rapport
[Research Report] Inria Nancy - Grand Est. 2017
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01616425
Contributeur : Véronique Cortier <>
Soumis le : vendredi 13 octobre 2017 - 16:16:02
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43
Document(s) archivé(s) le : dimanche 14 janvier 2018 - 13:51:37

Fichier

rapport-HAL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01616425, version 1

Citation

Véronique Cortier, David Galindo, Mathieu Turuani. A formal analysis of the Neuchâtel e-voting protocol. [Research Report] Inria Nancy - Grand Est. 2017. 〈hal-01616425〉

Partager

Métriques

Consultations de la notice

305

Téléchargements de fichiers

330