Steve Kremer: Verifying Properties of Electronic Voting Protocols

Verifying Properties of Electronic Voting Protocols

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Verifying Properties of Electronic Voting Protocols. In Proceedings of the IAVoSS Workshop On Trustworthy Elections (WOTE'06), pp. 45–52, Cambridge, UK, June 2006.

Download

[PDF] [PS]

Abstract

In this paper we report on some recent work to formally specify and verify electronic voting protocols. In particular, we use the formalism of the applied pi calculus: the applied pi calculus is a formal language similar to the pi calculus but with useful extensions for modelling cryptographic protocols. We model several important properties, namely fairness, eligibility, privacy, receipt-freeness and coercion-resistance. Verification of these properties is illustrated on two cases studies and has been partially automated using the Blanchet's ProVerif tool.

BibTeX

@inproceedings{DKR-wote06,
  abstract =      {In this paper we report on some recent work to
                   formally specify and verify electronic voting
                   protocols. In particular, we use the formalism of the
                   applied pi calculus: the applied pi calculus is a
                   formal language similar to the pi calculus but with
                   useful extensions for modelling cryptographic
                   protocols. We model several important properties,
                   namely fairness, eligibility, privacy,
                   receipt-freeness and coercion-resistance.
                   Verification of these properties is illustrated on
                   two cases studies and has been partially automated
                   using the Blanchet's ProVerif tool.},
  address =       {Cambridge, UK},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Ryan, Mark D.},
  booktitle =     {{P}roceedings of the {IAVoSS} {W}orkshop {O}n
                   {T}rustworthy {E}lections ({WOTE}'06)},
  month =         jun,
  pages =         {45-52},
  title =         {Verifying Properties of Electronic Voting Protocols},
  year =          {2006},
  acronym =       {{WOTE}'06},
  nmonth =        {6},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf},
}