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. So how to develop and verify a practical secure internet voting protocol is a challenging issue (Meng, 2009c, 2011b).

The practical secure remote internet voting protocol should include privacy, completeness, soundness, fairness and invariableness, universal verifiability, receipt-freeness and coercion-resistance. Previous research focused on implementation and formal analysis of receipt-freeness and coercion-resistance (Meng, 2009c). Besides these properties, owning to the huge damage and hard to prevention of denial of service attacks in security protocol, the secure remote internet voting protocol should also have resistance of denial of service attacks. In the last twenty years many remote internet voting protocols (Clarkson et al., 2008; Meng, 2007, 2009a; Meng et al., 2010a), claimed on their security, have be proposed. To our best knowledge until now resistance of denial of service attacks in these remote internet voting protocols has not been analyzed.

Owning to the huge damage and hard to prevention of denial of service attacks in security protocol and network, people pay serious attentions on analysis, verification and prevention of denial of service attacks (Tritilanunt, 2009). Denial of service attacks are attacks against availability, attempting to prevent legitimate users from accessing the network and distributed system. This kind of attack aims at rendering a network an system incapable of providing normal service by targeting either the network, bandwidth or connectivity. According to the methods of attacks, denial of service attacks can be classified into three types: resource exhaustion, out of service and physical destroy. Denial of service attacks is simple and effective, for example, the adversary can create many bogus messages and sent to target of attack. That make the target of attack can not provide normal service for legitimate user owning to process big bogus messages. At the same time it is not easy to find the adversary and adversary can mount another type attacks through denial of service attacks, for example, man-in-the-middle attack (Meadows, 2001).

In order to prevent denial of service attacks the first step is to analyze and proof resistance of denial of service attacks in protocol, network and distributed system with formal method and give the confidence of people in its security. There are two models can be used: one is symbolic model in which cryptographic primitives are ideally abstracted as black boxes, the other is computational 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 (Mei et al., 2009), NRL, Casper, Isabelle, Athena, Revere, SPIN, Brutus, ProVerif, Scyther (Meng, 2011b).

In symbolic model there are mainly three formal frameworks in resistance of denial of service attacks. One is Yu-Gligor formal model (Yu and Gligor, 1990) based on user agreement. The core of framework is based on access control policy. It does not deal with denial of service attacks are executed before authentication between sender and receiver in protocol, for example, SYN floods attacks. At the same time framework does not support the automated tools. The other is Meadows’s cost-based formal model (Meadows, 2001) which built on the notion that a protocol is a sequence of operations with cause-effect relationships: an action by one principle usually causes a sequence of actions by another principle that incurs some cost. He argues that his formal framework can be supported by modification of automated tools, for example, NRL protocol analyzer. Tritilanunt et al. (2007) and Tritilanunt (2009) think that the cost analysis has only taken into account honest runs of the protocol in Meadows’s cost-based formal model. At the same time they also think that Meadows used only a coarse measure of computational cost with three levels denoted as cheap, medium or expensive. In practice it can be quite difficult to classify and compare operations in such a coarse measure. The third one is Huang et al. formal model (Huang et al., 2011) which is the first automatic method of resistance of denial of service attacks based on theorem proof with first order theorem prover ProVerif. ProVerif is a 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 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 has been tested on protocols of the literature with very great results. In computational model resistance of denial of service attacks analysis model have not been proposed by Blanchet (2001).

Meng protocol (Meng, 2009b) is one of the most important remote internet voting protocols that claims to satisfy formal definitions of key properties without strong physical constrains. Until now resistance of denial of service attacks in Meng protocol is not analyzed. So here we use mechanized proof tool ProVerif to verify resistance of denial of service attacks in Meng protocol based on Huang et al. (2011) formal model.

The main contributions of this paper are summarized as follows:

RELATED WORK

In symbolic model there are mainly three formal frameworks in resistance of denial of service attacks: Yu-Gligor formal model (Yu and Gligor, 1990) based on user agreement, Meadows’s cost-based formal model (Meadows, 2001), Huang et al. (2011) formal model (Huang et al., 2011) based on theorem proof. In computational model resistance of denial of service attacks analysis model has not been proposed. To our best knowledge until now resistance of denial of service attacks in remote voting protocol is not analyzed.

