**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.

PDF Abstract XML References Citation

**Received:**August 29, 2010;

**Accepted:**October 01, 2010;

**Published:**November 12, 2010

####
**How to cite this article**

*Information Technology Journal, 10: 293-334.*

**DOI:**10.3923/itj.2011.293.334

**URL:**https://scialert.net/abstract/?doi=itj.2011.293.334

**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 V_{A} and V_{B} exchange their votes, then in general he can not know anything about how V_{A} (or V_{B}) voted. This definition is robust even in situations where the result of the election is such that the votes of V_{A} and V_{B} 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 V_{B} can change his vote and counterbalance the outcome. However, avoid the case where V' = V_{A} {c/v}^{c1,c2} letting V_{B} vote α is needed. Therefore, requirement that when we apply a context C, intuitively the coercer, requesting V_{A} {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 is set of function symbols, each with an arity. Terms and function symbols are sorted and of course function symbol application must respect sorts and arities. Typically, we let a, b and c range over channel names. Let, x, y and z range over variables and u over variables and names. We abbreviate an arbitrary sequence of terms .

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 is a sequence of name restrictions v_{n1},...,v_{n1}. The process in (u,x).P receives a message from channel u and runs the process P by replacing formal parameter x by the actual message. We use for the input of terms M_{1},...,M_{1}. The process out(u,N).P is firstly ready to output the message N on the channel u and then runs the process P. The process is the abbreviation for the output of terms N_{1},...,N_{1}. The conditional construct if M = N then P else Q runs that if M and N are equal, executes P, otherwise executes Q.

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 is equipped with an equational theory that is an equivalence relation on terms that is closed under substitutions of terms for variables. An equational theory is generated from a finite set of equational axioms. It models the algebraic properties of cryptographic primitives. We write |-M = N for equality within the equational theory and |-/M = N for inequality.

**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. A_{LIAS} enables the introduction of an arbitrary active substitution. S_{UBST} 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:

T_{HEN} and E_{LSE} directly depend on the underlying equational theory; using E_{LSE} sometimes requires that active substitutions in the context be applied first, to yield ground terms M and N.

We write when A can send a message on a, that is, when for some evaluation context C[O] that does not bind a. Observational equivalence constitutes an equivalence relation that captures the equivalence of processes with respect to their dynamic behavior. Observational equivalence (≈) is the largest symmetric relation R between closed extended processes with the same domain such that A R B implies:

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 V^{fake} 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 is an Extractor if and only if: |

