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
How to cite this article
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 doesnt 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 cant find if arbitrary honest voters VA and VB exchange their votes, then in general he cant know anything about how VA (or VB) voted. We can find that 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.
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 VB can change his vote according to the right-hand side and counterbalance the outcome. However, we need to avoid the case where letting VB 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 Bt and send it and its digital signature to bulletin board denoted by BB.
In registration phase firstly voter Vj generates the identj, then generates message4 and send it to the registration authority RA. RA receives the message and verifies identj that if it has registered. If voter has not registered, RA verifies sign(identj, SKVj).
|Fig. 1:||Simplified version of Meng protocol|
If the verification is wrong, RA sends the error message to Vj, the protocol ends. If the verification is right, RA generates ProofVjRF 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 Vj through one-way anonymous channel. At tha same time RA creats penc (Cj PKc) and send it to BB.
In voting phase Vj receives proofVjRA and verifies it. If the result is right, Vj generates penc (Cj, PKV)||penc(Bj, PKV) 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 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 Vj creates:
and sends it to RA. RA verifies sign (identj, SRKVj) If the verification is true, RA generates:
and sends it to Vj through one-way anonymous channel. At the same time RA generates penc (Cj, PKC) 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 Vj receives the m5 and decrypt m5 with the private key SRKVj to recover encrypt (CJ, PUKV)|| ndupproofVjRA.
|Fig. 6:||Registration process|
|Fig. 7:||Voting process|
|Fig. 8:||Tallying process|
Then Vj uses the projection function to extract ndupproofVjRA, which is the evidence that prove that the encrypt (CJ, PUKV) and penc (CJ, PUKV) are ciphertext of the same plaintext CJ. NdupproofVjRA is a non-interactive designated verifier proof. The Vj verifies the proof ndupproofVjRA. If the result is true Vj uses projection functions to get encrypt (CJ, PUKV) from m6. Finally it creates ballot penc (CJ, PUKV)||penc (BJ, PUKV) 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 (Cj, PUKV) and encrypt (BJ, PUKV). 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 V1 and V2 and their votes ballotuoter 1 and ballotuoter 2, respectively. We say that a voting protocol respects privacy whenever a process where, V1 votes ballotuoter 1 and V2 votes ballotuoter 2 is observationally equivalent to a process where, V1 votes ballotuoter 2 and V2 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:
lies in the two voter processes. We therefore first show that:
|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 Cj to vote a and sent the fakendupproofVjRA to the context C, it is the coercer and attacker. outputting scripts fakendupproofVjRA to the coercer. Voting process prepares all outputs as if he uses a CJ voting c. The context C cant 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 fakendupproofVjRA, proving that fakeCJ is legal credential of voter Vj, 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.
|:||Multiplication operator in homomorphic encryption|
|l||:||The No. Of the voters in the election|
|Vj||:||The jth legal voter (j = 1, 2, ..,l)|
|Bt||:||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|
|Cj||:||RA creates the secret number for Vj credential|
|PKC||:||The public key of RA and TA|
|SKC||:||The private key of RA and TA|
|PKV||:||The public key of RA and TA|
|SKV||:||The private key of RA and TA|
|PKRA||:||The public key of RA, the public key is used when the voter register|
|SKRA||:||The private key of RA, the private key is used when the voter register|
|PKAK||:||The public key of AK|
|SKAK||:||The private key of AK|
|PKVj||:||The public key of voter Vj|
|SKVj||:||The private key of voter Vj|
|ProofVjRA||:||The non-interactive designated verifier proof of knowledge that penc(Cj, PKV) and penc (Cj, PKC) are the ciphertext of Cj, which is generated by RA for Vj|
|identj||:||The identification of voter Vj|
- 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.
- 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.
- 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.