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

Florent Jacquemard
email: florent.jacquemard@lsv.ens-cachan.fr

A Theory of Dictionary Attacks and its Complexity *

We consider the problem of automating proofs of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks: we introduce an inference system modeling the guessing capabilities of an intruder. This system extends the classical Dolev-Yao rules. Using proof rewriting techniques, we show a locality lemma for our inference system which yields the PTIME-completeness of the deduction problem.

This result is lifted to the simultaneous solving of intruder deduction constraints with variables. Constraint solving is the basis of a NP algorithm for the protocol insecurity problem in the presence of dictionary attacks, assuming a bounded number of sessions. This extends the classical NP-completeness result for the Dolev-Yao model.

We illustrate the procedure with examples of published protocols. The model and decision algorithm have been validated on some examples in a prototype implementation.

Introduction

While the automatic verification of cryptographic protocols is undecidable, even with several restrictions, it has aroused a lot of interest during the last years. The undecidability of this problem 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 setbased 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 ses-sions [START_REF] Amadio | On the reachability problem in cryptographic protocols[END_REF][START_REF] Millen | Constraint solving for boundedprocess 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 NPcomplete.

In the works cited above, as well as in most approaches concerning automated verification of security protocols, the underlying cryptographic primitives are based on the so called Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF]. In this model, a malicious agent called intruder is assumed to have a complete control over the communication network: he is able to eavesdrop and replay messages, impersonate honest agents, generate nonces... These abilities still comply to the perfect cryptography assumption, which states that there is no way to obtain knowledge about an encrypted plaintext without knowing the decryption key, and 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 | Constraint solving, exclusive or and the decision of confidentiality for security protocols assuming a bounded number of sessions[END_REF][START_REF] Chevalier | An NP decision procedure for protocol insecurity with xor[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 protocols 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 this interest 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 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] Tsudik | Some remarks on protecting weak secrets and poorly-chosen keys 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 poorly-chosen 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 passwordauthenticated key exchange using human-memorable passwords[END_REF]. However, the application of automatic verification methods, which has been used for cryptographic protocol analysis, was not used 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 attacks [START_REF] Lowe | Analysing protocols subject to guessing attacks[END_REF][START_REF] Corin | Guess what? Here is a new tool that finds some new guessing attacks[END_REF]. However, neither the complexity or the completeness of the procedures, nor the decidability of the problem have been studied in these works.

In this paper, we propose a formal definition of an inference system modeling an intruder which extends the Dolev-Yao model with guessing abilities. We show, by a locality result à la [START_REF] Mcallester | Automatic recognition of tractability in inference relations[END_REF] for this system, that the corresponding intruder deduction problem (whether the intruder is able to deduce a given message from a given set of messages received) is decidable in polynomial time. With a lifting of this decision result to the simultaneous solving of intruder deduction constraints with variables, we propose a non-deterministic polynomial procedure to solve the problem of protocol insecurity in presence of dictionary attacks for a bounded number of sessions. 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 anymore in our extended model. The accuracy of our model has been confronted to many known examples of protocols using a prototype based on an efficient approximation of our procedure. A comparison with other models such as CSP [START_REF] Lowe | Analysing protocols subject to guessing attacks[END_REF] and the spi-calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] can be found at the end of the paper.

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, and formalize in particular the brute force procedure mentioned above. We then prove a locality theorem from which it follows that the ground intruder deduction problem can be decided in polynomial time. After the formal definition of dictionary attacks (Section 5), in term of solutions of symbolic constraint systems (where each individual constraint is a lifting of the ground intruder deduction problem) we give in Section 6 a nondeterministic polynomial time procedure to decide their existence.

Examples

A simple subcase of dictionary attacks is the knownplaintext attacks, where an intruder intercepts a message {M } K encrypted with a weak password K and whose en-crypted 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 challengeresponse scheme where a server sends to a user A a nonce N as a challenge and A responds with {N } K , where K is its a 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

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 in the standard Dolev-Yao model, because an intruder who intercepts the message {V } pub(S) will not be able to learn the value of the vote V 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 .

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 } pw (A,B) 1. B → A : {N + 1} pw (A,B)
A generates a random number (nonce) N and sends it to B encrypted with pw (A, B), B decrypts the message, computes N + 1, and returns to A the encrypted result. The cryptosystem is symmetric. 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.