May be one of the first attempts to formalize the notion of resistance of denial of service attacks was done by Gligor (1983, 1984) with maximum waiting time. Gligor defines availability as the guaranty of a maximum specified waiting time for any operation, even in case of concurrent accesses. If a system is resistance of denial of service attacks then any requesting user will wait no more than maximum waiting time units of time before the service is granted.

Yu and Gligor (1990) propose a formal specification on resistance of denial of service attacks based on temporal logic by introduction of notion of user agreement. The core of framework is based on access control policy. They argue that lack of specifications for these agreements makes it impossible to demonstrate denial of service prevention. If the shared services want to resist denial of services attacks the user must to obey the special constrains. They model availability as how to provide a shared service with a specified maximum waiting time. They argue that denial of service attacks is as the liveness which models the finite waiting time police and safety problem. Their specification model consists of the service specifications and the user-agreement specifications. The service specifications describe all the desired operations and properties that must be provided by the shared service. The user-agreement specifications describe all the desired properties. They use their framework to formalize and analyze denial of services attacks in resource allocator in operating system and Dining philosophers’ service. It does not deal with denial of service attacks are executed before authentication between sender and receiver in protocol, for example, SYN floods attacks. At the same time framework does not support the automated tools. Bacic and Kuchta (1991) argue that the core problem of resistance of denial of service attacks is resource allocation. They introduce the notion of a resource allocation monitor that has to have the following three reference monitor characteristics: it is tamper-proof and cannot be prevented from operating and guarantees authorized access to resources under its control. Millen (1993) extended Yu-Gligor formal model by representing the passage of time explicitly. The maximum-waiting-time policy can be expressed as easily as a finite-waiting-time policy. At the same time it can also support other policies of probabilistic nature. Policies and user agreements are expressed without temporal logic. He also proposes a resource allocation model for resistance of denial of service attacks. Waiting time policy consists of a security constraint which says that a subject which asks for a resource has to be provided with it with a maximum waiting time. His formal model catches the effect of realistic system behavior by introducing a state transition model of resource allocation and probabilistic waiting time policies. He also thinks that a denial of service protection base is similar to trusted computing base with strong trust assumptions to guarantee that the constraints on behavior can be reliably enforced. Millen’s idea is similar to the one suggested by Abadi and Lamport (1993). Both consider some resource management rules and suggest an approach to model and verify properties including liveness, safety and availability. But Millen’ formalism differs significantly which is based on a set-theoretic approach and includes n representation of passage of time explicitly.

