Automated Verification of Remote Electronic Voting Protocols

mass media, and the scientific community.
On the one hand, electronic voting promises to
simplify the voting procedure, to automate the count of votes, to guarantee the
correctness of elections, and to prevent voter coercion. On the other hand, the
errors in protocol design and the vulnerabilities in implementations raised
considerable concerns about the reliability and safety of electronic voting
systems. This is not particularly surprising since designing security protocols
has long been known to be error-prone and, owing to the distributed-system
aspects of multiple interleaved protocol runs, security analyses of such
protocols are awkward to make for humans. Formal methods, and in particular
language-based techniques, proved to constitute salient tools for reliably
analyzing security protocols. The main advantage of these techniques is
automation: the human effort is limited to the specification of the
protocol in a process calculus and the analysis is fully automated.

Coming up with a careful formalization and techniques for automated verification
of electronic voting systems is hence arguably of paramount importance for the
widespread acceptance of such systems in the scientific community, and hence
might ultimately facilitate their successful deployment in the future. While
attention has been traditionally focused on the problem of supervised voting,
where voters interact with a computing device under the supervision of election
authorities, the more general and harder problem to solve is the problem of
remote voting, where no supervision of voters or computing devices is in place.

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, we provide novel definitions that address several
important security properties and that are suitable for automation. 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 amenable to automation and
captures simulation and forced-abstention attacks. Additionally, we express
inalterability, eligibility, and non-reusability as a correspondence property on
traces. In the second part, we use ProVerif to provide the first automated
security proof of the coercion-resistant protocol proposed
by Juels, Catalano, and Jakobsson.