LSV Stéphanie Delaune
email: stephanie.delaune@lsv.ens-cachan.fr

Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks *

Keywords: Verification, Cryptographic protocols, Formal methods, Dictionary attacks, Probabilistic encryption

We consider the problem of formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well studied deduction rules for symmetric and public key encryption often called Dolev-Yao rules with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables which represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.

Introduction

The formal verification of cryptographic protocols in an insecure network is known to be an undecidable problem, even with strong restrictions. The undecidability results from several factors: the ability of agents to generate fresh random data (nonces), the unlimited size of terms, the unboundedness of the number of sessions. Removing the last condition is sufficient for decidability (while removing the others is not, see [START_REF] Durgin | Undecidability of bounded security protocols[END_REF][START_REF] Comon | Tree Automata with One Memory, Set Constraints and Cryptographic Protocols[END_REF][START_REF] Amadio | On Name Generation and Set-Based Analysis in the Dolev-Yao Model[END_REF]) and several procedures have been proposed to decide the protocol insecurity problem with a bounded number of sessions [START_REF] Amadio | On the Reachability Problem in Cryptographic Protocols[END_REF][START_REF] Millen | Constraint Solving for Bounded-Process Cryptographic Protocol Analysis[END_REF] and [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF] where the problem is shown NP-complete.

In the works cited above, as well as in many other approaches concerning automated verification of security protocols, the intruder model is based on the so-called Dolev-Yao deduction rules for publickey encryption [START_REF] Dolev | On the Security of Public-Key Protocols[END_REF]). This deduction system specifies how the attacker can obtain new information from previous knowledge, which he has obtained by silently eavesdropping the communication network (it is a passive intruder behavior) and by participating to protocol by sending new messages, thus provoking honest participants to reply according to the protocol rules (in this latter case, the intruder has an active behavior). The deduction abilities of the intruder still comply to the perfect cryptography assumption, which states that the only way to obtain knowledge about an encrypted plaintext is to know the decryption key, and there is no way to obtain the key from ciphertexts. This abstraction happened to be accurate enough to reveal many logical attacks on known cryptographic protocols in an automated way. However, it may be too strong to capture some specific attacks that may occur in real word situations. For instance, in the Dolev-Yao model it is not possible to take into account attacks based on algebraic properties of cryptographic operators, like exclusive or, in presence of which the protocol insecurity problem with a bounded number of sessions is still decidable [START_REF] Comon-Lundh | Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or[END_REF][START_REF] Chevalier | Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Product in Exponents[END_REF].

In this paper, we formalize another interesting attack technique which appears to be out of the scope of the Dolev-Yao model: the so-called dictionary attacks [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF][START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF]. In some situations, an intruder is able to guess poorly chosen passwords (or other data belonging to a reasonably small domain) by an offline brute force iteration through a dictionary, using messages previously collected on the network to verify his guess at each step. The reason for the interest of this kind of attacks is simple: password-guessing attacks are a common avenue for breaking into systems, and the application of formal method to analyze password protocols can help.

There are number of facets to the study of dictionary attacks. At the beginning of the nineties, several examples of dictionary attacks have been analyzed, and some countermeasures have been proposed to design protocols resistant to this kind of attacks [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF][START_REF] Gong | Optimal Authentication Protocols Resistant to Password Guessing Attacks[END_REF][START_REF] Tsudik | Some Remarks on Protecting Weak Keys and Poorly-Chosen Secrets from Guessing Attacks[END_REF][START_REF] Bellovin | Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks[END_REF]. Lot of effort seems to have been put into using provable security [START_REF] Goldwasser | Probabilistic Encryption[END_REF] for analysis such protocols that use poorlychosen data [START_REF] Wu | The Secure Remote Password Protocol[END_REF][START_REF] Bellare | Authenticated Key Exchange Secure against Dictionary Attacks[END_REF][START_REF] Katz | Efficient Password-Authenticated Key Exchange Using Human-Memorable Passwords[END_REF]. However, the automatic verification methods which have been used successfully guessNP.tex; 1/06/2005; 8:34; p.2 for cryptographic protocol analysis, were not used at this time for password protocols. Perhaps this is due to the complex nature of dictionary attacks, whose analysis involves complications similar to combining cryptanalytical and abstract protocol analysis. Only recently, some procedures have been implemented to automatically find dictionary attack [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF][START_REF] Corin | Guess what? Here is a new tool that finds some new guessing attacks[END_REF][START_REF] Cohen | Proving Cryptographic Protocols Safe from Guessing Attacks[END_REF][START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF]. However, neither the complexity or the completeness of the procedures, nor the decidability of the problem have been studied in these works.

We propose decision procedure (and complexity) results for the decision of the security of protocols against dictionary attacks, when the number of sessions is bounded. Our model of dictionary attacks is based on an inference system extending the Dolev-Yao rules for symmetric and public-key encryption to take into account probabilistic encryption and offline dictionary attacks. Our inference rules for dictionary attacks are semantically closed to the definition of [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF]. The first result is a locality result showing that the intruder deduction problem is PTIME. The second result concerns the case where the intruder is active. We show that the problem is NP-complete by reducing it to the problem of the satisfaisability of symbolic constraint systems. Though this complexity is the same as in the Dolev-Yao model, see [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF], the proofs of our decision procedure are made dramatically harder by the introduction of guessing abilities in the inference system. Indeed, some basic results easy to prove in the standard Dolev-Yao model are not basic anymore in our extended model.

Moreover, the extension of the intruder deduction model to probabilistic encryption operators is an important contribution when considering vulnerability to dictionary attacks. Indeed, this kind of encryption can be used as a countermeasure to prevent dictionary attacks.

After some motivating examples of dictionary attacks (Section 2) and preliminary definitions of protocols syntax and semantics (Section 3) we define in Section 4 our extended intruder model which formalize in particular dictionary attacks and we give in Section 5 decision problems (intruder deduction, trace insecurity, protocol insecurity) we are interested in. We then prove a locality result from which it follows that the intruder deduction problem protocol can be decided in polynomial time (Section 6). This yields to an NP algorithm for the trace and protocol insecurity problems in presence of a passive intruder. In Section 7, we reduce the trace and protocol insecurity problems in presence of an active intruder to the satisfaisability of symbolic constraint systems (where each individual constraint is a lifting of the problem defined in the passive case). We give in Section 8 a nondeterministic polynomial time procedure to decide the satisfaisability of such constraint systems. A comparison with other models based on CSP [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF] and the applied pi-calculus [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF] can be found at the end of the paper.

A preliminary version of this work as been published in [START_REF] Delaune | A Theory of Dictionary Attacks and its Complexity[END_REF].

Examples

A simple subcase of dictionary attacks is the known-plaintext attacks, where an intruder intercepts a message {M } K encrypted with a weak password K and whose encrypted content M is known (for instance an instruction like hello). The intruder can then try to decrypt this ciphertext with each word in a dictionary one by one, and verify for each guess d whether the value obtained is the known plaintext M , which means with a high probability that d = K. This method also works against a challenge-response scheme where a server sends to a user A a random number (nonce) N as a challenge and A responds with {N } K , where K is its weak password.

The examples below show that similar attacks are also possible in some cases where the plaintext is not known, with more subtle techniques to verify the guesses.

Naive Vote Protocol and Probabilistic Encryption

Consider the following naive vote protocol:

0. A → S : {V } pub(S)
The voter A encrypts his vote V with the public key pub(S) of the vote server S. The server decrypts the message with his private key priv (S) and registers the vote. The security requirement is that only A and S know V . This protocol is secure if we assume strong encryption primitives: an intruder who intercepts the message {V } pub(S) will not be able to learn the vote V of A as long as he does not know priv (S). However, if we assume that the intruder knows a finite set D (reasonably small) of values that V can take, then he can deduce V without knowing priv (S): for each value d ∈ D, he encrypts d with pub(S) and verifies whether the ciphertext {d} pub(S) obtained is equal to {V } pub(S) , which means that the guess d = V . Therefore, an intruder able to eavesdrop the vote messages will be able to deduce who voted for whom.

The attack described above can be mounted only if the encryption scheme is deterministic. This means that encrypting a given message with a key always returns the same result. This is the case of encryption algorithms such as e.g. RSA and AES. To prevent such of failure, in guessNP.tex; 1/06/2005; 8:34; p.4 real vote protocols, the algorithms used for encryption often include random choices and therefore are probabilistic. This kind of encryption scheme was invented by Shafi Goldwasser and Silvio Miscali (Goldwasser and Micali, 1984) and recent practical implementations have been proposed. The idea behind probabilistic encryption is roughly that the encryption algorithm relies on some random value, chosen by the agent involving encryption. It means that encrypting several times the same plaintext with the same key returns different ciphertexts. However, the decryption function will return the same plaintext from all these ciphertexts.

Let us consider the naive vote protocol is based on probabilistic encryption. We model this situation by adding a third parameter to the encryption primitive, which represents the random choice performed by the agent before applying the encryption algorithm. Hence, we obtain:

0. A → S : {V } r pub(S)
Assume that the attacker intercepts the ciphertext C (i.e. {V } r pub(S) ). Even if he guesses V correctly, encrypting V with the public key of S, the result will be a completely different ciphertext C . He, therefore, cannot compare C and C , and so cannot know that he has guessed the message V correctly.

Handshake Protocol

Consider this challenge-response transaction which is commonly used in authentication protocols, see [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF]:

0. A → B : {N } ra pw (A,B) 1. B → A : {N + 1} rb pw (A,B)
A generates a nonce N and sends it to B encrypted probabilistically with the symmetric key pw (A, B) (the cryptosystem is symmetric in this example). B decrypts the message, computes N + 1, and returns to A the encrypted result. In the standard Dolev-Yao model, an intruder who intercepts the messages cannot deduce pw (A, B), and the incrementation of N in the second message prevents replay attacks. However, if pw (A, B) is a poorly chosen password, and belongs to a finite dictionary D, then the challenge-response transaction can be attacked in other ways: the intruder guesses d ∈ D and tries to decrypt both messages 0 and 1 with d. He obtains two values, v 0 and v 1 respectively. If v 1 = v 0 + 1, then the attacker has guessed the correct value d = K with high probability.

This dictionary attack has been used to exploit systems in the past, often quite successfully. Note that using probabilistic encryption do not allow to prevent the attack described above since the attack uses only the decryption algorithm which is necessarily deterministic.

Enhanced Kerberos Protocol

As outlined in [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF], the Kerberos protocol [START_REF] Steiner | Kerberos: An Authentication Service for Open Network Systems[END_REF] contains some messages which make it vulnerable to knownplaintext attacks. To avoid this problem, [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF] propose the following modification, which we shall use as a running example. Like in Section 2.2, probabilistic encryption do not prevent the attack described below, hence, for sake of clarity, we shall use below the deterministic encryption symbol with only two parameters.

0. A → S : {A, B, N 1 , N 2 , Ca, {Ta} pw(A,S) } pub(S) 1. S → A : {N 1 , K ⊕ N 2 } pw(A,S) , {A, K, Ts} pw (B,S) 2. A → B : {A, K, Ts} pw (B,S)
In this protocol, the user A obtains from S a secret key K to be shared between himself and the ticket-granting service B. Afterward, A can obtain tickets for other services from B using this key K. The symbol ⊕ denotes the bit-wise exclusive or operation. We do not consider any algebraic properties of this operation here and rather see it as an encryption: K ⊕ N is equivalent to {K} N . pub(S) is the public-key of the server S, and pw (A, S), pw (B, S) are symmetric keys (passwords) that A and B respectively share with S.

