Research Article
 

Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif



Bo Meng
 
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail
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.

Services
Related Articles in ASCI
Search in Google Scholar
View Citation
Report Citation

 
  How to cite this article:

Bo Meng , 2011. Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif. Information Technology Journal, 10: 293-334.

DOI: 10.3923/itj.2011.293.334

URL: https://scialert.net/abstract/?doi=itj.2011.293.334
 
Received: August 29, 2010; Accepted: October 01, 2010; Published: November 12, 2010



INTRODUCTION

With the development of Internet and information technology, electronic government has got serious attention from enterprise and academic world. Owning to advantages of remote internet voting, it plays an important role in electronic government. In order to assess its security and increase confidence of the voters in remote internet voting system and protocols, many researchers have pay attention to design and verification on secure remote internet voting systems and protocols. Remote internet voting protocol is a key part of internet voting system. So how to develop and verify a practical secure internet voting protocol is a challenging issue (Abadi and Gordon, 1999).

The practical secure remote internet voting protocol should include the basic and expanded properties. Basic properties include privacy, completeness, soundness (Abadi and Fournet, 2001), fairness and invariableness. Expanded properties include universal verifiability (Sako and Killian, 1995), receipt-freeness (Benaloh and Tuinstra, 1994 ) and coercion-resistance (Juels and Jakobsson, 2002). Recently research focus on implementation and formal analysis of receipt-freeness and coercion-resistance.

Soundness is typically consists of inalterability, eligibility and unreusability (Backes et al., 2008a). Universal verifiability describes that any one can verify the fact that the election is fair and the published tally is correctly computed from the ballots that were correctly cast (Sako and Killian, 1995). Receipt-freeness is to protect against vote buying (Benaloh and Tuinstra, 1994). The voter can not produce a receipt to prove that he votes a special ballot. Coercion resistance means that it should offer not only receipt-freeness, but also defense against randomization, forced-abstention and simulation attacks (Juels and Jakobsson, 2002).

In the last twenty years many remote internet voting protocols (Benaloh and Tuinstra, 1994; Magkos et al., 2001; Juels and Jakobsson, 2002; Acquisti, 2004; Chaum, 2004; Juels et al., 2005; Chaum et al., 2005; Rivest, 2006; Cichon et al., 2008; Clarkson et al., 2008; Meng, 2007a, 2009a, c, d; Meng et al., 2010a-c; Meng and Wang, 2010), claimed on their security, have be proposed. In order to assess and verify security properties of remote internet voting protocol there are two model can be used: one is formal model (or Dolev-Yao, symbolic model) in which cryptographic primitives are ideally abstracted as black boxes, the other is computational model (or cryptographic model) based on complexity and probability theory. Firstly each model formally defines security properties expected from security protocol and then develop methods for strictly proving that given security protocols satisfy these requirements in adversarial environments. Computational model is complicated and is difficult to get the support of mechanized proof tools. In contrast, symbolic model is considerably simpler than the computational model, proofs are therefore also simpler and can sometimes benefit from mechanized proof tools support. For example: SMV (McMillan, 1992; Mei et al., 2009), NRL (Meadows, 1996), Casper (Lowe, 1998), Isabelle (Paulson, 1998), Athena (Song, 1999), Revere (Kindred, 1999), SPIN (Maggi and Sisto, 2002), Brutus (Clarke et al., 2000), ProVerif (Blanchet, 2001), Scyther (Joseph and Cremers, 2006).

