Information Technology Journal

Year: 2008 | Volume: 7 | Issue: 8 | Page No.: 1133-1140
DOI: 10.3923/itj.2008.1133.1140

Formal Analysis of Key Properties in the Internet Voting Protocol Using Applied Pi Calculus

Bo Meng

Abstract: The internet voting protocols is the core part of the internet voting system. In order to put the internet voting protocols into practice they should have several key properties, such as privacy, completeness, soundness, unreusability, fairness, eligibility and invariableness, universal verifiability, receipt-freeness and coercion-resistance. Formal method is an important tool to assess these properties. But most of these properties are analyzed with informal method. The applied pi calculus can be used to model and verify the security protocols, such as internet voting protocol. In this study, firstly, privacy and coercion-resistance properties are researched. Then a typical internet voting protocol is modeled with applied pi calculus. Thirdly privacy and coercion-resistance of the typical internet voting protocol are analyzed with applied pi calculus. According to the result of analysis the typical internet voting protocol has privacy and coercion-resistance properties.

Keywords: formal method, Internet voting protocol, privacy and coercion-resistance

INTRODUCTION

With the popularization of Internet and advance of process of democracy of nation, a new voting system called Internet voting is introduced. The internet voting protocol is the core part of the internet voting system. The secure and practical Internet voting protocols should have basic properties: privacy, completeness, soundness, unreusability, fairness, eligibility and invariableness and expanded properties: universal verifiability, receipt-freeness (Benaloh and Tuinstra, 1994), coercion-resistance (Juels and Jakobsson, 2002; Juels et al., 2005).

Privacy describes the fact that a particular voted in a particular way is not revealed to anyone. Its purpose aims to guarantee that the link between a given voter and his vote remains hidden. Anonymity and privacy properties have been successfully studied.

However, research on privacy in the field of voting protocols is rather subtle. While generally most security properties should hold against many dishonest participants and authorities coalitions.

To ensure privacy we need to hide the link between the voter and the vote and not the voter or the vote itself. Coercion-resistance is introduced by Juels and Jakobsson (2002) and should offers not only receipt-free, but also defense against randomization, forced-abstention and simulation attacks.

Research on coercion-resistance is at the beginning. It is firstly researched by Juels and Jakobsson (2002) and Acquisti (2004), which mainly applied the credential of voter and designated verifier proof to accomplish it. Voter can cheat the coercer by producing a false credential. Owning to designate verifier proof the coercer cannot verify the proof.

Recently internet voting protocols (Acquisti, 2004; Juels et al., 2005; Meng, 2007) were proposed without the strong physical assumptions. Meng (2007) is the improvement of the protocols (Acquisti, 2004; Juels et al., 2005) which applies the idea and addresses the problems of protocols (Acquisti, 2004; Juels et al., 2005).

Meng protocol is a practical and efficient internet voting protocol and doesn’t use strong physical assumptions in the implementation of these properties. This is the trend of advance in Internet voting protocol. But Meng (2007) does not analyze privacy and coercion-resistance with formal methods.

Formal method is the key tool to assess properties of internet voting protocols. Many universal formal methods have been proposed to analyze security protocols. Owning to specialties of internet voting protocol, Delaune (2006) introduced a formal model for analyzing privacy, receipt-freeness and coercion-resistance of internet voting protocol. Kremer and Ryan (2005) have used the applied pi calculus to analyze the protocol (Fujioka et al., 1992). Lee et al. (2004) protocol is analyzed by Ryan et al. (2006) with applied pi calculus.

The purpose of the study is to use DKR model (Delaune et al., 2006) to analyze privacy and coercion-resistance in Meng protocol.

PRIVACY AND COERCION-RESISTANCE IN DKR MODEL

In DKR model, it uses the applied pi calculus to formalize the privacy and coercion-resistance of internet voting protocol. Privacy is formalized as an observational equivalence. Coercion-resistance is expressed in terms of adaptive simulation and labeled bisimilarity. In the following we describe the definition of privacy and coercion-resistance. The other contents of DKR model can be found (Delaune et al., 2006).

DKR point out the informal and formal definition of privacy:

The idea is that if the attacker can’t find if arbitrary honest voters V_A and V_B exchange their votes, then in general he can’t know anything about how V_A (or V_B) voted. We can find that this definition is robust even in situations where the result of the election is such that the votes of V_A and V_B are necessarily revealed.

At the same time DKR give the informal and formal definition of coercion-resistance:

The coercer has not only the ability that gets the information from observing the election process but also the ability that can interact with the voter.

The coercer can be an active attacker.

The ideas of this definition is that whenever the coercer requests a given vote on the left-hand side then V_B can change his vote according to the right-hand side and counterbalance the outcome. However, we need to avoid the case where letting V_B vote α. Therefore we require that when we apply a context C, intuitively the coercer, requesting 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 α.

THE SIMPLIFIED VERSION OF MENG PROTOCOL

Meng protocol is secure and practical with related properties. But it does not formally analyze these properties. Here we describe the simplified version in Fig. 1 in order to concentrate on the key aspect on privacy and coercion-resistance.

Meng protocol consists of preparation phase, registration phase, voting phase and tallying phase.

In preparation phase authorities and voters generate the public/private ElGamal keys. The private keys of voter and authorities are secret. Authorities generate the ballot B^t and send it and its digital signature to bulletin board denoted by BB.

In registration phase firstly voter V_j generates the ident_j, then generates message4 and send it to the registration authority RA. RA receives the message and verifies ident_j that if it has registered. If voter has not registered, RA verifies sign(ident_j, SKV_j).

