Abstract: Secure remote internet voting protocols play an important role in electronic government. In order to assess its claimed security, several formal models of soundness and coercion-resistance have been proposed in the past literatures, but these formal models are not supported by mechanized tools. Recently, Backes et al. propose a new mechanized formal model of security properties including soundness and coercion-resistance in applied PI calculus. Acquisti protocol is one of the most important remote internet voting protocols that claims to satisfy formal definitions of key properties without strong physical constrains. But in the study the analysis of its claimed security is finished by hand. Owning to the contribution of Backes et al., Acquisti protocol can be analyzed with mechanized tool. In this study, firstly the review of the formal analysis of electronic voting protocols are introduced we can find that the formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistance. Until now the security analysis model based on computational model have not been proposed; then applied PI calculus and the mechanized proof tool ProVerif are examined. After that Acquisti protocol is modeled in applied PI calculus. Finally security properties, including soundness and coercion resistance, are proved with ProVerif, a resolution-based mechanized theorem prover for security protocols. The result we obtain is that Acquisti protocol has the soundness and coercion-resistance in some conditions. To our best knowledge, the first mechanized proof of Acquisti protocol for an unbounded number of honest and corrupted voters is presented.
INTRODUCTION
With the development of Internet and information technology, electronic government has got serious attention from enterprise and academic world. Owning to advantages of remote internet voting, it plays an important role in electronic government. In order to assess its security and increase confidence of the voters in remote internet voting system and protocols, many researchers have pay attention to design and verification on secure remote internet voting systems and protocols. Remote internet voting protocol is a key part of internet voting system. So how to develop and verify a practical secure internet voting protocol is a challenging issue (Abadi and Gordon, 1999).
The practical secure remote internet voting protocol should include the basic and expanded properties. Basic properties include privacy, completeness, soundness (Abadi and Fournet, 2001), fairness and invariableness. Expanded properties include universal verifiability (Sako and Killian, 1995), receipt-freeness (Benaloh and Tuinstra, 1994 ) and coercion-resistance (Juels and Jakobsson, 2002). Recently research focus on implementation and formal analysis of receipt-freeness and coercion-resistance.
Soundness is typically consists of inalterability, eligibility and unreusability (Backes et al., 2008a). Universal verifiability describes that any one can verify the fact that the election is fair and the published tally is correctly computed from the ballots that were correctly cast (Sako and Killian, 1995). Receipt-freeness is to protect against vote buying (Benaloh and Tuinstra, 1994). The voter can not produce a receipt to prove that he votes a special ballot. Coercion resistance means that it should offer not only receipt-freeness, but also defense against randomization, forced-abstention and simulation attacks (Juels and Jakobsson, 2002).
In the last twenty years many remote internet voting protocols (Benaloh and Tuinstra, 1994; Magkos et al., 2001; Juels and Jakobsson, 2002; Acquisti, 2004; Chaum, 2004; Juels et al., 2005; Chaum et al., 2005; Rivest, 2006; Cichon et al., 2008; Clarkson et al., 2008; Meng, 2007a, 2009a, c, d; Meng et al., 2010a-c; Meng and Wang, 2010), claimed on their security, have be proposed. In order to assess and verify security properties of remote internet voting protocol there are two model can be used: one is formal model (or Dolev-Yao, symbolic model) in which cryptographic primitives are ideally abstracted as black boxes, the other is computational model (or cryptographic model) based on complexity and probability theory. Firstly each model formally defines security properties expected from security protocol and then develop methods for strictly proving that given security protocols satisfy these requirements in adversarial environments. Computational model is complicated and is difficult to get the support of mechanized proof tools. In contrast, symbolic model is considerably simpler than the computational model, proofs are therefore also simpler and can sometimes benefit from mechanized proof tools support. For example: SMV (McMillan, 1992; Mei et al., 2009), NRL (Meadows, 1996), Casper (Lowe, 1998), Isabelle (Paulson, 1998), Athena (Song, 1999), Revere (Kindred, 1999), SPIN (Maggi and Sisto, 2002), Brutus (Clarke et al., 2000), ProVerif (Blanchet, 2001), Scyther (Joseph and Cremers, 2006).
ProVerif (Blanchet, 2001) is an mechanized proof of
cryptographic protocol verifier based on a representation of the protocol by
Horn clauses or applied PI calculus. It can handle many different cryptographic
primitives, including shared- and public-key encryption and signatures, hash
functions and Deffie-Hellman key agreements, specified both as rewrite rules
and as equations. It can also deal with an unbounded number of sessions of the
protocol (even in parallel) and an unbounded message space. When ProVerif cannot
prove a property, it can reconstruct an attack, that is, an execution trace
of the protocol that falsifies the desired property. This verifier can prove
the following properties: secrecy, authentication and more generally correspondence
properties, strong secrecy, equivalences between processes that differ only
by terms. ProVerif has been tested on protocols of the literature with very
great results
(http://www.proverif.ens.fr/proverif-users.html).
Acquisti (2004) protocol is one of the most important remote internet voting protocols that claims to satisfy formal definitions of key properties, such as soundness, individual verifiability, as well as receipt-freeness and coercion resistance without strong physical constrains. In their study, analysis of security properties of Acquisti protocol is done by hand, this method depend on experts knowledge and skill and is prone to make mistakes, so here we use mechanized proof tool ProVerif to verify security properties of Acquisti protocol.
The main contributions of this study are summarized as follows:
| • | Review the formal analysis of security properties in electronic voting protocol. Many formal models have been proposed, but only the Bakes et al. model supports the mechanized proof tool. The formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistance which are important properties. Until now the security analysis model based on computational model have not been proposed |
| • | Apply the mechanized formal model proposed by Backes et al. (2008a) for mechanized proof of Acquisti protocol and its security properties. Therefore, Acquisti protocol is modeled in applied PI calculus and the soundness and coercion-resistance take into account. The proof itself is performed by mechanized proof tool ProVerif developed by Blanchet (2001) |
| • | The result we obtain is that Acquisti protocol has coercion-resistance in some conditions. At the same time it also has the soundness. To our best knowledge, we are conducting the first mechanized proof of Acquisti protocol for an unbounded number of honest and corrupted voters |
Formal methods are an important tool for designing and implementing secure cryptographic protocol. By applying techniques concerned with the construction and analysis of models and proving that certain properties hold in the context of these models, formal methods can significantly increase one’s confidence that a protocol will meet its requirements in the real world.
The development of formal methods has started in 1980s (Yao, 1982; DeMillo et al., 1982; Dolev and Yao, 1983; Merritt, 1983; Blum and Micali, 1984; Hoare, 1985; Burrows et al., 1989, 1990). This field matured considerably in the 1990s. Some of the methods rely on rigorous but informal frameworks, sometimes supporting sophisticated complexity-theoretic definitions and arguments. Others rely on formalisms specially tailored for this task. Yet others are based on Mur (Mitchell et al., 1997) strand space (Thayer et al., 1998), SPI calculus (Abadi and Gordon, 1999) Kessler and Neumann logic (Kessler and Neumann, 1998) applied PI calculus (Abadi and Fournet, 2001).
Owning to the abstraction ideally of cryptography, formal methods are often quite effective; a fairly abstract view of cryptography often suffices in the design, implementation and analysis of security protocols. Formal methods enable relatively simple reasoning and also benefit from substantial work on proof methods and from extensive tool support, for example, SMV (McMillan, 1992), NRL (Meadows, 1996), Casper (Lowe, 1998), Isabelle (Paulson, 1998), Athena (Song, 1999), Revere (Kindred, 1999), SPIN (Maggi and Sisto, 2002), Brutus (Clarke et al., 2000), ProVerif (Blanchet, 2001), Scyther (Joseph and Cremers, 2006).
Delaune et al. (2006a) have done a path breaking work on the formal definition of receipt-freeness and coercion-resistance in applied PI calculus. Their formal model is based on Dolev-Yao model. They formalize receipt-freeness as an observational equivalence. The idea is that if the attacker can not find if arbitrary honest voters VA and VB exchange their votes, then in general he can not know anything about how VA (or VB) voted. This definition is robust even in situations where the result of the election is such that the votes of VA and VB are necessarily revealed. They also assume that the voter cooperates with the coercer by sharing secrets, but the coercer cannot interact with the voter to give her some prepared messages. They use adaptive simulation to formalize coercion-resistance. The ideas of this definition is that whenever the coercer requests a given vote then VB can change his vote and counterbalance the outcome. However, avoid the case where V' = VA {c/v}c1,c2 letting VB vote α is needed. Therefore, requirement that when we apply a context C, intuitively the coercer, requesting VA {c/v}c1,c2 to vote c, V' in the same context votes α. There may be circumstances where V' may need not to cast a vote that is not. In the case of coercion-resistance, the coercer is assumed to communicate with voter during the protocol and can prepare messages which she should send during the election process. Their formal definition of coercion-resistance base on the informal definition: a voter cannot cooperate with a coercer to prove to him that she voted in a certain way. Lee et al. (2003) protocol is analyzed with their formal model. Meng (2008) also apply their formal model to analyze the protocol (Meng, 2007a). Delaune et al. (2005) model receipt-freeness and analyze Lee et al. (2003) protocol. Delaune et al. (2006b) use applied PI calculus to model fairness, eligibility, privacy, receipt-freeness and coercion-resistance and analyze the protocols (Fujioka et al., 1992; Lee et al., 2003). Backes et al. (2008a) point out that definitions of coercion-resistance Delaune et al. (2006a) are not amenable to automation and do not consider forced-abstention attacks and do not apply to remote voting protocols, they give an formal model of security properties of remote internet voting protocol in applied PI calculus and use the ProVerif to mechanized verify the security properties of Juels et al. (2005) protocol. Gerling et al. (2008) apply the model (Backes et al., 2008a) with ProVerif to mechanized verify Clarkson et al. (2008) protocol. Meng et al. (2010b, c) also use the Backes et al. (2008a) model to mechanized verify Acquisti (2004) protocol and Meng et al. (2010a) protocol.
Jonker and de Vink (2006) also point out that the formal model (Delaune et al., 2006a) offers little help to identify receipts when receipts are present. So Jonker and de Vink present a new formal method, which uses the process algebra, to analyze receipts based on their informal definition: a receipt r is an object that proves that a voter v cast a vote for candidate c. This means that a receipt has the following properties: (R1) receipt can only have been generated by v. (R2) receipt proves that voter chose candidate. (R3) receipt proves that voter cast her vote. Jonker and de Vink provide a generic and uniform formalism that captures a receipt. Jonker and de Vink formal model is also simpler than Delaune et al. formal model. They use the formalism to analyze the voting protocols (Benaloh and Tuinstra, 1994; Sako and Killian, 1995; Hirt and Sako, 2000; Aditya et al., 2004; Hubbers et al., 2005). Meng (2007b) analyzes receipt-freeness of the protocols (Fujioka et al., 1992; Cramer et al., 1997; Juels and Jakobsson, 2002; Acquisti, 2004) based on formalism (Jonker and de Vink, 2006).
About definition of receipt proposed by Jonker and de Vink (2006) think it is worth discussing. Firstly, about (R1) r can only have been generated by v, in some voting protocol, one part of receipt is generated by the authority, not generated by voter. Secondly, they give the following auxiliary receipt decomposition functions: a: Rcpt ?AT, which extracts the authentication term from a receipt. Authentication term should be the identification of voter. Thirdly the author does not prove the generic and uniform formalism that is right in their study. Finally they use a special notation, it difficult to use and generalize it. Hence, Meng gives a formal logic framework for receipt-freeness based on Kessler and Neumann (1998) and apply it to analyze (Fujioka et al., 1992) protocol.
Knowledge-based logics have been also used in the studies (Jonker and Pieters, 2006; Baskar et al., 2007; Van Eijck and Orzan, 2007) to formally analyze the security properties of e-voting protocol. Jonker and Pieters (2006) formalize the concept of receipt-freeness from the perspective of a anonymity approach in epistemic logic which offers, among others, the possibility to write properties allowing to reason about the knowledge of an agent a of the system with respect to a proposition p. They classify receipt-freeness into two types: weak receipt-freeness and strong receipt-freeness. Weak receipt-freeness implies that the voter cannot prove to the spy that she sent message m during the protocol, where m is the part of a message representing the vote. Here, no matter what information the voter supplies to the spy, any vote in the anonymity set is still possible. In other words, for all possible votes, the spy still suspects that the voter cast this particular vote; or: the spy is not certain she did not cast this vote. Baskar et al. (2007) gave the formal definition of secrecy, receipt-freeness, fairness, individual verifiability based on knowledge-based logic and analyze receipt-freeness of Fujioka et al. (1992) protocol. Van Eijck and Orzan (2007) use dynamic epistemic Logic to model security protocols and properties, in particular anonymity properties. They apply it to Fujioka et al. (1992) scheme and find the three phases should be strictly separated, otherwise anonymity is compromised. Mauw et al. (2007) use the process algebra to analyze the data anonymity of the voting scheme (Fujioka et al., 1992). Talbi et al. (2008) use ADM logic to specify security properties (fairness, eligibility, individual verifiability and universal verifiability) and analyze Fujioka et al. (1992) protocol. Their goal is to verify these properties against a trace-based model. Groth (2004) evaluated the voting scheme based on homomorphic threshold encryption with universal composability framework. He formalizes the privacy, robustness, fairness and accuracy.
The formal methods used in formal models of soundness, receipt-freeness and coercion-resistance are presented in Table 1. We can found in Table 1 until now only the Bakes et al. model supports the mechanized proof tool. The security properties formally modeled is presented in Table 2. The formally analyzing security properties in the Internet voting protocol is described in Table 3. From Table 1-3 we can get that the formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistacne that are important properties.
| Table 1: | The formal methods used in formal models of soundness, receipt-freeness and coercion-resistance |
| The mark • represents the formal method is used. The mark u represents the formal models is supported by mechanized proof tool | |
| Table 2: | The security properties formally modeled |
| The mark • represents the property is formally defined; The mark u represents the formal definitions is supported by mechanized proof tool | |
| Table 3: | Formally analyzing security properties in the Internet voting protocol |
| The mark • represents the protocol has the property; The mark □ represents the protocol has not the property; The mark Δ represents the protocol has the property with some condition | |
Above previous formal models and analysis is based on symbolic model. Until now people have not proposed a security analysis model based on computational model.
CONTRIBUTION AND OVERVIEW
In the last two decades many remote internet voting protocol have been introduced. Owning to the complexity how to assess their security is a challenging issue. Formal method is crucial to assess their security. So, in this study we firstly review the development of the formal method on remote electronic voting protocol, we found that several formal model have been proposed, but only the Bakes et al. model support the mechanized proof tool and the formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistance that are important properties. Until now people have not proposed a security proof model based computational model; and then apply the mechanized formal model proposed by Backes et al. (2008a) to prove Acquisti protocol and its security properties including soundness and coercion-resistance. Therefore, first, Acquisti protocol is modeled in applied PI calculus and then its proof is performed by mechanized proof tool ProVerif. The result is that Acquisti protocol has the soundness. At the same time it has also coercion-resistance in the conditions that the channel between registration authority and voter is private. To our best knowledge, we are conducting the first mechanized proof of Acquisti protocol for an unbounded number of honest and corrupted voters.
Acquisti protocol is modeled with applied PI calculus (Abadi and Fournet, 2001). Our choice is based on the fact that applied PI calculus allows the modeling of relations between data in a simple and precise manner using equational theories over term algebra. The general analysis model is introduced in Fig. 1. Acquisti protocol in applied PI calculus is illustrated in Fig. 2. There, the security properties model is equivalence between processes, while the attacker is thought as an arbitrary process running in parallel with the protocol process representing the adversary model, which is the parallel composition of the (sequential) protocol participants’ processes. The considered attacker is stronger than the basic Dolev_Yao attacker since it can exploit particular relations between the messages by using particular equational theories stating the message relations.
| Fig. 1: | Analysis model of remote internet voting protocol with applied PI calculus |
| Fig. 2: | Mechanized proof of Acquisti protocol |
REVIEW OF THE APPLIED PI CALCULUS
Applied PI calculus is a language for describing concurrent processes and their interactions based on Delov_Yao model. Applied PI calculus is an extension of the PI calculus that inherits the constructs for communication and concurrency from the pure pi-calculus. It preserves the constructs for generating statically scoped new names and permits a general systematic development of syntax, operational semantics equivalence and proof techniques. At the same time there are several powerful mechanized proof tool supported applied pi-calculus, for example, ProVerif. Applied PI calculus with ProVerif has been used to study a variety of complicated security protocols, such as a certified email protocol, just fast keying protocol (Abadi et al., 2004; Juels et al., 2005) remote electronic voting protocol (Backes et al., 2008a), a key establishment protocol, direct anonymous attestation protocol (Backes et al., 2008b), TLS protocol (Bhargavan et al., 2008; Meng et al., 2010a) remote internet voting protocol (Meng et al., 2010c).
Syntax: In applied PI calculus, terms in Fig. 3 consists
of name, variables and signature
| Fig. 3: | Terms |
| Fig. 4: | Plain process |
| Fig. 5: | Extended process |
In applied PI calculus, it has plain processes and extended processes. Plain processes in Fig. 4 are built up in a similar way to processes in the PI calculus, except that messages can contain terms (rather than just names) and that names need not be just channel names:
The process 0 is an empty process. The process Q|P is the parallel composition
of P and Q. The replication !P produces an infinite number of copies of P which
run in parallel. The process vn.P firstly creates a new, private name then executes
as P. The abbreviation
Extended processes in Fig. 5 add active substitutions and restriction on variables:
We write {M/x} for active substitution which replaces the variable x with the term M. The substitution typically appears when the term M has been sent to the environment, but the environment may not have the atomic names that appear in M; the variable x is just a way to refer to M in this situation. We write fv(A), fn(A) for the free variables and name in a process A, respectively. We write bv(A) ,bn(A) for the bound variables and name in a process A, respectively.
A frame is an extended process built up from 0 and active substitutions of the form {M/x} by parallel composition and restriction. Let, φ and ψ range over frames. The domain dom(φ) of a frame φ is the set of the variables that φ exports. Active substitutions are useful because they allow us to map an extended process A to its frame φ(A) by replacing every plain process in A with 0. The frame φ(A) can be viewed as an approximation of A that accounts for the static knowledge A exposes to its environment, but not A’s dynamic behavior. The domain of dom(A) is the domain of φ(A). A process or extended process with a hole is called a context. The plain process with a hole is called plain context. Those plain contexts without replications, conditionals, inputs or outputs are called sequential contexts. A context C[5] closes A if C[A] is closed.
A signature
Operational semantics: The operational semantic is inherited from the applied PI calculus and is defined by structural equivalence (≡) and internal reduction (→).
Structural equivalence in Fig. 6 (≡) is the smallest equivalence relation on extended processes that is closed by α conversion on both names and variables, by application of evaluation contexts, Structural equivalence can make the introduction and application of an active substitution and the equational rewriting of the terms in a process. Structural equivalence satisfies the rules in the following:
The rules for parallel composition and restriction are standard. ALIAS enables the introduction of an arbitrary active substitution. SUBST describes the application of an active substitution to a process that is in contact with it. Rewrite deals with equational rewriting.
Internal reduction (→) relies on the equational theory and defines the semantics of process conditionals as well as input and output. Internal reduction in Fig. 7 is the smallest relation on extended processes closed by structural equivalence and application of evaluation contexts such that:
THEN and ELSE directly depend on the underlying equational theory; using ELSE sometimes requires that active substitutions in the context be applied first, to yield ground terms M and N.
We write
| Fig. 6: | Structural equivalence |
| Fig. 7: | Internal reduction |
MECHANIZED PROOF TOOL PROVERIF
ProVerif is a mechanized cryptographic protocol verifier based on a representation of the protocol by Horn clauses or applied PI calculus. It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signatures), hash functions and Deffie-Hellman key agreements, specified both as rewrite rules and as equations. It can also deal with an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space. When ProVerif cannot prove a property, it can reconstruct an attack, that is, an execution trace of the protocol that falsifies the desired property. ProVerif can prove the following properties: secrecy, authentication and more generally correspondence properties, strong secrecy, equivalences between processes that differ only by terms. ProVerif has been tested on protocols of the literature with very encouraging results (http://www.proverif.ens.fr/proverif-users.html). Recent research came up with an abstraction of zero-knowledge proofs, a primitive heavily used within electronic voting protocols such as Juels et al. (2005), Meng et al., (2010a) and Clarkson et al. (2008) protocols that is accessible to an mechanized proof using ProVerif (Backes et al., 2008a; Gerling et al., 2008; Meng et al., 2010c).
ProVerif in Fig. 8 is for the proof of trace-based security properties and observational equivalence. Since, the security definitions for basic properties and expanded properties including receipt-freeness and coercion-resistance for Backes et al. (2008b) model heavily rely on observational equivalences, ProVerif is the only tool for our purpose of an mechanized proof of Acquisti protocol.
| Fig. 8: | Mechanized proof tool ProVerif (Blanchet, 2007) |
Inspired by study of Backes et al. (2008a) and Gerling et al. (2008), we use it to mechanized prove Acquisti protocol.
BACKES ET AL. (2008a) MODEL
Here, we describes Backes et al. (2008a) model used to mechanized prove Acquisti protocol. Backes et al. (2008a) model formalize key properties including the soundness, receipt-freeness and coercion-resistance in remote internet voting protocol with applied PI calculus. Backes et al., 2008a model mainly model the soundness, receipt-freeness and coercion-resistance. In Backes et al. (2008a) model the voter are classified into three types of voter: honest voter, corrupted voter and ad-hoc voter. Honest voter are issued an identity by an issuer authority and behave according to the protocol specification. Corrupted voter will register and then simply output all their registration credentials on a public channel, thus the coercer and vote buyer can impersonate him in order to mount any sort of attack. Ad-hoc voters can behave arbitrarily; they do not necessarily follow the protocol, but are also not necessarily corrupted. In the following section we first introduce the soundness including inalterability, eligibility and unreusability, then receipt-freeness and coercion-resistance in Backes et al. (2008a) model.
Soundness:
| • | Informal definition: In the study (Backes et al., 2008a), soundness is typically consists of the following three separate properties: |
| • | Inalterability: No one can change anyone else’s vote |
| • | Eligibility: Only eligible voters are able to vote |
| • | Unreusability: Every voter can vote only once |
Backes et al. (2008a) model formalizes the definition of soundness with the events including beginvote(id,v), endvote(v), startid(id) and startcorid(id). The events in the soundness property are also used later in the modeled processes. beginvote(id, v) starts the voting phase for a voter with id and the intention to vote for v whereas endvote(v) is the tallying of this vote. startid(id) and startcorid(id) indicate the start of the registration phase for an eligible voter or an corrupted voter with id.
| • | Formal definition: A trace t guarantees soundness if and only if the following conditions hold in Fig. 9 |
Condition 1a and b models the inalterability and eligibility, respectively. This is done through requiring that every counted vote is either a vote casted by an eligible voter or a corrupted voter. In order to achieve unreusability it has to be assured that the matching between endvote and beginvote(id, v) is injective. This is ensured by Condition 1a in combination with condition 2.
Receipt-freeness:
| • | Informal definition: The voter can not produce a receipt to prove that he votes a special ballot. Its purpose is to protect against vote buying. This definition thus refers to an attacker that does not try to vote by impersonating the voter, but just tries to get a proof that the voter voted in a special way |
| • | Formal definition: An election context S is receipt-freeness if there exists a plain process V' such that in Fig. 10 |
| Fig. 9: | Formal definition of soundness |
| Fig. 10: | Formal definition of receipt-freeness |
Condition 1 models that the voter V' does not only vote v' as a regular voter, but additionally uses Vfake to generate fake secrets, casts an extra vote using them and provides a receipt of this invalid voting. Condition 2 deal with that an additional voter k that votes with fake registration secrets in case the voter i complies with the request of the coercer and simply abstains if i cheats the vote buyer by casting a vote with fake secrets.
Coercion-resistances:
| • | Informal definition: A coercion-resistant voting protocol should offer not only receipt-freeness, but also defense against randomization, forced-abstention and simulation attacks |
| • | Receipt-freeness: The voter can not produce a receipt to prove that he votes a special ballot |
| • | Immunity to randomization attack: The idea is for an attacker to coerce a voter by requiring that she submit randomly composed balloting material. The effect of the attack is to nullify the choice of the voter |
| • | Immunity to forced-abstention attack: This is an attack related to the previous one based on randomization. In this case, the attacker coerces a voter by demanding that she refrain from voting |
| • | Immunity to simulation attack: An attacker coerce voters into divulging private keys or buying private keys from voters and then simulating these voters at will, i.e., voting on their behalf |
The formalization that encompasses all properties except randomization attacks depicted below is taken from Backes et al. (2008a) model.
In order to formalize coercion-resistance, the process called Extractor is introduced. Extractor plays an important role in formalization of coercion-resistance, which extracts the vote the coercer casts on behalf of Extractor and tallies it directly. Extractor depends on the construction of the particular electronic voting protocol and has to be provided by the user.
| • | Definition of Extractor: A context |
The channels c1 and c2 are the channels shared by the extractor with the coerced voter and the tallying authority, respectively. If the coercer casts a vote, then the variable z should hold this vote. The context C is required to be sequential so it does not contain any replications, which means that:
can tally at most one vote.
| • | Formal definition: An election context S guarantees coercion-resistance if there exist channels c, c1 and c2, a sequential process Vfake, an Extractor Ec1,c2,z and an election context S', such that in Fig. 11 |
In condition 1 (hypothesis) a modified election context s' is used that only differs from s in that the tallying authority additionally outputs messages on the channel c2 shared with Extractor. In condition 2 the left side process contains the voter Vi that is in accordance with the orders of the coercer, running in parallel with the voter Vj casting a vote v' and the process Ec1,c2,z[0], that is intuitively equivalent to a voter nullifying her vote. In the right side election process the voter Vi cheats the coercer by providing him with fake registration secrets and then votes v', the voter Vj participates in the registration phase and then abstains and the extractor process:
tallies the vote the coercer casts on behalf of vi. In condition 3 if the cheated coercer abstains, then the Extractor needs to abstain as well; In condition 4 if the cheated coercer casts a valid vote using the fake registration secrets he received from vi, the Extractor needs to tally precisely this vote.
| Fig. 11: | Formal definition of coercion-resistance |
In condition 5 an additional restriction is introduced that justifies the abstraction of the third voter by the Extractor: votes with invalid registration secrets are silently discarded by the tallying authority. If this was not the case a coercer could easily distinguish real from fake registration secrets.
ACQUISTI PROTOCOL
Acquisti (2004) protocol promises that it can protect voters’ privacy and achieves universal verifiability, receipt-freeness and coercion-resistance without ad hoc physical assumptions or procedural constraints. It mainly applies threshold Paillier cryptosystem (Paillier, 1999), bulletin board that is a public broadcast channel with memory where a party may write information that any party may read, Mix net that guarantees privacy is a distributed protocol that takes as input a set of messages and returns an output consisting of the re-encrypted messages permuted according to a secret function (Chaum, 1981), proof of knowledge that two ciphertexts are encryption of the same plaintext (Baudron et al., 2001), designated verifier Proof of knowledge (Jakobsson et al., 1996; Hirt and Sako, 2000). Acquisti assumes that the private key is private and that an attacker cannot control every possible communication between the voter and an authority.
In Acquisti protocol there are five entities: registration authority, issue authority, bulletin board, voters, tallying authority. Registration authority is responsible for authenticating the voters. Issue authority takes charge of issuing the related key and credentials. Voters register for voting, get their credentials and post a vote.
| Fig. 12: | Model of Acquisti protocol |
Tallying authority is responsible for tallying ballots. Model of Acquisti protocol is described in Fig. 12.
Acquisti protocol consists of preparation phase, voting phase and tallying phase. In preparation phase the related keys and ballot are generated. Issuer authority creates the voting credential shares and posts copies of the shares of credentials encrypted with Paillier cryptosystem to a bulletin board. The same credential shares encrypted with different Paillier public keys and attach a designated verifier proof of the equivalence between the encrypted share and the one the voter has received to its message are also provided to voters. Issuer authority also creates the ballots shares which are encrypted with the two different Paillier public keys. Both the sets of encrypted ballots shares are posted on the bulletin board together with zero-knowledge proofs that each pair of ciphertexts are encryptions of the same ballot share and are then signed by issuer Authority.
| Fig. 13: | The structure of message of Acquisti protocol |
In voting phase the voter vote his favor ballot and post it to bulletin board. Each voter multiplies the shares she has received from issuer authority together with the encrypted shares of the ballot. Because of the homomorphic properties of Paillier cryptosystems, the resulting ciphertext includes the sum of those shares and the ballot’s shares. The resulting ciphertext is sent to the bulletin board. In the last phase, tallying phase, the tallying authority tallies the ballot and publishes the result in bulletin board. The structure of message is described in Fig. 13.
Preparation phase: Every issue authority Ai(i = 1......l) creates l random numbers c as ci,j, representing shares of credentials, for each eligible voter veterj(l = 1......l). For each ci,j, Ai performs two operations: first, it encrypts ci,j using PKC and appropriate secret randomization, signs the resulting ciphertext with SKiC and publishes it on bulletin board on a row publicly reserved for the shares of credential of voter:
Evoterj represents RSA encryption under voterj’s public key.
Voting phase: For each encrypted share of credential she receives, voterj verifies the designated verifier proof of equality between EV(ci,j) and the corresponding EV(ci,j) that has been signed and published in her reserved area of bulletin board. Upon successful verification, she multiplies together the shares EV(ci,j).
Cj is the sum of the various shares of credentials. voterj.
Voter chooses the ballot shares
and sends
Tallying phase: After the voting time expires, all ballots on bulletin board posted by allegedly eligible voters are mixed by the tallying authorities. The shares of credentials posted by the registration authorities are also combined and then mixed. Tallying authorities thus obtain two lists: a list of encrypted, mixed credentials the registration authorities themselves had originally posted on the bulletin board; and a set of encrypted, mixed sums of credentials and ballots, posted on the bulletin board by the voters. The two lists have been encrypted with different Paillier public parameters. Using threshold protocols for the corresponding sets of private keys, the tallying authorities decrypt the elements in each list and then compare them through a search algorithm and publish the tallying result on bulletin board.
MODELING ACQUISTI PROTOCOL WITH APPLIED PI CALCULUS
Function and equational theory: The function and equational theory is introduced in this section. We use applied PI calculus to model Acquisti protocol. We model cryptography in a Dolev-Yao model as being perfect. Figure 14 describes the functions and Fig. 15 describes the equational theory in Acquisti protocol.
The probabilistic public key cryptosystem, for example Paillier cryptosystem, is modeled with decryption algorithm pPKdec(x,PR) and encryption algorithm pPKenc(x, PU,r). pPKdec(x, PR) decrypt the ciphertext x x with private key PR. pPKenc(x, PU, r) encrypt the plain text x with public key PU and random number r. The deterministic public key encryption scheme is expressed by decryption algorithm PKdnc(x,PR) and encryption algorithm Pkenc(x,PU). PKdnc(x,PR) decrypt the ciphertext x with private key PR. PKenc(x,PU) encrypt the plaintext x with public key PU.
| Fig. 14: | Functions |
| Fig. 15: | Equational theory |
The digital signature is modeled as being signature with message recovery, i.e., the signature itself contains the signed message which can be extracted using the function. The digital signature algorithm includes the generation signature algorithm sign(x, PR) sign the message x with private key PR and the verification algorithm verifysign(x, PU) verify the digital signature x with public key PU. decsign(x, PU) recover the message from the digital signature x with public key PU. The probabilistic threshold public key share decryption algorithm TpPKsubdec(xi, Pri, VKi) decrypt the secret share xi with private key PRi and verification key VKi. The probabilistic threshold combining algorithm TpPKdec(x1,...,x2) recovers x from x1,...,x2. The deterministic threshold public key share decryption algorithm TPKsubdec(xi, PRi, VKi) decrypt the secret share xi with private key PRi and verification key VKi. The deterministic threshold combining algorithm TPKdec(x1,...,x2) means that recover x from x1,...,x2. The projection function projectioni(x) generated the ith share from the formatted message x. The self blinding function SelfBlinding(x,r) blinds message x with r. The add function add(x,y) add x and y. checkciphertext(x1,x2) verify the two ciphertext x1 and x2 generated with the same plaintext. SK(x) PK(x) VK(x) generated the secret key, public key and verification key of x. equals(x,y) checks whether x is equal to y or not.
The basic equational theory is described in Fig. 15. The threshold decryption and combining algorithm are introduced.
The equational theory also contains and equational rules for abstractly reasoning about the knowledge proof that two ciphertexts are encryption of the same plaintext which is modeled in Fig. 16 and used in the voting phase and tallying phase. In the voting phase the voter need to verify the equivalence between the encrypted share and the one the voter has received to its message are also provided to itself. In the tallying phase the tally authority need to check the two lists: a list of encrypted, mixed credentials the registration authorities themselves had originally posted on the bulletin board; and a set of encrypted, mixed sums of credentials and ballots, posted on the bulletin board by the voters. It modeled as:
It can verify the two ciphertext, one is the ciphertext generated with the public key PUy and random number r1, the other is the ciphertext generated with the public key PUz and random number r2, are the same plaintext x1.
Designated verifier proofs modeled in Fig. 17 in the applied PI calculus (Backes et al., 2008b) is also contained in the equational theory and equational rules. During the registration phase, the voter acquires a private credential for voting. For this he contacts each of the registration authority and asks them for a share of the private credential. In order for a registration authority to prove the correctness of the share credential, a designated verifier proof is used. Designated verifier proof can convince only the voter of the correctness of the share credential and nobody else. In particular the voter should be able to generate a fake proof of this fact, e.g., using his secret key.
| Fig. 16: | Model of knowledge proof that two ciphertexts are encryption of the same plaintext |
| Fig. 17: | Model of designated verifier proofs |
| Fig. 18: | Main process |
| Fig. 19: | Voter process |
| Fig. 20: | Corrupted voter process |
Processes: The complete formal model of Acquisti protocol in applied PI calculus is given in Fig. 18-23 report the basic process include main process, voter process, corrupted voter process, registration authority process, issuer authority process and tallying authority process forming our of the model of Acquisti protocol. Figure 24-29 offer additional and modified processes for the analysis of coercion-resistance.
The main process in Fig. 18 sets up private channels chVR, chRI1, chRI2 and specifies how the processes are combined in parallel. chVR is the private channel between voter and registration authority. chRI1 and chRI2 are the private channel between registration authority and issuer authority. At the same time the main process generates the key parameters c for credentials, V for vote, S for non-homomorphic cryptosystem, keyV for voter and key1 for issuer authority.
| Fig. 21: | Registration authority process |
| Fig. 22: | Issuer authority process |
| Fig. 23: | Tallying authority process |
Voter process is modeled in applied PI calculus in Fig. 19. Using Paillier encryption, each voter get the shares ciphertext kVenccred1 and kVenccred2 from registration authority, then decrypt and get the credentials venccred1, venccred2 and the designated verifier proof NZDVP1 and NZDVP2. After that the voter use CheckNZDVPp,to verify NZDVP1 and NZDVP2. The voter also use checkciphertest( ) to verify the equivalence between the encrypted share: Public1 (NZDVP1), decsign (Public2 (NZCVP1)) and the one Public1 (NZDVP2), decsign (Public2 (NZCVP2)) the voter has received to its message are also provided to itself. The voter also gets the encrypted shares vencballottt of the ballot, which she has selected from the bulletin board. He multiplies:
| Fig. 24: | Cheating voter process |
| Fig. 25: | Coerced voter process |
Because of the homomorphic properties of Paillier cryptosystems, the resulting ciphertext result includes the sum of credential shares and the ballot’s shares. The resulting ciphertext TpPKenc(result, PK(S), r) is sent to the bulletin board.
Corrupted voters process is modeled in Fig. 20. The corrupted voter will register and get his secret credentials shares kVenccred1 and kVenccred2 from registration authority, then decrypt and get the credentials venccred1, venccred2 proof of the equivalence between the encrypted share it has posted on the bulletin board and the one it will sent to the voter. NZDVP1 and NZDVP2, after that, he simply output all their registration secrets venccred1 and venccred2 on a public channel, so that the attacker can impersonate them in order to mount any sort of attack.
| Fig. 26: | Modified tallying authority process |
| Fig. 27: | Abstained voter process |
| Fig. 28: | Extractor process |
The registration authority process is modeled in Fig. 21. The registration authority generate the voters id, then get the secret credentials shares cred1 and cred2. After that the registration authority creates designated verifier proof that the proof of the equivalence between the encrypted share it has posted on the bulletin board and the one it will sent to the voter NZDVP1 and NZDVP1.
The issuer authority is modeled in Fig. 22. The issuer authorities get the shares of ballot by projectioni (ballott) and send sign[pPKenc(ci(cred, PK(C), r1, SKi(C)] which is encrypted with a set of Paillier public parameters by the public channel pub.
| Fig. 29: | Acquisti-coercion-resistance2 process |
| Fig. 30: | Acquisti-coercion-resistance2 process |
Tallying authority process is modeled in Fig. 23. After the voting time expires, the tallying authorities get the all ballots on bulletin board posted by allegedly eligible voters and then mixed it by SelfBlinding(cenccred, PK(C)). The shares of credentials posted by the registration authorities are also combined and then mixed SelfBlinding(venccredvote, PK(V)). Tallying authorities thus obtain two lists: a list bcenccred of encrypted, mixed credentials the registration authorities themselves had originally posted on the bulletin board; and a set cencballott of encrypted, mixed sums of credentials and ballots, posted on the bulletin board by the voters. The two lists have been encrypted with different Paillier public parameters. Using threshold protocols for the corresponding sets of private keys, the tallying authorities decrypt the elements in each list by checkciphertext(test, bvenccredvote) and then compare them through a search algorithm and publish the tallying result on bulletin board.
According to the definition coerced-resistance of Backes et al. (2008a) in order to analyze coercion-resistance of Acquisti protocol, the processes including cheating voter process, coerced voter process, modified tallying authority process, abstained voter process, extractor process, Acquisti-coercion-resistance1 process and Acquisti-coercion-resistance2 process, are needed. The faking strategy of the cheating voter consists of generating a fake credential and sending it to the coercer. To generate the fake credential fakecred1 and fakecred2, the voter construct a valid designated verifier proof NZDVP that causes this fake share to appear real to the coercer in Fig. 24. In Fig. 25 the coerced voter sends his genuine (Public1 (NZDVP1), Public1 (NZDVP2)) and (Public1 (NZDVP1), Public1 (NZDVP2)) to the coercer.
In Fig. 26 the modified tallying authority sends the credentials and vote by chTE to the extractor process. The difference between the previous tallying authority process in Fig. 23 and modified tallying authority process is that the tallying authority process in Fig. 23 does not publish the credentials and vote. In Fig. 27 the abstained voter receives the related information and give up his vote. The extractor process in Fig. 28 can identify this fake designated verifier proof as being a coerced vote. Notice, that the modified tallying authority process in Fig. 26 shares a private channel chTE with the extractor aprivate channel chVE with voter. The processes Acquisti-coercion-resistance1 in Fig. 29 and Acquisti-coercion-resistance2 in Fig. 30 need to be observationally equivalent in order to satisfy the definition coercion resistance of Backes et al. (2008a) and to be able to mechanizedly prove this property of the protocol.
MECHANIZED PROOF OF ACQUISTI PROTOCOL WITH PROVERIF
ProVerif can take two formats as input. The first one is in the form of Horn clauses (logic programming rules) and applied PI calculus. The second one is in the form of a process in an extension of the PI calculus (Abadi and Blanchet, 2005). In both cases, the output of the system is essentially the same.
In this study we use an extension of the PI calculus as the input of ProVerif. In order to prove the soundness and coercion resistance in Acquisti protocol the applied PI calculus model are needed to be translated into the syntax of ProVerif and generated the ProVerif inputs in extension of the PI calculus (Abadi and Blanchet, 2005).
| Fig. 31: | Function 1 |
| Fig. 32: | Function 2 |
Firstly the soundness of Acquisti protocol is proved by ProVerif. In order to prove the soundness property, according to the definition of Backes et al. (2008a) model, the soundness consists of inalterability(condition 1a), ligibility(condition 1b) and non-reusability(condition 1a and condition 2). Figure 31-40 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of soundness in ProVerif. The analysis was performed by ProVerif and succeeded in Fig. 41. Bad is not derivable shows that observational equivalence is true. As a result, Acquisti protocol is proved to guarantee inalterability, eligibility and unbreusability for an unbounded number of honest voters and an unbounded number of corrupted participants.
The proof of coercion-resistance in Acquisti protocol is also finished by ProVerif. According to definition of coercion-resistance in Backes et al. (2008a) model, the coercion-resistance is composed of one hypothesis and four conditions. The hypothesis describes that election context S' that only differs from S in that the tallying authority additionally outputs messages on the channel c2 shared with Extractor.
| Fig. 33: | Equation |
| Fig. 34: | Soundness-vote chooser |
Condition 2 describes the special observational equivalence between:
and
contains the voter Vi that is in accordance with the orders of the coercer, running in parallel with the voter Vj casting
| Fig. 35: | Soundness-voter |
| Fig. 36: | Soundness-corrupted voter |
a vote v' and the process
the voter Vi cheats the coercer by providing him with fake registration secrets and then votes v', the voter Vi participates in the registration phase and then abstains and the extractor process:
tallies the vote the coercer casts on behalf of Vi. Figure 31-33, 42-55 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of Condition 2 in ProVerif. The result shows that the observational equivalence between:
and
is satisfied in Fig. 56. Bad is not derivable shows that observational equivalence is true.
| Fig. 37: | Soundness-tallying authority |
| Fig. 38: | Soundness-registration authority |
| Fig. 39: | Soundness-issuer authority |
| Fig. 40: | Soundness process |
| Fig. 41: | The result of soundness |
| Fig. 42: | Coercion-resistance-condition2-additional equation |
| Fig. 43: | Coercion-resistance-condition2-vote chooser |
| Fig. 44: | Coercion-resistance-condition2-voter |
| Fig. 45: | Coercion-resistance-condition2-corrupted voter |
| Fig. 46: | Coercion-resistance-condition2-voter registration |
Condition 3 describes the scenario that if the cheated coercer abstains, then the Extractor needs to abstain as well. The observational equivalence between:
and
| Fig. 47: | Coercion-resistance-condition2-coerced voter |
| Fig. 48: | Coercion-resistance-condition2-voter cast |
| Fig. 49: | Coercion-resistance-condition2-tallying authority |
| Fig. 50: | Coercion-resistance-condition2-registration authority |
| Fig. 51: | Coercion-resistance-condition2-issuer authority |
is need to be proved. Figure 31-33, 57-69 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of Condition 3 in ProVerif. The result shows that the observational equivalence between:
and
is true in Fig. 70. Bad is not derivable shows that observational equivalence is true.
| Fig. 52: | Coercion-resistance-condition2-extractor |
| Fig. 53: | Coercion-resistance-condition2-modified-tallying authority |
In condition 4 if the cheated coercer casts a valid vote using the fake registration secrets he received from Vi, the Extractor needs to tally precisely this vote. The observational equivalence between:
and
is to be proved. Figure 31-33, 71-83 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of Condition 4 in ProVerif. The result shows that the observational equivalence between:
and
is true in Fig. 84. Bad is not derivable shows that observational equivalence is true.
In condition 5 an additional restriction is introduced that justifies the abstraction of the third voter by the
| Fig. 54: | Coercion-resistance-condition2-modified registration authority |
| Fig. 55: | Coercion-resistance-condition2-process |
| Fig. 56: | The result of coercion-resistance-condition2 |
| Fig. 57: | Coercion-resistance-condition3-vote chooser |
| Fig. 58: | Coercion-resistance-condition3-voter |
| Fig. 59: | Coercion-resistance-condition3-corrupted voter |
| Fig. 60: | Coercion-resistance-condition3-voter registration |
| Fig. 61: | Coercion-resistance-condition3-coerced voter |
| Fig. 62: | Coercion-resistance-condition3-voter casting |
| Fig. 63: | Coercion-resistance-condition3-tallying authority |
| Fig. 64: | Coercion-resistance-condition3-registration authority |
| Fig. 65: | Coercion-resistance-condition3-issuer authority |
| Fig. 66: | Coercion-resistance-condition3-extractor |
| Fig. 67: | Coercion-resistance-condition3-modified tallying authority |
| Fig. 68: | Coercion-resistance-condition3-modified registration authority |
Extractor: votes with invalid registration secrets are silently discarded by the tallying authority. If this was not the case a coercer could easily distinguish real from fake registration secrets. The observational equivalence between:
and
| Fig. 69: | Coercion-resistance-condition3-process |
| Fig. 70: | The result of coercion-resistance-condition3 |
| Fig. 71: | Coercion-resistance-condition4-vote choose |
| Fig. 72: | Coercion-resistance-condition4-voter |
| Fig. 73: | Coercion-resistance-condition4-corrupted voter |
| Fig. 74: | Coercion-resistance-condition4-voter registration |
| Fig. 75: | Coercion-resistance-condition4-coerced voter |
| Fig. 76: | Coercion-resistance-condition4-voter casting |
| Fig. 77: | Coercion-resistance-condition4-tallying authority |
| Fig. 78: | Coercion-resistance-condition4-registration authority |
| Fig. 79: | Coercion-resistance-condition4-issuer authority |
| Fig. 80: | Coercion-resistance-condition4-extractor |
| Fig. 81: | Coercion-resistance-condition4-modified tallying authority |
| Fig. 82: | Coercion-resistance-condition4-modified registration authority |
is proved in ProVerif. Figure 31-33, 85-91 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of Condition 2 in ProVerif. The result shows that the observational equivalence is true in Fig. 92. Bad is not derivable shows that observational equivalence is true.
| Fig. 83: | Coercion-resistance-condition4-process |
| Fig. 84: | The result of coercion-resistance-condition4 |
| Fig. 85: | Coercion-resistance-condition5-vote chooser |
| Fig. 86: | Coercion-resistance-condition5-voter |
| Fig. 87: | Coercion-resistance-condition5-corrupted voter |
| Fig. 88: | Coercion-resistance-condition5-voter choice |
According to the above analysis we can found that the Acquisti protocol has the coercion-resistance with the assumption that the channel chVR1, chVR2 and chVR3 between modified registration authority and coerced voter is private channel.
| Fig. 89: | Coercion-resistance-condition5-tallying authority |
| Fig. 90: | Coercion-resistance-condition5-registration authority |
| Fig. 91: | Coercion-resistance-condition5-process |
If these channels are public then the coercer could easily distinguish real
from fake registration secrets, thus the condition2 of coercion-resistance is
not satisfied. The result is showed in Fig. 93.
| Fig. 92: | The result of coercion-resistance-condition5 |
| Fig. 93: | The result of coercion-resistance-condition2 with the condition that the channels are public |
CONCLUSION AND FUTURE WORK
Internet voting protocol play an important role in remote voting system. Acquisti protocol is one of the most important remote internets voting protocol that claims to satisfy formal definitions of key properties, such as soundness, individual verifiability, as well as receipt-freeness and coercion resistance without strong physical constrains. But the analysis of its claimed security properties is finished by hand which depends on experts’ knowledge and skill and is prone to make mistakes. Recently owning to the contribution of Backes et al. (2008a) Acquisti protocol can be proved with mechanized proof tool ProVerif. In this study the review of the formal method of electronic voting protocols are introduced we found that several formal models have been proposed, but only the Backes et al. (2008b) model supports the mechanized proof tool; the formal model and proof of security properties mainly focus on receipt-freeness and coercion-resistance which are important properties. Until now people have not proposed a security analysis model based on computational model, then applied PI calculus and the mechanized proof tool ProVerif are examined. After that Acquisti protocol is modeled in applied PI calculus. Security properties, including soundness and coercion resistance, are verified with ProVerif. The result we obtain is that Acquisti protocol has the soundness. At the same time it has also coercion-resistance in the conditions that the channel between registration authority and voter is private. To our best knowledge, the first mechanized proof of Acquisti protocol for an unbounded number of honest and corrupted voters is finished.
As future work, we plan to prove other internet voting protocols. It would also be interesting to formalize the security properties in wireless communication protocol in the formal model with mechanized proof tool ProVerif. At the same time we will formalize the security properties of remote internet voting protocols in the computational model with mechanized tool CryptoVerif.
ACKNOWLEDGMENT
This study was supported in part by Natural Science Foundation of South-Center University for Nationalities under the grants No: YZZ06026, titled Research on the internet voting protocols with receipt-freeness, conducted in Wuhan, China from 06/11/2006 to 20/11/2009. The preliminary part work in this study is published in Meng et al. (2010c).