Steve Kremer: Election verifiability in electronic voting protocols (Preliminary version)

Election verifiability in electronic voting protocols (Preliminary version)

Ben Smyth, Mark D. Ryan, Steve Kremer, and Mounira Kourjieh. Election verifiability in electronic voting protocols (Preliminary version). In Proceedings of the 4th Benelux Workshop on Information and System Security (WISSEC'09), Louvain-la-Neuve, Belgium, November 2009.

Download

[PDF]

Abstract

We present a symbolic definition 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 tool ProVerif. The definition distinguishes three aspects of verifiability, which we call individual, universal, and eligibility verifiability. It also allows us to determine precisely what aspects of the system are required to be trusted. We demonstrate our formalism by analysing the protocols due to Fujioka, Okamoto & Ohta and Juels, Catalano & Jakobsson; the latter of which has been implemented by Clarkson, Chong & Myers.

BibTeX

@inproceedings{SRKK-wissec09,
  abstract =      {We~present a symbolic definition 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 tool ProVerif.
                   The~definition distinguishes three aspects of
                   verifiability, which we call individual, universal,
                   and eligibility verifiability. It also allows us to
                   determine precisely what aspects of the system are
                   required to be trusted. We demonstrate our formalism
                   by analysing the protocols due to Fujioka, Okamoto
                   \&~Ohta and Juels, Catalano \&~Jakobsson; the~latter
                   of which has been implemented by Clarkson, Chong
                   \&~Myers.},
  address =       {Louvain-la-Neuve, Belgium},
  author =        {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and
                   Kourjieh, Mounira},
  booktitle =     {{P}roceedings of the 4th {B}enelux {W}orkshop on
                   {I}nformation and {S}ystem {S}ecurity ({WISSEC}'09)},
  editor =        {Pereira, Olivier and Quisquater, Jean-Jacques and
                   Standaert, François-Xavier},
  month =         nov,
  title =         {Election verifiability in electronic voting protocols
                   (Preliminary version)},
  year =          {2009},
  acronym =       {{WISSEC}'09},
  nmonth =        {11},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf},
}