The password pw (B, S) can be assumed to be well-chosen since B is a server, but the password pw (A, S) of the user A is likely to come from a dictionary. This protocol implements some protections against dictionary attacks on pw (A, S), using the nonces N 1 , N 2 , the confounder Ca (which is a long nonce whose role is to confound attacks like in Section 2.2), and the timestamps Ta and Ts, added in order to prevent the replay of messages 0 and 1. We refer the reader to [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF] for the details about this protocol.

As described in [START_REF] Tsudik | Some Remarks on Protecting Weak Keys and Poorly-Chosen Secrets from Guessing Attacks[END_REF][START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF][START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF] for similar protocols, if the server S does not record the timestamp Ta, and if moreover the clocks of S and A are not well synchronized, an intruder can replay a copy of an eavesdropped message 0 within the clock skew, making possible the attack described in Figure 1.

In the session β, the intruder replays A's message α.0, so as to get the server to issue (in β.1) another message using the same nonces N 1 and N 2 . Hence, N 1 can be used as a verifier to guess pw (A, S): the intruder can decrypt {N 1 , K ⊕N 2 } pw (A,S) and {N 1 , K ⊕N 2 } pw(A,S) with a value d chosen in a dictionary, and if the first field of the two values obtained is the same, then it means that the value guessed d = pw (A, S). After guessNP.tex; 1/06/2005; 8:34; p.6

α.0. A → S : {A, B, N 1 , N 2 , Ca, {Ta} pw (A,S) } pub(S) α.1. S → A : {N 1 , K ⊕ N 2 } pw (A,S) , {A, K, Ts} pw (B,S) β.0. I(A) → S : {A, B, N 1 , N 2 , Ca, {Ta} pw (A,S) } pub(S) β.1. S → I(A) : {N 1 , K ⊕ N 2 } pw (A,S) , {A, K , Ts } pw (B,S)
I guesses pw (A, S) offline

γ.0. I(A) → S : {A, B, M 1 , M 2 , Ci , {Ti} pw (A,S) } pub(S) γ.1. S → I(A) : {M 1 , K ⊕ M 2 } pw (A,S) , {A, K , Ts } pw (B,S) γ.2. I(A) → B : {A, K , Ts } pw(B,S)
The notation I(A) represents: on the left hand side of an arrow, the intruder I masquerading A to send a message, and on the right hand side of an arrow, the intruder intercepting a message intended for A. that, the intruder can impersonate A in a third session γ, with chosen nonces M 1 and M 2 , and he obtains in γ.1 the session key K which is assumed to be a secret shared between A, S and B.

Abstract Model for Protocols

We assume given a signature F containing the symbols , (pairing1 ), { } (deterministic encryption), { } (probabilistic encryption), some unary function symbols representing invertible functions, others representing one way functions, and three other special constructors: pw ( ) (for symmetric keys, or passwords shared between agents), pub( ) (for asymmetric public keys of agents), and priv ( ) (for the corresponding private keys).

The signature F contains also an arbitrary subset F 0 of constant symbols representing objects like keys, agent names, nonces... We also assume given an infinite set of variables X . The set of terms built with F and X is denoted by T (F , X ) and the subset of ground terms (terms without variables) T (F ). We denote vars(t) the set of variables occurring in a term t ∈ T (F , X ), and st(t) the set of subterms of t. These two notations are extended as expected to a structure T containing some terms: vars(T ) (resp. st(T )) is the union of the sets vars(t) (resp. st(t)) for every term t occurring in T .

Delaune, Jacquemard

We assume a linear well-founded ordering ≺ on the ground terms of T (F ) such that the constant 0 is minimal w.r.t. ≺. We shall use below the (well-founded) extension of ≺ to multisets of ground terms, see [START_REF] Dershowitz | Termination of rewriting[END_REF]. For sake of notations, given two substitutions σ 1 and σ 2 , we write σ 1 σ 2 iff img(σ 1 ) img(σ 2 ) (img(σ i ) is the multiset of all xσ such that x ∈ dom(σ i )).

Among the terms of T (F ), we distinguish a finite subset G of guessable symbols such that G ⊆ F 0 ∪ {pw (t), pub(t), priv(t)|t ∈ T (F )}. Theses symbols all have the distinctive feature of taking their values in finite (quite small) dictionaries known by everyone. Moreover, we assume a bijective mapping denoted -1 from T (F , X ) into T (F , X ) which associates to a public key the corresponding private key and reciprocally. More precisely, if k ∈ F 0 represents an asymmetric key, public or private, then k -1 ∈ F 0 represents its private (resp. public) counterpart. For every t ∈ T (F , X ), we have pub(t) -1 = priv (t) and priv (t) -1 = pub(t), and for every other s ∈ T (F , X ) (which does not represent a public or private key), we have s -1 = s.

A substitution is the term morphism extension of a finite mapping {x 1 → t 1 , . . . , x n → t n } where x 1 , . . . , x n ∈ X and t 1 , . . . t n ∈ T (F , X ). If t 1 , . . . t n ∈ T (F ), the substitution is called ground. As usual, the application of a substitution σ to a term t and the composition of substitutions σ 1 by σ 2 are written in postfix notation, respectively tσ and σ 1 σ 2 . A substitution σ is grounding for t if tσ ∈ T (F ). Given two terms u and v the replacement of u by v, denoted by [u → v], maps every term t to the term t[u → v] which is obtained by replacing all occurrences of u in t by v. Note that the result of such replacement is uniquely determined.

In the paper, |S| denotes the cardinal of the set S. The size t of a term t is the number of nodes in t. This notation is extended as expected to a set of terms T . The dag-size T d of a term container T is the number of distinct subterms of T (i.e. the number of nodes in a representation of T as a dag with maximal sharing). More details about the dag representations of terms can be found in [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF].

Protocol Syntax

Definition 1. (protocol) A protocol is a finite set of programs, each program being a finite sequence of pairs of instructions of the form recv(r); send(s) with r, s ∈ T (F , X ).

It is semantically equivalent to consider programs which are sequences of send and recv in an arbitrary order, since we may add some instructions send(0) and recv(0) where 0 ∈ F 0 \ G is a special constant known to everyone.

The formalism used here to model protocols is close to so-called strand spaces [START_REF] Thayer | Strand Spaces: Proving Security Protocols Correct[END_REF] and is sufficiently general to describe a lot of protocols. However, like the strand space model, it suffers from some drawbacks. For instance, it does not permit to model an agent who receives a ciphertext and who later verifies after he receives the decryption key.

Example 1. (Kerberos protocol) The Kerberos protocol variant described in Section 2.3 is made of three programs:

role A : 0. recv(0); send({x 0 A , x 0 B , x 0 N 1 , x 0 N 2 , x 0 Ca , {x 0 T a } x 0 pw (A,S) } x 0 pub(S) ) 1. recv({x 0 N 1 , x 0 K ⊕ x 0 N 2 } x 0 pw (A,S) , x 0 ); send(x 0 ) role S : 0. recv({x 1 A , x 1 B , x 1 N 1 , x 1 N 2 , x 1 Ca , {x 1 T a } pw (x 1 A ,x 1 S ) } x 1 pub(S)
);

send({x 1 N 1 , x 1 K ⊕ x 1 N 2 } pw(x 1 A ,x 1 S ) , {x 1 A , x 1 K , x 1 T s } pw (x 1 B ,x 1 S ) ) role B : 0. recv({x 2 A , x 2 K , x 2 T s } x 2 pw (B,S)
); send(0)

The symbols x i A . . . (i = 0, 1, 2) are distinct variables of X . Note that A receives (in step 1) the ciphertext {A, K, Ts} pw (B,S) as a value x 0 , and forwards it blindly (to B), since he does not know B's password pw (B, S). The program of role B implements only the reception of the last message by B.

Protocol Semantics

Definition 2. (process) Given a protocol P, a process (p, σ) following P is made of a program p ∈ P and a ground substitution σ whose domain is a subset of vars(p).

Every program of the protocol P defines a role, and a process (p, σ) is an honest agent playing the role p. A configuration is a pair (S, N ) where S is a finite set of processes whose programs have disjoint sets of variables, and N is a set of ground terms representing the messages currently in the network (the message sent and not yet received).

We define operational semantics for the execution of processes. Each step changes the running configuration, denoted (S, N ) i (S , N ) for some 0 ≤ i < |S|, if the i th process of S is (p, σ) with p = recv(r); send(s); p and:

the instruction recv(r) is executed properly, i.e. there exists a ground substitution θ such that rσθ ∈ N , S is obtained from S by updating the i th process to (p , σ ), where σ = σθ, and leaving the other process unchanged, and the message rθ is later removed from the network, -the instruction send(s) is executed, by adding the term sσ to the network, i.e. N = (N \ {rθ}) ∪ {sσ }.

We assume that the protocol and the initial configuration are such that after every such step, sσ is ground. It means that the messages sent are built from values completely defined by the previous steps of the protocol and the initial knowledge of the processes. More formally:

Definition 3. (runnable) An initial configuration ({(p 0 , σ 0 ), . . . , (p m , σ m )}, N 0 ) of a protocol P is called runnable iff for each i ≤ m such that the program p i is the sequence (recv(r i,j ); send(s i,j
)) j≤n , for each j ≤ n, we have:

vars(s i,j ) ⊆ dom(σ i ) ∪ k<j vars(r i,k ) Example 2. (Kerberos protocol)
The set of processes ((p 0 , σ 0 ), (p 1 , σ 1 ), (p 2 , σ 2 )) described below is the first component of a runnable initial configuration of the protocol of Example 1:

σ 0 =    x 0 A → A, x 0 B → B, x 0 S → S, x 0 Ca → Ca, x 0 N 1 → N 1 , x 0 N 2 → N 2 , x 0 Ta → Ta, x 0 pub(S) → pub(S), x 0 pw (A,S) → pw (A, S),    σ 1 = x 1 K → K, x 1 Ts → Ts, x 1 S → S, x 1 pub(S) → pub(S) σ 2 = {x 2 pw (B,S) → pw (B, S)}
where A, B, S, N 1 , N 2 , Ca, Ta, K, Ts are constants of F 0 .

In this paper, we are interested in proving the reachability (from a given runnable initial configuration) of a configuration where some security property is compromised, assuming the presence of an intruder who has some control over the communication network, as defined in the next section.

Axiom (A) u ∈ T T u Pairing (P) T u T v T u, v Unpairing (UL) T u, v T u Unpairing (UR) T u, v T v Encryption (E) T u T v T {u} v Decryption (D) T {u} v T v -1 T u Figure 2. The Standard Dolev-Yao Model.

Intruder Model

We consider now an intruder with some control over the communication network. He is able to read any message in the network and to analyze the messages read in order to deduce new messages, using some inference rules like the ones defined in the following subsections 4.1, 4.2, and 4.3. When the abilities of the intruder are limited to the two former actions, we call him a passive intruder. The problems of the complexity of intruder deduction, as well as protocol verification in presence of a passive intruder with guessing abilities are studied in Section 6.

The intruder can also be assumed to be able to send new messages to the network: he is then called an active intruder. The verification of protocol insecurity in presence of an active intruder is studied in Section 7 and 8.

We shall give more formal definitions of passive and active intruders in Section 4.6.

Dolev-Yao Deduction Model

The most widely used deduction relation representing the analysis abilities of an intruder is often refereed as Dolev-Yao model after [START_REF] Dolev | On the Security of Public-Key Protocols[END_REF], though the formalism of this paper is not exactly the same as the one used here. It is denoted by a "sequent" T u (the intruder is able to deduce the term u ∈ T (F ) from the finite set of terms T ⊆ T (F )), and is defined by the inference rules in Figure 2.

