Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus

We present a general technique for modeling remote electronic voting protocols in the applied pi-calculus and for automatically verifying their security. In the first part of this paper, we provide novel definitions that address several important security properties. In particular, we propose a new formalization of coercion-resistance in terms of observational equivalence. In contrast to previous definitions in the symbolic model, our definition of coercion-resistance is suitable for automation and captures simulation and forcedabstention attacks. Additionally, we express inalterability, eligibility, and non-reusability as a correspondence property on traces. In the second part, we use ProVerif to illustrate the feasibility of our technique by providing the first automated security proof of the coercion-resistant protocol proposed by Juels, Catalano, and Jakobsson.

• Type: Conference
• Year: 2008
• Where: CSFW
• Authors: Michael Backes, Catalin Hritcu, Matteo Maffei
• Keywords: Applied Pi-calculus, CSFW 2008, Important Security Properties, Remote Electronic Voting, Security Privacy