Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster. In David Chaum, Markus Jakobsson, Ronald L. Rivest, Peter Y. A. Ryan, Josh Benaloh, Mirosław Kutyłowski, and Ben Adida, editors, Towards Trustworthy Elections -- New Directions in Electronic Voting, Lecture Notes in Computer Science, pp. 289–309, Springer, May 2010.

Download

[PDF] 

Abstract

While electronic elections promise the possibility of convenient, efficient and secure facilities for recording and tallying votes, recent studies have highlighted inadequacies in implemented systems. These inadequacies provide additional motivation for applying formal methods to the validation of electronic voting protocols.
In this paper we report on some of our recent efforts in using the applied pi calculus to model and analyse properties of electronic elections. We particularly focus on anonymity properties, namely vote-privacy and receipt-freeness. These properties are expressed using observational equivalence and we show in accordance with intuition that receipt-freeness implies vote-privacy.
We illustrate our definitions on two electronic voting protocols from the literature. Ideally, these properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy privacy or receipt-freeness 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

@incollection{DKR-lncs6000,
  abstract =      {While electronic elections promise the possibility of
                   convenient, efficient and secure facilities for
                   recording and tallying votes, recent studies have
                   highlighted inadequacies in implemented systems.
                   These inadequacies provide additional motivation for
                   applying formal methods to the validation of
                   electronic voting protocols.\par In this paper we
                   report on some of our recent efforts in using the
                   applied pi calculus to model and analyse properties
                   of electronic elections. We particularly focus on
                   anonymity properties, namely vote-privacy and
                   receipt-freeness. These properties are expressed
                   using observational equivalence and we show in
                   accordance with intuition that receipt-freeness
                   implies vote-privacy.\par We illustrate our
                   definitions on two electronic voting protocols from
                   the literature. Ideally, these properties should hold
                   even if the election officials are corrupt. However,
                   protocols that were designed to satisfy privacy or
                   receipt-freeness 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.},
  booktitle =     {{T}owards {T}rustworthy {E}lections -- {N}ew
                   {D}irections in {E}lectronic {V}oting},
  OPTDOI =           {10.1007/978-3-642-12980-3_18},
  editor =        {Chaum, David and Jakobsson, Markus and
                   Rivest, Ronald L. and Ryan, Peter Y. A. and
                   Benaloh, Josh and Kuty{\l}owski, Miros{\l}aw and
                   Adida, Ben},
  month =         may,
  pages =         {289-309},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Verifying Privacy-Type Properties of Electronic
                   Voting Protocols: A~Taster},
  volume =        {6000},
  year =          {2010},
  nmonth =        {5},
  lsv-category =  {chap},
  wwwpublic =     {public and ccsb},
}