Steve Kremer: Formalising security properties in electronic voting protocols

Formalising security properties in electronic voting protocols

Stéphanie Delaune and Steve Kremer. Formalising security properties in electronic voting protocols. Deliverable AVOTE 1.2, (ANR-07-SESU-002), April 2010. 17 pages.

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 security properties of electronic elections. We particularly focus on privacy and verifiability properties. Our definitions allow us to specify and easily change which authorities are supposed to be trustworthy and are compatible with a large class of electronic voting schemes, including those based on blind signatures, homomorphic encryptions, and mixnets.
We distinguish three notions of privacy: vote-privacy, receipt-freeness and coercion-resistance. These properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness which implies vote-privacy. Concerning verifiability, we distinguish three aspects of verifiability, which we call individual verifiability, universal verifiability, and eligibility verifiability.

BibTeX

@misc{avote-D12,
  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 security properties of
                   electronic elections. We particularly focus on
                   privacy and verifiability properties. Our definitions
                   allow us to specify and easily change which
                   authorities are supposed to be trustworthy and are
                   compatible with a large class of electronic voting
                   schemes, including those based on blind signatures,
                   homomorphic encryptions, and mixnets.\par We
                   distinguish three notions of privacy: vote-privacy,
                   receipt-freeness and coercion-resistance. These
                   properties are expressed using observational
                   equivalence and we show in accordance with intuition
                   that coercion-resistance implies receipt-freeness
                   which implies vote-privacy. Concerning verifiability,
                   we distinguish three aspects of verifiability, which
                   we call individual verifiability, universal
                   verifiability, and eligibility verifiability.},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve},
  howpublished =  {Deliverable AVOTE~1.2, (ANR-07-SESU-002)},
  month =         apr,
  note =          {17~pages},
  type =          {Contract Report},
  title =         {Formalising security properties in electronic voting
                   protocols},
  year =          {2010},
  nmonth =        {4},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/avote-d12.pdf},
}