Meadows (2001) introduce a very important formal framework of resistance of denial of service attacks based on the costs spending on computation by the principles in security protocols. His formal model based on fail-stop protocol. A fail-stop protocol is one that can provide a certain degree of security against attack and will stop if a message that is interfered with is detected or the verification is failed. The framework is built on the notion that a protocol is a sequence of operations with cause-effect relationships: an action by one principle usually causes a sequence of actions by another principle that incurs some cost. According to Meadows’s framework when in a protocol execution at which an attacker can send a message to cause a denial of service attack if the cost of creating the message is small with respect to his resources while the cost to the defender to accept and process the message is relatively more expensive. If this relationship of costs between attacker and defender is not true during a protocol execution, then the protocol is resistance of denial of service attacks. He argues that his formal framework can be supported by modification of automated tools, for example, NRL protocol analyzer. He analyzes the station to station protocol and point out that it is not resistance of denial of service attacks. But Meadows’s formal model maybe not practical because the costs of generating a bogus message is small than costs of processing and verifying, so every protocols is not resistance of denial of service attacks. Based on Meadows’s cost-based formal model Ramachandran (2002) analyzes JFK protocol and point that JFK protocol is resistance of denial of service attacks with the conditions bogus messages are handled in an appropriate way. Smith et al. (2006) also analyze JFK protocol with Meadows’s cost-based formal model. They point that because both of the Diffie-Hellman exponentials (g^r and gⁱ) can be reused the coordinated attackers can launch the denial of services attacks. At the same time they also think that owning to that availability of IP addresses makes that the cost of revealing an address may be more expensive to an initiator. JFK protocol can be denial of service attacks in the presence of attackers is not willing to reveal a source IP address. But we think these arguments are worth discussing. Lafrance and Mullins (2003) present a method based on admissible interference for finding denial of service attacks in security protocols. Using SPPA and Meadows’s cost-based framework, they introduce an information flow property called impassivity which detects whenever an enemy process may cause interference, using its low-cost actions, on high-cost actions of other principals. It is based on the fact that such interference may lead to an attack on the protocol by exploiting this single flaw several times and, thus, causing denial of services through resource exhaustion. Their model is suitable to the model of resource exhaustion denial of service attacks. They point out that 1kp electronic payment protocol is not denial of services attacks. Abadi et al. (2007) use the observational equivalence relation to formalize denial of services attacks and find JFK protocol is resistance of denial of services attacks. Tritilanunt et al. (2007) and Tritilanunt (2009) firstly point out that the cost analysis has only taken into account honest runs of the protocol in Meadows’s cost-based formal model. At the same time they also think that Meadows used only a coarse measure of computational cost with three levels denoted as cheap, medium or expensive. In practice it can be quite difficult to classify and compare operations in such a coarse measure. So they use the colored Petri nets to model the denial of services attacks based on cost-based and time-based model and analyzed the HIP protocol. They find that HIP protocol is not resistance of denial of services attacks in the conditions Type 3 adversary or Type 4 adversary. Zhou et al. (2008) propose a model based on strand spaces and 4-way handshakes protocol is analyzed. They find that it is not resistance of denial of services attacks.

Huang et al. (2011) present the first automatic method of resistance of denial of service attacks based on theorem proof with first order theorem prover ProVerif. They extend the applied pi calculus from the attacker contexts and process expression and then from the view of protocol state, they propose the first automatic method of resistance of denial of service attacks based on extended applied calculus. At the same time they analyze resistance of denial of service attacks in JFK protocol and IEEE 802.11 i four-way handshake protocol. The results they obtained are that JFK protocol is resistance of denial of service attacks and IEEE 802.11 i four-way handshake protocol is not. The methods to prevent resistance of denial of service attacks in IEEE 802.11 i four-way handshake protocol are also proposed.

Besides the formal model of Yu-Gligor formal model, Meadows’s cost-based formal model and Huang et al. (2011) formal model, Amoroso (1990) emphasizes the need for specifying a service model in terms of prevent (p, c) policies as predicates concerned subjects, resources and resource consumption operations. Denial of service attacks policies are specified based on predicates that specify conditions, using priorities, under which a subject can deny other authorized subjects access to critical objects. He analyzes resistance of denial of service attacks in system V/MLS with prevent (2, 2).

Based on modal logic and deontic logic, Cuppens and Saurel (1999) propose a formal model to formalize availability policy by the four predicates expression of permissions, prohibitions and obligations of subjects: use-right, disposal-right, realization-right and run-right. They use disposal-right predicate to model waiting time policy and use-right to model use time policy. Their formal framework enables users to express their own required availability properties and to formally check these properties over a given system or protocol by simulating its logical specification. Gabillon and Gallon (2003) resembles the Cuppens and Saurel model. The main difference is that we do not have an explicit waiting time policy. They consider an availability policy as a special case of security policy where the distribution of rights varies with the time. They apply their method to analyze other protocols like the ARINC629 CP or Ethernet. Cuppens et al. (2006) use the formal security model called Nomad which combines deontic and temporal logics to specify availability requirements. Each availability requirement expressed in the Nomad model is transformed into a security aspect that can be woven into a program. They mainly concern the denial of service attacks in program. Nomad can transform an insecure program into a secure program.

