International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News item: 17 January 2015

Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, Cyrille Wiedling
ePrint Report ePrint Report
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.

Expand

Additional news items may be found on the IACR news page.