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
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.
@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},
lsv-category = {cont},
wwwpublic = {perso},
}