Steve Kremer: Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus

Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus

Steve Kremer and Mark D. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus. In Programming Languages and Systems --- Proceedings of the 14th European Symposium on Programming (ESOP'05), pp. 186–200, Lecture Notes in Computer Science 3444, Springer, Edinburgh, Scotland, UK, April 2005.
doi:10.1007/b107380

Download

[PDF] [PS] [HTML]

Abstract

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.

BibTeX

@inproceedings{KremerRyan2005,
  abstract =      {Electronic voting promises the possibility of a
                   convenient, efficient and secure facility for
                   recording and tallying votes in an election. Recently
                   highlighted inadequacies of implemented systems have
                   demonstrated the importance of formally verifying the
                   underlying voting protocols. The applied pi calculus
                   is a formalism for modelling such protocols, and
                   allows us to verify properties by using automatic
                   tools, and to rely on manual proof techniques for
                   cases that automatic tools are unable to handle. We
                   model a known protocol for elections known as FOO~92
                   in the applied pi calculus, and we formalise three of
                   its expected properties, namely fairness,
                   eligibility, and privacy. We use the ProVerif tool to
                   prove that the first two properties are satisfied. In
                   the case of the third property, ProVerif is unable to
                   prove it directly, because its ability to prove
                   observational equivalence between processes is not
                   complete. We provide a manual proof of the required
                   equivalence.},
  address =       {Edinburgh, Scotland, UK},
  author =        {Kremer, Steve and Ryan, Mark D.},
  booktitle =     {{P}rogramming {L}anguages and {S}ystems~---
                   {P}roceedings of the 14th {E}uropean {S}ymposium on
                   {P}rogramming ({ESOP}'05)},
  DOI =           {10.1007/b107380},
  editor =        {Sagiv, Mooly},
  month =         apr,
  pages =         {186-200},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Analysis of an Electronic Voting Protocol in the
                   Applied Pi-Calculus},
  volume =        {3444},
  year =          {2005},
  acronym =       {{ESOP}'05},
  nmonth =        {4},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf},
}