Article Preview
TopIntroduction
Electronic voting promises many advantages over the traditional way of voting. It aims to simplify the voting procedure, to guarantee a lower cost and to have faster tabulation. In fact, electronic voting supporters believe that these systems are more accurate and efficient than traditional paper ballots, while critics are concerned with their security. Indeed, error design and hiatus in protocols security schema have raised considerable concerns with the safety of the electronic voting systems. That’s why electronic voting protocols security should be verified.
Among the security properties which electronic voting protocols should satisfy, are the following (Delaune & Kremer, 2009):
- •
Fairness: no early results can be obtained which could influence the remaining voters.
- •
Eligibility: only legitimate voters can vote, and only once.
- •
Privacy: the system cannot reveal how a particular voter voted. In other terms, no one can do the match between a voter and her vote.
- •
Receipt-freeness: a voter does not gain any information (a receipt) which can be used to prove to a coercer that she voted in a certain way, in order to prevent against the vote-buying.
- •
Coercion-resistance: a voter cannot cooperate with a coercer to prove to him that she voted in a certain way. Thereby, a coercer cannot force any voter to vote against her intentions.
- •
Individual verifiability: a voter can verify that her vote was really counted (Chevallier-Mames, Fouque, Pointcheval, Stern, & Traore, 2006).
- •
Universal verifiability: anyone can verify that the published outcome is the sum of all the votes (Pieters, 2006).
It has been proved (Delaune, Kremer, & Ryan, 2009; Delaune & Kremer, 2009) that formal verification of electronic voting protocols gives an effcient way to check their security, so we drive here a formal verification using manual or automated tools for a newly designed electronic voting protocol of Arujo et al. (2010) which has not been yet verified in the symbolic model.
Note that, due to the complexity of e-voting protocols, only few automated tools have been proposed for verifying such protocols. ProVerif (Blanchet, 2006) is among these tools. It was developed by B. Blanchet to analyze cryptographic protocols. It can accept as input a model in Pi-calculus which is translated to Horn clauses in classical logic, and then, it uses resolution on these clauses. ProVerif was successfully used by S. Kremer and M. Rayan (2005a) to prove fairness and eligibility properties of the FOO protocol (Fujioka, Okamoto, & Ohta, 1992). It was also used by M. Bakes et al. (2008) to prove coercion-resistance property of the JCJ protocol (Juels, Catalano, & Jakobsson, 2005) even though its limitations. Indeed, ProVerif excels at solving reachability problems, but it is unable to prove some equivalence properties and fails to model protocols which require synchronization.