In this model, the intruder can form pairs and ciphertexts from known terms (rules P, E), decompose pairs (rules UL, UR), and decrypt ciphertexts, providing that he can deduce the decryption key (rules D). The latter condition is known as the perfect cryptography assumption.

Enc. (Ep) T u T v T r T {u} r v Dec. (Dp) T {u} r v T v -1 T u Figure 3. Probabilistic Encryption à la Dolev-Yao.

Probabilistic Encryption

We have seen the importance of the probabilistic encryption primitive in the context of dictionary attacks (see Section 2.1). We propose here an extension of the above Dolev-Yao model by adding two inference rules, described in Figure 3, to deal with probabilistic encryption. The rule (Ep) says that the intruder can form a ciphertext from a known term (plaintext) u, and a random value r. The ciphertext depends on the input r. The rule (Dp) do not depends on the random input r: a decryption algorithm is necessarily deterministic.

The Dolev-Yao model of Section 4.1 extended with the two inference rules displayed in Figure 3 is called the Dolev-Yao model with probabilistic encryption.

Guessing Model

We shall now describe how dictionary attacks can be modeled as an extension of the above Dolev-Yao model. For this purpose, we refer to the following definition of dictionary attacks from [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF]) that claims to generalize the definition of [START_REF] Gong | Protecting Poorly Chosen Secrets from Guessing Attacks[END_REF]:

A dictionary attack consists of the intruder guessing a value d, and then verifying it. The verification will be by the intruder using d to produce a value v, which we call the verifier and can take a number of different forms:

1. the intruder knew v initially, (see Section 2.1)

2. the intruder produced v in two distinct ways from d, (see Section 2.2) 3. v is an asymmetric key, and the intruder knows v's inverse from somewhere.

Intuitively, the intruder knows that g ∈ G belongs to a dictionary, in which he picks d. If the verifier v, built with d and the intruder's knowledge ensures one of the three conditions above, then the probability is high that d = g. We shall use a variant of the rules of Figure 2 in order to model the guessing of a d, and the production of a verifier v ∈ T (F ) by the intruder. In the rules of this variant, presented in Figure 4 introduce a new form of sequent T/T v, which means that if the intruder knows the messages in T ⊆ T (F ) and guessed values for the symbols of T ⊆ G, then he can build the verifier v ∈ T (F ). In other words, he can deduce that v belongs to a finite set that he can compute. The members of T and T are respectively called the strong and weak hypotheses of T/T v, and v is called its target. Figure 5 introduces a deduction rule Compare which models the verification of a guess d with one of the 3 cases described above. The conditions (i) and (ii) ensure that one of the proofs P 1 or P 2 really uses the guessable value g and it is necessary to prevent certain false attacks (see Section 4.5). The normality condition (ii) will prohibit deduction steps that simply undo previous steps. It refers to the notion of normal DY'-proof which is formally defined in Section 4.4. Lastly, (iii) ensures that the two proofs P 1 and P 2 do not end with the same instance of the same rule. Hence, the two ways to obtain the verifier v are really distinct.

Axiom u ∈ T (A ) T/∅ u Guess u ∈ G (G) T/u u Pairing T/T 1 u T/T 2 v (P ) T/T 1 ∪ T 2 u, v Encryption T/T 1 u T/T 2 v (E ) T/T 1 ∪ T 2 {u} v Unpairing T/T u, v (UL ) T/T u T/T u, v (UR ) T/T v Decryption T/T 1 {u} v T/T 2 v -1 (D ) T/T 1 ∪ T 2 u Enc. T/T 1 u T/T 2 v T/T 3 r (Ep ) T/T 1 ∪ T 2 ∪ T 3 {u} r v Dec. T/T 1 {u} r v T/T 2 v -1 (Dp ) T/T 1 ∪ T 2 u
P 1    ... u 1 ... ... u n 1 (R 1 ) T/T 1 u P 2    ... v 1 ... ... v n 2 (R 2 ) T/T 2 v (C) T g where: (i) g ∈ T 1 ∪ T 2 (ii) P 1 and P 2 are normal DY'-proofs (iii) R 1 = R 2 or {u, u 1 , .., u n 1 } = {v, v 1 , ..., v n 2 } (iv) u = v or u = v -1 Figure 5. The Compare Rule.
The inference system made of the rules displayed in Figures 2,3 and 4 and the rule Compare of Figure 5 is called the guessing model.

Proof Trees

