Type-Based Verification of Electronic Voting Protocols
Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, and Cyrille Wiedling. Type-Based Verification of Electronic Voting Protocols. In Proceedings of the 4th Conference on Principles of Security and Trust (POST'15), pp. 303–323, Lecture Notes in Computer Science 9036, Springer, London, UK, April 2015.
doi:10.1007/978-3-662-46666-7_16
Download
[PDF] [PDF (long version)] [HTML]
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.
BibTeX
@inproceedings{CEKMW-post15,
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. \par 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.},
address = {London, UK},
author = {Cortier, V\'eronique and Eigner, Fabienne and
Kremer, Steve and Maffei, Matteo and Wiedling,
Cyrille},
booktitle = {{P}roceedings of the 4th {C}onference on
{P}rinciples of {S}ecurity and {T}rust (POST'15)},
DOI = {10.1007/978-3-662-46666-7_16},
month = apr,
pages = {303-323},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Type-Based Verification of Electronic Voting
Protocols},
volume = {9036},
year = 2015,
acronym = {{POST}'15},
nmonth = 4,
url = {https://members.loria.fr/skremer/files/Papers/CEKMW-post15.pdf},
}