Agha et al. (2005) use probabilistic extension of the Maude term rewriting system called PMAUDE to model denial of services attacks and a sublogic of Continuous Stochastic Logic to describe the rate of success of attack and use the statistical model-checking tool VESTA to analyze the TCP 3 3-way Handshaking protocol and find it is not resistance of denial of services attacks. Mahimkar and Shmatikov (2005) use the alternating time temporal logic (ATL) to model bandwidth consumption and resource exhaustion attacks and verify JFKr using MOCHA a model checker. They find that JFKr is resistance of denial of services attacks.

REVIEW OF HUANG ET AL. FORMAL MODEL

In this section we firstly review the extended applied pi calculus, then the definitions of resistance of denial of services, finally the method of automated proof of resistance of denial of service attacks.

EXTENDED APPLIED PI CALCULUS

In this section we review extended applied calculus which is based on applied pi calculus. Applied pi calculus (Abadi and Fournet, 2001) is a language for describing concurrent processes and their interactions based on Dolev-Yao model and 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 automatic 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 Just Fast Keying protocol (Abadi et al., 2004, 2007), remote electronic voting protocol (Backes et al., 2008a; Meng et al., 2010c, 2010b, 2011a), a key establishment protocol, direct anonymous attestation protocol (Backes et al., 2008b), TLS protocol (Bhargavan et al., 2008) .

In order to model the protocol state and resistance of denial of service attacks, Huang et al. (2011). extend the applied pi calculus from two aspects: one is the adversary context, the other is process expression. In the following we review the extended applied pi calculus. The extended applied pi calculus is also supported by ProVerif. Here we only review the adversary contexts and process context in extended applied calculus. The other content in extended applied calculus can be found in the reference (Huang et al., 2011)

Adversary contexts: In applied pi calculus the adversary is in Dolev-Yao model. But in extended applied pi calculus, according to abilities of adversary the contexts of adversary are classified into two contexts: one is ideal context, the other is real context. Real context is formalized as:

Fig. 1:	Process context

where, real context is insecure environments where the adversary is in Dolev-Yao model. The adversary in real context can overhear, intercept and synthesize any message and is only limited by the constraints of the cryptographic methods used. Ideal context is formalized as:

where . Ideal context is secure environments. The adversary in ideal context can not overhear, intercept and synthesize any message.

Process context: Process context in Fig. 1 is a process with a hole []. The process 0 is an empty process context. The process Q/P is the parallel composition of P and Q. The replication !c produces an infinite number of copies of c which run in parallel. The process un.C firstly creates a new, private name then executes as C. The process in (u, x). C receives a message from channel u and runs the process context c by replacing formal parameter x by the actual message. We use in (u.M). C for the input of terms M₁,..., M_t. The process out (u, N).C is firstly ready to output the message N on the channel u and then runs the process context c. The process is the abbreviation for the output of terms . The conditional construct if M = N then C else Q runs that if M and N are equal, executes process context C, then C is a verified context. The conditional construct if M = N then P else C runs that if M and N are not equal, executes c, then c is not a verified context.

DEFINITIONS OF RESISTANCE OF DENIAL OF SERVICE ATTACKS

Here, we review related definitions of resistance of denial of service attacks in Huang et al. (2011).

Definition 1: An annotated Alice-and-bob specification in protocol: An annotated Alice-and-bob specification in protocol consists of n statements of form:

where, iε [1, n], M₆, denotes the ith message in protocol.

Protocol consists of n messages exchanged between two principles A, B. A statement:

describes that firstly the sequences of operations performed by principles A to generate a message M_i and then it is sent to principle B, finally the sequence of operations performed by principle B. denotes the sequence of operations performed by principle A for generating M_i. denotes the sequence of operations performed by principle B after receiving M_i and processing and verifying M_i.

Let:

is an annotated Alice-and-bob specification in protocol, A_cti (A) is a set of operations performed by principle A on l. denotes that the set of the sequence of operations preceding principle sends message M_i to B.

denotes that the set of the sequence of operations performed by principle B after receiving M_i, if any verification operations, for example, decryption, verification of digital signature, failed then the operation stops.

Definition 2: authentication of message M_i: If the statement:

is carry out successfully then the fact that principle B receives message M_i from A is exist; if principle B receives message M_i but principle A does not performance the sequence of operations , then message M_i received by principle B is altered by the adversary; If message M_i received by principle B is altered by the adversary and B can find the fact that message M_i is modified, then message M_i received by principle B is authenticated.

