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. Cryptology ePrint Archive, Report 2015/039, 2015.

Download

[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

@misc{cryptoeprint:2015:039,
    howpublished = {Cryptology ePrint Archive, Report 2015/039},
    year = {2015},
  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.  },
  author =     {Cortier, V\'eronique and Eigner, Fabienne and
                  Kremer, Steve and Maffei, Matteo and Wiedling,
                  Cyrille},
  title =     {Type-Based Verification of Electronic Voting
                  Protocols},
}