If the verification is wrong, RA sends the error message to V_j, the protocol ends. If the verification is right, RA generates ProofV_j^RF based on none-intractive proofs of knwledge that two ciphertexts are encryption of tha same plaintext with ElGamal crypto system. At last RA generate massage 5and send it to voter V_j through one-way anonymous channel. At tha same time RA creats penc (C_j PK^c) and send it to BB.

In voting phase V_j receives proofV_j^RA and verifies it. If the result is right, V_j generates penc (C_j, PK^V)||penc(B_j, PK^V) and send it to BB.

In tallying phase tallying authority TA tallies the ballot and publishes its results in BB.

MODELING MENG SIMPLIFIED PROTOCOL WITH APPLIED PI CALCULUS

We use the applied pi calculus (Abadi and Fournet, 2001) to model Meng simplified protocol. Figure 2 describes the functions and Fig. 3 describes the equational theory in Meng simplified protocol.

We model cryptography in a Dolev-Yao style as being perfect. 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 checksign function.

The main process is modeled in Fig. 4. In this model the main process consists of preparation process, registration process, voting process and tallying process (Fig. 4). At the same time it sets up private channels. These processes are described in detail in the following parts.

The preparation process is modeled in Fig. 5. In the model authority AK generates the public/private ElGamal keys. The private keys of voter and RA and TA are sent by secure channel. RA generates uotechoice(t) and sends it to BB.

Where, x is a fresh free variable value.

The registration process can be modeled in Fig. 6. In this model voter V_j creates:

and sends it to RA. RA verifies sign (ident_j, SRKV_j) If the verification is true, RA generates:

and sends it to V_j through one-way anonymous channel. At the same time RA generates penc (C_j, PK^C) and sends it to BB.

The voting process is described in Fig. 7. In the model V_j receives the m5 and decrypt m5 with the private key SRKV_j to recover encrypt (C_J, PUK^V)|| ndupproofV_j^RA.

Then V_j uses the projection function to extract ndupproofV_j^RA, which is the evidence that prove that the encrypt (C_J, PUK^V) and penc (C_J, PUK^V) are ciphertext of the same plaintext C_J. NdupproofV_j^RA is a non-interactive designated verifier proof. The V_j verifies the proof ndupproofV_j^RA. If the result is true V_j uses projection functions to get encrypt (C_J, PUK^V) from m6. Finally it creates ballot penc (C_J, PUK^V)||penc (B_J, PUK^V) and sends it to BB.

The tallying process is modeled in Fig. 8. In the model the BB receives the ballot bbballot, then uses the projection function to extract encrypt (C_j, PUK^V) and encrypt (B_J, PUK^V). Finally TA tally based the homomorphic encryption property and publishes the results in BB.

ANALYSIS OF PRIVACY WITH DKR MODEL

We do not give full formal proofs here owning to multifarious procedure and the space the limitation. According the DKR model, in order to prove privacy, we need to show:

According to the definition of privacy, in order to get the proof of privacy, we need to suppose that at least two voters are honest. We denote the voters V₁ and V₂ and their votes ballotuoter 1 and ballotuoter 2, respectively. We say that a voting protocol respects privacy whenever a process where, V₁ votes ballotuoter 1 and V₂ votes ballotuoter 2 is observationally equivalent to a process where, V₁ votes ballotuoter 2 and V₂ votes ballotuoter 1.

The processes modeling the two voters are shown in Fig. 9.

The proof can be sketched as follows. The only difference between:

and

lies in the two voter processes. We therefore first show that:

Note that the use of phase is the key to hold privacy in the protocol. The phrase is a global synchronization command. The process first executes all instructions of a given phase before moving to the nest phase. When we omit the synchronization after the registration phase with the administrator, privacy is violated.

ANALYSIS OF COERCION-RESISTANCE WITH DKR MODEL

We also do not give full formal proofs here owning to multifarious procedure and the space the limitation. According to the DKR model, in order to prove concerion-resistance, we need to show:

We only introduce the ideas on how to construct the voting process’ and context C.

For coercion-resistance the coercer can provides the inputs for the messages and make voter to send it out to BB. If the coercer prepares messages corresponding to a given vote, voter can fake the scripts and know that voter will counterbalance the outcome, by adaptively choosing the same vote. The possible voting process’ and the possible context C required for the definition of coercion resistance are shown in Fig. 10 and 11.

The idea is that voting process’ to use fake C_j to vote a and sent the fakendupproofV_j^RA to the context C, it is the coercer and attacker. outputting scripts fakendupproofV_j^RA to the coercer. Voting process’ prepares all outputs as if he uses a C_J voting c. The context C can’t find the truth. The context C creates its own vote and send it to voting process’.

The key part is that, using his private key, the voter provides a fakendupproofV_j^RA, proving that fakeC_J is legal credential of voter V_j, which make the coercer believe that he can use it to vote its special ballot.

CONCLUSION

The secure and practical Internet voting protocols should have privacy, completeness, soundness, unreusability, fairness, eligibility and invariableness, universal verifiability, receipt-freeness and coercion-resistance. Firstly, we talk about the privacy and coercion-resistance. Secondly, a typical internet voting protocol is modeled with applied pi calculus. Finally the typical protocol with DKR privacy and coercion-resistance formal model is analyzed. The result shows that the protocol has the privacy and coercion-resistance properties.

In the future we will work on analysis of the eligibility, fairness, university verification, completeness, soundness, unreusability and invariableness with the applied pi calculus.

NOTATIONS

REFERENCES