Steve Kremer: Towards automatic analysis of election verifiability properties

Towards automatic analysis of election verifiability properties

Ben Smyth, Mark D. Ryan, Steve Kremer, and Mounira Kourjieh. Towards automatic analysis of election verifiability properties. In Proceedings of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'10), pp. 146–163, Lecture Notes in Computer Science 6186, Springer, Paphos, Cyprus, October 2010.
doi:10.1007/978-3-642-16074-5_11

Download

[PDF] [HTML]

Abstract

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 aspects of verifiability, which we call individual, universal, and eligibility verifiability. 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).

BibTeX

@inproceedings{SRKK-arspawits10,
  abstract =      {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 aspects of verifiability, which we call
                   individual, universal, and eligibility verifiability.
                   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).},
  address =       {Paphos, Cyprus},
  author =        {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and
                   Kourjieh, Mounira},
  booktitle =     {{P}roceedings of the {J}oint {W}orkshop on
                   {A}utomated {R}easoning for {S}ecurity {P}rotocol
                   {A}nalysis and {I}ssues in the {T}heory of {S}ecurity
                   ({ARSPA-WITS}'10)},
  DOI =           {10.1007/978-3-642-16074-5_11},
  editor =        {Armando, Alessandro and Lowe, Gavin},
  month =         oct,
  pages =         {146-163},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Towards automatic analysis of election verifiability
                   properties},
  volume =        {6186},
  year =          {2010},
  acronym =       {{ARSPA-WITS}'10},
  nmonth =        {10},
  conf-year =     {2010},
  conf-month =    mar,
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-arspawits10.pdf},
}