Type-Based Verification of Electronic Voting Protocols
Type-Based Verification of Electronic Voting Protocols. Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, and Cyrille Wiedling. 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.
Download
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)},
month = apr,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Type-Based Verification of Electronic Voting
Protocols},
year = 2015,
volume = {9036},
pages = {303--323},
acronym = {{POST}'15},
DOI = {10.1007/978-3-662-46666-7_16},
{http://www.loria.fr/~skremer/Papers/CEKMW-post15.pdf},
}