Abstract: Soundness and coercion resistance are the important and intricate security requirements for remote voting protocols. In this study firstly the review of the formal methods of security protocols is introduced, then applied pi calculus and the automatic tool ProVerif are examined. Thirdly Meng et al. protocol recently proposed is modeled in applied pi calculus. Finally soundness and coercion resistance are verified with automatic tool ProVerif. The result we obtain is that Meng et al. protocol has coercion resistance. But it has not soundness because ProVerif found an attack on soundness. Finally the improvement of Meng et al. protocol is proposed and also modeled in applied pi calculus and automatically analyzed in ProVerif. The result we get is that the improvement of protocol has soundness. To our best knowledge, the first automated analysis of Meng et al. protocol for an unbounded number of honest and corrupted voters is finished.
INTRODUCTION
With the development of Internet and information technology, electronic government has got serious attention from government, enterprise and academic world. Owning to advantages of remote internet voting, it plays an important role in electronic government. In order to increase confidence of the voters in remote internet voting system, many researchers have focused on 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 are challenging issues (Meng, 2009c).
The practical secure remote internet voting protocol should include the following properties:
Basic properties include privacy, completeness, soundness, 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).
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; Juels and Jakobsson, 2002; Chaum et al., 2005; Rivest, 2006; Cichon et al., 2008; Magkos et al., 2001; Chaum, 2004; Juels et al., 2005; Acquisti, 2004; Meng, 2007a, 2009a; Meng et al., 2010), claimed on their security, have be proposed. In order to 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 automatic tools. In contrast, symbolic model is considerably simpler than the computational model, proofs are therefore also simpler and can sometimes benefit from automatic tools support. For example: SVM (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).
ProVerif (Blanchet, 2001) is an automatic cryptographic protocol verifier based on a representation of the protocol by Horn clauses. 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).
Owning to analysis manually of security properties of (Meng et al., 2010) in their study, this method depend on experts’ knowledge and skill and is prone to make mistakes, we use automatic tool ProVerif to verify security properties of Meng protocol.
The main contributions of this paper are summarized as follows:
| • | Review the formal analysis security properties in electronic voting protocol |
| • | Apply the automatic formal model proposed by Backes et al. (2008a) for automatically analyzing Meng et al. (2010) protocol and its security properties. Therefore, Meng et al. (2010) protocol is modeled in applied pi calculus and the soundness and coercion-resistance take into account. The analysis itself is performed by automatic tool ProVerif developed by Blanchet. To our best knowledge, we are conducting the first automated analysis of Meng et al. (2010) protocol for an unbounded number of honest and corrupted voters |
| • | The result of analysis of Meng et al. (2010) protocol is that it has coercion resistance. But it has not soundness because ProVerif found an attack on it. Then the improvement of Meng et al. (2010) protocol is proposed. After that the soundness of the improvement of Meng et al. (2010) protocol is modeled in applied pi calculus and automatically analyzed by ProVerif. The result we get is that the improvement of Meng et al. (2010) protocol has soundness |
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). The 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, SVM (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).
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 and is not
supported by the automatic tools. 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 idea is that
whenever the coercer requests a given vote then VB can change his
vote and counterbalance the outcome. However, avoid the case where
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 (2006), 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 formal model. They use the formalism to analyze several 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, Meng (2009b) 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: α: 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 paper. 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 by Fujioka et al. (1992).
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) give the formal definition of secrecy, receipt-freeness, fairness, individual verifiability based on knowledge-based logic and analyze receipt-freeness of Fujioka et al. (1992). 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) 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 protocol Fujioka et al. (1992). Their goal is to verify these properties against a trace-based model. Groth (2004) evaluate the voting scheme based on homomorphic threshold encryption with universal composability framework. He formalizes the privacy, robustness, fairness and accuracy.
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.
| Fig. 1: | Analysis model of remote internet voting protocol with applied pi calculus |
So, in this paper we firstly review the development of the formal method on remote electronic voting protocol and then apply the automatic formal model proposed by Backes et al. (2008a) to analyze by Meng et al. (2010) protocol and its security properties including soundness and coercion-resistance. Therefore, first, Meng et al. (2010) protocol is modeled in applied pi calculus and then its analysis is performed by automatic tool ProVerif. The result shows that: Meng et al. (2010) protocol has coercion-resistance. But it has not soundness because ProVerif found an attack on soundness. Finally the improvement of Meng et al. (2010) protocol is proposed. After that the soundness of the improvement of Meng et al. (2010) protocol is modeled in applied pi calculus and automatically analyzed by ProVerif. The result we get is that the improvement of Meng et al. (2010) protocol has soundness. To our best knowledge, we are conducting the first automated analysis of Meng et al. (2010) protocol for an unbounded number of honest and corrupted voters.
Meng et al. (2010) 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. Meng et al. (2010) 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 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. 2: | Automatic verification of remote internet voting protocol |
REVIEW OF THE APPLIED PI CALCULUS
Applied pi calculus is a language for describing concurrent processes and their interactions based on Dolev-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 automatic 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), JCJ 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).
Syntax: In applied pi calculus, terms in Fig. 3 consists of names, 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.
| Fig. 3: | Terms |
| Fig. 4: | Plain process |
Typically, we let a, b and c range over channel names. Let x, y and z range
over variables and u range over variables and names. We abbreviate an arbitrary
sequence of terms M1, ..., Ml to
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.
| Fig. 5: | Extended process |
We write fu(A), fv(A) for the free variables and name in a process A, respectively. We write bu(A), bv(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[_] 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:
| Fig. 6: | Structural equivalence |
| Fig. 7: | Internal reduction |
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 ELES sometimes requires that active substitutions in the context be applied first, to yield ground terms M and N.
We write A\a when A can send a message on a, that is, when
PROVERIF
ProVerif is an automatic cryptographic protocol verifier based on a representation of the protocol by Horn clauses. 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 JCJ and Civitas that is accessible to an automated analysis using ProVerif (Backes et al., 2008a; Gerling et al., 2008).
ProVerif in Fig. 8 is for the analysis 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.(2008a ,b) model heavily rely on observational equivalences, ProVerif is the only tool for our purpose of an automated verification of Acquisti protocol and Meng et al. (2010) protocol. Inspired by works of Backes and Gerling, we use it to automatically verify Meng et al. (2010) protocol.
BACKES ET AL. (2008a,b) MODEL
This section describes Backes et al. (2008a) used to automatically verify Meng et al. (2010) 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. It mainly models 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.
| Fig. 8: | ProVerif model (Blanchet, 2008) |
| Fig. 9: | Formal definition of soundness |
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, b) model.
Soundness
Informal definition: In the paper (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, b) model formalizes the definition of soundness with the events including begin, begibvote (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(v) 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.
| Fig. 10: | Formal definition of receipt-freeness |
Formal definition: An election context S is receipt-freeness if there exists a plain process V' such that in Fig. 10:
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-resistance
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, b) 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 Vi 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 Ekc1, c2, z is an S' if and only if:
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
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 Ekc1, 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
| Fig. 11: | Formal definition of coercion-resistance |
MENG ET AL. (2010) PROTOCOL
Assumptions and model: In Meng et al. (2010) protocol when coerced by the coercer the voter wants to lie about the decrypted message to a coercer and hence, escape coercion. On one hand, the voter is able to decrypt the correct message from the registration authority, on the other hand, all the information held by the voter when opened to a coercer, do not allow this coercer to verify the encrypted message, or the coercer can not find the message is a fake message. Consequently, bribing or coercing the voter becomes useless from the very beginning.
The participants in Meng et al. (2010) protocol consist of the voters, registration authority, tallying authority, bulletin board that is a public broadcast channel with memory where a party may write information that any party may read. As usual, the registration authority and tallying authority can be beyond the reach of any coercer by introducing threshold encryption while the voter is possibly coerced or bribed.
The briber can bribe the voter and voter want to provide the evidence to prove that he vote a special ballot according to requirement of the briber. The briber has the ability to monitor the communication channels. The briber is a passive attacker.
The coercer has the power to approach the voter coercing him to reveal the decrypted message, the decryption key and all the parameters he used during decryption.
| Fig. 12: | The idea of Meng et al. (2010) protocol |
In our proposed protocol, we assume that the coercer has the ability to eavesdrop all the communication channels.
In Meng et al. (2010) protocol it also assumes that the channel between the voter and registration authority and the voter and bulletin board are tappable channel. That is mean everyone including briber and coercer can get the content on the channel.
The idea of Meng et al. (2010) protocol in Fig. 12 with receipt-freeness and coercion-resistance is that: if everyone knows that the voter has the ability that generates the fake credential and the ballot, when the voter provides the evidence to the vote-buyer or briber or coercer, they has not the ability to found that it is the fake evidence which is also be verified by the vote-buyer, so the vote-buyer does not give the money to the voter. At the same time the voter can escape the coercion. In Meng et al. (2010) protocol MW deniable encryption which can be used against revealing information that the owner of the information may decrypt it in an alternative way to a different plaintext. Namely if this user opens all his inputs including the claimed encrypted message to a coercer, the coercer fails to prove the validity or invalidity of the opened message (Meng and Wang, 2010) and BCP commitment scheme which is collision-resistance: unless one knows the trapdoor, it is infeasible to find two inputs that map to the same value. On the other hand, knowledge of the trapdoor suffices to find collisions easily (Bresson et al., 2003) are mainly used to implement the ability. At the same time it also used ElGamal cryptosystem, threshold ElGamal cryptosystem, 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).
Meng et al. (2010) protocol includes four phases: preparation phase, registration phase, voting phase and tallying phase. The structure of message is described in Fig. 13.
Preparation phase: The registration authority AR chooses
a random element
| Fig. 13: | The structure of message |
Because everyone can know the public key BCPPUR = (N, g, h) of registration authority AR, the voter Vj can get the registration authority AR’ private key BCP PRj = athrough the knowledge of h = ga mod N2 and N = pxq. Finally the registration authority AR generates his public key and private key EIGPUR, EIGPRR based on ElGamal cryptosystem registration authority AR generates the ballot Bt and send Bt and its digital signature to bulletin board denoted by BB. Tallying authority AT generates his public key BCPPUT = (N, h) and private key BCPPRT = (p, q) according to BCP commitment scheme.
Registration phase: Voter Vj generates Identifj and EIGPRj(Identifj)||EIGPUj||Identifj, then sends it to registration authority AR. Registration authority AR receives the message and uses its private key to verify the digital signature. Registration authority AR checks Identifj that whether he has registered or not. If he has registered, registration authority AR sends the error message to Vj. The protocol ends. If he has not registered, registration authority AR produces [EIGPRR{(∂, γ)||B = C (r, Cj)}||(∂, γ)||B = C(r, CJ)] according to requirements of MW deniable encryption scheme, then send it to the voter by tappable channel. Finally, registration authority AR sends EIGPRR (EIGPUR(Cj))||EIGPUR(Cj) to bulletin board.
Voting phase: Voter Vj chooses his favor ballot. Using tallying authority AT’ public key BCPPUT = (N, h) voter Vj generates BC = C(r1, Cj)||BB = C(r1, Bt) with BCP commitment scheme and sends it to randomly in bulletin board by a tappable channel.
Tallying phase: Firstly according to the rules the tallying authority eliminates the duplicate BC = C(r1, Cj)||BB = C(r1,Bt), then mixing authority mixes BC = C(r1, Cj)||BB = C(r, Cj) and get the corresponding results are Φ[BC = C(r1, Cj)]||Φ[BB = C(r1, BT)]. After that tallying authority AT decrypts Φ[BC = C(r1, Cj)||BB = C(r1, Bt)] and gets Cj and Bt. At the same time tallying authority AT verifies EIGPRR (EIGPUR(Cj))||EIGPUR (Cj) and let registration authority AR decrypt EIGPUR(Cj) and gets Cj. Finally tallying authority AT tallies the ballot and publishes the results.
MODELING MENG ET AL 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 Meng et al 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 Meng et al. (2010) protocol.
ElGamal cryptosystem is modeled with decryption algorithm ELG_dec(x, PR) and encryption algorithm ELG_enc(x, PK, r). ELG_dec(x, PR) decrypt the ciphertext x with private key PR.ELG_enc(x, PK, r) encrypt the plain text x with public key PK and random number r. BCP encryption scheme is expressed by decryption algorithm BCP_dec(x, PR) and encryption algorithm BCP_enc(x, PK). BCP_dec(x, PR) decrypt the ciphertext x with private key PR.BCP_enc(x, PK) encrypt the plaintext x with public key PK.
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 sng(x, PR) sign the message x with private key PR and the verification algorithm checksign (y, PK, x) verify the digital signature y with public key PK and the message x. PK(x, r) is the algorithm of generating the public key of cryptosystem r with the random number x. PR(x, r) is the algorithm of generating the private key of cryptosystem r with the random number x. BCP_com(x, y) is Meng and Wang deniable encryption scheme which is the arguments: private part x and public part y.
| Fig. 14: | Functions |
| Fig. 15: | Equational theory |
Public (x) is open trapdoor commitment algorithm that extract the public part x. Private(x) is open trapdoor commitment algorithm that extract the private part x. equals(x, y) checks whether x is equal to y or not.
Processes: The complete formal model of Meng et al. (2010) protocol in applied pi calculus is given in figures below. Figure 16 to 21 report the basic process include main process, voter process, corrupted voter process, registration authority process, identity issuer authority process and tallying authority process forming our of the model of Meng et al. (2010) protocol. Figure 22 to 28 offers additional and modified processes for the analysis of coercion-resistance.
The main process in Fig. 16 sets up private channels chVR; chVII; chIIR; chTR and specifies how the processes are combined in parallel. chVR is the private channel between voter and registration authority. chVII is the private channel between voter and identity issuer authority. chIIR is the private channel between registration authority and identity issuer authority. chTR is the private channel between registration authority and tallying authority. At the same time the main process generates the key parameters voter for voter, reg for registration authority, tal for tallying authority.
Voter process is modeled in applied pi calculus in Fig. 17. Each voter gets the credential id from identity issuer authority and then sends it to registration authority. After that registration authority generate the ciphertext of the genius credential Bc according to Meng and Wang deniable encryption scheme and sent it to voter. Voter verifies Bc with checksign (signed, ELG_PK_Tal). If the result is true then voter open Bc with his private key BCP_PR_voter in BCP cryptosystem. Voter chooses his favorite ballot vote and generates ciphertext BCP_enc((r1, cred), BCP_PK_Tal) of credential cred with public key BCP_PK_Tal of tallying authority. He also generates ciphertext BCP_enc((r2, vote), BCP_PK_Tal) of ballot vote with public key BCP_P_Tal of tallying authority. Finally voter sends BCP_enc((r1,cred), BCP_PK_Tal) and BCP_enc((r2, vote), BCP_PK_Tal) through public channel com to bulletin board.
| Fig. 16: | Main process |
| Fig. 17: | Voter process |
| Fig. 18: | Corrupted voter process |
Corrupted voters process is modeled in Fig. 18. The corrupted voter will register and get his secret credentials id from identity issuer authority and then sends it to registration authority. After that registration authority generate the ciphertext of the genius credential Bc according to Meng and Wang deniable encryption scheme and sent it to voter. Voter verifies Bc with checksign(signed, ELG_PK_Reg, (alphabet, Bc)). If the result is true then voter open Bc with his private key BCP_PR_voter in BCP cryptosystem, sends credentials cred on a public channel, so that the attacker can impersonate them in order to mount any sort of attack.
The registration authority process is modeled in Fig. 19. The registration authority receives voters id and then generates the secret credentials cred. After that the registration authority creates ELG_enc((r1, r2), ELG_PK_voter, r4) and BCP_enc((r2, cred), BCP_PK_voter) according to Meng and Wang deniable encryption scheme. He creates the digital signature sign ((alphabet, Bc), ELG_PR_Reg) of ELG_enc((r1, r2), ELG_PK_voter, r4) and BCP_enc((r2, cred), BCP_PK_voter) and sends it to voter by channel chVR from voter to registration authority. The registration authority generates the ciphertext ELG_enc(cred, ELG_PK_reg, r3) of credential cred and sends it to bulletin board through public channel pub.
| Fig. 19: | Registration authority process |
| Fig. 20: | Identity issue authority process |
He also decrypts ciphertext ELG of credential with his private key ELG_PR_reg and gets credential and sent it to tallying authority through channel chTR from tallying authority to registration authority.
The identity issue authority is modeled in Fig. 20. The identity issuer authority generates id and sends it to voter and tallying authority. He also publish id bulletin board in through the channel pub.
Tallying authority process is modeled in Fig. 21. After the voting time expires, the tallying authority gets the all ballots on bulletin board posted by allegedly eligible voters and then decrypt Bc and Bb with his private key BCP_PR_Tal to get cred and vote. Tallying authority get ciphertext ELG_ec(cred, ELG_PK_Reg, r3) of the voter’s credential and verify checksign(signed, ELG_PK_reg, enccred) the digital signature enccred. If the result is true then he sends enccred to registration authority. Registration authority decrypt enccred with his private key to recover plaintext cred1 which is the credential. Finally tallying authority compares it with cred, if it is true, he publish the tallying result vote on bulletin board.
According to the definition coerced resistance of Backes et al. (2008a) in order to analyze coercion resistance of Meng et al. (2010) protocol, the processes including cheating voter process, coerced voter process, modified tallying authority process, abstained voter process, extractor process, coercion-resistance process 1 of Meng et al. (2010) protocol and coercion-resistance process 2 of Meng et al. (2010) protocol, are needed.
| Fig. 21: | Tallying authority process |
| Fig. 22: | Cheating voter process |
The faking strategy of the cheating voter consists of generating a fake credential and sending it to the coercer. The registration authority generates the fake credential fake and genius credential cred and sends it to the cheating voter in Fig. 22. The cheating voter constructs a valid proof that causes this fake share to appear real to the coercer. In Fig. 23 the coerced voter sends his genuine cred to coercer and abstained.
In Fig. 24 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. 21 and modified tallying authority process is that the tallying authority process in Fig. 21 does not publish the credentials and vote to the extractor process. In Fig. 25 the abstained voter receives the related information and give up his vote. The extractor process in Fig. 26 can identify this fake ballot as being a coerced vote.
| Fig. 23: | Coerced voter process |
| Fig. 24: | Modified tallying authority process |
| Fig. 25: | Abstained voter process |
Notice, that the modified tallying authority process in Fig. 24 shares a private channel chTE with the extractor a private channel chVE with voter. The coercion-resistance process1 of Meng et al. (2010) protocol in Fig. 27 and coercion-resistance process 2 of Meng et al. (2010) protocol in Fig. 28 need to be observationally equivalent in order to satisfy the definition coercion resistance of Backes et al. (2008a) and to be able to automatically verify this property of the protocol.
AUTOMATIC VERIFICATION OF Meng et al. (2010) PROTOCOL WITH PROVERIF
ProVerif can take two formats as input. The first one is in the form of Horn clauses (logic programming rules).
| Fig. 26: | Extractor process |
| Fig. 27: | Coercion-resistance process1 of Meng et al.protocol |
| Fig. 28: | Coercion-resistance process2 of Meng et al.protocol |
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 Meng et al. (2010) 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).
Firstly the soundness of Meng et al. (2010) protocol is proved by ProVerif. In order to prove the soundness property, according to the definition of Backes et al. 2008a), the soundness consists of inalterability (condition 1a), elegibility (condition 1b) and non-reusability (condition 1a and condition 2). Figure 29-37 gives the inputs in extension of the pi calculus (Abadi and Blanchet, 2005) of verification of soundness in ProVerif.
| Fig. 29: | Functions |
| Fig. 30: | Equation |
| Fig. 31: | Soundness-vote chooser |
The analysis was performed by ProVerif and the result is showed in Fig. 38. In Fig. 31:
| Fig. 32: | Soundness-voter |
| Fig. 33: | Soundness-corrupted voter |
| Fig. 34: | Soundness-tallying authority |
| Fig. 35: | Soundness-registration authority |
| Fig. 36: | Soundness-issuer authority |
means that if event ENDVOTE(x) occurs then event:
must have been occurs. As a result, Meng et al. (2010) protocol is not proved to guarantee inalterability for an unbounded number of honest voters and an unbounded number of corrupted participants.
ProvVeif found an attack on Meng et al. (2010) protocol in Fig. 38. The attack is that in voting phrase the attacker can intercept the message BC = C(r1, Cj)||BB = C (r1, Bt) and can instead BB = C(r1, Bt) with the ballot BB = C(r', B') he chooses and then attacker send the message BC = C(r1, Cj)||BB = C(r', B') to the bulletin board. After the time expired tallying authority can tally the ballot and publish the results. The attack makes Meng et al. (2010) protocol that it has not inalterability.
In order to deal with the attack on inalterability we can use the message BC = C(r1, Cj)||BB = C(r1, Bt) or ELG_enc((BC = C(r1, Cj)||BB = C(r1, Bt)), ELG_PK_Tal) to instead the message BC = C(r1, Cj)||BB = C(r1, Bt) in voting phrase. Thus Meng et al. (2010) protocol is proved to guarantee inalterability, legibility and non-reusability for an unbounded number of honest voters and an unbounded number o f corrupted participants. Figure 29-31, 33-37, 39 gives the inputs in extension of the pi calculus (Abadi and Blanchet, 2005) of verification of soundness in ProVerif. The result is showed in Fig. 40.
The proof of coercion-resistance in Meng et al. (2010) protocol is also finished by ProVerif. According to definition of coercion resistance in Backes et al. (2008a),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. 37: | Soundness process |
| Fig. 38: | The result of soundness |
Condition 2 which is the most intricate condition describes the special observational equivalence between:
and
| Fig. 39: | Soundness-voter of the improvement of Meng et al. protocol |
| Fig. 40: | The result of soundness of the improvement of Meng et al. protocol |
In
| Fig. 41: | Coercion-resistance-condition2- vote chooser |
| Fig. 42: | Coercion-resistance-condition2- voter |
| Fig. 43: | Coercion-resistance-condition2- corrupted voter |
| Fig. 44: | Coercion-resistance-condition2- voter registration |
In Fig. 54 Bad is not derivable shows that observational equivalence is true.
Condition 3 describes the scenario that if the cheated coercer abstains, then
the extractor needs to abstain as well. The observational equivalence between
| Fig. 45: | Coercion-resistance-condition2-coerced voter |
Figure 29, 30, 41-43, 47-49, 51, 52, 55-59 give the inputs in extension of the pi calculus (Abadi and Blanchet, 2005) of verification of Condition 3 in ProVerif. The result in Fig. 60 shows that the observational equivalence between:
| Fig. 46: | Coercion-resistance-condition2-voter cast |
| Fig. 47: | Coercion-resistance-condition2-tallying authority |
and S[Vt (v')|Vjabs|Vkabs] is true. In Fig. 60 Bad is not derivable shows that observational equivalence is true.
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 29, 30, 41-43, 47-49, 51, 52, 61-64 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. 66 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 Extractor: votes with invalid registration secrets are silently discarded by the tallying authority.
| Fig. 48: | Coercion-resistance-condition2-registration authority |
| Fig. 49: | Coercion-resistance-condition2-identity issue authority |
| Fig. 50: | Coercion-resistance-condition2-extractor |
| Fig. 51: | Coercion-resistance-condition2-modified-tallying authority |
| Fig. 52: | Coercion-resistance-condition2-modified-registration authority |
| Fig. 53: | Coercion-resistance-condition2-process |
| Fig. 54: | The result of coercion-resistance-condition2 |
| Fig. 55: | Coercion-resistance-condition3-voter registration |
| Fig. 56: | Coercion-resistance-condition3-coerced voter |
| Fig. 57: | Coercion-resistance-condition3-voter casting |
| Fig. 58: | Coercion-resistance-condition3-extractor |
| Fig. 59: | Coercion-resistance-condition3-process |
| Fig. 60: | The result of coercion-resistance-condition3 |
| Fig. 61: | Coercion-resistance-condition4-voter registration |
| Fig. 62: | Coercion-resistance-condition4-coerced voter |
| Fig. 63: | Coercion-resistance-condition4-voter casting |
| Fig. 64: | Coercion-resistance-condition4-extractor |
If this was not the case a coercer could easily distinguish real from fake registration secrets. The observational equivalence between S[Viinv-reg] and vcvotes (!cvotes(x))|S[Vi(v)] is proved in ProVerif. Figure 29, 30, 41-43, 48, 67-69 give the inputs in extension of the pi calculus (Abadi and Blanchet, 2005) of verification of Condition 2 in ProVerif. The result in Fig. 70 shows that the observational equivalence is true. Bad is not derivable shows that observational equivalence is true.
According to the above verification we can conclude that Meng et al. (2010) protocol has coercion resistance.
| Fig. 65: | Coercion-resistance-condition4-process |
| Fig. 66: | The result of coercion-resistance-condition4 |
| Fig. 67: | Coercion-resistance-condition5-voter choice |
| Fig. 68: | Coercion-resistance-condition5-tallying authority |
| Fig. 69: | Coercion-resistance-condition5-process l |
| Fig. 70: | The result of coercion-resistance-condition5 |
CONCLUSION AND FUTURE WORK
Internet voting protocol play an important role in remote voting system. Meng et al. (2010) protocol is the famous typically remote internet 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 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) Meng et al. (2010) protocol can be analyzed with automatic tool ProVerif. In this paper Meng et al. (2010) protocol is modeled in applied pi calculus. Soundness and coercion resistance are verified with ProVerif. The result shows that Meng et al. (2010) protocol has coercion resistance. But it has not soundness because ProVerif found an attack on soundness. Then the improvement of Meng et al. (2010) protocol is proposed. After that the soundness of the improvement of Meng et al. (2010) protocol is modeled in applied pi calculus and automatically analyzed by ProVerif. The result we get is that the improvement of Meng et al. (2010) protocol has soundness. To our best knowledge, the first automated analysis of Meng et al. (2010) protocol for an unbounded number of honest and corrupted voters is finished.
As future work, we plan to analyze other remote internet voting protocols, such as Meng (2009a, d) recently proposed and the protocol claimed that has the soundness, receipt-freeness and coercion-resistance with weak physical assumption. It would also be interesting to formalize the security properties in wireless communication protocol in the formal model with automatic tool ProVerif.
ACKNOWLEDGMENT
This study was supported in part by Natural Science Foundation of South-Center University for Nationalities under the grants: YZZ06026.