Sciweavers

Share
CSFW
2008
IEEE

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

8 years 4 months ago
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.
Michael Backes, Catalin Hritcu, Matteo Maffei
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSFW
Authors Michael Backes, Catalin Hritcu, Matteo Maffei
Comments (0)
books