**Bo Meng**

School of Computer, South-Center University for Nationalities, Wuhan, 430074, Hubei, People`s Republic of China

School of Computer, South-Center University for Nationalities, Wuhan, 430074, Hubei, People`s Republic of China

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.

PDF Abstract XML References Citation

Bo Meng, 2008. Formal Analysis of Key Properties in the Internet Voting Protocol Using Applied Pi Calculus. *Information Technology Journal, 7: 1133-1140.*

**DOI:** 10.3923/itj.2008.1133.1140

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

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:

• | Informal definition of privacy: The system cannot reveal how a particular voter voted |

• | Formal definition of privacy: A voting protocol respects privacy, if: |

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:

• | Informal definition of coercion-resistance: A voter cannot cooperate with a coercer to prove to him that she voted in a certain way |

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.

• | Formal definition of coercion-resistance: A voting protocol is coercion-resistance if there have a closed extended process V’ and a strict evaluation context C such that: |

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

Fig. 1: | Simplified version of Meng protocol |

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.

Fig. 2: | Functions in Meng simplified protocol |

Fig. 3: | Equational theory in Meng simplified protocol |

Fig. 4: | Main process |

Fig. 5: | Preparation process |

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

Fig. 6: | Registration process |

Fig. 7: | Voting process |

Fig. 8: | Tallying process |

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_{1} and V_{2} and their votes ballotuoter 1 and ballotuoter 2, respectively. We say that a voting protocol respects privacy whenever a process where, V_{1} votes ballotuoter 1 and V_{2} votes ballotuoter 2 is observationally equivalent to a process where, V_{1} votes ballotuoter 2 and V_{2} 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:

Similarly

Fig. 9: | Two voters for analyzing privacy property |

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

Fig. 10: | Voting process |

Fig. 11: | Context C: attacker |

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.

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

+ | : | Addition operator |

: | Multiplication operator in homomorphic encryption | |

|| | : | Concatenation |

l | : | The No. Of the voters in the election |

V_{j} | : | The jth legal voter (j = 1, 2, ..,l) |

B^{t} | : | The ba;;ot which the voter vote the tth candatite |

AK | : | Authority for generating the keys of TA, RA and voter |

TA | : | The registration authority |

BB | : | Bullion board |

C_{j} | : | RA creates the secret number for V_{j}’ credential |

PK^{C} | : | The public key of RA and TA |

SK^{C} | : | The private key of RA and TA |

PK^{V} | : | The public key of RA and TA |

SK^{V} | : | The private key of RA and TA |

PK_{RA} | : | The public key of RA, the public key is used when the voter register |

SK_{RA} | : | The private key of RA, the private key is used when the voter register |

PK_{AK} | : | The public key of AK |

SK_{AK} | : | The private key of AK |

PKV_{j} | : | The public key of voter V_{j} |

SKV_{j} | : | The private key of voter V_{j} |

ProofV_{j}^{RA} | : | The non-interactive designated verifier proof of knowledge that penc(C_{j}, PK^{V}) and penc (C_{j}, PK^{C}) are the ciphertext of C_{j}, which is generated by RA for V_{j} |

ident_{j} | : | The identification of voter V_{j} |

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

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

CrossRefDirect Link - 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 - 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 - Juels, A., D. Catalano and M. Jakobsson, 2005. Coercion-resistance electronic elections Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, November 7, 2005, Alexandria, VA., USA., pp: 61-70.

CrossRefDirect Link - Kremer, S. and M.D. Ryan, 2005. Analysis of an electronic voting protocol in the applied Pi calculus. Lect. Notes Comput. Sci., 3444: 186-200.

CrossRefDirect Link - Lee, B., C. Boyd, E. Dawson, K. Kim, J. Yang and S. Yood, 2004. Providing receipt-freeness in mixnet based voting protocols. Proceeding of the 6th International Conference on Information Security and Cryptology, November 27-28, 2004, Springer Berlin/Heidelberg, UK., pp: 1-14.

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

CrossRefDirect Link - Ryan, K.M. and S.S. Delaune, 2006. Verifying properties of electronic voting protocols. Proceedings of the IAVoSS Workshop on Trustworthy Elections, June 29-30, 2006, Robinson College, Cambridge, UK., pp: 1-8.

Direct Link