This attack is called a dictionary attack and has been used to exploit systems in the past, often quite successfully.

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, Gong et al. [START_REF] Gong | Protecting poorly chosen secrets from guessing attacks[END_REF] propose the following modification, which will be used as a running example.

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 bitwise 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 wellchosen 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 secrets and poorly-chosen keys from guessing attacks[END_REF][START_REF] Gong | Protecting poorly chosen secrets from guessing attacks[END_REF][START_REF] Lowe | Analysing protocols subject to guessing attacks[END_REF] for similar protocols, if the server S does not record the timestamps 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 below.

α.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 of an arrow, the intruder I masquerading A to send a message, and on the right of an arrow, the intruder intercepting a message intended for A.

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 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 that, the intruder can impersonate A in session γ, with chosen nonces M 1 and M 2 , and obtains in γ.1 the session key K ′′ which is assumed to be a secret shared between A, S and B.

Protocols

We assume given a signature F containing the symbols , (pairing), { } (encryption), some unary function symbols representing invertible functions, others representing one way functions, and 3 other special constructors pw ( ) (for symmetric keys, or passwords shared between agents1 ), 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 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 contained in T . Among the terms of T (F), we shall distinguish a restricted subset G ⊆ F 0 ∪ {pw (t), pub(t), priv(t)|t ∈ T (F)} of guessable values, i.e. values which are known to belong to a finite dictionary. 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.

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

A replacement is the term morphism extension of a finite mapping {s 1 → t 1 , . . . , s n → t n } where s 1 , . . . , s n , t 1 , . . . t n ∈ T (F, X ). If t 1 , . . . t n ∈ T (F), the replacement is called ground. A substitution is a replacement which domain is a subset of X . As usual, the application of a replacement σ to a term t and the composition of replacements σ 1 by σ 2 are written in postfix notation, respectively tσ and σ 1 σ 2 . A substitution σ is grounding for t is tσ ∈ T (F).

Definition 1 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 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.

Example 1 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 N1 , x 0 N2 , x 0 Ca , {x 0 Ta } x 0 pw (A,S) x 0 pub(S) 1. recv {x 0 N1 , x 0 K ⊕ x 0 N2 } x 0 pw (A,S) , x 0 ; send(x 0 ) role S 0. recv {x 1 A , x 1 B , x 1 N1 , x 1 N2 , x 1 Ca , {x 1 Ta } pw (x 1 A ,x 1
S ) } x 1 pub(S) ; send {x 1 N1 , x 1 K ⊕ x 1 N2 } pw (x 1 A ,x 1 S ) , {x 1 A , x 1 K , x 1 Ts } pw (x 1 B ,x 1 S ) role B 0. recv {x 2 A , x 2 K , x 2 Ts } x 2 pw (B,S) ; send(0)
The symbols x i A . . . (i = 0, 1, 2) are all distinct variables of X . Note that A receives (in step 1) the cipher {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.

Definition 2 A process (p, σ) is made of a program p and a ground substitution σ whose domain is a subset of vars(p).

Every program of a protocol defines a role, and a process (p, σ) is an honest agent playing the role p.

Let N be a set of ground terms called the network. We define small step semantics for the execution of processes. A process (p, σ) changes to (p ′ , σ ′ ) by an execution step if the first element of the program p is recv(r); send(s) and p ′ is the rest of the sequence p, the instruction recv(r) is executed properly, i.e. there exists a ground substitution θ such that rθ ∈ N and σ ′ = σθ, and send(s) is executed, by adding the term sσ ′ to the network N . We assume that the protocol and the initial configuration are such that sσ ′ is ground. It means that every participant is able to construct a term to be sent with the substitution in its initial process (its initial knowledge) or with the values received from other participants, as defined below.

Definition 3 An initial configuration (p 0 , σ 0 ), . . . , (p m , σ m ) of a protocol P is called runnable iff p 0 , . . . p m are copies of programs of P whose variables sets are pairwise disjoint and 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, for each x ∈ vars(s i,j ), x is in the domain of σ i or there exists k ≤ j such that x ∈ vars(r i,k ).

Example 2

The sequence of processes (p 0 , σ 0 ), (p 1 , σ 1 ), (p 2 , σ 2 ) described below is 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 confidentiality of some data sent by processes of a given runnable initial configuration, assuming the presence of an intruder who has strong control over the network N , as defined in the next section.

Intruder Model

We assume that the intruder has a complete control over the network: he systematically diverts messages, possibly modifies them and forwards them to the receiver under the identity of the official sender. In other words all the communications are mediated by a hostile environment represented by the intruder. The intruder actions for analyzing and modifying the messages are modeled below by inference rules.

Dolev-Yao Model

The most widely used deduction relation representing the control of the intruder on the network is known as the Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF] and is defined in Figure 1. The sequent T ⊢ u means that if the intruder knows the messages in T ⊆ T (F), then he can deduce the message u ∈ T (F). In this model, the intruder can form pairs and ciphertexts from known terms (rules P, E), decompose pairs, and decrypt ciphertexts only when he can deduce the decryption key (rules UL, UR, D). The latter condition is known as the perfect cryptography assumption.

