Towards Verifying Voter Privacy Through Unlinkability

Abstract : The increasing official use of security protocols for electronic voting deepens the need for their trustworthiness, hence for their formal verification. The impossibility of linking a voter to her vote, often called voter privacy or ballot secrecy, is the core property of many such protocols. Most existing work relies on equivalence statements in cryptographic extensions of process calculi. This paper provides the first theorem-proving based verification of voter privacy and overcomes some of the limitations inherent to process calculi-based analysis. Unlinkability between two pieces of information is specified as an extension to the Inductive Method for security protocol verification in Isabelle/HOL. New message operators for association extraction and synthesis are defined. Proving voter privacy demanded substantial effort and provided novel insights into both electronic voting protocols themselves and the analysed security goals. The central proof elements are described and shown to be reusable for different protocols with minimal interaction.
Type de document :
Communication dans un congrès
ESSoS13 - International Symposium on Engineering Secure Software and Systems, Feb 2013, Rocquencourt, France. Springer, pp.91-106, 2013, Lecture Notes in Computer Science. 〈https://distrinet.cs.kuleuven.be/events/essos/2013/〉. 〈10.1007/978-3-642-36563-8_7〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00766201
Contributeur : Denis Butin <>
Soumis le : vendredi 8 mars 2013 - 19:23:12
Dernière modification le : mercredi 11 avril 2018 - 01:52:43
Document(s) archivé(s) le : dimanche 9 juin 2013 - 04:10:18

Fichier

cameraready.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Denis Butin, David Gray, Giampaolo Bella. Towards Verifying Voter Privacy Through Unlinkability. ESSoS13 - International Symposium on Engineering Secure Software and Systems, Feb 2013, Rocquencourt, France. Springer, pp.91-106, 2013, Lecture Notes in Computer Science. 〈https://distrinet.cs.kuleuven.be/events/essos/2013/〉. 〈10.1007/978-3-642-36563-8_7〉. 〈hal-00766201〉

Partager

Métriques

Consultations de la notice

281

Téléchargements de fichiers

206