Definition 3: correspondent in operations: α and β are correspondent in operations if and only if message M_i in:

are same to message M_i in

where,

denotes that the set of the sequence of operations for generating the message M_i by principle A.

denotes that the set of the sequence of operations for processing and verifying the message M_i by principle B.

Definition 4: γ₁ casually precedes γ₂: P is an annotated Alice-and-bob specification in protocol, S is a set of all operations in P. For any operation γ₁ and γ₂ in S, γ₁ casually precedes γ₂ if and only if:

If:

or:

at the same time γ₁ occurred before γ₂;

If:

at the same time γ₁ and γ₂ are correspondent.

There is operations γ₈, γ₈ casually precedes γ₂, γ₁ casually precedes γ₈.

denotes that the set of the sequence of operations for generating the message M_i by principle A. denotes that the set of the sequence of operations for processing and verifying the message M_i by principle B.

Definition 5: set of association in message M_i and M_i: Set of association ω between any message M_i and M_i in protocol P is intersection of set and set ψ: ω = ∩ψ, where I, jε[1, n], i<j, is set of data items in verification operations υ in , ψ is the set of data items in message M_i in .

Set of association ω describe the degree and relation of influence among messages in protocol. If ω is null set, then messages in protocol are independent and are not related; if ω is not null and includes many data items, then messages M_i and M_i are related deeply.

Definition 6: resistance of denial of service attacks: P is an annotated Alice-and-bob specification in protocol, B is resistance of denial of service attacks if and only if set of association ω between any message M_i and M_i in set Recv(B):

Where Recv(B) is set where data items are in operations that are ordered in casually precedes in:

If any message M_i and M_i in protocol P are not related, then contexts of processing the message M_i and M_i are independent, then B is resistance of denial of service attacks; if any message M_i and M_i in protocol P are related, then contexts of processing and verifying message M_i and M_i are not independent, then B is resistance of denial of service attacks if and only if set of association ω of any message M_i and M_i in protocol P are authenticated.

METHOD OF AUTOMATED PROOF OF RESISTANCE OF DENIAL OF SERVICE ATTACKS

In this section we review the automated proof of resistance of denial of service attacks in protocol by Hung et al. (2011) formal model.

Applying the extended applied pi calculus the protocol can be modeled as an annotated Alice-and-Bob specification. It assumes that the protocol exchanges 2n messages between principles Alice and Bob in a run. Principles Bob receives n messages M_i, i, ε[1, n]. Principles Bob sends n messages M'_i, i, ε[1, n]. Protocol process is a closed process and consists of parallel composition of any initiator processes Alice and responder processes Bob. According to the extended applied pi calculus process Alice and Bob can be reduced into one process in Fig. 2.

Fig. 2:	Processes

Fig. 3:	The formal model of messages Mi iε [1, n]

In order to use ProVerif to automatic proof of resistance of denial of service attacks of Bob, the any messages M_i, i, ε[1, n] is modeled with the extended applied pi calculus. If the adversary can get the secret on the public channel c, then the adversary can launch a denial of service attacks by attacks of message M_i.

The method is used to model the messages M_i, i, ε[1, n] in Fig. 3. The message M_i is exchanged and processed in real context. The messages

are exchanged and processed in idea context. Protocol process PP is

c is public channel. c_j, jε|2, n|∩j≠i are private channels used to receive messages M_i Jε|2, n|∩j≠i.

If the adversary can get the secret message secret on the public channel c, then the adversary can launch a denial of service attacks by attacks of message M_i.

Theorem: resistance of denial of service attacks: Responder Bob in protocol process PP is resistance of denial of services attacks if and only if the formal model of all messages M_i, i, ε[1, n] received by principle Bob, PP can not output the secret message secret, in other words, there is not processes P', P"and attacker process attacker to cause:

According to the theorem, people can use the extended applied pi calculus to model resistance of denial of services attacks in protocol, then based on the proposed theorem, apply ProVerif to automated prove the resistance of denial of services attacks.

