IACR News item: 17 January 2015
Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, Cyrille Wiedling
ePrint Reportautomated 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.
Additional news items may be found on the IACR news page.