Extended Dolev-Yao Model

We shall now describe how dictionary attacks can be modeled by extending the intruder Dolev-Yao model. For this purpose, we use the following definition of dictionary attacks from [START_REF] Lowe | Analysing protocols subject to guessing attacks[END_REF] which generalizes the definition of [START_REF] Gong | Protecting poorly chosen secrets from guessing attacks[END_REF]:

Axiom u ∈ T (A) T ⊢ u Pairing T ⊢ u T ⊢ v (P) T ⊢ u, v Encryption T ⊢ u T ⊢ v (E) T ⊢ {u} v Unpairing T ⊢ u, v (UL) T ⊢ u T ⊢ u, v (UR) T ⊢ v Decryption T ⊢ {u} v T ⊢ v -1 (D) T ⊢ u
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, (cf. Section 2.1) 2. the intruder produced v in two distinct ways from d, (cf. 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 1 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 2, we 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 3 introduces a deduction rule Compare which models the verification of a guess d following 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.4). 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

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 Figure 2.
The Dolev-Yao' model.

P 1          . . . ⊢ ′ u 1 . . . . . . ⊢ ′ u n1 (R 1 ) T /T ′ 1 ⊢ ′ u P 2          . . . ⊢ ′ v 1 . . . . . . ⊢ ′ v n2 (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). R(u, v) where R = Id ∪ {(k, k -1 )| k is a key}

Proofs

Definition 4 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 1 (resp. Figure 2) 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 3.

Let P be a DY-proof (resp. DY'-proof). We say that the pair γ 1 , γ 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 γ 1 , γ 2 . Similarly, the ciphertext {γ 1 } γ 2 is said decomposed in P if P contains an instance of the rule D (resp. D') whose targets of premises are {γ 1 } γ 2 and γ -1 2 . Definition 5 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.

Definition 6 A DY'-proof P is called normal if the rewrite rules defined in Figure 4 can not be applied to P .

Note that every minimal DY'-proof is normal. Indeed, if a DY'-proof P in not normal, then a rewrite rule can be applied to P which means that P contains two nodes on the same path labeled by sequents with the same target (but not necessarily with the same set of weak hypotheses). The normality of DY-proofs is defined with a similar set of rewrite rules, where D', E', P', UL',UR' are replaced respectively by D, E, P, UL,UR.

Lemma 1

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

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 . So, we can consider the other which is the root of a minimal proof of T ⊢ u. 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 application conditions of the rule Compare.

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
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} g , he obtains from the agent the answer {n} g , {n} 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 (D ′ )) and compares the values obtained. But, since both projections are {n} 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} g , {n} g ∈ T (A ′ ) T /∅ ⊢ ′ {n} g , {n} g (UL ′ ) T /∅ ⊢ ′ {n} g g ∈ G (G) T /{g} ⊢ ′ g (D ′ ) T /{g} ⊢ ′ n {n} g , {n} g ∈ T (A ′ ) T /∅ ⊢ ′ {n} g , {n} g (UR ′ ) T /∅ ⊢ ′ {n} g g ∈ G (G) T /{g} ⊢ ′ g (D ′ ) T /{g} ⊢ ′ n