MECHANIZED PROOF TOOL PROVERIF

ProVerif is an automatic cryptographic protocol verifier based on a representation of the protocol by Horn clauses. 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 in Fig. 11 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 that are accessible to an automated analysis using ProVerif (Blanchet, 2001).

ProVerif is the only tool for our purpose of an automated verification of Meng protocol based on Huang et al. (2011) model. Inspired by works of Huang et al. (2011) model we use it to automatically verify resistance of denial of services attacks in Meng protocol.

MENG PROTOCOL

Meng protocol (Meng, 2009b) promises that it can protect voters’ privacy and achieves universal verifiability, receipt-freeness and coercion-resistance with weak physical assumptions or procedural constraints. It mainly applies the encryption technologies which include threshold ElGamal cryptosystem, Mix net, homomorphic encryption, Meng non-interactive deniable authentication protocol (Meng, 2009c) and the improved proof protocol that knowledge that two ciphertexts are encryption of the same plaintext. Meng protocol assumes that the private key is private and that the channel between voters and registration authority is one way anonymous channel. Meng protocol consists of the five authorities: registration authority that is responsible for authenticating the voters, issue authority that takes charge of issuing the related key and credentials, bulletin board, voters, tallying authority that is responsible for tallying ballots. The message structure is depicts in Fig. 4.

In preparation phase issuer authority generates the public/private ElGamal keys. The private keys of voter and authorities are secret. It also generates the ballot B^t and send B^t and its digital signature to bulletin board denoted by bulletin board.

In registration phase firstly voter voter_i generates message

and send it to the registration authority A_i. A_i receives the message and open the digital envelope with its private key. He checks ident_i that weather it has registered or not. If it has not registered, he checks Sk_i (ident_i).Then A_i generates his public key and public keys for the ciphertext E^v (c_i,j) of credential shares with the public key of voter, after that he generates based on Meng non-interactive deniable protocol and the improved proof protocol that knowledge that two ciphertexts are encryption of the same plaintext with ElGamal cryptosystem. Finally A_i generates . Other registration authorities generate to voter V_i by one way anonymous channel.

with the similar method. A_i gets

from other authorities and sends

Fig. 4:	The structure of message

