Election verifiability in electronic voting protocols ? (Preliminary version ?? )
Ben Smyth, Mark Dermot Ryan, Steve Kremer, Mounira Kourjieh · 2009
We present a symbolic definition that captures some cases of election verifiability for electronic voting protocols. Our definition is given in terms of reachability assertions in the applied pi calculus and is amenable to automated reasoning using the software tool ProVerif. The definition distinguishes three as- pects of verifiability, which we call individual, universal, and eligibility verifiabil- ity. We demonstrate the applicability of our formalism by analysing the protocols due to Fujioka, Okamoto & Ohta and a variant of the one by Juels, Catalano & Jakobsson (implemented as Civitas by Clarkson, Chong & Myers as Civitas).