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.
Category / Keywords: cryptographic protocols / e-voting, type systems, verifiability, vote privacy Original Publication (with minor differences): Proceedings of the 4th Conference on Principles of Security and Trust Date: received 15 Jan 2015 Contact author: eigner at cs uni-saarland de Available format(s): PDF | BibTeX Citation Version: 20150117:074755 (All versions of this report) Short URL: ia.cr/2015/039