Steve Kremer: Verifying Privacy-type Properties of Electronic Voting Protocols

Verifying Privacy-type Properties of Electronic Voting Protocols

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. Journal of Computer Security, 17(4):435–487, IOS Press, July 2009.
doi:10.3233/JCS-2009-0340

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. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness, and coercion-resistance.
We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy.
We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.

BibTeX

@article{DKR-jcs08,
  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. We study three
                   privacy-type properties of electronic voting
                   protocols: in increasing order of strength, they are
                   vote-privacy, receipt-freeness, and
                   coercion-resistance.\par We use the applied pi
                   calculus, a formalism well adapted to modelling such
                   protocols, which has the advantages of being based on
                   well-understood concepts. The privacy-type properties
                   are expressed using observational equivalence and we
                   show in accordance with intuition that
                   coercion-resistance implies receipt-freeness, which
                   implies vote-privacy.\par We illustrate our
                   definitions on three electronic voting protocols from
                   the literature. Ideally, these three properties
                   should hold even if the election officials are
                   corrupt. However, protocols that were designed to
                   satisfy receipt-freeness or coercion-resistance may
                   not do so in the presence of corrupt officials. Our
                   model and definitions allow us to specify and easily
                   change which authorities are supposed to be
                   trustworthy.},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Ryan, Mark D.},
  DOI =           {10.3233/JCS-2009-0340},
  journal =       {Journal of Computer Security},
  month =         jul,
  number =        {4},
  pages =         {435-487},
  publisher =     {{IOS} Press},
  title =         {Verifying Privacy-type Properties of Electronic
                   Voting Protocols},
  volume =        {17},
  year =          {2009},
  nmonth =        {7},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf},
}