Type-Based Verification of Electronic Voting Protocols

Véronique Cortier 1 Fabienne Eigner 2 Steve Kremer 1 Matteo Maffei 2 Cyrille Wiedling 3
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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : E-voting protocols aim at achieving a wide range of sophisticated security properties and, consequently, commonly employ advanced cryptographic primitives. This makes their design as well as rigorous analysis quite challenging. As a matter of fact, existing automated analysis techniques, which are mostly based on automated theorem provers, are inadequate to deal with commonly used cryptographic primitives, such as homomorphic encryption and mix-nets, as well as some fundamental security properties, such as verifiability. This work presents a novel approach based on refinement type systems for the automated analysis of e-voting protocols. Specifically, we design a generically applicable logical theory which, based on pre- and post-conditions for security-critical code, captures and guides the type-checker towards the verification of two fundamental properties of e-voting protocols, namely, vote privacy and verifiability. We further develop a code-based cryptographic abstraction of the cryptographic primitives commonly used in e-voting protocols, showing how to make the underlying algebraic properties accessible to automated verification through logical refinements. Finally, we demonstrate the effectiveness of our approach by developing the first automated analysis of Helios, a popular web-based e-voting protocol, using an off-the-shelf type-checker.
Keywords : type systems e-voting
Type de document :
Communication dans un congrès
4th Conference on Principles of Security and Trust (POST), Apr 2015, London, United Kingdom. Springer, Proceedings of the 4th Conference on Principles of Security and Trust (POST)
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01103545
Contributeur : Steve Kremer <>
Soumis le : jeudi 8 octobre 2015 - 20:41:41
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : samedi 9 janvier 2016 - 10:42:13

Fichier

CEKMW-post15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01103545, version 1

Citation

Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, Cyrille Wiedling. Type-Based Verification of Electronic Voting Protocols. 4th Conference on Principles of Security and Trust (POST), Apr 2015, London, United Kingdom. Springer, Proceedings of the 4th Conference on Principles of Security and Trust (POST). 〈hal-01103545〉

Partager

Métriques

Consultations de la notice

485

Téléchargements de fichiers

130