Kremer, S., Ryan, M., & Smyth, B. (2010) Election verifiability in electronic voting protocols. Technical Report CSR-10-06, University of Birmingham, UK.
This work has been superseded by the conference version.
We present a symbolic definition of election verifiability (sometimes called end-to-end verifiability) for electronic voting protocols in the context of the applied pi calculus. Our definition is given in terms of boolean tests which can be performed on the data produced by an election. The definition distinguishes three aspects of verifiability, which we call individual verifiability, universal verifiability, and eligibility verifiability. It also allows us to determine precisely which aspects of the system's hardware and software must be trusted for the purpose of election verifiability. In contrast with earlier work our definition is compatible with a large class of electronic voting schemes, including those based on blind signatures, homomorphic encryption and mixnets. We demonstrate the applicability of our formalism by analysing two protocols which have been deployed; namely Helios 2.0, and Civitas. In addition we consider the FOO protocol.