ProVerif (Blanchet, 2001) is an mechanized proof of cryptographic protocol verifier based on a representation of the protocol by Horn clauses or applied PI calculus. It can handle many different cryptographic primitives, including shared- and public-key encryption and signatures, hash functions and Deffie-Hellman key agreements, specified both as rewrite rules and as equations. It can also deal with an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space. When ProVerif cannot prove a property, it can reconstruct an attack, that is, an execution trace of the protocol that falsifies the desired property. This verifier can prove the following properties: secrecy, authentication and more generally correspondence properties, strong secrecy, equivalences between processes that differ only by terms. ProVerif has been tested on protocols of the literature with very great results
(http://www.proverif.ens.fr/proverif-users.html).

Acquisti (2004) protocol is one of the most important remote internet voting protocols that claims to satisfy formal definitions of key properties, such as soundness, individual verifiability, as well as receipt-freeness and coercion resistance without strong physical constrains. In their study, analysis of security properties of Acquisti protocol is done by hand, this method depend on experts knowledge and skill and is prone to make mistakes, so here we use mechanized proof tool ProVerif to verify security properties of Acquisti protocol.

The main contributions of this study are summarized as follows:

Review the formal analysis of security properties in electronic voting protocol. Many formal models have been proposed, but only the Bakes et al. model supports the mechanized proof tool. The formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistance which are important properties. Until now the security analysis model based on computational model have not been proposed
Apply the mechanized formal model proposed by Backes et al. (2008a) for mechanized proof of Acquisti protocol and its security properties. Therefore, Acquisti protocol is modeled in applied PI calculus and the soundness and coercion-resistance take into account. The proof itself is performed by mechanized proof tool ProVerif developed by Blanchet (2001)
The result we obtain is that Acquisti protocol has coercion-resistance in some conditions. At the same time it also has the soundness. To our best knowledge, we are conducting the first mechanized proof of Acquisti protocol for an unbounded number of honest and corrupted voters

Formal methods are an important tool for designing and implementing secure cryptographic protocol. By applying techniques concerned with the construction and analysis of models and proving that certain properties hold in the context of these models, formal methods can significantly increase one’s confidence that a protocol will meet its requirements in the real world.

The development of formal methods has started in 1980s (Yao, 1982; DeMillo et al., 1982; Dolev and Yao, 1983; Merritt, 1983; Blum and Micali, 1984; Hoare, 1985; Burrows et al., 1989, 1990). This field matured considerably in the 1990s. Some of the methods rely on rigorous but informal frameworks, sometimes supporting sophisticated complexity-theoretic definitions and arguments. Others rely on formalisms specially tailored for this task. Yet others are based on Mur (Mitchell et al., 1997) strand space (Thayer et al., 1998), SPI calculus (Abadi and Gordon, 1999) Kessler and Neumann logic (Kessler and Neumann, 1998) applied PI calculus (Abadi and Fournet, 2001).

Owning to the abstraction ideally of cryptography, formal methods are often quite effective; a fairly abstract view of cryptography often suffices in the design, implementation and analysis of security protocols. Formal methods enable relatively simple reasoning and also benefit from substantial work on proof methods and from extensive tool support, for example, SMV (McMillan, 1992), NRL (Meadows, 1996), Casper (Lowe, 1998), Isabelle (Paulson, 1998), Athena (Song, 1999), Revere (Kindred, 1999), SPIN (Maggi and Sisto, 2002), Brutus (Clarke et al., 2000), ProVerif (Blanchet, 2001), Scyther (Joseph and Cremers, 2006).

Delaune et al. (2006a) have done a path breaking work on the formal definition of receipt-freeness and coercion-resistance in applied PI calculus. Their formal model is based on Dolev-Yao model. They formalize receipt-freeness as an observational equivalence. The idea is that if the attacker can not find if arbitrary honest voters VA and VB exchange their votes, then in general he can not know anything about how VA (or VB) voted. This definition is robust even in situations where the result of the election is such that the votes of VA and VB are necessarily revealed. They also assume that the voter cooperates with the coercer by sharing secrets, but the coercer cannot interact with the voter to give her some prepared messages. They use adaptive simulation to formalize coercion-resistance. The ideas of this definition is that whenever the coercer requests a given vote then VB can change his vote and counterbalance the outcome. However, avoid the case where V' = VA {c/v}c1,c2 letting VB vote α is needed. Therefore, requirement that when we apply a context C, intuitively the coercer, requesting VA {c/v}c1,c2 to vote c, V' in the same context votes α. There may be circumstances where V' may need not to cast a vote that is not. In the case of coercion-resistance, the coercer is assumed to communicate with voter during the protocol and can prepare messages which she should send during the election process. Their formal definition of coercion-resistance base on the informal definition: a voter cannot cooperate with a coercer to prove to him that she voted in a certain way. Lee et al. (2003) protocol is analyzed with their formal model. Meng (2008) also apply their formal model to analyze the protocol (Meng, 2007a). Delaune et al. (2005) model receipt-freeness and analyze Lee et al. (2003) protocol. Delaune et al. (2006b) use applied PI calculus to model fairness, eligibility, privacy, receipt-freeness and coercion-resistance and analyze the protocols (Fujioka et al., 1992; Lee et al., 2003). Backes et al. (2008a) point out that definitions of coercion-resistance Delaune et al. (2006a) are not amenable to automation and do not consider forced-abstention attacks and do not apply to remote voting protocols, they give an formal model of security properties of remote internet voting protocol in applied PI calculus and use the ProVerif to mechanized verify the security properties of Juels et al. (2005) protocol. Gerling et al. (2008) apply the model (Backes et al., 2008a) with ProVerif to mechanized verify Clarkson et al. (2008) protocol. Meng et al. (2010b, c) also use the Backes et al. (2008a) model to mechanized verify Acquisti (2004) protocol and Meng et al. (2010a) protocol.

Jonker and de Vink (2006) also point out that the formal model (Delaune et al., 2006a) offers little help to identify receipts when receipts are present. So Jonker and de Vink present a new formal method, which uses the process algebra, to analyze receipts based on their informal definition: a receipt r is an object that proves that a voter v cast a vote for candidate c. This means that a receipt has the following properties: (R1) receipt can only have been generated by v. (R2) receipt proves that voter chose candidate. (R3) receipt proves that voter cast her vote. Jonker and de Vink provide a generic and uniform formalism that captures a receipt. Jonker and de Vink formal model is also simpler than Delaune et al. formal model. They use the formalism to analyze the voting protocols (Benaloh and Tuinstra, 1994; Sako and Killian, 1995; Hirt and Sako, 2000; Aditya et al., 2004; Hubbers et al., 2005). Meng (2007b) analyzes receipt-freeness of the protocols (Fujioka et al., 1992; Cramer et al., 1997; Juels and Jakobsson, 2002; Acquisti, 2004) based on formalism (Jonker and de Vink, 2006).

About definition of receipt proposed by Jonker and de Vink (2006) think it is worth discussing. Firstly, about (R1) r can only have been generated by v, in some voting protocol, one part of receipt is generated by the authority, not generated by voter. Secondly, they give the following auxiliary receipt decomposition functions: a: Rcpt ?AT, which extracts the authentication term from a receipt. Authentication term should be the identification of voter. Thirdly the author does not prove the generic and uniform formalism that is right in their study. Finally they use a special notation, it difficult to use and generalize it. Hence, Meng gives a formal logic framework for receipt-freeness based on Kessler and Neumann (1998) and apply it to analyze (Fujioka et al., 1992) protocol.

Knowledge-based logics have been also used in the studies (Jonker and Pieters, 2006; Baskar et al., 2007; Van Eijck and Orzan, 2007) to formally analyze the security properties of e-voting protocol. Jonker and Pieters (2006) formalize the concept of receipt-freeness from the perspective of a anonymity approach in epistemic logic which offers, among others, the possibility to write properties allowing to reason about the knowledge of an agent a of the system with respect to a proposition p. They classify receipt-freeness into two types: weak receipt-freeness and strong receipt-freeness. Weak receipt-freeness implies that the voter cannot prove to the spy that she sent message m during the protocol, where m is the part of a message representing the vote. Here, no matter what information the voter supplies to the spy, any vote in the anonymity set is still possible. In other words, for all possible votes, the spy still suspects that the voter cast this particular vote; or: the spy is not certain she did not cast this vote. Baskar et al. (2007) gave the formal definition of secrecy, receipt-freeness, fairness, individual verifiability based on knowledge-based logic and analyze receipt-freeness of Fujioka et al. (1992) protocol. Van Eijck and Orzan (2007) use dynamic epistemic Logic to model security protocols and properties, in particular anonymity properties. They apply it to Fujioka et al. (1992) scheme and find the three phases should be strictly separated, otherwise anonymity is compromised. Mauw et al. (2007) use the process algebra to analyze the data anonymity of the voting scheme (Fujioka et al., 1992). Talbi et al. (2008) use ADM logic to specify security properties (fairness, eligibility, individual verifiability and universal verifiability) and analyze Fujioka et al. (1992) protocol. Their goal is to verify these properties against a trace-based model. Groth (2004) evaluated the voting scheme based on homomorphic threshold encryption with universal composability framework. He formalizes the privacy, robustness, fairness and accuracy.

The formal methods used in formal models of soundness, receipt-freeness and coercion-resistance are presented in Table 1. We can found in Table 1 until now only the Bakes et al. model supports the mechanized proof tool. The security properties formally modeled is presented in Table 2. The formally analyzing security properties in the Internet voting protocol is described in Table 3. From Table 1-3 we can get that the formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistacne that are important properties.


Table 1: The formal methods used in formal models of soundness, receipt-freeness and coercion-resistance
Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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
Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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
Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 1: Analysis model of remote internet voting protocol with applied PI calculus


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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 Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif 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 Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 3: Terms


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 4: Plain process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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 Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif is a sequence of name restrictions vn1,...,vn1. 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 Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif for the input of terms M1,...,M1. 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 Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif is the abbreviation for the output of terms N1,...,N1. 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 Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif 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 writeImage for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif |-M = N for equality within the equational theory Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif andImage for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif |-/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. ALIAS enables the introduction of an arbitrary active substitution. SUBST describes the application of an active substitution to a process that is in contact with it. Rewrite deals with equational rewriting.

Internal reduction (→) relies on the equational theory and defines the semantics of process conditionals as well as input and output. Internal reduction in Fig. 7 is the smallest relation on extended processes closed by structural equivalence and application of evaluation contexts such that:

THEN and ELSE directly depend on the underlying equational theory; using ELSE sometimes requires that active substitutions in the context be applied first, to yield ground terms M and N.

We write Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif when A can send a message on a, that is, when Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif 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:


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 6: Structural equivalence


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 7: Internal reduction

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

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.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 9: Formal definition of soundness


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 10: Formal definition of receipt-freeness

Condition 1 models that the voter V' does not only vote v' as a regular voter, but additionally uses Vfake to generate fake secrets, casts an extra vote using them and provides a receipt of this invalid voting. Condition 2 deal with that an additional voter k that votes with fake registration secrets in case the voter i complies with the request of the coercer and simply abstains if i cheats the vote buyer by casting a vote with fake secrets.

Coercion-resistances:

Informal definition: A coercion-resistant voting protocol should offer not only receipt-freeness, but also defense against randomization, forced-abstention and simulation attacks
Receipt-freeness: The voter can not produce a receipt to prove that he votes a special ballot
Immunity to randomization attack: The idea is for an attacker to coerce a voter by requiring that she submit randomly composed balloting material. The effect of the attack is to nullify the choice of the voter
Immunity to forced-abstention attack: This is an attack related to the previous one based on randomization. In this case, the attacker coerces a voter by demanding that she refrain from voting
Immunity to simulation attack: An attacker coerce voters into divulging private keys or buying private keys from voters and then simulating these voters at will, i.e., voting on their behalf

The formalization that encompasses all properties except randomization attacks depicted below is taken from Backes et al. (2008a) model.

In order to formalize coercion-resistance, the process called Extractor is introduced. Extractor plays an important role in formalization of coercion-resistance, which extracts the vote the coercer casts on behalf of Extractor and tallies it directly. Extractor depends on the construction of the particular electronic voting protocol and has to be provided by the user.

Definition of Extractor: A context Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif is an Extractor if and only if:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

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:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

can tally at most one vote.

Formal definition: An election context S guarantees coercion-resistance if there exist channels c, c1 and c2, a sequential process Vfake, an Extractor Ec1,c2,z and an election context S', such that in Fig. 11

In condition 1 (hypothesis) a modified election context s' is used that only differs from s in that the tallying authority additionally outputs messages on the channel c2 shared with Extractor. In condition 2 the left side process contains the voter Vi that is in accordance with the orders of the coercer, running in parallel with the voter Vj casting a vote v' and the process Ec1,c2,z[0], that is intuitively equivalent to a voter nullifying her vote. In the right side election process the voter Vi cheats the coercer by providing him with fake registration secrets and then votes v', the voter Vj participates in the registration phase and then abstains and the extractor process:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

tallies the vote the coercer casts on behalf of vi. In condition 3 if the cheated coercer abstains, then the Extractor needs to abstain as well; In condition 4 if the cheated coercer casts a valid vote using the fake registration secrets he received from vi, the Extractor needs to tally precisely this vote.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 13: The structure of message of Acquisti protocol

In voting phase the voter vote his favor ballot and post it to bulletin board. Each voter multiplies the shares she has received from issuer authority together with the encrypted shares of the ballot. Because of the homomorphic properties of Paillier cryptosystems, the resulting ciphertext includes the sum of those shares and the ballot’s shares. The resulting ciphertext is sent to the bulletin board. In the last phase, tallying phase, the tallying authority tallies the ballot and publishes the result in bulletin board. The structure of message is described in Fig. 13.

Preparation phase: Every issue authority Ai(i = 1......l) creates l random numbers c as ci,j, representing shares of credentials, for each eligible voter veterj(l = 1......l). For each ci,j, Ai performs two operations: first, it encrypts ci,j using PKC and appropriate secret randomization, signs the resulting ciphertext with SKiC and publishes it on bulletin board on a row publicly reserved for the shares of credential of voter:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

SKAi represents the signature of authority Ai Second, Ai also encrypts ci,j using PKV and appropriate secret randomization, without signing it, but attaching to it a designated verifier proof DVPvj of equality of plaintexts EC(ci,j) and EV(ci,j). The proof is designated to be verifiable only by voterj. Ai encrypts this second message with voterj’s public key and sends it:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

Evoterj represents RSA encryption under voterj’s public key.

Voting phase: For each encrypted share of credential she receives, voterj verifies the designated verifier proof of equality between EV(ci,j) and the corresponding EV(ci,j) that has been signed and published in her reserved area of bulletin board. Upon successful verification, she multiplies together the shares EV(ci,j).

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

Cj is the sum of the various shares of credentials. voterj. Voter chooses the ballot shares Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif, generates:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and sends Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverifto 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.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 14: Functions


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 15:

Equational theory

The digital signature is modeled as being signature with message recovery, i.e., the signature itself contains the signed message which can be extracted using the function. The digital signature algorithm includes the generation signature algorithm sign(x, PR) sign the message x with private key PR and the verification algorithm verifysign(x, PU) verify the digital signature x with public key PU. decsign(x, PU) recover the message from the digital signature x with public key PU. The probabilistic threshold public key share decryption algorithm TpPKsubdec(xi, Pri, VKi) decrypt the secret share xi with private key PRi and verification key VKi. The probabilistic threshold combining algorithm TpPKdec(x1,...,x2) recovers x from x1,...,x2. The deterministic threshold public key share decryption algorithm TPKsubdec(xi, PRi, VKi) decrypt the secret share xi with private key PRi and verification key VKi. The deterministic threshold combining algorithm TPKdec(x1,...,x2) means that recover x from x1,...,x2. The projection function projectioni(x) generated the ith share from the formatted message x. The self blinding function SelfBlinding(x,r) blinds message x with r. The add function add(x,y) add x and y. checkciphertext(x1,x2) verify the two ciphertext x1 and x2 generated with the same plaintext. SK(x) PK(x) VK(x) generated the secret key, public key and verification key of x. equals(x,y) checks whether x is equal to y or not.

The basic equational theory is described in Fig. 15. The threshold decryption and combining algorithm are introduced.

The equational theory also contains and equational rules for abstractly reasoning about the knowledge proof that two ciphertexts are encryption of the same plaintext which is modeled in Fig. 16 and used in the voting phase and tallying phase. In the voting phase the voter need to verify the equivalence between the encrypted share and the one the voter has received to its message are also provided to itself. In the tallying phase the tally authority need to check the two lists: a list of encrypted, mixed credentials the registration authorities themselves had originally posted on the bulletin board; and a set of encrypted, mixed sums of credentials and ballots, posted on the bulletin board by the voters. It modeled as:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

It can verify the two ciphertext, one is the ciphertext generated with the public key PUy and random number r1, the other is the ciphertext generated with the public key PUz and random number r2, are the same plaintext x1.

Designated verifier proofs modeled in Fig. 17 in the applied PI calculus (Backes et al., 2008b) is also contained in the equational theory and equational rules. During the registration phase, the voter acquires a private credential for voting. For this he contacts each of the registration authority and asks them for a share of the private credential. In order for a registration authority to prove the correctness of the share credential, a designated verifier proof is used. Designated verifier proof can convince only the voter of the correctness of the share credential and nobody else. In particular the voter should be able to generate a fake proof of this fact, e.g., using his secret key.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 16: Model of knowledge proof that two ciphertexts are encryption of the same plaintext


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 17: Model of designated verifier proofs


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 18: Main process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 19: Voter process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 20: Corrupted voter process

Processes: The complete formal model of Acquisti protocol in applied PI calculus is given in Fig. 18-23 report the basic process include main process, voter process, corrupted voter process, registration authority process, issuer authority process and tallying authority process forming our of the model of Acquisti protocol. Figure 24-29 offer additional and modified processes for the analysis of coercion-resistance.

The main process in Fig. 18 sets up private channels chVR, chRI1, chRI2 and specifies how the processes are combined in parallel. chVR is the private channel between voter and registration authority. chRI1 and chRI2 are the private channel between registration authority and issuer authority. At the same time the main process generates the key parameters c for credentials, V for vote, S for non-homomorphic cryptosystem, keyV for voter and key1 for issuer authority.


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 21: Registration authority process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 22: Issuer authority process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 23: Tallying authority process

Voter process is modeled in applied PI calculus in Fig. 19. Using Paillier encryption, each voter get the shares ciphertext kVenccred1 and kVenccred2 from registration authority, then decrypt and get the credentials venccred1, venccred2 and the designated verifier proof NZDVP1 and NZDVP2. After that the voter use CheckNZDVPp,to verify NZDVP1 and NZDVP2. The voter also use checkciphertest( ) to verify the equivalence between the encrypted share: Public1 (NZDVP1), decsign (Public2 (NZCVP1)) and the one Public1 (NZDVP2), decsign (Public2 (NZCVP2)) the voter has received to its message are also provided to itself. The voter also gets the encrypted shares vencballottt of the ballot, which she has selected from the bulletin board. He multiplies:


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 24: Cheating voter process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 25: Coerced voter process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

Because of the homomorphic properties of Paillier cryptosystems, the resulting ciphertext result includes the sum of credential shares and the ballot’s shares. The resulting ciphertext TpPKenc(result, PK(S), r) is sent to the bulletin board.

Corrupted voters process is modeled in Fig. 20. The corrupted voter will register and get his secret credentials shares kVenccred1 and kVenccred2 from registration authority, then decrypt and get the credentials venccred1, venccred2 proof of the equivalence between the encrypted share it has posted on the bulletin board and the one it will sent to the voter. NZDVP1 and NZDVP2, after that, he simply output all their registration secrets venccred1 and venccred2 on a public channel, so that the attacker can impersonate them in order to mount any sort of attack.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 26: Modified tallying authority process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 27: Abstained voter process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 28: Extractor process

The registration authority process is modeled in Fig. 21. The registration authority generate the voters id, then get the secret credentials shares cred1 and cred2. After that the registration authority creates designated verifier proof that the proof of the equivalence between the encrypted share it has posted on the bulletin board and the one it will sent to the voter NZDVP1 and NZDVP1.

The issuer authority is modeled in Fig. 22. The issuer authorities get the shares of ballot by projectioni (ballott) and send sign[pPKenc(ci(cred, PK(C), r1, SKi(C)] which is encrypted with a set of Paillier public parameters by the public channel pub.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 29:

Acquisti-coercion-resistance2 process


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 30: Acquisti-coercion-resistance2 process

Tallying authority process is modeled in Fig. 23. After the voting time expires, the tallying authorities get the all ballots on bulletin board posted by allegedly eligible voters and then mixed it by SelfBlinding(cenccred, PK(C)). The shares of credentials posted by the registration authorities are also combined and then mixed SelfBlinding(venccredvote, PK(V)). Tallying authorities thus obtain two lists: a list bcenccred of encrypted, mixed credentials the registration authorities themselves had originally posted on the bulletin board; and a set cencballott of encrypted, mixed sums of credentials and ballots, posted on the bulletin board by the voters. The two lists have been encrypted with different Paillier public parameters. Using threshold protocols for the corresponding sets of private keys, the tallying authorities decrypt the elements in each list by checkciphertext(test, bvenccredvote) and then compare them through a search algorithm and publish the tallying result on bulletin board.

According to the definition coerced-resistance of Backes et al. (2008a) in order to analyze coercion-resistance of Acquisti protocol, the processes including cheating voter process, coerced voter process, modified tallying authority process, abstained voter process, extractor process, Acquisti-coercion-resistance1 process and Acquisti-coercion-resistance2 process, are needed. The faking strategy of the cheating voter consists of generating a fake credential and sending it to the coercer. To generate the fake credential fakecred1 and fakecred2, the voter construct a valid designated verifier proof NZDVP that causes this fake share to appear real to the coercer in Fig. 24. In Fig. 25 the coerced voter sends his genuine (Public1 (NZDVP1), Public1 (NZDVP2)) and (Public1 (NZDVP1), Public1 (NZDVP2)) to the coercer.

In Fig. 26 the modified tallying authority sends the credentials and vote by chTE to the extractor process. The difference between the previous tallying authority process in Fig. 23 and modified tallying authority process is that the tallying authority process in Fig. 23 does not publish the credentials and vote. In Fig. 27 the abstained voter receives the related information and give up his vote. The extractor process in Fig. 28 can identify this fake designated verifier proof as being a coerced vote. Notice, that the modified tallying authority process in Fig. 26 shares a private channel chTE with the extractor aprivate channel chVE with voter. The processes Acquisti-coercion-resistance1 in Fig. 29 and Acquisti-coercion-resistance2 in Fig. 30 need to be observationally equivalent in order to satisfy the definition coercion resistance of Backes et al. (2008a) and to be able to mechanizedly prove this property of the protocol.

MECHANIZED PROOF OF ACQUISTI PROTOCOL WITH PROVERIF

ProVerif can take two formats as input. The first one is in the form of Horn clauses (logic programming rules) and applied PI calculus. The second one is in the form of a process in an extension of the PI calculus (Abadi and Blanchet, 2005). In both cases, the output of the system is essentially the same.

In this study we use an extension of the PI calculus as the input of ProVerif. In order to prove the soundness and coercion resistance in Acquisti protocol the applied PI calculus model are needed to be translated into the syntax of ProVerif and generated the ProVerif inputs in extension of the PI calculus (Abadi and Blanchet, 2005).

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 31: Function 1

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 32: Function 2

Firstly the soundness of Acquisti protocol is proved by ProVerif. In order to prove the soundness property, according to the definition of Backes et al. (2008a) model, the soundness consists of inalterability(condition 1a), ligibility(condition 1b) and non-reusability(condition 1a and condition 2). Figure 31-40 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of soundness in ProVerif. The analysis was performed by ProVerif and succeeded in Fig. 41. Bad is not derivable shows that observational equivalence is true. As a result, Acquisti protocol is proved to guarantee inalterability, eligibility and unbreusability for an unbounded number of honest voters and an unbounded number of corrupted participants.

The proof of coercion-resistance in Acquisti protocol is also finished by ProVerif. According to definition of coercion-resistance in Backes et al. (2008a) model, the coercion-resistance is composed of one hypothesis and four conditions. The hypothesis describes that election context S' that only differs from S in that the tallying authority additionally outputs messages on the channel c2 shared with Extractor.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 33: Equation

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 34: Soundness-vote chooser

Condition 2 describes the special observational equivalence between:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

contains the voter Vi that is in accordance with the orders of the coercer, running in parallel with the voter Vj casting

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 35: Soundness-voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 36: Soundness-corrupted voter

a vote v' and the process Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif, that is intuitively equivalent to a voter nullifying her vote. In:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

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

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

tallies the vote the coercer casts on behalf of Vi. Figure 31-33, 42-55 give the inputs in extension of the PI calculus (Abadi and Blanchet, 2005) of verification of Condition 2 in ProVerif. The result shows that the observational equivalence between:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

is satisfied in Fig. 56. Bad is not derivable shows that observational equivalence is true.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 37: Soundness-tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 38: Soundness-registration authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 39: Soundness-issuer authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 40: Soundness process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 41: The result of soundness

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 42: Coercion-resistance-condition2-additional equation

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 43: Coercion-resistance-condition2-vote chooser

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 44: Coercion-resistance-condition2-voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 45: Coercion-resistance-condition2-corrupted voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 47: Coercion-resistance-condition2-coerced voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 48: Coercion-resistance-condition2-voter cast

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 49: Coercion-resistance-condition2-tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 50: Coercion-resistance-condition2-registration authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

is true in Fig. 70. Bad is not derivable shows that observational equivalence is true.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 52: Coercion-resistance-condition2-extractor

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 53: Coercion-resistance-condition2-modified-tallying authority

In condition 4 if the cheated coercer casts a valid vote using the fake registration secrets he received from Vi, the Extractor needs to tally precisely this vote. The observational equivalence between:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

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:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

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

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 54: Coercion-resistance-condition2-modified registration authority


Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 55: Coercion-resistance-condition2-process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 56: The result of coercion-resistance-condition2

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 57: Coercion-resistance-condition3-vote chooser

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 58: Coercion-resistance-condition3-voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 59: Coercion-resistance-condition3-corrupted voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 60: Coercion-resistance-condition3-voter registration

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 61: Coercion-resistance-condition3-coerced voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 62: Coercion-resistance-condition3-voter casting

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 63: Coercion-resistance-condition3-tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 64: Coercion-resistance-condition3-registration authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 65: Coercion-resistance-condition3-issuer authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 66: Coercion-resistance-condition3-extractor

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 67: Coercion-resistance-condition3-modified tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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:

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

and

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 69: Coercion-resistance-condition3-process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 70: The result of coercion-resistance-condition3

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 71: Coercion-resistance-condition4-vote choose

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 72: Coercion-resistance-condition4-voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 73: Coercion-resistance-condition4-corrupted voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 74: Coercion-resistance-condition4-voter registration

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 75: Coercion-resistance-condition4-coerced voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 76: Coercion-resistance-condition4-voter casting

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 77: Coercion-resistance-condition4-tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 78: Coercion-resistance-condition4-registration authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 79: Coercion-resistance-condition4-issuer authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 80: Coercion-resistance-condition4-extractor

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 81: Coercion-resistance-condition4-modified tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 83: Coercion-resistance-condition4-process

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 84: The result of coercion-resistance-condition4

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 85: Coercion-resistance-condition5-vote chooser

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 86: Coercion-resistance-condition5-voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 87: Coercion-resistance-condition5-corrupted voter

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 89: Coercion-resistance-condition5-tallying authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 90: Coercion-resistance-condition5-registration authority

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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.

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
Fig. 92: The result of coercion-resistance-condition5

Image for - Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
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

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


  2. 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
    CrossRef  |  Direct Link  |  


  3. 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
    CrossRef  |  Direct Link  |  


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


  5. Acquisti, A., 2004. Receipt-free homomorphic elections and write-in voter verified ballot. CMU-ISRI-04-116, 2004, Carnegie Mellon Institute for Software Research International. http://www.heinz.cmu.edu/~acquisti/papers/acquisti-electronic_voting.pdf.


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


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


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


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


  10. 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
    CrossRef  |  Direct Link  |  


  11. 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
    CrossRef  |  Direct Link  |  


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


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


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


  15. Blum, M. and S. Micali, 1984. How to generate cryptographically strong sequences of pseudo-random bits. SIAM J. Comput., 13: 850-864.


  16. Burrows, M., M. Abadi and R. Needham, 1989. A logic of authentication. SIGOPS Operat. Syst. Rev., 23: 1-13.


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


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


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


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


  21. Chaum, D., P. Y.A. Ryan and S. Schneider, 2005. A practical voter-verifiable election scheme. Proceedings of the ESORICS, Sept. 12-14, Milan, Italy, pp: 118-139


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


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


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


  25. Delaune, S., S. Kremer and M. Ryan, 2005. Receipt-freeness: Formal definition and fault attacks. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf.


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


  27. Delaune, S., S. Kremer and M. Ryan, 2006. Verifying properties of electronic voting protocols. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf.


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


  29. Dolev, D. and A.C. Yao, 1983. On the security of public key protocols. IEEE Trans. Inform. Theor., 29: 198-208.


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


  31. Gerling, S., D. Jednoralski and X.Y. GU, 2008. Towards the verification of the civitas remote electronic voting protocol using proverif. http://www.infsec.cs.uni-sb.de/teaching/WS07/Seminar/reports/civitas-proverif.pdf.


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


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


  34. Hoare, C.A., 1985. Communicating Sequential Processes. Prentice-Hall, Inc., USA


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


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


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


  38. Jonker, H.L. and W. Pieters, 2006. Receipt-freeness as a special case of anonymity in epistemic logic. Proceedings of the IAVoSS Workshop on Trustworthy Elections, June 29-30, 2006, Cambridge, UK. http://doc.utwente.nl/65116/.


  39. Joseph, C. and F. Cremers, 2006. Scyther-semantics and verification of security protocols. http://alexandria.tue.nl/extra2/200612074.pdf.


  40. Juels, A. and M. Jakobsson, 2002. Coercion-resistant electronic elections, 2002. http://www.vote-auction.net/VOTEAUCTION/165.pdf.


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


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


  43. Kindred, D., 1999. Theory generation for security protocols. Doctoral Thesis, Carnegie Mellon University.


  44. Lee, B., C. Boyd, E. Dawson, K. Kim, J. Yang and S. Yoo, 2003. Providing receipt-freeness in mixnet-based voting protocols. http://caislab.icu.ac.kr/Paper/paper_files/2003/ICISC03/mnvoting-final-icisc20.pdf.


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


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


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


  48. 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.
    CrossRef  |  Direct Link  |  


  49. McMillan, K.L., 1992. Symbolic model checking: An approach to the state explosion problem. Ph.D. Thesis, Carnegie Mellon University.


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


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


  52. 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
    CrossRef  |  Direct Link  |  


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


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


  55. 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.
    CrossRef  |  Direct Link  |  


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


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


  58. 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.
    CrossRef  |  Direct Link  |  


  59. 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.
    CrossRef  |  Direct Link  |  


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


  61. Meng, B., W. Huang and D.J. Wang, 2010. Automatic verification of remote internet voting protocol in symbolic model. Recent Advances in Electronic Commerce and Information Technology of ISECS.


  62. 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.
    CrossRef  |  Direct Link  |  


  63. Merritt, M.J., 1983. Cryptographic protocols. Ph.D. Thesis, Georgia Institute of Technology.


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


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


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


  67. Rivest, R.L., 2006. The threeBallot voting system. http://theory.csail.mit.edu/~rivest/Rivest-TheThreeBallotVotingSystem.pdf.


  68. Sako, K. and J. Kilian, 1995. Receipt-Free Mix-Type Voting Scheme, A Practical Solution to the Implementation of a Voting Booth. In: Advances in Cryptology-EUROCRYPT `95, Guillou, L.C. and J.J. Quisquater (Eds.). Springer-Verlag, Berlin Heidelberg, pp: 393-403


  69. 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
    CrossRef  |  Direct Link  |  


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


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


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


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


©  2023 Science Alert. All Rights Reserved