Locality

In order to prove the intruder deduction problem is polynomial in time (Section 4.6), we shall prove below 3 locality [START_REF] Mcallester | Automatic recognition of tractability in inference relations[END_REF] results for the respective theories DY, DY' and DY'+Compare.

The proposition 1 is a locality result for DY-proofs, its proof (folklore knowledge, see e.g. [START_REF] Comon-Lundh | Constraint solving, exclusive or and the decision of confidentiality for security protocols assuming a bounded number of sessions[END_REF]) can be straightforwardly extended to show the similar locality result (Proposition 2) for the 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), then P contains only terms in st(T ).

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 } 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
Similar rules exist for (P'/UR') and (P'/UL')

Figure 4. The proof rewriting rules.

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 ′ ), 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. (sketch) 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, whether u 1 = u 2 or not. In both cases, we show that P 1 or P 2 ends with a decomposition rule. Hence, we conclude thanks to Proposition 2.

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

Intruder Deduction Problem

The intruder deduction problem, which corresponds to the security decision problem in the presence of a passive attacker, is a significant question to the verification problem as well as to the search for attacks. We can formulate this problem in the following way: given a finite set T of messages (ground terms) and a message s (the secret), can the intruder deduce s? In other words, does there exist a proof of T ⊢ s in the intruder deduction model? This deduction problem clearly depends on the deduction capabilities of the intruder. The proofs of the following complexity results use the locality results of Propositions 1 and 3.

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 normal DY-proof P of T ⊢ u, and Proposition 1, which says that P only involves terms in st(T ∪{u}). Indeed, we can code, following [START_REF] Mcallester | Automatic recognition of tractability in inference relations[END_REF], by a set S of ground Horn clauses the instances of the inference rules that can be used in a normal DY-proof of T ⊢ u. This way, we reduce the problem of deciding whether there exists a (normal) DY-proof of T ⊢ u to the HORN-SAT problem for S. Hence, the existence of a DY-proof of T ⊢ u can be decided in polynomial time in T ∪ {u} d , since |S| is linear in T ∪ {u} d .

2

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. The construction of S is detailed in Appendix A. 2

Corollary 1 Given a set of messages T ⊆ T (F), and a message s ∈ T (F), the intruder deduction problem T ⊢ s can be decided in polynomial time in T ∪ G ∪ {s} d for the extended Dolev-Yao intruder model.

Proof. Let us compute first the set G 1 of guessable symbols g ∈ G such that there exists a guessing-proof of T ⊢ g (Proposition 5) and then solve the problem of the existence of a DY-proof of T ∪G 1 ⊢ s (Proposition 4), which is equivalent to the intruder deduction problem T ⊢ s in the extended Dolev-Yao intruder model. Both above steps can be performed in polynomial time in T ∪ G ∪ {s} d . 2

Attacks

We assume given a protocol P, a runnable initial configuration S = (p 0 , σ 0 ), . . . , (p m , σ m ) of P, and a finite set S 0 ⊆ T (F) of initial knowledge of the intruder, such that 0 ∈ S 0 . Now that we have semantics for the protocol execution (Section 3) and for the intruder (Section 4), we shall de-fine the security attacks (with guessing) that the intruder can mount, starting with S 0 , against the processes of S. Our definition involves simultaneous solving of intruder deduction problems with variables, presented as symbolic constraints of the following form. Definition 7 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.

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. For sake of notation, given two solutions σ 1 and σ 2 of sets of constraints, we write

σ 1 ≪ σ 2 iff img(σ 1 ) ≪ img(σ 2 ) (img(σ i ) is the multiset of all xσ such that x ∈ dom(σ i )).
An interleaving of S is a finite sequence I, without repetition, of values which can be either constants of G or pairs of integers (i, j) where 0 ≤ i ≤ m (i is the index of a process of S) and 0 ≤ j < |p i | (j is the index of a pair of instruction of p i ), which satisfies the following ordering condition: for each i with 0 ≤ i ≤ m, the subsequence of I of pairs with first component i has the form (i, 0), (i, 1), . . . , (i, n) with n < |p i |. This condition expresses that I describes a partial linear execution of the respective programs of the processes, up to some point.

