Steve Kremer: Election verifiability in electronic voting protocols

Election verifiability in electronic voting protocols

Steve Kremer, Mark D. Ryan, and Ben Smyth. Election verifiability in electronic voting protocols. In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS'10), pp. 389–404, Lecture Notes in Computer Science 6345, Springer, Athens, Greece, September 2010.
doi:10.1007/978-3-642-15497-3_24

Download

[PDF] [HTML]

Abstract

We present a formal, symbolic definition of election 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: individual, universal 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 three protocols: FOO, Helios 2.0, and Civitas (the latter two have been deployed).

BibTeX

@inproceedings{KRS-esorics10,
  abstract =      {We present a formal, symbolic definition of election
                   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: individual, universal 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 three protocols: FOO, Helios~2.0, and
                   Civitas (the latter two have been deployed).},
  address =       {Athens, Greece},
  author =        {Kremer, Steve and Ryan, Mark D. and Smyth, Ben},
  booktitle =     {{P}roceedings of the 15th {E}uropean {S}ymposium on
                   {R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)},
  DOI =           {10.1007/978-3-642-15497-3_24},
  editor =        {Gritzalis, Dimitris and Preneel, Bart},
  month =         sep,
  pages =         {389-404},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Election verifiability in electronic voting
                   protocols},
  volume =        {6345},
  year =          {2010},
  acronym =       {{ESORICS}'10},
  nmonth =        {9},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KRS-esorics10.pdf},
}