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