Let s ∈ T (F) be a term whose confidentiality must be ensured by the protocol. We associate to s, S, S 0 and to an interleaving I of length ℓ a set C = C(s, S, S 0 , I) = {C 0 , . . . , C ℓ } of DY-and guess-constraints, which solvability defines the problem of protocol insecurity in presence of dictionary attacks. We construct in parallel the constraints of C and the sequences T 0 , . . . , T ℓ of their hypotheses sets. Let T 0 = S 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), if I k = (i, j), then let recv(r i,j ); send(s i,j ) be the jth instruction pair of the program p i , then C k := T k ⊢ dy r i,j σ i (r i,j σ i can be received from the network) and T k+1 := T k ∪ {s i,j σ i } (s i,j σ i 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 3

The attack described in Section 2.3 can be executed starting with a (runnable) initial configuration S made of 5 processes: the processes 0, 1 for the respective roles A and S of session α which were described in Example 2, a process 4 for the role S of session β and other processes 7 and 8 for 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:

(0, 0), (1, 0), (4, 0), pw(A, S), (7, 0), [START_REF] Comon-Lundh | Constraint solving, exclusive or and the decision of confidentiality for security protocols assuming a bounded number of sessions[END_REF]0) α.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. define the intruder's initial knowledge by S 0 = {0, S, pub(S), A, B, M 1 , M 2 , Ci , Ti}. The constraint system C(K ′′ , S, S 0 , I) is described in Figure 5.

Lemma 2 For all i ≤ ℓ and all variable x of a term in the hypotheses of C i , there exists j < i such that x occurs in the target of C j .

Proof. By the construction of C(s, S, S 0 , I), the ordering condition for the interleaving I and the hypothesis that the initial configuration S is runnable (Definition 3).

2

Definition 8 An attack on the security of s ∈ T (F) with the protocol P, the runnable initial configuration S and the initial intruder's knowledge S 0 ⊆ T (F) is a pair (I, σ) where I is an interleaving of S and σ is a solution of C(s, S, S 0 , I).

Note that this definition conforms to the semantics of Section 3, in the sense that a solution σ of C(s, S, S 0 , I) is the (disjoint) union of the substitutions of the processes, after the execution of the trace summarized in I. In the above construction of C(s, S, S 0 , I), we instantiate the terms by the substitutions σ i of the processes of the initial configuration S, to ensure that every solution of C(s, S, S 0 , I) really subsumes these substitutions.

(0,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,0)

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,0)

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,0) 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

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 ,S) S answers, I diverts S answer (8,0)

C 5 := T 5 ⊢ dy {x 8 A , x 8 K , x 8 Ts } pw (B,S)
B accepts I's message

T 6 := T 5 , 0 B answers 0 C 6 := T 6 ⊢ dy K ′′
and the secret K ′′ is revealed

Decision Procedure

We present in this section a non deterministic polynomial time algorithm to find security attacks, given a protocol, a secret, an initial configuration and an initial intruder's knowledge. The idea is that if there exists an attack, then there exists a minimal attack whose dag-size is polynomial in the size of the problem. This fact has been shown in [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NP-complete[END_REF] for 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 DY-proofs are not true for DY'-proofs (see Section 4.3). 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 decision algorithm takes as input a secret s ∈ T (F), a protocol P, a set of initial processes S and an initial intruder's knowledge S 0 ⊆ T (F) like in Section 5, and checks the existence of an attack.

1. choose an interleaving I of S; let C = C(s, S, S 0 , I) and let {x 1 , . . . , x m } = vars(C), 2. 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 },
3. if σ is ground, check whether σ is a solution of C, if so return Yes.

Complexity

By construction, the number m of variables in C is smaller than |vars(S)|, hence, E ≤ |vars(S)|.M , where M is the maximal size of a term in P ∪ S 0 ∪ {s}. At step 2, 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 S, P, S 0 and s.