A_i also generates (E^o (c_{i, j})) Sk_Ai and sends (E^o (c_{i, j}) and (E^o (c_{i, j})) Sk_Ai (i = 1,..., i,..., s) to Bulletin Board. After voter_i receives (E^v (c_{i, j}) and (E^o (c_{i, j}), he verifies Meng non-interactive deniable protocol proof and proof of equality between (E^v (c_{i, j}) and the corresponding (E^o (c_{i, j}) that has been signed and published in her reserved area of bulletin board. Upon successful verification, she multiplies together the shares (E^v (c_{i, j}) and gets (E^v (cj). Then voter_i chooses his favorite ballot shares and gets:

then sends (E^v (cj), to bulletin board. The registration phase ends.

After the voting time expires, all ballots on bulletin board posted by allegedly eligible voters are mixed by the tallying authorities. Tallying authority publishes the tallying result on bulletin board.

MODELING MENG PROTOCOL WITH EXTENDED APPLIED PI CALCULUS IN HUANG ET AL. FORMAL MODEL

In order to use ProVerif to analyze resistance of denial of service attacks in Meng protocol, in this section we use the extended applied pi calculus to model Meng protocol.

Firstly the function and equational theory is introduced. Cryptography in a Dolev-Yao model is modeled as being perfect. Figure 5 describes the functions and Fig. 6 describes the equational theory in Meng protocol.

Function and equational theory: Encryption algorithm and decryption algorithm in the probabilistic public key cryptosystem is denoted with pPKenc (x, pu, r) and pPKdec (x, PR), respectively. The deterministic public key encryption scheme consists of encryption algorithm PK enc (x, PR) and decryption algorithm PK dec (x, PR).

Fig. 5:	Functions

Fig. 6:	Equational theory

Fig. 7:	Model of zero knowledge proof (Backes et al., 2008b)

Digital signature algorithm includes the generation signature algorithm sugn (x, PR) sign the message x with private key PU and the verification algorithm verify sign (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 combining algorithm TpPKdec (x₁,..., x₂) recovers x from x₁,..., x₂. The deterministic threshold combining algorithm TpPKdec (x₁,..., x₂) means that recover x from x₁,..., x₂. The projection function projection_i (x) generated the ith share from the formatted message x. The self blinding function selfBinding (x, r) blinds message x with r. The add function add (x, y) add x and y. checkciphertext verify the two ciphertext x₁ and x₂ generated with the same plaintext. SK (x), PK (x), VK (x) generated the secret key, public key and verification key of x. NDAMAC (x, PR_S, PU_R) generates MAC in Meng non-interactive deniable protocol.

The equational theory is described in Fig. 6. It also contains and equational rules for abstractly reasoning about the knowledge proof that two ciphertexts are encryption of the same plaintext and used in the voting phase which is modeled as checkciphertext (TpPKenc (x₁, Pu_g, r₁), TpPKenc (x₁, Pu_g, r₂)) = true. It can verify the two ciphertexts TpPKenc (x₁, Pu_g, r₁) generated with the public key PU_y and random number r₂ and TpPKenc (x₁, Pu_g, r₂), TpPKenc (x₁, Pu_g, r₁) generated with the public key PU_z and random number r₁, are the same plaintext x₁. Voter can use the equation NDAMAC (x, SK (y), PK (z)) to compare the MAC receives from registration authority in non-interactive deniable authentication protocol to the MAC generated itself with relative parameters.

Zero knowledge proof modeled in Fig. 7 is used to model the improved proof protocol that knowledge that two ciphertexts are encryption of the same plaintext with ElGamal cryptosystem.

Then in the following section we model the process in Meng protocol which consists of the basic process include main process, voter process, corrupted voter process, registration authority process, issuer authority process, BB process and tallying authority process.

The main process in Fig. 8 sets up private channels chVR, chRI₁, chRI₂ and specifies how the processes are combined in parallel. chVR denotes the private channel between voter and registration authority. chRI₁ and chRI₂ are the private channel between registration authority and issuer authority, respectively. The main process also generates the key parameters c for credentials, v for vote, s for non-homomorphic cryptosystem, keyV for voter and keyI for issuer authority.

Voter process is modeled in extended applied pi calculus in Fig. 9. Each voter get the non-interactive deniable authentication proof’s ciphertexts kencNDA₁ and kencNDA₂ from registration authority, then decrypt and get the knowledge proofs PEP₁ and PEP₂, the MAC in non-interactive deniable authentication proof NDAMAC1 and NDAMAC2, respectively.

Fig. 8:	Main process

Fig. 9:	Voter process

Fig. 10:	Corrupted voter process

After that the voter checks NDAMAC₁ and NDAMAC₂, then uses checkciphertext to verify the equivalence between public₁ (PEP_i) and public₂ (PEP_i). If the verification is fail then it output secret by public channel c. The voter multiplies:

Because of the homomorphic properties of ElGamal cryptosystem, the resulting ciphertext cred includes the sum of credential shares. The resulting ciphertext (cred, vencvote = TpPKenc (vote, PK (V), r)) is sent to bulletin board.

Corrupted voters process is modeled in Fig. 10. He can sends cred through a public channel, thus the attacker can get the credential cred, so that the attacker can use the cred to impersonate them in order to mount any sort of attack.

Registration authority process is modeled in Fig. 11 that firstly generates the voters id, then gets the secret credentials shares cred₁ and cred₂ from issuer authority.

Fig. 11:	Registration authority process

Fig. 12:	Issuer authority process

Fig. 13:	BB process

Fig. 14:	Tallying authority process

Then he creates the ciphertexts of non-interactive deniable authentication proof that the proof of the equivalence between the encrypted share sent to the voter pPKenc (NDAMAC (PEP₁, SK (key R), PK (key V)), PEP₁, PK (key R), PK (key V), r) and pPKenc (NDAMAC (PEP₂, SK (key R), PK (key V)), PEP₂, PK (key R), PK (key V), r).

Issuer authority is modeled in Fig. 12 that firstly gets the shares of credential by projection_i (cred), then send sign [TpPKenc (projection_i), PK (C), r), Sk_i (C)] which encrypted with a set of ElGamal public parameters by the public channel pub.

BB process is modeled in Fig. 13. BB process receives k-voter, pk-reg, pk-iss1, pk-iss2 through public channel pub and out public key pk-reg from public channel chBV.

Tallying authority process is modeled in Fig. 14. After the voting time expires, the tallying authorities get the all ballots on bulletin board and then mixed it by elfBlinding (cencered, PK (C)). At the same time the shares of credentials posted by the registration authorities are also combined and then mixed selfBlinding (venccredvote, PK (V)). Thus he obtain two lists: a list:

and a set res. The two lists have been encrypted with different ElGamal public parameters. Using threshold protocols for the corresponding sets of private keys, the tallying authorities decrypt the elements in each list by TpPKdec (bcenccred, SK (C)) and TpPKdec (bcenccred, SK (V)) then compare them through a search algorithm and publish the tallying result on bulletin board.

MECHANIZED PROOF OF MENG PROTOCOL WITH PROVERIF

ProVerif can take two formats as input: one is Horn clauses, the other is process in an extension of the pi calculus (Abadi and Blanchet, 2005; Huang et al., 2011). In both cases, the output of the system is essentially the same. In this paper we use the extended pi calculus as the input of ProVerif.

In order to prove resistance of denial of services attacks in Meng protocol the formal model in extended applied pi calculus are needed to be translated into the syntax of ProVerif and generated the ProVerif inputs in the extended pi calculus. The code in analysis of resistance of denial of service attacks in voter in Meng protocol is presented in Fig. 15.

The result of resistance of denial of services attacks in Meng protocol in Fig. 16. We find that Meng protocol is not resistance of denial of services attacks because ProVerif out the message “Secret” by public channel c. In Meng protocol there is one resistance of denial of services attack by us: in preparation phase issuer authority publishes public keys Pk^o, PK^v for voter and his public key PK^Ai on BB without protecting security of these public keys by public channels. Thus the adversary can intercept public keys Pk^o, PK^v, PK^Ai and modify it,then send it to BB.

Fig. 15:	The code in analysis of resistance of denial of service attacks in voter in Meng protocol

Fig. 16:	The result of resistance of denial of services attacks in Meng protocol

In voting phrase voter v_i firstly verifies non-interactive deniable authentication proof DAMAC₁ and DAMAC₂, then he uses cheekciphertext to check the equivalence between the encrypted share public₁ (PEP_i) and the one E^o (c_{i, j}) the voter has received to its message is also provided to itself. PK^Ai has been publish on BB with digital signature with authority. Owning the adversary has modified the public keys PK^Ai, hence the verification of DAMAC₁ and DAMAC₂ failed, thus voter v_i can not vote. Hence make a resistance of denial of services attack. In order to protect Meng protocol against the denial of service attack we can use the digital certificate to distribute these public keys: Pk^o, PK^v and PK^Ai .

ACKNOWLEDGMENT

This study was supported in part by Natural Science Foundation of The state Ethnic Affairs Commission of PRC under the grants No: 10ZN09, titled “Research on the Provably Secure Remote Internet Voting Protocols without Physical Constrains”, conducted in Wuhan, China from 1/1/2011 to 30/12/2011.

CONCLUSION

Internet voting protocol play an important role in remote voting system. Owning to the huge damage and hard to prevention of denial of service attacks in security protocol, the secure remote internet voting protocol should have resistance of denial of service attacks.

Recently Huang et al proposed an automatic model that can be used to analyze the denial of service attacks in security protocol, so Meng protocol can be proved with mechanized proof tool ProVerif. In this paper the review formal model of resistance of denial of service attacks in security protocol are presented. Then apply the mechanized formal model proposed by Huang et al. (2011) The result is that Meng protocol has not resistance of denial of service attacks. One denial of service attack is found by us. At the same time we give the method against the denial of service attack.

As future work we plan to prove other resistance of denial of service attacks 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.