The channels c_{1} and c_{2} 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, c_{1} and c_{2}, a sequential process V^{fake}, an Extractor E^{c1,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 c_{2} shared with Extractor. In condition 2 the left side process contains the voter V_{i} that is in accordance with the orders of the coercer, running in parallel with the voter V_{j} casting a vote v' and the process E^{c1,c2,z}[0], that is intuitively equivalent to a voter nullifying her vote. In the right side election process the voter V_{i} cheats the coercer by providing him with fake registration secrets and then votes v', the voter V_{j} participates in the registration phase and then abstains and the extractor process:

tallies the vote the coercer casts on behalf of v_{i}. 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 v_{i}, 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 A_{i}(i = 1......*l*) creates *l* random numbers c as c_{i,j}, representing shares of credentials, for each eligible voter veter_{j}(*l* = 1......*l*). For each c_{i,j}, A_{i} performs two operations: first, it encrypts c_{i,j} using PK^{C} and appropriate secret randomization, signs the resulting ciphertext with SK_{i}^{C} and publishes it on bulletin board on a row publicly reserved for the shares of credential of voter:

SKA_{i} represents the signature of authority A_{i} Second, A_{i} also encrypts c_{i,j} using PK^{V} and appropriate secret randomization, without signing it, but attaching to it a designated verifier proof DVPv_{j} of equality of plaintexts E^{C}(c_{i,j}) and E^{V}(c_{i,j}). The proof is designated to be verifiable only by voter_{j}. A_{i} encrypts this second message with voter_{j}’s public key and sends it:

E^{voterj} represents RSA encryption under voter_{j}’s public key.

**Voting phase:** For each encrypted share of credential she receives, voter_{j} verifies the designated verifier proof of equality between E^{V}(c_{i,j}) and the corresponding E^{V}(c_{i,j}) that has been signed and published in her reserved area of bulletin board. Upon successful verification, she multiplies together the shares E^{V}(c_{i,j}).

C_{j} is the sum of the various shares of credentials. voter_{j}. Voter chooses the ballot shares , generates:

and sends to bulletin board.

**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(x_{i}, Pr_{i}, VK_{i}) decrypt the secret share x_{i} with private key PR_{i} and verification key VK_{i}. The probabilistic threshold combining algorithm TpPKdec(x_{1},...,x_{2}) recovers x from x_{1},...,x_{2}. The deterministic threshold public key share decryption algorithm TPKsubdec(x_{i}, PR_{i}, VK_{i}) decrypt the secret share x_{i} with private key PR_{i} and verification key VK_{i}. The deterministic threshold combining algorithm TPKdec(x_{1},...,x_{2}) means that recover x from x_{1},...,x_{2}. The projection function projection_{i}(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(x_{1},x_{2}) verify the two ciphertext x_{1} and x_{2} 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 PU_{y} and random number r_{1}, the other is the ciphertext generated with the public key PU_{z} and random number r_{2}, are the same plaintext x_{1}.

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, chRI_{1}, chRI_{2} and specifies how the processes are combined in parallel. chVR is the private channel between voter and registration authority. chRI_{1} and chRI_{2} 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 kVenccred_{1} and kVenccred_{2} from registration authority, then decrypt and get the credentials venccred_{1}, venccred_{2} and the designated verifier proof NZDVP_{1} and NZDVP_{2}. After that the voter use CheckNZDVPp,to verify NZDVP_{1} and NZDVP_{2}. The voter also use checkciphertest( ) to verify the equivalence between the encrypted share: Public_{1} (NZDVP_{1}), decsign (Public_{2} (NZCVP_{1})) and the one Public_{1} (NZDVP_{2}), decsign (Public_{2} (NZCVP_{2})) the voter has received to its message are also provided to itself. The voter also gets the encrypted shares vencballot^{t}_{t} 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 kVenccred_{1} and kVenccred_{2} from registration authority, then decrypt and get the credentials venccred_{1}, venccred_{2 }proof of the equivalence between the encrypted share it has posted on the bulletin board and the one it will sent to the voter. NZDVP_{1} and NZDVP_{2}, after that, he simply output all their registration secrets venccred_{1} and venccred_{2} 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 cred_{1} and cred_{2}. 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 NZDVP_{1} and NZDVP_{1}.

The issuer authority is modeled in Fig. 22. The issuer authorities get the shares of ballot by projection_{i} (ballot^{t}) and send sign[pPKenc(c_{i}(cred, PK(C), r_{1}, SK_{i}(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 cencballot^{t} 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 fakecred_{1} and fakecred_{2}, 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 (Public_{1} (NZDVP_{1}), Public_{1} (NZDVP_{2})) and (Public_{1} (NZDVP_{1}), Public_{1} (NZDVP_{2})) 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 c_{2} shared with Extractor.

Fig. 33: | Equation |

Fig. 34: | Soundness-vote chooser |

Condition 2 describes the special observational equivalence between:

and

contains the voter V_{i} that is in accordance with the orders of the coercer, running in parallel with the voter V_{j} casting

Fig. 35: | Soundness-voter |

Fig. 36: | Soundness-corrupted voter |

a vote v' and the process , that is intuitively equivalent to a voter nullifying her vote. In:

the voter V_{i} cheats the coercer by providing him with fake registration secrets and then votes v', the voter V_{i} participates in the registration phase and then abstains and the extractor process:

tallies the vote the coercer casts on behalf of V_{i}. 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 V_{i}, 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).

####
**REFERENCES**

- Abadi, M. and A.D. Gordon, 1999. A calculus for cryptographic protocols: The spi calculus. Inform. Comput., 148: 1-70.

CrossRefDirect Link - Abadi, M. and C. Fournet, 2001. Mobile values, new names and secure communication. Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK., January 17-19, 2001, ACM New York, USA., pp: 104-115.

CrossRefDirect Link - Abadi, M., B. Blanchet and C. Fournet, 2004. Just Fast Keying in the Pi Calculus. In: Programming Languages and Systems, Schmidt, D. (Ed.). LNCS., 2986, Springer, Berlin, Heidelberg, ISBN-13: 978-3-540-21313-0, pp: 340-354.

CrossRefDirect Link - Abadi, M. and B. Blanchet, 2005. Analyzing security protocols with secrecy types and logic programs. J. ACM, 52: 102-146.

Direct Link - Aditya, R., B. Lee, C. Boyd and E. Dawson, 2004. An efficient mixnet-based voting scheme providing receipt-freeness. Lecture Notes Comput. Sci., 3184: 152-161.

Direct Link - Backes, M., C. Hritcu and M. Maffei, 2008. Automated verification of remote electronic voting protocols in the applied Pi-calculus. Proceedings of the 21st Computer Security Foundations Symposium, June 23-25, 2008, IEEE Computer Society, Washington, DC, pp: 195-209.

Direct Link - Backes, M., M. Maffei and D. Unruh, 2008. Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. Proceedings of the 29th IEEE Symposium on Security and Privacy, May 2008, Preprint on IACR ePrint, pp: 202-215.

Direct Link - Baskar, A., R. Ramanujam and S.P. Suresh, 2007. Knowledge-based modelling of voting protocols. Proceedings of the 11th Conference on theoretical Aspects of Rationality and Knowledge, June 25-27, 2007, Brussels, Belgium, pp: 62-71.

Direct Link - Baudron, O., P.A. Fouque, D. Pointcheval, G. Poupard and S. Jacques, 2001. Practical multi-candidate election system. Proceedings of the Annual ACM Symposium on Principles of Distributed Computing, August 26-29, 2001, ACM, New York, USA., pp: 274-283.

CrossRefDirect Link - Benaloh, J. and D. Tuinstra, 1994. Receipt-free secret-ballot elections. Proceedings of the 26th Annual ACM Symposium on Theory of Computing, May 23-25, 1994, ACM, New York, USA., pp: 544-553.

CrossRefDirect Link - Bhargavan, K., R. Corin, C. Fournet and E. Zalinescu, 2008. Cryptographically verified implementations for TLS. Proceedings of the 15th ACM Conference on Computer and Communications Security, Oct. 27-31, Alexandria, Virginia, USA., pp: 459-468.

Direct Link - Blanchet, B., 2001. An efficient cryptographic protocol verifier based on prolog rules. Proceedings of the 14th IEEE Workshop on Computer Security Foundations, June 11-13, 2001, IEEE Computer Society, Washington, DC., pp: 82-96.

Direct Link - Blanchet, B., 2008. A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput., 5: 193-207.

CrossRef - Burrows, M., M. Abadi and R. Needham, 1990. A logic of authentication. ACM Trans. Comput. Syst., 8: 18-36.

CrossRef - Clarkson, M.R., S. Chong and A.C. Myers, 2008. Civitas: Toward a secure voting system. Proceeding of the 2008 IEEE Symposium on Security and Privacy, May 18-21, 2008, Oakland, California, USA., pp: 354-368.

Direct Link - Chaum, D.L., 1981. Untraceable electronic mail, return addresses and digital pseudonyms. Commun. ACM, 24: 84-88.

CrossRef - Chaum, D., 2004. Secret-ballot receipts: True voter-verifiable elections. IEEE Security Privacy, 2: 38-47.

CrossRefDirect Link - Cichon, J., M. Kutyłowski and B. Glorz, 2008. Short Ballot Assumption and Threeballot Voting Protocol. In: SOFSEM 2008: Theory and Practice of Computer Science, Geffert, V.
*et al*. (Eds.). Springer-Verlag, Berlin Heidelberg, pp: 585-598.

CrossRef - Clarke, E.M., S. Jha and W. Marrero, 2000. Verifying security protocols with Brutus. ACM Trans. Softw. Eng. Methodol., 9: 443-487.

Direct Link - Cramer, R., R. Gennaro and B. Schoenmakers, 1997. A Secure and Optimally Efficient Multi-Authority Election Scheme. In: Trustworthy Global Computing, Fumy, W. (Ed.). Springer-Verlag, Berlin Heidelberg, pp: 103-118.

CrossRef - Delaune, S., S. Kremer and M.D. Ryan, 2006. Coercion-resistance and receipt-freeness in electronic voting protocol. Proceedings of the 19th Computer Security Foundations Workshop, July 5-7, 2006, Venice, Italy, pp: 28-42.

CrossRef - DeMillo, R.A., N.A. Lynch and M.J. Merritt, 1982. Cryptographic protocols. Proceedings of the 14th Annual ACM Symposium on theory of Computing, May 5-7, 1982, San Francisco, California, United States, pp: 383-400.

Direct Link - Fujioka, A., T. Okamoto and K. Ohta, 1992. A practical secret voting scheme for large-scale elections. Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, December 13-16, 1992, Springer-Verlag, London, UK., pp: 244-251.

Direct Link - Groth, J., 2004. Evaluating Security of Voting Schemes in the Universal Composability Framework. In: Applied Cryptography and Network Security, Jakobsson, M., M. Yung and J. Zhou (Eds.). Springer-Verlag, Berlin Heidelberg, pp: 46-60.

CrossRef - Hirt, M. and K. Sako, 2000. Efficient receipt-free voting based on homomorphic encryption. Proceedings of the International Conference on the Theory and Application of Cryptographic Techniques, May 14-18, 2000, Bruges, Belgium, pp: 539-556.

Direct Link - Hubbers, E., B. Jacobs and W. Pieters, 2005. RIES-internet voting in action. Proceedings of the 29th Annual International Computer Software and Applications Conference, July 26-28, 2005, IEEE Computer Society, Washington, DC., pp: 417-424.

Direct Link - Jakobsson, M., K. Sako and R. Impagliazzo, 1996. Designated verifier proofs and their applications. Proceedings of the International Conference on the Theory and Application of Cryptographic Techniques, May 12-16, 1996, Saragossa, Spain, pp: 143-154.

CrossRef - Jonker, H.L. and E.P. De-Vink, 2006. Formalising receipt-freeness. Proceedings of the 9th International Conference on Information Security, August 30-September 2, 2006, Samos Island, Greece, pp: 476-488.

CrossRef - Juels, A., D. Catalano and M. Jakobsson, 2005. Coercion-resistant electronic elections. Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, November 7, 2005, Alexandria, VA, USA., pp: 61-70.

Direct Link - Kessler, V. and H. Neumann, 1998. A sound logic for analysing electronic commerce protocols. Proceedings of the 5th European Symposium on Research in Computer Security, September 16-18, 1998, London, UK., pp: 345-360.

Direct Link - Lowe, G., 1998. Casper: A complier for the analysis of security protocols. J. Comput. Sec., 6: 53-84.

Direct Link - Maggi, P. and R. Sisto, 2002. Using SPIN to verify security properties of cryptographic protocols. Proceedings of the 9th International SPIN Workshop on Model Checking of Software, April 11-13, Springer-Verlag, London, pp: 187-204.

CrossRef - Magkos, E., M. Burmester and V. Chrissikopoulos, 2001. Receipt-freeness in large-scale elections without untappable channels. Proceedings of the IFIP Conference on Towards the E-Society: E-Commerce, E-Business, E-Government, October 3-5, 2001, Kluwer B.V., Deventer, The Netherlands, pp: 683-694.

Direct Link - Mauw, S., J. Verschuren and E.P. De Vink, 2007. Data anonymity in the FOO voting scheme. Elect. Notes Theor. Comput. Sci., 168: 5-28.

CrossRefDirect Link - Meadows, C.A., 1996. The NRL protocol analyzer: An overview. J. Logic Program., 26: 113-131.

CrossRef - Mei, J., H. Miao and P. Liu, 2009. Applying SMV for security protocol verification. Infom. Technol. J., 8: 1065-1070.

CrossRefDirect Link - Meng, B., 2007. An internet voting protocol with receipt-free and coercion-resistant. Proceedings of the 7th International Conference on Computer and Information Technology, October 16-19, 2007, IEEE Computer Society, Washington DC, USA., pp: 721-726.

CrossRefDirect Link - Meng, B., 2007. Analysis of internet voting protocols with jonker-vink receipt freeness formal model. Proceedings of the International Conference on Convergence Information Technology, November 21-23, 2007, ICCIT., IEEE Computer Society, Washington, DC., pp: 663-669.

CrossRef - Meng, B., 2008. Formal analysis of key properties in the internet voting protocol using applied pi calculus. Inform. Technol. J., 7: 1133-1140.

CrossRefDirect Link - Meng, B., 2009. A secure internet voting protocol based on non-interactive deniable authentication protocol and proof protocol that two ciphertexts are encryption of the same plaintext. J. Networks, 4: 370-377.

CrossRefDirect Link - Meng, B., 2009. A formal logic framework for receipt-freeness in internet voting protocol. J. Comput., 4: 184-192.

Direct Link - Meng, B., 2009. A critical review of receipt-freeness and coercion-resistance. Inform. Technol. J., 8: 934-964.

CrossRefDirect Link - Meng, B., 2009. A secure non-interactive deniable authentication protocol with strong deniability based on discrete logarithm problem and its application on Internet voting protocol. Inform. Technol. J., 8: 302-309.

CrossRefDirect Link - Meng, B., Z. Li and J. Qin, 2010. A receipt-free coercion-resistant remote internet voting protocol without physical assumptions through deniable encryption and trapdoor commitment scheme. J. Software, 5: 942-949.

CrossRefDirect Link - Meng, B. and J.Q. Wang, 2010. An efficient receiver deniable encryption scheme and its applications. J. Networks, 5: 683-690.

CrossRef - Meng, B., W. Huang and J. Qin, 2010. Automatic verification of security properties of remote internet voting protocol in symbolic model. Inform. Technol. J., 9: 1521-1556.

CrossRefDirect Link - Mitchell, J.C., M. Mitchell and U. Stern, 1997. Automated analysis of cryptographic protocols using Mur. Proceedings of the 1997 Symposium on Security and Privacy, May 4-7, 1997, Digital Library, pp: 141.

Direct Link - Paillier, P., 1999. Public-Key Cryptosystems Based on Composite Degree Residuosity Classes. In: Advances in Cryptology-EUROCRYPT '99, Stern, J. (Ed.). Springer-Verlag, Berlin Heidelberg, pp: 223-238.

CrossRef - Paulson, L.C., 1998. The inductive approach to verifying cryptographic protocols. J. Comput. Sec., 6: 85-128.

Direct Link - Song, D.X., 1999. Athena: A new efficient automatic checker for security protocol analysis. Proceedings of the 12th IEEE Workshop on Computer Security Foundations, June 28-30, IEEE Computer Society, Washington, DC., pp: 192-202.

CrossRefDirect Link - Talbi, M., B. Morin, V. V.T. Tong, A. Bouhoula and M. Mejri, 2008. Specification of electronic voting protocol properties using ADM logic: FOO case study. Proceedings of the 10th international Conference on information and Communications Security, Oct. 20-22, Birmingham, UK., pp: 403-418.

Direct Link - Fabrega, F.J.T., J.C. Herzog and J.D. Guttman, 1998. Strand space: Why is a security protocol correct? Proceedings of the Symposium on Security and Privacy, May 3-6, 1998, ACM, USA., pp: 160-171.

CrossRef - Van Eijck, J. and S. Orzan, 2007. Epistemic verification of anonymity. Elect. Notes Theor. Comput. Sci., 168: 159-174.

CrossRefDirect Link - Yao, A.C., 1982. Theory and application of trapdoor functions. Proceedings of the 23rd Annual Symposium on Foundations of Computer Science, Nov. 3-5, IEEE Computer Society, Washington, DC., pp: 80-91.

Direct Link