The test of step 3 consists in checking that each constraint of C is satisfied by σ. The number |C| of constraints, which is also the length |I| of the chosen interleaving I is at most |G|.|S|. p∈P |p|. Moreover, 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 S, P, S 0 and s. The results of Propositions 4 and 5 yield polynomial procedures for checking the satisfaction of each constraint by σ. Altogether, the complexity of step 3 is polynomial in the sizes of G, S, P, S 0 , and s.

Completeness

The completeness of our algorithm is ensured by the corollary 2 of the key proposition 6. The following technical lemmas 3,4, 5 will be used in the proof of this proposition. Given a proof P of a sequent T ⊢ u, the aim of Lemmas 3 and 5 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.

Lemma 3 [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NP-complete[END_REF] Let P be a DY-proof of T ⊢ t and P ′ be a minimal DY-proof of T ⊢ γ ending with a composition rule (E 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 5 below is an analogous of Lemma 3 for guessing proofs. Its proof requires the following auxiliary Lemma 4 which gives us sufficient conditions to have a guessing-proof of a given sequent T ⊢ g.

Lemma 4

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 are very similar. 2 In the following Lemma 5, equivalent of Lemma 3 for the guessing-proofs, we impose an extra condition (condition b) to ensure that the replacement we are going to perform on a such guessing-proof doesn't lose the only relevant information in the weak hypothesis set.

Lemma 5 Let P be a guessing-proof of T ⊢ g and P ′ a minimal DY'-proof of T /∅ ⊢ ′ γ ending with a composition rule (E' 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 ′ ⊢ ′ γ) of a composition rule (P ′ or E ′ ) is such that g / ∈ T ′ .

Proof. 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 -⊢ ′ γ.

Case (a + ): Let γ = γ 1 , γ 2 (the case γ = {γ 1 } γ 2 is similar), 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 γ = γ 1 , γ 2 (the case γ = {γ 1 } γ 2 is similar), 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 which are not described here for sake of place, and show by induction on the number of simplification steps (using Lemma 4) 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 the Appendix B of the long version of this paper [START_REF] Delaune | A theory of guessing attacks and its complexity[END_REF].

Case (b): Let (s 1 , s 2 , T /g + ⊢ ′ γ) be an instance of a composition rule in P which does not satisfy (b), with γ = γ 1 , γ 2 (the case {γ 1 } γ 2 is similar). Hence, we have a normal DY'-proof P ′ 1 of T /g + ⊢ ′ γ, and we can apply Lemma 4 to P ′ and P ′ 1 in order to obtain a guessing-proof P ′′ of T ⊢ g to which we apply the induction hypothesis. 2 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. 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 σ).

Proof. This is a consequence of Lemma 2 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σ).

2 Fact 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. The proof of the following Fact can be found in Appendix B.

Fact 2 There exists a minimal DY-proof of S m σ ⊢ xσ ending with a composition rule E 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 (DYor guessing-) proof of (C i σ)δ for each i ≥ m.

Case (1): C i is a guess-constraint S i ⊢ g g. There exists a guessing-proof 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 5, 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' 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. This fact is proved in Appendix B. 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 3, 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 σ)δ.

(the x i are pairwise distinct and every t j / ∈ X by construction). The converse 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 θ = σ. 2

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.

Related Work

In the spi-calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF], the protocol security is defined by behavioral equivalence between processes: the secrecy of V is ensured by the protocol P (V ) if for every V ′ , and every process O, we have P (V )|O ∼ = P (V ′ )|O (the relation ∼ = is barbed equivalence). In particular, the "intruder" O can perform some comparisons, by matching, and we may wonder how Definition 8 can be compared to security in spicalculus.