Definition 4. (proof ) A DY-proof (resp. DY'-proof) P of T u (resp. T/T u) is a tree such that:

every leaf of P is labeled with some v ∈ T (resp. v ∈ T ∪ G), -for every node n labeled with s with k sons labeled with s 1 , . . . , s k , (s 1 , . . . , s k , s) is an instance of an inference rule R of Figure 2, 3 (resp. Figure 4) which s 1 , . . . , s k are the premises and s the conclusion. We say that P contains the instance (s 1 , . . . , s k , s), or ends with this instance (or simply with rule R) if n is the root of P , -the root is labeled with some T u (resp. T/T u).

A guessing-proof is a tree ending with an instance of the rule Compare and whose two sons are DY'-proofs which satisfy the conditions (i)-(iv) of Figure 5.

Let P be a DY-proof (resp. DY'-proof). We say that the pair u 1 , u 2 is decomposed in P if P contains an instance of the rule (UL)

or (UR) (resp. (UL') or (UR')) whose target of the premise is u 1 , u 2 . Similarly, the ciphertext {u 1 } u 2 (resp. {u 1 } u 3 u 2 ) is said decomposed in P if P contains an instance of the rule (D) or (D') (resp. (Dp) or (Dp')) whose targets of premises are {u 1 } u 2 and u -1 2 (resp. {u 1 } u 3 u 2 , u -1 2 and u 3 ).
guessNP.tex; 1/06/2005; 8:34; p.14 Definition 5. (minimality) A DY-proof or DY'-proof P is called minimal if it does not contain two nodes on the same path labeled by sequents with the same target.

The following notion of normal proof is used in the definition of the rule Compare. Definition 6. (normality) A DY'-proof P is called normal if the rewrite rules defined in Figure 6 can not be applied to P .

The normality of DY-proofs is defined with a similar set of rewrite rules, where (D', E', P', UL', UR', Dp', Ep') are replaced respectively by (D, E, P, UL, UR, Dp, Ep).

The rewrite rules of Figure 6 correspond to algebraic properties of the operators. For instance, the first rule expresses that the composition of encryption and decryption (with the keys of the same keypair) is the identity. The third rewrite rule states that this is also the case of the composition of decryption and deterministic encryption. To be more precise, the rewrite rules described in Figure 6 are used to model the algebraic properties listed below. The pairing, the left and right projection operators are respectively denoted P, UL, UR. The encryption and decryption operators, and their probabilistic counterparts, are respectively denoted E, D, Ep, Dp.

-D(E(x, y), y -1 ) = x and E(D(x, y -1 ), y) = x, -Dp(Ep(x, y, z), y -1 ) = x, -UL(P(x 1 , x 2 )) = x 1 , UR(P(x 1 , x 2 )) = x 2 and P(UL(x), UR(x)) = x.

Note that there is no analogous of the rule E(D(x, y -1 ), y) = x, for Ep and Dp. Indeed, while the decryption of a ciphertext {u 1 } r u 2 returns u 1 , the probabilistic re-encryption of u 1 returns {u 1 } r u 2 , with r = r and hence this ciphertext differs from the original one. In the setting of dictionary attacks, it is crucial to be able to find proof which are not equivalent modulo these rewrite rules, as explained in Section 4.5.

Note that every minimal DY'-proof is normal. Indeed, every left member of rewrite rule of Figure 6 contains two nodes on the same path labeled by sequents with the same target (but not necessarily with the same set of weak hypotheses).

Lemma 1. If there exists a DY-proof of T u, then there exists a minimal DY-proof of T u.

Q 1 T/T 1 u 1 Q 2 T/T 2 u 2 (E ) T/T 1 ∪ T 2 {u 1 } u 2 Q 3 T/T 3 u -1 2 (D ) T/T 1 ∪ T 2 ∪ T 3 u 1 → Q 1 T/T 1 u 1 Q 1 T/T 1 u 1 Q 2 T/T 2 u 2 Q 3 T/T 3 r (Ep ) T/T 1 ∪ T 2 ∪ T 3 {u 1 } r u 2 Q 4 T/T 4 u -1 2 (Dp ) T/T 1 ∪ T 2 ∪ T 3 ∪ T 4 u 1 → Q 1 T/T 1 u 1
We also have an additional rule for the deterministic encryption:

Q 1 T/T 1 {u 1 } u 2 Q 2 T/T 2 u -1 2 (D ) T/T 1 ∪ T 2 u 1 Q 3 T/T 3 u 2 (E ) T/T 1 ∪ T 2 ∪ T 3 {u 1 } u 2 → Q 1 T/T 1 {u 1 } u 2
Concerning the pairing symbol, we have the following rules:

Q 1 T/T 1 u 1 Q 2 T/T 2 u 2 (P ) T/T 1 ∪ T 2 u 1 , u 2 (UL ) T/T 1 ∪ T 2 u 1 → Q 1 T/T 1 u 1
and a similar rewrite rule for (P',UR'). Proof. We can show this result by induction on the proof P of T u. If P is reduced to an instance of the rule (A), then it is obvious. Otherwise, by induction hypothesis the direct subproofs of P are minimal. So, if P is not minimal, there exists two nodes on the same path labeled by the sequent T u and one of these is the root of P . Hence, the other is the root of a minimal proof of T u.

Q 1 T/T 1 u 1 , u 2 (UL ) T/T 1 u 1 Q 2 T/T 2 u 1 , u 2 (UR ) T/T 2 u 2 (P ) T/T 1 ∪ T 2 u 1 , u 2 → Q i T/T i u 1 , u 2 for i = 1, 2.
However this result is not valid for DY'-proofs, unless the set of weak hypotheses is empty for every node. The problem with DY'-proofs is that we can not assume that two nodes on the same path and with the same target have the same set of weak hypotheses.

Rule Compare

In this section, we shall explain in more details the conditions of application of the rule Compare. We also provide some examples to illustrate this rule.

Condition (ii) By the condition (i), one son P 1 or P 2 contains the guess g among the weak hypotheses, but it is not sufficient to ensure that P 1 or P 2 really depends on the guess g: only the condition (ii) ensures this property. Indeed, without this condition, there would be a guessing-proof with the two (non normal) sons below, which would mean that the intruder is able to guess any g ∈ G from any message m known by the intruder.

m ∈ T (A ) T/∅ m m ∈ T (A ) T/∅ m g ∈ G (G) T/{g} g (P ) T/{g} m, g (UL ) T/{g} m
The idea behind condition (ii) is that in a proof like the one above, re-obtaining the value m after the successive applications of pairing (P') and projection (UL') is not a commitment that the guess of g is correct. It is just an algebraic property of the operators, characterized by a rewrite rule of Figure 6.

Condition (iii)

The condition (iii) also prevents certain false attacks. Consider the program which is made up of one pair of instructions recv(x); send( x, x ). An agent executing this program will answer to any message m with the pair m, m . Thus, if the intruder knows the message m = {n} r g , he obtains from the agent the answer {n} r g , {n} r g . The two DY'-proofs below verify the conditions (i), (ii) and (iv) of the rule Compare. However, the condition (iii) is not verified and these two proofs indeed represent a fake dictionary attack. Intuitively, in this attack, the intruder guesses a value d for g, computes the left and right projections ((UL ) and (UR )) of m, tries to decrypt each projection with d (rule (Dp )) and compares the values obtained. But, since both projections are {n} r g , the values will always be equal, even when d = g. We see that the two proofs differ (the first step is left or right projection) but that their last instance is the same (decryption applied to the same premises).

{n} r g , {n} r g ∈ T (A ) T/∅ {n} r g , {n} r g (UL ) T/∅ {n} r g g ∈ G (G) T/{g} g (Dp ) T/{g} n {n} r g , {n} r g ∈ T (A ) T/∅ {n} r g , {n} r g (UR ) T/∅ {n} r g g ∈ G (G) T/{g} g (Dp ) T/{g} n
Note that if the two ciphertexts of the pair would have been obtained by two distinct applications of the probabilistic encryption algorithm, we would have obtained a pair which is composed of two distinct terms, i.e. {n} r g , {n} r g , allowing surprisingly the intruder to mount a dictionary attack.

We illustrate the application of the rule Compare on the protocols given in Section 2.

Example 3. (naive vote protocol) Let T = {{V } pub(S) , pub(S)} and G = {V }. The following guessingproof models the guessing attack performed by the intruder on V :

V ∈ G (G) T/{V } V pub(S) ∈ T (A ) T/∅ pub(S) (E ) T/{V } {V } pub(S)
{V } pub(S) ∈ T (A )

T/∅ {V } pub(S) (C) T V Example 4. (handshake protocol) Let T = {{N } ra pw (A,B) , {N + 1} rb pw(A,B) } and G = {pw (A, B)}.
The required guessing-proof of T pw (A, B) can be obtained by applying the rule Compare to the two DY'-proofs below:

{N } pw(A,B) ∈ T (A ) T/∅ {N } ra pw (A,B) pw (A, B) ∈ G (G) T/{pw (A, B)} pw (A, B) (Dp ) T/{pw (A, B)} N T/{pw (A, B)} N + 1 {N + 1} rb pw (A,B) ∈ T (A ) T/∅ {N + 1} pw (A,B) pw (A, B) ∈ G (G) T/{pw (A, B)} pw (A, B) (Dp ) T/{pw (A, B)} N + 1
Note that the conditions (i)-(iv) required to apply the rule Compare are satisfied.

Passive and Active Intruder

A ground term u ∈ T (F ) is called deducible from a set of ground terms N ⊆ T (F ) if and only if there exists a finite subset T of N and a DY-proof of T u. We note ded(N ) the set of ground terms deducible from N .

In order to define the transition performed by the intruder, we extend the configurations of the system with a third component representing the intruder's knowledge. Therefore, a configuration is a triple (S, N, K) where S and N are as in Section 3.2 and K ⊆ T (F ). The transitions of the intruder, denoted , are defined as follows: listen (S, N, K) (S, N, K ∪ {s}) for some s ∈ N deduce (S, N, K) (S, N, K ∪ {s}) if s ∈ ded(K) write (S, N, K) (S, N ∪ {s}, K) for some s ∈ K divert (S, N, K) (S, N \ {s}, K) for some s ∈ N We define a passive intruder as able of performing the transitions listen and deduce and an active intruder as able of performing the two latter transitions and moreover write and divert.

Finally, we define the relation g , for g ∈ G, by (S, N, K) g (S, N, K ∪ {g}), if and only if there exists a finite subset T of K and a guessing-proof of T g.

Security Problems

The first problem, we are interested in, is the so-called intruder deduction problem, which is the following one: OUT: Is s deducible from T knowing that G are guessable values?

In other words, does there exists a proof of T s in the guessing model ?

There are two factors of non determinism in the semantics of protocols and intruder defined respectively in Sections 3 and 4:

the selection of the process who is going to proceed, -the choice, by the intruder, of a value that he will be trying to guess offline, and when he makes the offline dictionary attack.

The following definition of interleavings is a characterization of these two choices.

Definition 8. (interleaving) Given an initial configuration S = ({(p 0 , σ 0 ), . . . , (p m , σ m )}, N 0 ) of a protocol P, an interleaving of S is a finite sequence I of values which can be either terms of G or integers in 0...m (indices of processes of S) such that the number of occurrences of every index i in I is smaller than or equal to the number of instruction pairs in p i .

Hence, an interleaving defines a scenario for processes execution and intruder guessing in a potential attack. The problem of trace insecurity consists in deciding whether such a scenario can be directed by the intruder, and whether, when following this scenario, the system reaches a critical state.

We define the relation → i on configurations, for an integer i, by → i := * i * ( * denotes the reflexive and transitive closure of , and i is extended to triples as expected) and we define the relation → g , for g ∈ G, by → g := * g * . The relation → I , for an interleaving I, is defined recursively as follows: → ∅ is the identity, → I,i := → I → i for an integer i (I, i denotes the interleaving obatined by appending i to I) and → I,g := → I → g for g ∈ G.

Definition 9. (Trace Insecurity problem (TI))

IN: a protocol P, a runnable initial configuration (S 0 , N 0 ) of P, a finite set K 0 ⊂ T (F ) (the initial knowledge of the intruder), an interleaving I of (S 0 , N 0 ), and a ground term s ∈ T (F ).

OUT: does there exists (S, N, K) such that (S 0 , N 0 , K 0 ) → I (S, N, K) and s is deducible from K?

We study in Section 6, the case of a passive intruder. In particular, we prove that the intruder deduction problem is decidable in PTIME. This yields to an NP decision procedure for the trace insecurity problem in presence of a passive intruder. Sections 7 and 8 are devoted to prove that the trace insecurity problem is NP-complete when the intruder is active.

Remark 1. For sake of simplicity, the signature F and the set G of guessable terms are assumed fixed, hence their size is a constant in the complexity results below. However, the complexity results would remain the same if G would be part of the input of the problem.

We can express several trace properties of protocols as instances of (TI), like for instance failure of authentication (one process p completes the protocol presumably with an interlocutor p whereas p did not even start to run, and hence p has been fooled in communicating only with the intruder), or confidentiality.

The problem of the existence of an interleaving I, given P, G, (S 0 , N 0 ), K 0 and s as above, returning a positive answer to (TI) is sometimes called Protocol Insecurity (PI) in the literature. The number of processes and their size is bounded by S 0 , and hence the length of every possible interleaving is polynomially bounded in this measure. Therefore, a consequence of the results of Sections 6, 7 and 8 is that (PI) is decidable in NP in presence of a passive or active intruder.

Decision Procedures in Presence of a Passive Intruder

When the intruder is passive, the only messages circulating over the network are sent by the protocol participants (the processes). Given a protocol P, an initial configuration (S 0 , N 0 ), and an interleaving I, the set T of messages known by the intruder at the end is bounded and can be computed in advance (in non-deterministic polynomial time). Therefore, in this case, the trace insecurity problem (w.r.t. P, (S 0 , N 0 ), I, and some K 0 ⊂ T (F ) and s ∈ T (F )) is reducible to the existence of one DY-proof and some guessing-proofs. The complexity of the decision of the existence of (DY, DY', guessing) proofs are given in Section 6.2. Then, we give complexity results for the problems (ID, TI, PI) presented in Section 5 for the case of a passive intruder. These latter results are based on technical lemmas proved in Section 6.1.

Locality

The notion of locality was coined by [START_REF] Mcallester | Automatic Recognition of Tractability in Inference Relations[END_REF] to characterize theories with a deduction problem decidable in polynomial time. We follow a similar approach and prove below three locality results for, respectively, the Dolev-Yao and Dolev-Yao' model with probabilistic encryption, and the guessing model.

The proposition 1 is a locality result for DY-proofs.

Proposition 1. A normal DY-proof P of T u contains only terms in st(T ∪ {u}). If moreover P ends with a decomposition rule (A, UL, UR, D, Dp), then P contains only terms in st (T ).

Proof. We prove the following results simultaneously by induction on the proof P of T u:

1. P contains only terms in st(T ∪ {u}),

2. if the last inference rule of P is a decomposition rule (A, UL, UR, D, Dp), then P contains only terms in st(T ).

We consider all possible cases for the last inference rule:

rule (A), the result is straightforward.

rule (E), then u = {u 1 } u 2 . By induction hypothesis (1), the proof P i (i = 1, 2) of T u i contains only terms in st(T ∪ {u i }). So the proof which consists of applying the rule (E) on the proofs P 1 and P 2 contains only terms in st(T ∪ {u}).

rule (P) and (Ep), it is similar to (E).

rule (UL), then we have a normal DY-proof P 1 of T u, v for which the last inference rule is necessarily a decomposition rule by normality of the proof P . By induction hypothesis (2), P 1 contains only terms in st(T ). Hence u, v ∈ st(T ), and we deduce that P contains only terms in st(T ).

rule (UR), it is similar to (UL).

rule (Dp), then we have the following derivation:

P 1 . . . T {u} r k P 2 . . . T k -1 (Dp) T u
We consider the last inference rule of P 1 . This rule is necessarily (A, UL, UR, D, Dp). (Ep) is impossible by normality of P . Now, we apply the induction hypothesis (2) and obtain that P 1 involves only terms in st(T ). We distinguish two possible cases. Firstly, if k is a symmetric key then k -1 = k. By induction hypothesis, P 2 involves only terms in st(T ∪ {k}) and we have k ∈ st(T ). So, P involves only terms in st(T ). Secondly, if k is an asymmetric key then k -1 ∈ F 0 ∪ {pub(t), priv (t)|t ∈ T (F )}. Consider the last inference rule of P 2 . This rule is necessarily (A, UL, UR, D, Dp). By induction hypothesis, P 2 involves only terms in st(T ). So P involves only terms in st(T ).

rule (D), it is similar to (Dp).

The proof of Proposition 1 can be straightforwardly extended to the following analogous locality result for the DY'-proofs.

Proposition 2. A normal DY'-proof P of T/T u contains only terms in st(T ∪ T ∪ {u}), and if P ends with a decomposition rule (G, A', UL', UR', D', Dp') then P contains only terms in st (T ∪ T ).

Proposition 3. A guessing-proof of T g contains only terms in st(T ∪ G).

Proof. A guessing-proof is made up of two normal DY'-proofs P 1 of T/T 1 u 1 and P 2 of T/T 2 u 2 . We distinguish two cases:

-u 1 = u 2
If the last inference rule of P 1 is (G, A', UL', UR', D', Dp'), then by Proposition 2, P 1 involves only terms in st(T ∪ T 1 ), and we have u 1 ∈ st(T ∪ T 1 ). So, since T 1 ⊆ G, we deduce that P involves only terms in st(T ∪ G).

If the last inference rule of P 2 is (G, A', UL', UR', D', Dp'), then we have also that P involves only terms in st(T ∪ G).

Otherwise both of P 1 and P 2 end with (E'), (Ep') or (P'); this case is inconsistent with the condition (iii).

u 1 is an asymmetric key and u 2 its inverse (u 2 = u -1 1 ) In this case, u 1 , u 2 ∈ F 0 ∪ {pub(t), priv (t)|t ∈ T (F )}, and the last inference rule of P 1 (and P 2 ) is (G, A', UL', UR', D', Dp'). By Proposition 2, P 1 (resp. P 2 ) involves only terms in st(T ∪ T 1 ) (resp. st(T ∪ T 2 )), and we deduce that P involves only terms in st(T ∪ G).

This result allows us to consider only subterms of the attacker's knowledge as potential verifiers to do a dictionary attack.

Decidability and Complexity

We show now (see Theorem 1 and Corollary 1) that when the intruder is passive, the intruder deduction problem and the trace insecurity problem (w.r.t. P, (S 0 , N 0 ), I, K 0 ⊂ T (F ) and s ∈ T (F )) can be decided by reduction to the existence of one DY-proof, for the deducibility of s (solved in Proposition 4), and several guessing-proofs(solved in Proposition 5).

Proposition 4. Given a set of messages T ⊆ T (F ), and a message u ∈ T (F ), the existence of a DY-proof of T u can be decided in polynomial time in T ∪ {u} d .

Proof. This result follows from Lemma 1, which guarantees the existence of a minimal (hence normal) DY-proof P of T u, and Proposition 1, which says that P only involves terms in st(T ∪ {u}). Indeed, in order to decide the existence of such a DY-proof, we construct (following [START_REF] Mcallester | Automatic Recognition of Tractability in Inference Relations[END_REF]), the set S of ground Horn clauses described in Figure 7 which implements a marking of every ground subterms t ∈ st(T ∪ {u}) such that there exists a proof of T t. Therefore, the existence of a proof of T u is equivalent to the non-satisfiability of S, hence to the non-satisfiability of a set of proposition Horn clauses (HORN-SAT) which size is polynomial in T ∪ {u} d . Hence, the existence of a DY-proof of T u can be decided in linear time in the size of S, i.e. in polynomial time in T ∪ {u} d .

Proposition 5. Given a set of messages T ⊆ T (F ), and a guessable symbol g ∈ G, the existence of a guessing-proof of T g can be decided in polynomial time in T ∪ G d .

Proof. Like in the above proof of Proposition 4, we reduce the problem with the construction of a set of ground Horn clauses S . In order to code the instances of the rule Compare with its conditions of application, we need though to add some additional information into the atoms of the clauses.

Given a set of messages T ⊆ T (F ), and a guessable symbol g ∈ G, we describe in Figure 8 a set S of ground Horn clauses from which one can derive the empty clause if and only if there exists a (normal) guessingproof of T g. Since the size of S is polynomial is T ∪ G d , this provides a decision procedure with the complexity wanted. The clauses of S are built with two binary predicates I 0 and I 1 . The ground terms occurring in the first arguments of atoms are elements of st(T, G), and in the second argument, one of the nullary symbols A, P , E, Ep, G corresponding to rules of the system of Figure 4, or UL(u), UR(u), D(u), Dp(u, v) with u, v ∈ st(T, G). The meaning of I 0 (u, l) is that there exists a normal DY'-proof which root is labeled with T/T u, with T ⊆ G, and moreover, if l is A, P , E, Ep or G then the proof ends by the corresponding inference rule, and if l = UL(v), then the proof has the following form (and similarly if l = UR(v) or if l = Dp(k, r)):

⇒ I(u 1 ) u 1 ∈ T I(u 1 ), I(u 2 ) ⇒ I( u 1 , u 2 ) u 1 , u 2 ∈ st(T ∪ {u}) I( u 1 , u 2 ) ⇒ I(u 1 ) I( u 1 , u 2 ) ⇒ I(u 2 ) I(u 1 ), I(u 2 ) ⇒ I({u 1 } u 2 ) {u 1 } u 2 ∈ st(T ∪ {u}) I({u 1 } u 2 ), I(u 2 -1 ) ⇒ I(u 1 ) I(u 1 ), I(u 2 ), I(u 3 ) ⇒ I({u 1 } u 3 u 2 ) {u 1 } u 3 u 2 ∈ st(T ∪ {u}) I({u 1 } u 3 u 2 ), I(u 2 -1 ) ⇒ I(u 1 ) I(u) ⇒
...

T/T u, v (UL )

T/T u

This second argument l is used to ensure the conditions (ii) and (iii) of the rule Compare. The meaning of I 1 (u, l) is the same as I 0 (u, l) except that moreover g ∈ T .

The measure G d in Proposition 5 should not be confused with the size of the dictionary. Indeed, recall that G is the set of guessable symbols, each of which is assume to belong to a finite dictionary. Therefore, |G| is rather the number of (finite) dictionaries.

Theorem 1. The intruder deduction problem is decidable in polynomial time.

S :=                                                                                      ⇒ I 1 (g, G) ⇒ I 0 (u, G) u ∈ G \ {g} ⇒ I 0 (u, A) u ∈ T I ε (u 1 , l), I ε (u 2 , l ) ⇒ I ε+ε ( u 1 , u 2 , P ) l = UL(u 2 ), l = UR(u 1 ), u 1 , u 2 ∈ st(T ) I ε ( u 1 , u 2 , l) ⇒ I ε (u 1 , UL(u 2 )) l = P , u 1 , u 2 ∈ st(T ) I ε ( u 1 , u 2 , l) ⇒ I ε (u 2 , UR(u 1 )) I ε (u 1 , l), I ε (u 2 , l ) ⇒ I ε+ε ({u 1 } u 2 , E) l = D(u 2 -1 ), {u 1 } u 2 ∈ st(T ) I ε ({u 1 } u 2 , l), I ε (u 2 -1 , l ) ⇒ I ε+ε (u 1 , D(u 2 -1 )) l = E, I ε (u 1 , l), I ε (u 2 , l ), I ε (u 3 , l ) ⇒ I ε+ε +ε ({u 1 } u 3 u 2 , Ep) l = Dp(u 2 -1 , u 3 ), {u 1 } u 3 u 2 ∈ st(T ) I ε ({u 1 } u 3 u 2 , l), I ε (u 2 -1 , l ) ⇒ I ε+ε (u 1 , Dp(u 2 -1 , u 3 )) l = Ep, I ε (u, l), I ε (u, l ) ⇒ Goal l = l , ε + ε = 1, I ε (u, l), I ε (u -1 , l ) ⇒ Goal u = u -1 , ε + ε = 1 Goal ⇒                                                                                     
where ε, ε , ε ∈ {0, 1} and + denotes the Boolean operation or. Proof. First, we compute the set G 1 of guessable symbols g ∈ G such that there exists a guessing-proof of T g (Proposition 5). Then, we solve the existence of a DY-proof of T ∪ G 1 s (Proposition 4). Both above steps can be performed in polynomial time in T ∪G ∪{s} d .

Corollary 1. Trace Insecurity (TI) is decidable in non-deterministic polynomial time when the intruder is passive.

Proof. Let P, (S 0 , N 0 ), K 0 , I and s ∈ T (F ) be an instance of (TI). First, we have to choose which message (among those currently in the network) is read by the current protocol rule. It is the non-determinitic part of the algorithm. Then, we have to verify that the chosen message matches the message expected by the agents, and also that the secret s is deducible by the intruder by using all the messages previously gathered. These verifications can both be performed in polynomial time (Theorem 1).

Corollary 2. Protocol Insecurity (PI) is decidable in non-deterministic polynomial time when the intruder is passive.

Proof. The complexity result follows from the facts that the length of every possible interleaving is polynomially bounded in the size of the problem, and we have an NP decision procedure for solving the trace insecurity problem.

Note that the three above complexity results are independent from the concrete size of the dictionary. This is not surprising since we are interested in the complexity of the decision of the theoretical existence of a guessing attack rather than on the cost of mounting such an attack.

Decision Procedures in Presence of an Active Intruder

When the intruder is active, the situation is much more complicated than in Section 6. Indeed, in this case, the messages circulating over the network are either sent by the protocol participants (the processes) or by the intruder. Therefore, they cannot be computed in advance, and will be represented by terms with variables. More precisely, (TI) is reduced to a problem of symbolic constraint solving. An effective constraint solving procedure is presented in Section 8.

Symbolic Constraints

Definition 10. (constraint, solution) A constraint is a sequent of the form T dy u ( DY-constraint) or T g u ( guess-constraint) where T is a finite subset of T (F , X ) and u ∈ T (F , X ). A solution of a finite set (or system) C of constraints is a grounding substitution σ such that for every T dy u ∈ C (resp. every T g u ∈ C) there exists a DY-proof (resp. guessing-proof ) of T σ uσ.

Note that we do not assume that the constraints of the set C are variable disjoint.

Definition 11. (well-formed) A finite set C of constraints is well-formed if its elements can be ordered as T 0 x 0 r 0 , . . . , T l x l r l such that the following conditions holds:

-0 ∈ T 0 , -for all i ≤ l, x i is either dy or g, -for all i < l, T i ⊆ T i+1 , -for all i ≤ l, for all x ∈ vars(T i ), there exists j < i such that x ∈ vars(r j ).

Reduction of (TI) to Constraint Solving

Let π be an instance of (TI) made of a protocol P, a runnable initial configuration (S 0 , N 0 ), a set K 0 ⊂ T (F ), an interleaving I of length and a secret term s ∈ T (F ). We associate to this input a set C(π) = {C 0 , . . . , C } of DY-and guess-constraints the solvability of which is equivalent to the problem of protocol insecurity in presence of an active intruder. We construct in parallel the constraints of C(π) and the sequences T 0 , . . . , T of their hypotheses sets. Let T 0 = N 0 ∪K 0 . For each k < , if I k ∈ G, then C k := T k g g (the intruder can deduce g by guessing)

and T k+1 := T k ∪ {g} (he adds this value to his knowledge),

Otherwise I k is an index representing a process, say (p, σ). Let j be the number of instances of this index in I 0 I 1 . . . I k-1 and let recv(r); send(s) be the jth instruction pair of the program p. Then C k := T k dy rσ (rσ can be received from the network) and T k+1 := T k ∪ {sσ} (sσ is sent to the network).

And finally, if s ∈ G then C := T g s and otherwise, C := T dy s (the secret s is revealed).

Example 5. (Kerberos protocol)

The attack described in Section 2.3 can be executed starting with a (runnable) initial configuration (S 0 , ∅) where S 0 contains five processes, (p i , σ i ) with i ∈ {0, 1, 4, 7, 8}, and with the initial intruder's knowledge K 0 = {0, S, pub(S), A, B, M 1 , M 2 , Ci, Ti}.

The processes p 0 , p 1 correspond to the respective roles A and S of session α which were described in Example 2, the process p 4 to the role S of session β and the other processes p 7 and p 8 to the role S and B of session γ, with:

σ 4 =        x 4 K → K , x 4 T s → T s , x 4 S → S, x 4 pub(S) → pub(S)        σ 7 =        x 7 K → K , x 7 T s → T s , x 7 S → S, x 7 pub(S) → pub(S)        σ 8 = {x 8 pw (B,S) → pw (B, S)} where K , T s , K , T s are constants of F 0 .
The interleaving I describing the trace of the attack is (together with the corresponding steps with the notation of Section 2.3):

0 1 4 pw(A, S) 7 8 α.0 α.1 β.1 pw(A, S) γ.1
The steps β.0, γ.0 and γ.2 do not occur in I since they are performed by the intruder (on behalf of A) in the attack. The step (8, 0) (reception of last message by B) has no corresponding label. The associated constraint system C is described in Figure 9.

Lemma 2. For every instance π of (TI), the size of C(π) is polynomial in the size of π.

Lemma 3. For every instance π of (TI), the set of constraints C(π) is well-formed.

Proof. By the construction of C(π) and the hypothesis that the initial configuration (S 0 , N 0 ) in π is runnable (Definition 3).

Main Results

We shall give in the next section a resolution procedure for the problem of satisfiability of a set of constraints, showing the following theorem. 0

T 0 := S 0 , C 0 := T 0 dy 0 A receives 0 T 1 := T 0 , {A, B, N 1 , N 2 , Ca, {Ta} pw(A,S) } pub(S)
A sends his request to S 1

C 1 := T 1 dy {x 1 A , x 1 B , x 1 N 1 , x 1 N 2 , x 1 Ca , {x 1 Ta } pw (x 1
A ,S) } pub(S) S receives the request

T 2 := T 1 , {x 1 N 1 , K ⊕ x 1 N 2 } pw(x 1 A ,S) , {x 1 A , K, Ts} pw (x 1 B ,S)
S answers the request 4

C 2 := T 2 dy {x 4 A , x 4 B , x 4 N 1 , x 4 N 2 , x 4 Ca , {x 4 Ta } pw (x 4
A ,S) } pub(S) S receives a second request

T 3 := T 2 , {x 4 N 1 , K ⊕ x 4 N 2 } pw (x 4 A ,S) , {x 4 A , K , Ts } pw(x 4 B ,S)
S answers, I diverts S answer pw (A, S) C 3 := T 3 g pw (A, S)

I guesses pw (A, S) using S answer

T 4 := T 3 , pw (A, S) pw (A, S) is added to I's knowledge 7 C 4 := T 4 dy {x 7 A , x 7 B , x 7 N 1 , x 7 N 2 , x 7 Ca , {x 7 Ta } pw (x 7
A ,S) } pub(S) S receives a third request Theorem 2. Given a finite well-formed set C of constraints and a set G of guessable symbols, the existence of a solution is decidable in non-deterministic polynomial time in C and G.

T 5 := T 4 , {x 7 N 1 , K ⊕ x 7 N 2 } pw(x 7 A ,S) , {x 7 A , K , Ts } pw (x 7 B ,
Corollary 3. Trace Insecurity (TI) is NP-complete when the intruder is active.

Proof. The NP part follows from the above polynomial construction of set of constraints associated to instances of (TI) (Lemmas 2 and 3) and from Theorem 2. Concerning the NP-hardness, if we choose G = ∅, then we fall into the trace insecurity problem in presence of a standard active attacker (without guessing abilities). This problem can be shown NP-hard by a reduction from 3-SAT. Indeed, the reduction given by [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF] can easily be adapted in order to obtain a protocol with only one process. It allows to remove the choice of the interleaving, and hence to obtain a reduction from 3-SAT to the trace insecurity problem.

Corollary 4. Protocol Insecurity (PI) is NP-complete when the intruder is active.

Proof. The NP part follows from the facts that the length of every possible interleaving is polynomially bounded in the size of the problem, and we have an NP decision procedure for solving the trace insecurity problem.

Concerning the NP-hardness, if we choose G = ∅, then we fall into the problem of [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF] which has been shown NP-hard.

Constraint Solving Procedure

We present in this section a non deterministic polynomial time algorithm to decide the satisfiability of a well-formed set of DY-and guess-constraints. The idea is that if there exists a solution, then there exists a minimal one whose dag-size is polynomial in the size of the system. This fact has been shown in [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF] for the verification of protocols in the Dolev-Yao model and we can use it to treat DY-constraints. However the case of guess-constraints is much more difficult because some results which are obvious for DYproofs are not true for DY'-proofs (see Section 4.4). Indeed, we have shown that we can always assume that a DY-proof is in normal form, and we often use this result, but the transformation rules to normalize a DY'-proof of T/T u must be used very carefully since we can lose weak hypotheses in T when we apply them. Moreover, a guessing-proof ends with an instance of the rule Compare which is inherently difficult.

Algorithm

The following non-deterministic decision algorithm takes as input a finite well-formed set C of DY-and guess-constraints, and checks the existence of a solution. Let {x 1 , . . . , x m } = vars(C).

1. choose for each i ≤ m a term t i ∈ st(C), and let σ be a most general unifier (if any) of the equational problem

E = {x 1 ≈ t 1 , . . . , x m ≈ t m }, 2. if σ is ground, check whether σ is a solution of C.
If the answer of 2 is positive for some choices of 1, answer Yes. Otherwise, answer No.

Example 6. (Kerberos protocol)

We consider the set of constraints C described in Figure 9. At the first step of the algorithm, we build the following equational problem E:

x 1 A ≈ A, x 1 B ≈ B, x 1 N 1 ≈ N 1 , x 1 N 2 ≈ N 2 , x 1 Ca ≈ Ca, x 1 Ta ≈ Ta, x 4 A ≈ A, x 4 B ≈ B, x 4 N 1 ≈ N 1 , x 4 N 2 ≈ N 2 , x 4 Ca ≈ Ca, x 4 Ta ≈ Ta, x 7 A ≈ A, x 7 B ≈ B, x 7 N 1 ≈ M 1 , x 7 N 2 ≈ M 2 , x 7 Ca ≈ Ci , x 7 Ta ≈ Ti, x 8 A ≈ A, x 8 K ≈ K , x 8
Ts ≈ Ts . Let σ be the most general unifier of E. Now, we can check that σ is a solution of C, i.e. there exists a DY-proof of C i σ for each i ∈ {0, 1, 2, 4, 5, 6} and also a guessing-proof of C 3 σ.

For instance, the required guessing-proof can be obtained by applying the rule Compare to the two DY'-proofs below:

{N 1 , K ⊕ N 2 } pw (A,S) ∈ T 3 σ (A ) T 3 σ/∅ {N 1 , K ⊕ N 2 } pw (A,S) pw (A, S) ∈ G (G) T 3 σ/pw (A, S) pw (A, S) (D ) T 3 σ/pw (A, S) N 1 , K ⊕ N 2 (UL ) T 3 σ/pw (A, S) N 1 {N 1 , K ⊕ N 2 } pw (A,S) ∈ T 3 σ (A ) T 3 σ/∅ {N 1 , K ⊕ N 2 } pw (A,S) pw (A, S) ∈ G (G) T 3 σ/pw (A, S) pw (A, S) (D ) T 3 σ/pw (A, S) N 1 , K ⊕ N 2 (UL ) T 3 σ/pw (A, S) N 1 8.2. Complexity By construction, E ≤ |vars(C)|.
M , where M is the maximal size of a term in C. At step 1, the mgu σ (represented as a dag) can be computed in polynomial time in E , using syntactic transformation rules for solving unification problems, see e.g. [START_REF] Jouannaud | Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification[END_REF]. The dag-size of the terms in the codomain of σ is polynomial in the size of E, hence in the size of C.

The test of step 2 consists in checking that each constraint of C is satisfied by σ. By construction of C, and according to the above bound on the size of σ, the instance of any constraint of C by σ has a dag-size polynomial in the size of C. The results of Propositions 4 and 5 yield polynomial procedures for checking the satisfaction of each constraint of C by σ. Altogether, the complexity of the algorithm is polynomial in the sizes of G and C.

Completeness

The completeness of our algorithm is ensured by the corollary 5 of the key proposition 6. The following technical lemmas 4,5, 6 will be used in the proof of this proposition. Given a proof P of a sequent T u, the aim of Lemmas 4 and 6 is to ensure the existence of a particular proof of T u which respects some extra conditions in order to guarantee some results when we are going to apply transformations, as replacement, on proof trees.

The following lemma 4 has been proved in [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF] for a slightly less general model than the one we have presented here, roughly, the DY-model without probabilistic encryption. Despite this slight difference in models, the proof of [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-Complete[END_REF] can be translated in a straightforward way to prove the following lemma.

Lemma 4. Let P be a DY-proof of T t and P be a minimal DYproof of T γ ending with a composition rule (E, Ep or P). There exists a proof of T t in which γ is never decomposed.

One may observe that in a guessing-proof of T g, the only relevant information in the weak hypotheses T of a node T/T t is whether T contains g or not. Below, in order to simplify the notations, the weak hypotheses in DY'-proofs will be noted g + , g -or ∅: g + and g -represent arbitrary subsets of G respectively containing g and not containing g. Although ∅ is a subcase of g -, we shall still use this notation to emphasis that every DY'-proof of T/∅ u is isomorphic a DY-proof of T u. Note that a set of guessing-proof defined with the g + and g -notation can be represented by a unique guessing-proof, which real contents of weak hypotheses are deduced from the leaves.

Lemma 6 below is an analogous of Lemma 4 for guessing proofs. Its proof requires the following auxiliary Lemma 5 which gives us sufficient conditions to have a guessing-proof of a given sequent T g.

Lemma 5. Let P 1 and P 2 be two normal DY'-proofs of respectively T/∅ t and T/g + t. There exist two DY'-proofs P 1 and P 2 , subtrees of P 1 and P 2 respectively and a guessing-proof of T g whose two sons are P 1 and P 2 .

Proof. We prove this result by induction on the proof P 2 . If the proof P 2 is an instance of (G), then we can apply the rule Compare since the conditions (i), (ii) and (iv) are clearly verified, and (iii) also because the proof P 1 of T/∅ t can not end with an instance of (G).

If the last rule of P 2 is (UL') then the conditions (i), (ii) and (iv) of Compare are clearly met. Either the proof P 1 and P 2 verify the condition (iii), and we can apply the rule Compare, or these proofs end respectively by the instances (T/∅ t 1 , t 2 , T/∅ t 1 ) and (T/g + t 1 , t 2 , T/g + t 1 ) of (UL'). In such a case we apply the induction hypotheses on the subtrees of P 1 and P 2 which root are labeled with T/∅ t 1 , t 2 and T/g + t 1 , t 2 respectively. The other cases, (UR', P', D', Dp', E', Ep') are very similar.

In the following Lemma 6, equivalent of Lemma 4 for the guessingproofs, we impose an extra condition (condition b) to ensure that the replacement we are going to perform on a such guessing-proof does not lose the only relevant information in the weak hypothesis set. Lemma 6. Let P be a guessing-proof of T g and P a minimal DY'proof of T/∅ γ ending with a composition rule (E', Ep' or P'). There exists a guessing-proof of T g in which: (a) γ is never decomposed, (b) every instance (s 1 , s 2 , T/T γ) (resp. (s 1 , s 2 , s 3 , T/T γ) of the composition rule (P , E ) (resp. Ep ) is such that g / ∈ T .

Proof. (for sake of readability, a part of the proof has been moved in Appendix A)

We make an induction on the number of instances of rules in P which do not satisfy (a) or (b). First, we consider the case of an instance which does not satisfy the condition (a), and we distinguish two subcases, depending on whether a premise of the instance is labeled with T/g + γ or T/g - γ. Let γ = γ 1 , γ 2 (the other cases γ = {γ 1 } γ 2 and γ = {γ 1 } γ 3 γ 2 are similar). Case (a + ): Let (T/g + γ, s) be an instance of (UL') (the case (UR') is similar) in P which does not satisfy the condition (a), and let P 1 the subproof of P whose root is the above T/g + γ. We can apply the induction hypothesis to the guessing-proof P of T g whose direct subproofs are P 1 and P Case (a -): Let P 1 and P 2 be the two direct (DY'-) subproofs of P . Let (T/g - γ, s) be an instance of (UL') (the case (UR') is similar) in P i (say i = 1 for simplicity) which does not satisfy (a) and let P 1 be the tree obtained from P 1 by replacing the subproof of P 1 whose root is the above T/g - γ by P (whose root is T/∅ γ). This tree P 1 is a DY'-proof since ∅ is a subcase of g -in our notation. It is not normal, and hence the condition (ii) of Compare is not satisfied by P 1 . We normalize the proof P 1 using simplification rules, and show by induction on the number of simplification steps (using Lemma 5) that we obtain a guessing-proof P to which we can apply the induction hypothesis. The simplification rules and the detailed induction proof can be found in Appendix A.

Case (b): Let (s 1 , s 2 , T/g + γ) be an instance of the composition rule (P') in P which does not satisfy (b). Hence, we have a normal DY'-proof P 1 of T/g + γ, and we can apply Lemma 5 to P and P 1 in order to obtain a guessing-proof P of T g on which we apply the induction hypothesis. Proposition 6. Let σ be a minimal (w.r.t. ) solution of C. For all x ∈ vars(C), there exists t ∈ st(C) \ vars(C) such that tσ = xσ.

Proof. (the proofs of the facts can be found in Appendix A) We reason by contradiction. Assume that there exists x ∈ vars(C) such that for all t ∈ T (F , X ) \ X with tσ = xσ, we have t / ∈ st(C). We will show that under this condition there exists a smaller solution σ of C.

Let C = {C 1 , . . . C } and for each i ≤ , let r i be the target of C i and C i σ be the (ground) constraint obtained from C i by instantiating all the terms in its hypotheses and target with σ.

Fact 1. If xσ ∈ st(sσ) for some hypothesis s of C i (i ≤ ), then there exists j < i such that xσ ∈ st(r j σ). Fact 2. There exists a minimal DY-proof of S m σ xσ ending with a composition rule (E, Ep or P). Now, we let δ be the replacement {xσ → 0} (0 is a special constant introduced in Section 3). We will show that σ := σδ is also a solution of C, which is a contradiction since σ σ. For this purpose, we have to build a proof of each C i σ , i ≤ l. For each i < m, xσ / ∈ st(C i σ), by definition of m and Fact 1. Hence, (C i σ)δ = C i σ = C i σ , i.e. σ is a solution of C i . Let us show that σ is also a solution of C i for each i ≥ m. We may note first that C i (σδ) = (C i σ)δ, because of the hypothesis that there does not exists t ∈ st(C i ) \ X such that tσ = xσ. So, we are going to show that there exists a (DY-or guessing-) proof of (C i σ)δ for each i ≥ m.

Case (1): C i is a guess-constraint S i g g. There exists a guessingproof of S i σ g and moreover, thanks to Fact 2, there exists a normal DY'-proof of S i σ/∅ xσ ending with a composition rule. Thanks to Lemma 6, there exists a guessing-proof GP of S i σ g which verify the condition (a) and (b). We shall build from GP a guessing-proof of (S i σ)δ g. We replace first in GP every subtree ended by an instance (s 1 , s 2 , S i σ/g -xσ) of composition rule (E', Ep' or P') by the following "instance" of (A'): (xσ ∈ S i σ, S i σ/g -xσ). Then we apply δ to every term of the tree obtained, getting GP . Fact 3. GP is a guessing-proof of (S i σ)δ g.

It follows that σ is a solution of C i .

Case (2): C i is a DY-constraint S i dy r i . By hypothesis, there exists a DY-proof of S i σ r i σ, and thanks to Fact 2 and Lemma 4, there exists a DY-proof of S i σ r i σ in which xσ is never decomposed. We can build as in the previous case a DY-proof of (S i σ)δ (r i σ)δ.

Corollary 5. If C admits a solution then there exists an equational problem of the form E = {x 1 ≈ t 1 , . . . , x n ≈ t n }, where {x 1 , . . . , x n } = vars(C) and t 1 , . . . , t n ∈ st(C) such that σ is the unique most general unifier of E.

Proof. Let σ be a minimal solution of C. By Proposition 6, for each x i , i ≤ n, there exists t i ∈ st(C) \ vars(C) such that t i σ = x i σ, i.e. σ is a solution of E = {x 1 ≈ t 1 , . . . , x n ≈ t n }. We can permute the indexes of the variables x 1 , . . . , x n in order to have E in dag solved form, i.e. such that:

for every 1 ≤ i < j ≤ n, x i / ∈ vars(t j )

(the x i are pairwise distinct and every t j / ∈ X by construction). The opposite would mean that E has no solution, using the completeness results for the dag based syntactic unification procedure presented in [START_REF] Jouannaud | Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification[END_REF]. Indeed, the only transformation rule of this procedure applicable to a system of the form of E is the "occur-check", and its application would mean that E has no solution.

Hence, see [START_REF] Jouannaud | Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification[END_REF]), E has a unique most general unifier θ = θ 1 . . . θ n where each θ i is {x i → t i }. Since for each i ≤ n, t i ∈ st(C), and hence vars(t i ) ∈ {x 1 , . . . , x n }, and by condition (1), θ is ground. It implies that θ = σ.

Related Work

Lowe presents in [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF]) a formal CSP model of an intruder able of mounting dictionary attacks and a procedure to detect such attacks, which is implemented as an extension of the framework based on the protocol compiler Casper and the model checker FDR. We believe that our model is compatible with the one of [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF], though the formalisms differ, and hence that our decidability and complexity results are also valid for this system.

An other implementation of dictionary attacks detection is presented in [START_REF] Corin | Guess what? Here is a new tool that finds some new guessing attacks[END_REF]. The authors, like us, define the existence of dictionary attacks by the solvability of a system of constraints, but unlike us, they use only Dolev-Yao constraints (of the form dy ). Indeed, the guessing-constraints T g g are encoded in [START_REF] Corin | Guess what? Here is a new tool that finds some new guessing attacks[END_REF] into some DY-constraints and negation of DY-constraints. However, this gives a definition of attacks strictly coarser than our Definition. For instance, the tree of the second example of Section 4.5, which is not a guessing-proof, and which, in our opinion does not represent a real dictionary attack, is considered as a dictionary attack in [START_REF] Corin | Guess what? Here is a new tool that finds some new guessing attacks[END_REF].

In [START_REF] Cohen | Proving Cryptographic Protocols Safe from Guessing Attacks[END_REF], the tool TAPS for protocol verification is extended to deal with offline dictionary attacks. The problem treated is the verification of protocols for an unbounded number of sessions, and hence, it is not a decision procedure. The definition of dictionary attacks is closed to the one of [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF].

In [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF], offline dictionary attacks are modeled in a general and powerful framework: the applied-pi calculus of [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF]. To illustrate their definition, the authors analyze manually in some protocols w.r.t. resistance to dictionary attacks. Applied-pi calculus is an extension of pi-calculus in which the messages are terms built on an arbitrary signature and considered modulo an equational theory E. This theory characterize the properties of operators such as encryption and decryption (like the deduction rules defining the intruder deduction abilities in our paper). This calculus allows also special processes called active substitutions, of the form {x = t}, meaning that the term t has been sent and read by the intruder but its contents are unknown, and t can be refereed using the variable x. A frame is a parallel composition of active substitutions with name restriction, denoted νn.{x 1 = t 1 , . . . , x n = t n }. Two closed (without free variable) frames νn.σ and νn.σ are statically equivalent if for every pair of terms u, v which do not contains the names of n, we have uσ = E vσ iff uσ = E vσ . It means that the frames cannot be distinguished by any pair of terms. Offline dictionary attacks can be defined naturally in this settings: roughly, a weak secret g can be guessed from the terms t 1 , . . . , t n which have been read by the intruder iff νn.σ and νn.σ are not statically equivalent, where σ = {x 1 = t 1 , . . . , x n = t n }, and σ is obtained from σ by replacing g by a fresh nonce g (the intruder is able to distinguish a good guess of g from a wrong one). This definition is of course more general than our. In particular, it is not restricted to a particular equational theory. We believe however that our definition is an instance of the one of [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF], for the case where E contains axioms for symmetric, public-key and probabilistic encryption, and pairing. Indeed, the DY'-proofs can be represented by terms with explicit destructors. For instance, a DY'proof P ending with an instance of (D') is represented by d(t 1 , t 2 ) where d is an (explicit) symbol for decryption and t 1 , t 2 represent the two direct subproofs of P . With such a correspondence, the two terms u and v in the definition of (non-)static equivalence represent the two direct subproof of a guessing-proof. Therefore, we believe that our procedure can be seen as a decision procedure for a particular case of [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF].

Conclusion

We have defined a formal model of intruder with both deduction abilities à la Dolev-Yao, extended with a representation of probabilistic encryption, and guessing abilities. The verification of the protocol insecurity in this intruder model is shown decidable (when the number of sessions is bounded) in non-deterministic polynomial time. One may note that our procedure is not restricted to one intruder's guess per attack.

This paper gives a new complexity result and does not investigate practical issues, as the opposed of [START_REF] Lowe | Analysing Protocol Subject to Guessing Attacks[END_REF][START_REF] Corin | Guess what? Here is a new tool that finds some new guessing attacks[END_REF]: the algorithm given in this paper is not intended to be implemented as it is, due to its highly non-deterministic nature. However, the NP-completeness result of this paper should not be interpreted as the intractibility of the problem. Indeed, in this field, several security problems that belong theoretically to NP or even harder classes have appeared to be tractable in practice. Hence, we think it would be possible to implement the procedure in a clever manner in order to apply this framework on real protocols.

In this paper, we focused on offline dictionary attacks. The problem of online dictionary attacks, where the intruder uses an online exchange of messages to verify each of his guesses, is claimed to be realistic in some situations [START_REF] Ding | Undetectable On-line Password Guessing Attacks[END_REF], but its formalization needs quite a different model than the one presented here.

Another possible extension is to work on an generalization of our procedure for the definition of protocol resistance against offline dictionary attacks of [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF]. In [START_REF] Abadi | Deciding Knowledge in Security Protocols under Equational Theories[END_REF], it is shown that static equivalence of closed frames is decidable in polynomial time when the equational theory is a subterm theory (set of equations t = s where s is a subterm of t). A consequence is that protocol security against dictionary attacks, following the definition of [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF], is decidable in subterms theories for a bounded number of agents in the case of a passive intruder. The extension of this result to the case of an active intruder remains a challenging open question. We believe that the techniques developed in this paper could help in that direction.

3.

Q

1 T/∅ u 1 Q 2 T/∅ u 2 Q 3 T/∅ u 3 (Ep') T/∅ {u 1 } u 3 u 2 Q 4 T/g u -1 2 (Dp') T/g u 1 → Q 1
T/∅ u 1 with ∈ {-, +}.

We have also an additional rule for deterministic encryption.

4.

Q 1

T/∅ {u 1 } u 2 Q 2 T/∅ u -1 2 (D') T/∅ u 1 Q 3 T/g u 2 (E') T/g {u 1 } u 2 → Q 1 T/∅ {u 1 } u 2 with ∈ {-, +}.
We have also some additional rules concerning pairing. We have omitted them since they do not bring any trouble. They transform a DY'-proof into a DY'-proof and can be treated as the rewriting rule 1.

We can show by induction on the number of simplification steps that every simplification rules is applied to a tree Q whose root is a node of P 1 and such that exactly one of the son of Q is a subproof of P . This explains that the only instances of the simplification rules which may be applied are such that the set of weak hypotheses in the nodes of the upper part of the left member are empty, i.e. those described above.

Remark 2. Note first that with our hypotheses (γ = γ 1 , γ 2 is decomposed by (UL')) the rule of case 1 must necessarily be applied first in the simplification sequence, and this removes one instance of rule which do not satisfy (a).

We may first observe among the instances described above, some of them (for example 1), transforms a DY'-proof into a DY'-proof. Indeed, the simplification by one of these rules replaces a DY'-subproof of T/∅ u or T/g - u by a DY'-subproof of T/∅ u. Hence, the iterated simplification of P 1 by these rules terminates with a normal DY'-proof N 1 which has the same target u as the initial proof P 1 . So, the conditions (i), (ii) and (iv) to apply the rule Compare on the proofs N 1 and P 2 are clearly verified. Either the iterated simplification of P 1 by the simplification rules has not modified its last instance of inference rule and in such a case N 1 and P 2 verify (iii) since P 1 and P 2 verify also this condition. We let P be the guessing-proof of T g with sons N 1 and P 2 .

Or the iterated simplification of P 1 has modified its last instance of inference rule, hence N 1 is a DY'-proof whose set of weak hypotheses is empty and we can apply Lemma 5. In such a case, we let P the guessing-proof provided by Lemma 5. Since N 1 contains at least one instance of rule which does not satisfy (a) or (b) less than P 1 , by the Remark 2 above, we can apply the induction hypothesis to P .

However the rules of cases 2, 3 and 4 with = + may not transform a DY'-proof into a DY'-proof, because they may replace a DY'-subproof of T/g + u by a DY'-subproof of T/∅ u, hence the information about g is lost. Assume that one of these instances is applied during the simplification of P 1 and consider the first application.

If the first application case is 2 (with = +), let Q 1 be the right DY'proof above the instance of (D') (this is a DY'-proof of T/g + u -1

2 ) and Q 2 be the right DY'-proof above the instance of (E') (this is a DY'-proof of T/∅ u 2 ).

By hypothesis, these subproof Q 1 of Q 2 are minimal hence normal. Hence, we have a normal DY'-proof of T/g + u -1 2 and a normal DY'proof of T/g + u 2 . If u -1 2 = u 2 (it is a symmetric key) we can apply Lemma 5 as above. Otherwise, we can apply the rule Compare directly to these two normal DY'-proofs, since the condition (iii) is satisfied. By Remark 2, P contains at least one instance of rule which do not satisfy (a) less than P and we can apply the induction hypothesis to P to conclude. The situation is almost the same for the cases 3 and 4 (with = +).

Fact 1. If xσ ∈ st(sσ) for some hypothesis s of C i (i ≤ ), then there exists j < i such that xσ ∈ st(r j σ).

Proof. This is a consequence of Lemma 3 since, by hypothesis, if xσ ∈ st(C i σ) then xσ ∈ st(yσ) for some y ∈ vars(C i ) (otherwise there exists a t ∈ st(C i ) \ X such that tσ = xσ).

Fact 2. There exists a minimal DY-proof of S m σ xσ ending with a composition rule (E, Ep or P).

Proof. By hypothesis, there exists a DY-proof P of S m σ r m σ and by Lemma 1, we can assume that P is a minimal DY-proof of S m σ r m σ. If P contains a node labeled by S m σ xσ, then it is the root of a minimal subproof as expected. This proof indeed ends with a composition rule: otherwise, by minimality of P , we would have an occurrence of xσ as a subterm of S m σ, which contradicts the definition of m by Fact 1.

We show now that P necessarily contains one node labeled by S m σ xσ. Assume that P contains no such node. We will construct recursively a path in P , from the root up to one leaf, every node of which is labeled by S m σ u such that xσ ∈ st(u), and we shall show in parallel that the existence of such a path conducts to a contradiction.

By definition of m, the condition xσ ∈ st(r m σ) is true for the root of P , which is labeled by S m σ r m σ. Assume that this condition is also true for each node of (a prefix of) a path labeled by S m σ u 0 , . . . , S m σ u k , with u 0 = r m σ and let us consider the sons of s = S m σ u k is P :

if s has 1 son s 1 and (s 1 , s) is an instance of (A), then u k ∈ S m σ and xσ ∈ st(u k ) contradicts the definition of m, because of Fact 1.

if s has 1 son s 1 and (s 1 , s) is an instance of (UL) or (UR), then u k is a subterm of the target of s 1 , hence also xσ, and we let s 1 be the next node of the path.

if s has 2 sons s 1 , s 2 and (s 1 , s 2 , s) is an instance of (D), then u k is a subterm of the target of s 1 or s 2 (say s 1 ), hence also xσ, and we let s 1 be the next node of the path.

if s has 2 sons s 1 , s 2 and (s 1 , s 2 , s) is an instance of (P) or (E).

By hypothesis, we have xσ = u k since we have assume that P contains no such node. So, xσ is a strict subterm of u k and it is also a subterm of the target of one of s 1 and s 2 (say s 1 ). Hence, we can let s 1 be the next node of the path.

Fact 3. GP is a guessing-proof of (S i σ)δ g.

Proof. The tree GP has been obtained from a guessing-proof GP of S i σ g which verify the condition (a) and (b), by:

Figure 1 .

 1 Figure 1. The description of the attack on the Kerberos protocol.

Figure 4 .

 4 Figure 4. The Dolev-Yao' model with probabilistic encryption.

Figure 6 .

 6 Figure 6. The proof rewrite rules.

Definition 7 .

 7 (Intruder Deduction problem (ID)) IN: a finite set of terms T , a finite set of guessable values G, a term s (the secret).

Figure 7 .

 7 Figure 7. The set S of ground Horn clauses (proof of Proposition 4)

Figure 8 .

 8 Figure 8. The set S of ground Horn clauses (proof of Proposition 5)

A , x 8 K , x 8 Figure 9 .

 889 Figure 9. The constraint system of Example 5.

Fact 1

 1 allows us to define: m = min{j | xσ ∈ st(r j σ)}. Note that the constraint C m is a DY-constraint of the form S m dy r m . Otherwise, r m would be a ground term, hence xσ ∈ st(r m σ) ⊆ st(C), a contradiction.

guessNP.tex; 1/06/2005; 8:34; p.3

guessNP.tex; 1/06/2005; 8:34; p.5

For sake of simplicity we usually write t 1 , t

instead of t 1 , t 2 . guessNP.tex; 1/06/2005; 8:34; p.7

guessNP.tex; 1/06/2005; 8:34; p.8

guessNP.tex; 1/06/2005; 8:34; p.9

guessNP.tex; 1/06/2005; 8:34; p.10

guessNP.tex; 1/06/2005; 8:34; p.11

guessNP.tex; 1/06/2005; 8:34; p.13

guessNP.tex; 1/06/2005; 8:34; p.15

guessNP.tex; 1/06/2005; 8:34; p.17

guessNP.tex; 1/06/2005; 8:34; p.18

guessNP.tex; 1/06/2005; 8:34; p.19

guessNP.tex; 1/06/2005; 8:34; p.20

guessNP.tex; 1/06/2005; 8:34; p.21

guessNP.tex; 1/06/2005; 8:34; p.22

guessNP.tex; 1/06/2005; 8:34; p.23

guessNP.tex; 1/06/2005; 8:34; p.24

guessNP.tex; 1/06/2005; 8:34; p.25

guessNP.tex; 1/06/2005; 8:34; p.27

guessNP.tex; 1/06/2005; 8:34; p.28

guessNP.tex; 1/06/2005; 8:34; p.29

guessNP.tex; 1/06/2005; 8:34; p.31

Delaune, Jacquemard

guessNP.tex; 1/06/2005; 8:34; p.32

guessNP.tex; 1/06/2005; 8:34; p.33

guessNP.tex; 1/06/2005; 8:34; p.35

guessNP.tex; 1/06/2005; 8:34; p.36

guessNP.tex; 1/06/2005; 8:34; p.37

guessNP.tex; 1/06/2005; 8:34; p.38

guessNP.tex; 1/06/2005; 8:34; p.39

guessNP.tex; 1/06/2005; 8:34; p.41

guessNP.tex; 1/06/2005; 8:34; p.43

guessNP.tex; 1/06/2005; 8:34; p.44 Decision Procedures for the Security of Protocols against Dictionary Attacks

guessNP.tex; 1/06/2005; 8:34; p.45

guessNP.tex; 1/06/2005; 8:34; p.47 guessNP.tex; 1/06/2005; 8:34; p.48

Acknowledgement

We are grateful to the anonymous referees whose many relevant comments helped us to improve the paper.

* This work has been partly supported by the RNTL project PROUV É 03V360 and the ACI-SI Rossignol.

Appendix

A. Completeness of the Decision Procedure Lemma 6. Let P be a guessing-proof of T g and P a minimal DY'proof of T/∅ γ ending with a composition rule (E', Ep' or P'). There exists a guessing-proof of T g in which: (a) γ is never decomposed, (b) every instance (s 1 , s 2 , T/T γ) (resp. (s 1 , s 2 , s 3 , T/T γ) of the composition rule (P , E ) (resp. Ep ) is such that g / ∈ T .

Proof. Case (a -) We assume (w.l.o.g.) that γ = γ 1 , γ 2 and (T/g -γ, s) be an instance of (UL') which does not satisfy (a). Let P 1 and P 2 be the two direct DY'-subproofs of P . Let P 1 be the tree obtained from P 1 by replacing the subproof of P 1 whose root is the above T/g -γ by P .

We have a DY'-proof P 1 of T/∅ u (u is the verifier used in the guessing-proof P ) which is clearly not in normal form. So, we are going to normalize P 1 in order to obtain a guessing-proof P of T g on which we can apply the induction hypothesis. Let us normalize P 1 using the simplification rules of Figure 6. During this normalization, the following instances of the simplification rules may be applied:

We have a similar rule with (UR') instead of (UL').

2. replacing first in GP every subtree ended by an instance (s 1 , s 2 , S i σ/g - xσ) of composition rule (E', Ep' or P') by the following "instance" of (A'): (xσ ∈ S i σ, S i σ/g -xσ).

applying δ to every term of the tree obtained, getting GP .

Note that the tree GP obtained is not a proof (since xσ not belongs to S i σ). The weak hypotheses are left untouched by δ since xσ ∈ st(G). We can show that the tree GP we have obtained is a guessing-proof of (S i σ)δ g. We show first that in the two sons GP 1 and GP 2 of GP , for every node labeled by s and with n sons labeled respectively by s 1 , . . . , s n (s 1 , . . . , s n , s ) is an instance of a rule of Figure 4.

if n = 1 and (s 1 , s ) is an instance of (A') added by replacement in GP of an instance (s 1 , s 2 , s) of a composition rule in the construction of GP above. By construction, we have s = sδ = (S i σ)δ/g - 0 and we have 0 ∈ S 0 ⊆ (S i σ)δ. Hence, (s 1 , s ) is an instance of (A').

if n = 1 and we are not in the above case, we have (s 1 , s ) = (s 1 δ, sδ) where (s 1 , s) is an instance of (G, A',UL' or UR') contained in GP .

Case (G): let (s 1 , s) be (u ∈ G, S i σ/u u). As shown above, xσ / ∈ G, therefore (s 1 , s ) = (s 1 δ, sδ) is also an instance of (G). Case (A'): this case is immediate.

Case (UL'), (UR'): by construction, we have (s 1 , s) = (s 1 δ, sδ) where (s 1 , s) is an instance of (UL') (the case of (UR') is similar). Let (s 1 , s) be (S i σ/g ε u 1 , u 2 , S i σ/g ε u 1 ). By condition (a) on GP , u 1 , u 2 = xσ. Hence u 1 , u 2 δ = u 1 δ, u 2 δ . Therefore (s 1 , s ) is an instance of (UL ).

if n = 2 and we have (s 1 , s 2 , s ) = (s 1 δ, s 2 δ, sδ) where (s 1 , s 2 , s) is an instance of a composition rule, say (P') (the case of (E') is similar), contained in GP . Let (s 1 , s 2 , s) be (S i σ/g

. By construction of GP , u 1 , u 2 = xσ. Indeed, according to condition (b), all the instances of composition rules with xσ as target of the root has been replaced in the construction of GP . Therefore, u 1 , u 2 δ = u 1 δ, u 2 δ . Thus, (s 1 , s 2 , s ) is an instance of (P ).

if n = 2 and we have (s 1 , s 2 , s ) = (s 1 δ, s 2 δ, sδ) where (s 1 , s 2 , s) is an instance of (D') (the case of (Dp') is similar), contained in GP . Let (s 1 , s 2 , s) be (

) is an instance of (D').

guessNP.tex; 1/06/2005; 8:34; p.46 -if n = 3 and we have (s 1 , s 2 , s ) = (s 1 δ, s 2 δ, sδ) where (s 1 , s 2 , s) is an instance of (Ep') contained in GP . Let (s 1 , s 2 , s 3 , s) be (

We have shown that GP 1 and GP 2 are both DY'-proofs. The condition (i) of the rule (Compare) of Figure 5 is ensured, and the other conditions (ii)-(iv), for GP , are preserved in the construction of GP . So, we have a guessing-proof GP of (S i σ)δ g.