For instance, assume that (the role A of) the protocol of Section 2.1 is represented by the process P (V ) = p {V } pub(S) (the encrypted vote is sent on the channel p). Consider the observer process O := p(x).[x is {V } pub(S) ] q x (x is received on channel p, and if it is equal to {V } pub(S) then x is resent on channel q). For V ′ = V , P (V )|O and P (V ′ )|O do not have the same behavior w.r.t. the channel q, hence P (V )|O ∼ = P (V ′ )|O. Therefore, the vote V , which is secret in the Dolev-Yao model, is vulnerable in spi-calculus like in our extended intruder model. Nevertheless, some protocols that are considered secure in our model are not in spi-calculus. Consider a process P (K) = (νn)p {n} K which sends a nonce n encrypted with key K on channel p. The one message protocol implemented by P (K) is considered secured for the key K in our settings, and not in spi-calculus: consider for instance the observer O := p(x).case x of {y} K in q x . Lowe presents in [START_REF] Lowe | Analysing protocols subject to guessing attacks[END_REF] a formal CSP model of an intruder able of 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 protocols subject to guessing attacks[END_REF], though the formalisms differ, and hence that our decidability and complexity results are also valid for this system.

Another 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 8. For instance, the tree of the second example of Section 4.4, 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].

Conclusion

We have defined a formal model of an intruder with Dolev-Yao and guessing abilities, and of the security attacks that he can mount against cryptographic protocols. A non-deterministic polynomial time procedure is described which decides whether there exists such attacks on a given protocol and a given finite set of sessions. It is based on a polynomial time algorithm for the decision of the intruder deduction problem. A conservative approximation of our procedure has been implemented in a prototype which has been executed successfully on some of the examples presented in this paper and others.

One may note that our procedure is not restricted to one intruder's guess per attack. We may also wonder whether it is easier to detect attacks of a weaker intruder, for instance a passive intruder who can only listen to communications on the network and guess offline weakly chosen passwords. The existence of such attacks, for a finite number of processes, can actually be reduced to the intruder deduction problem in the extended Dolev-Yao model, and hence can be decided in polynomial time by Corollary 1.

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, can also 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. As future work we consider to study the design of a general framework, in the style of the one of Section 4, covering several kinds of intruder techniques such as online and offline dictionary attacks or e.g. chosen plaintext attacks.

Figure 1 .

 1 Figure 1. The Dolev-Yao model.

Figure 3 .

 3 Figure 3. The rule Compare.

Figure 5 .

 5 Figure 5. The constraint system C(K ′′ , S, S 0 , I).

2

  Corollary 2 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. such that σ 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 )

We sometimes write pw (t 1 , t

) for pw ( t 1 , t 2 ).

Acknowledgments

The authors wish to thank Hubert Comon-Lundh for his precious assistance to this work, and Ralf Treinen for his reading of a preliminary version of this paper.

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

Appendix A. Proof of Proposition 5

Given a set of messages T ⊆ T (F), and a guessable symbol g ∈ G, we describe below a set S of ground Horn clauses from which one can derive the empty clause if and only if there exists a (normal) guessing-proof of T ⊢ g. Since the dag size of S is polynomial is T ∪ G d , this provides a decision procedure with the complexity wanted. The ground terms in the clauses of S are either elements of st(T, G) or one of the nullary symbols A, P , E, G corresponding to rules of the system of Figure 2, or also UL(u), UR(u), D(u) with u ∈ 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 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 = D(v)):

...

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 set S contains (ε + ε ′ denotes the Boolean or, for ε, ε ′ ∈ {0, 1}):

Appendix B. Proof of Proposition 6

Fact 2 There exists a minimal DY-proof of S m σ ⊢ xσ ending with a composition rule E 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 : ) 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 ′ . By construction, we have s ′ = sδ = (S i σ)δ/g -⊢ ′ 0 and 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

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

) 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

. 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' contained in GP . Let (s 1 , s 2 , s) be (S i σ/g ε 1 ⊢ ′ {u 1 } u 2 , S i σ/g ε 2 ⊢ ′ u -1 2 , S i σ/g ε 1 ∪ε 2 ⊢ ′ 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 ′ 2 , s ′ ) is an instance of D'. We have shown that GP ′ 1 and GP ′ 2 are both DY'-proofs. The condition (i) of the rule (Compare) of Figure 3 is ensured, and the other conditions (ii)-(iv), for GP , are preserved in the construction of GP ′ . Hence GP ′ if a guessing-proof of (S i σ)δ ⊢ g.