Adel Bouhoula
email: bouhoula@planet.tn

Florent Jacquemard
email: florent.jacquemard@inria.fr

Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction

We present a procedure for the verification of cryptographic protocols based on a new method for automatic implicit induction theorem proving for specifications made of conditional and constrained rewrite rules. The method handles axioms between constructor terms which are used to introduce explicit destructor symbols for the specification of cryptographic operators. Moreover, it can deal with non-confluent rewrite systems. This is required in the context of the verification of security protocols because of the non-deterministic behavior of attackers. Our induction method makes an intensive use of constrained tree grammars, which are used in proofs both as induction schemes and as oracles for checking validity and redundancy criteria by reduction to an emptiness problem. The grammars make possible the development of a generic framework for the specification and verification of protocols, where the specifications can be parametrized with (possibly infinite) regular sets of user names or attacker's initial knowledge and complex security properties can be expressed, referring to some fixed regular sets of bad traces representing potential vulnerabilities. We present some case studies giving very promising results, for the detection of attacks (our procedure is complete for refutation), and also for the validation of protocols.

Introduction

Inductive theorem proving techniques and tools have been successfully applied in last years to the verification of security protocols, both for proving security properties and for identifying attacks on faulty protocols.

Paulson's inductive approach [START_REF] Paulson | The inductive approach to verifying cryptographic protocol[END_REF] has been applied to many case studies. In this method, protocols are formalized in typed higher-order logic and the Isabelle/HOL interactive theorem prover is used to prove security properties. Paulson's technique handles infinite state protocols and does not assume any restriction on the number of protocol participants. However, it is not automatic and requires interaction with the user and also a good expertise (if a proof fails with Isabelle, it is difficult to conclude whether the proof attempt failed or the conjecture to be proved is not valid). Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction Bundy and Steel [START_REF] Bundy | Attacking group protocols by refuting incorrect inductive conjectures[END_REF] derive attacks on faulty protocols specified in first-order logic using a proof by consistency technique. Such a technique is sometimes also called inductionless induction [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF] since it does not construct an induction proof following an induction schema but rather tries to automatically derive an inconsistency using first-order theorem proving techniques. This technique is hence fully automatic but its outcome may be difficult to analyze and convergence is difficult to achieve.

In this paper we present a new method for the formal verification of security protocols based on an implicit induction procedure. The protocol, the insecure communication network (attackers) and the security assumptions are modeled with an equational specification which is passed to an inductive theorem prover in order to validate the protocol or to derive an attack. The advantage of this procedure is that it is automatic and returns readable proofs or counter-examples.

The specifications are strongly typed and follow a constructor discipline: we distinguish in the signature the constructor symbols, used to build terms representing the values of the computation, in our case the list (trace) of messages exchanged. The other symbols, called defined symbols, represent functions defined on these values (for instance, we use below a predicate trace characterising the protocol traces) and are specified by Horn clauses.

Equational axioms between terms made of constructors are very difficult to deal with in automated induction and are generally not allowed. Our procedure however allows such axioms, and we use them in order to specify cryptographic operators like decryption. This approach with explicit destructors is the base of a uniform framework for the verification of security protocols in an insecure communication environment [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Explicit destructors both simplify the specification of attacker's capabilities and increase the expressiveness of specification as models with explicit destructors are strictly more expressive than models based on free algebra, in the sense that they captures more attacks [START_REF] Lynch | On the relative soundness of the free algebra model for public key encryption[END_REF].

Our induction procedure introduces another important novelty, compared to other implicit induction techniques, since it handles specifications which are not confluent. The property of ground confluence (any two divergent reduction sequences starting from the same ground term converge ultimately) is usually required for induction procedures. For the application to protocol verification, we consider a model with an active attacker which interferes non-deterministically with the communications of honest users. Such a model, relevant in the context of security, can not be expressed with a ground-confluent specification.

The axioms of the specification contain constraints such as equations, disequations and membership to fixed term languages (characterized by tree grammars). The membership constraints come almost for free as our induction procedure is based on constrained tree grammars. This feature appeared however extremely useful in a setting of protocol specification. It permits to parametrize the specifications of protocols and attackers with (possibly infinite) regular sets of user names or attacker's initial knowledge. Moreover, and more important, it also allows to deal with a rich language of security properties, not limited to the confidentiality of some fixed piece of data as it is the case in many approaches.

FCS-ARSPA'07

Indeed, assume given a set B of bad traces (lists of messages exchanged corresponding to an attack) which is a regular tree language (of constructor terms), characterized by a tree grammar. We can express as a conjecture to be proved the property that every protocol trace (as defined by the predicate trace) does not belong to B. This allows to write a wide range of security properties, like for instance variants of authenticity.

In contrast to the technique of [START_REF] Bundy | Attacking group protocols by refuting incorrect inductive conjectures[END_REF], implicit induction is a goal directed proof technique, and we believe that it is therefore quite efficient for automatically finding attacks on faulty protocols. The use of tree automata techniques permits in particular to focus on traces of events in normal form, and consequently to minimize the set of traces to be checked. Since our procedure is refutationally complete (under some conditions for the specification) its application on any flawed protocol will return a readable attack in finite (and typically very small) time and in a completely automatic way, as illustrated by the examples of Section 3. Moreover, it can also help in protocol validation (proof that there is no attack), though the interactive addition of lemmas may be required for that purpose, see the example in Section 4.

Preliminaries

We consider a many-sorted signature F. As explained in introduction, F is partitioned into a subset C of constructor symbols and a subset D of defined symbols. Each symbol f is given with a profile f : S 1 × . . . × S n → S where S 1 , . . . , S n , S are sorts and n is the arity of f . We note T (F, X ) (resp. T (C, X )) the set of well-sorted terms over F (resp. constructor well-sorted terms) with variables in X and T (F) (resp. T (C)) and the subsets of variable-free terms, or ground terms. The subterm of t at position p is denoted by t| p . The result of replacing t| p with s at position p in t is denoted by t[s] p . This notation is also used to indicate that s is a subterm of t, in which case p may be omitted. A term t is linear if every variable occurs at most once in t. A substitution is a finite mapping from variables to terms, extended as usual as a morphism from terms to terms, written in postfix notation.

Conditional constrained rewriting. We shall consider below constraints which are Boolean combinations of atoms of the form P (t 1 , . . . , t n ) where P belongs to a fixed language of constraints predicates interpreted over terms of T (C) and t 1 , . . . , t n ∈ T (C, X ). The solutions of a constraint c, whose set is denoted sol (c), are (constructor) substitutions σ grounding for all terms in c and such that cσ is interpreted to true. Constrained terms have the form t c where t ∈ T (F, X ) and c is a constraint and conditional constrained rewrite rules are constrained Horn clauses such as:

u 1 = v 1 , . . . , u n = v n ⇒ → r c
Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction where u 1 , v 1 , . . . , u n , v n , , r ∈ T (F, X ), the terms and r (called resp. left-and right-hand side of the rule, → r is an oriented equation) are linear 3 and have the same sort, and c is a constraint. Our procedure takes as input a constrained constructor rewrite system (CTRS) R C , which is a set of rules such that n = 0 (no conditions) and , r ∈ T (C, X ) and a conditional constrained rewrite system (CCTRS) R D , with rules such that n ≥ 0, = f ( 1 , . . . , k ) where f ∈ D and 1 , . . . , n , r ∈ T (C, X ). We note R = R C R D .

A term t d rewrites to s d by the above rule, denoted by t d --→ R s d , if t| p = σ for some position p and substitution σ, s = t[rσ] p , the substitution σ is such that d ∧ ¬cσ is unsatisfiable and Note that the two notions of inductive and joinable inductive theorem coincide when R is ground-confluent. However, they can differ otherwise. Consider for instance R = {c → a, c → b}. The conjecture a = b is an inductive theorem (since a ← --→ * R b) but it is not a joinable inductive theorem (as a and b are R-normal forms). On the other hand, a = b ⇒ f (x) = c is a joinable inductive theorem but not an inductive theorem (for the same reasons).

u i σ ↓ R v i σ for all i ∈ [1..n]; where ↓ R denotes --→ * R • ← -- * R and --→ * R is the reflexive transitive closure of --→ R . If
We call tautology of R a constrained clause of the form a = a ∨ L c such that a is ground irreducible by R or of the form a = b ∨ a = b ∨ L c such that a and b are ground irreducible by R. Note that every tautology is both an inductive and a joinable inductive theorem of R.

Constrained tree grammars A constrained tree grammar G = (Q, ∆) is given by a finite set Q of non-terminals of the form u , where u is a linear term of T (F, X ), and a finite set ∆ of production rules of the form

t := f ( u 1 , . . . , u n ) c where f ∈ F, t , u 1 ,. . . , u n ∈ Q and c is a constraint. fst `pair(x1, x2) ´→ x1 snd `pair(x1, x2) ´→ x2
inv `inv(y) ´→ y dec `enc(x, y), y ´→ x adec `aenc(x, y), inv(y) ´→ x adec `aenc(x, inv(y)), y ´→ x The non-terminals are always considered modulo variable renaming. In particular, we assume that the term f (u 1 , . . . , u n ) is linear. The production relation x G on constrained terms is defined by:

t[x] x: u ∧ d x G t[f (x 1 , . . . , x n )] x 1 : u 1 ∧ . . . ∧ x n : u n ∧ c ∧ dσ if there exists u := f ( u 1 , . . . , u n ) c ∈ ∆ such that f (u 1 , . . . , u n ) = uσ
(we assume that the variables of u 1 , . . . , u n and c do not occur in the constrained term t[x] x: u ∧ d ) and x 1 ,. . . ,x n are fresh variables. The variable x, constrained to be in the language defined by the non-terminal u , is replaced by f (x 1 , . . . , x n ) where x 1 , . . . , x n are constrained to the respective languages of u 1 , . . . , u n . The union of the relations x G for all x is denoted G and the reflexive transitive and transitive closures of the relation G are respectively denoted by * G and + G . The language L G, u is the set of ground terms t generated by a constrained tree grammar G starting with the non-terminal u , i.e. such that x x: u * G t c where c is satisfiable. The above membership constraints t: u , with u ∈ Q, are interpreted by: sol (t: u ) = {σ tσ ∈ L(G, u )}. Note that we shall use below such membership constraints in order to restrict a term to a given sort or a given regular tree language.

Verification of a Key Distribution Protocol

In this section, we describe in an example how to specify a protocol, its environment and security properties with conditional constrained rewrite rules, and how the implicit induction procedure of Section 5 can be applied to the verification of the security properties, expressed as a joinable inductive conjectures.

Signature. Assume some sorts Nat, Bool, Name, Id, Key, Msg, MsgList, with the subsort relations: Name ⊆ Msg and Key ⊆ Msg. The messages exchanged during the protocol execution are abstracted by well sorted terms built with constructor symbols pair : Msg × Msg → Msg, and projections fst, snd : Msg → Msg, encryption and decryption in symmetric and asymmetric key cryptography enc, aenc, dec, adec, all with profile Msg × Msg → Msg and which follow the rules in Figure 1. The variables x represents the encrypted plaintext and the y is a symmetric or a public encryption key. The idempotent operator inv : Key → Key associates to a public key its corresponding private key (for decryption), and conversely; We assume moreover an operator pub : Name → Key which associates to the identity of a user its public key. The symbol inv is called secret and all the others symbols are called public.

Let us also consider a public constructor sent : Id×Name×Name×Msg → Msg used to encapsulate messages with a header. Its first argument is a message identifier, the second and third arguments are respectively the names of sender and receiver of the message and the last argument is the message itself. The public constructor symbol body : Msg → Msg can be used for removing the header, with the rule: body sent(x i , x a , x b , x) → x.

We assume moreover some additional secret constructors for Boolean: true, false : Bool, for natural numbers 0 : Nat, s : Nat → Nat, for lists of messages, nil : MsgList, :: : Msg × MsgList → MsgList and constant values used in the protocol messages: K : Key, S : Msg. Finally, we assume that the set of names of honest users (i.e. the set of terms of sort Name) is a (possibly infinite) regular tree set 4 whose terms are made only of public constructor symbols.

Let us denote R C the set of rewrite rules given above, which are sometimes referred as explicit destructors rules in the protocol verification literature. We propose in Appendix A a constrained tree grammar G NF (R C ) which generates the constructor normal forms. It contains in particular the non terminals y List and x Nat generating normal forms of respective sorts List and Nat.

Protocol. We consider a simplification (without certificates and timestamps) of a key distribution protocol of Denning & Sacco [START_REF] Denning | Timestamps in Key Distribution Protocols[END_REF] for a symmetric key exchange in an asymmetric cryptosystem. Following the approach of [START_REF] Paulson | The inductive approach to verifying cryptographic protocol[END_REF], we consider traces of messages modelled as lists (built with nil and ::) and characterized by the defined symbol trace : Int × MsgList → Msg. In trace(n, ), is a list of messages exchanged (protocol trace) and n can be seen as a resource consumed by each operation executed by an honest or dishonest agent. As we shall see below (in the description of the conjectures proved), the principle of our verification method is to perform an induction on the initial value of this resource (at the beginning of the protocol).

The symbol trace is defined recursively by extension with messages sent by the users participating to the protocol (honest or not). In the case of the Denning & Sacco protocol, the conditional rule (DS-A) of R D describes the user x a sending to user x b a message with identifier 1, which contains a freshly chosen symmetric key K for further secure communications:

trace(s(n), y) → trace n, sent(1, x a , x b , pair(x a , aenc(aenc(K, inv(pub(x a ))), pub(x b )))) :: y x a : Name, x b : Name, x a ≈ x b (DS-A)
This key K is encrypted, for authentication purpose, using the asymmetric encryption function aenc and the secret key of x a , represented as the inverse inv(pub(x a )) of its public key pub(x a ). The result of this encryption is then encrypted with x b 's public key pub(x b ) so that only x b shall be able to learn K. Moreover, x a appends its name at the beginning of the message (using pair) so that the receiver x b knows which public key to use in order to recover K.

In the second conditional rule (DS-B) of R D , the honest user x b , while reading a message x m , expects that x m has the above form (though he does not check this) and extracts the symmetric key K, applying twice the asymmetric decryption function adec to the second component of x m , obtained by application of the projection function snd. This key K is then used by x b to encrypt (with the function enc) a secret code S that he wants to communicate to the user x a , and this ciphertext is sent in a message with identifier 2.

sent(1, x a , x b , x m ) ∈ y = true ⇒ trace s(n), y) → trace(n, sent(2, x b , fst(x m ), enc(S, adec(adec(snd(x m ), inv(pub(x b ))), pub(fst(x m ))))) :: y (DS-B)
Attacker. We assume asynchronous communication of the messages through an insecure public network controlled by a dishonest user called attacker. The attacker is able to read and analyse any message sent to the network and to resend new messages composed from the information collected. Both the extraction of information from the messages read and the composition of new messages are modeled by the application of public constructor symbols and the reduction using the rules of R C . This makes the framework with explicit destructors more uniform that others (often called "Dolev-Yao" models) where information extraction is modeled with extra ad-hoc inference rules. Note that we do not need here the extra predicates analyze and synthesis of [START_REF] Paulson | The inductive approach to verifying cryptographic protocol[END_REF] for the specification of trace. Besides uniformity, the addition of explicit destructor rules makes the model strictly more expressive, in the sense that it captures strictly more attacks, like for instance the attack described below. The operations of the attacker are specified by the following rules of R D for the specification of trace: trace s(n), y → trace(n, x :: y) x : Init (att-init)

x 1 ∈ y, . . . , x k ∈ y ⇒ trace s(n), y → trace n, f (x 1 , . . . , x k ) :: y (att-anlz)

In the rule (att-init), Init is an extra non-terminal of G NF (R C ) which generates a regular tree language representing the initial knowledge of the attacker. In this example, we assume that this language contains all the terms of sort Name and Id. In the rule (att-anlz), x i ∈ y has to be read as x i ∈ y = true. This rule actually represents one conditional rule for each public constructor symbol f of arity k.

The function ∈: Msg × MsgList → Bool is defined by the three rules of R D :

x ∈ nil → false,

x 1 ∈ x 2 :: y → true x 1 ≈ x 2 , x 1 ∈ x 2 :: y → x 1 ∈ y x 1 ≈ x 2
Note that the set of the above rules form a CCTRS sufficiently complete and terminating, but not ground-confluent.

Security properties. We construct a tree grammar G by intersection of G NF (R C ) and a regular tree grammar Bad which generates bad traces. The grammar G is built with a product construction and for the sake of readability, every non-terminal of G will be denoted below

N 1 ∩ N 2 where N 1 is a non-terminal of G NF (R C
) and N 2 is a non-terminal of Bad . We assume two particular nonterminal in the grammar Bad :

a non-terminal B DS auth which generates the set of lists (built with nil, :: and the other constructor symbols) containing a message of the form sent(2, B, A, . . .) not preceded by a message of the form sent(1, A, B, . . .). Such a list corresponds to an authentication flaw. Note that this set is a regular tree language.

a non-terminal B sec which generates the set of lists containing the constant S. Such a list corresponds to a secrecy flaw: it indicates that the secret value S is publicly revealed.

The two conjectures (C auth ), (C sec ) express that every bad trace y cannot be a trace of the protocol obtained in n steps, for any n:

trace(n, nil) = y) y : y List ∩ B DS auth , n : x Nat (C auth ) trace(n, nil) = trace(0, y) y : y List ∩ B sec , n : x Nat (C sec )
More precisely, (C auth ) expresses that no authentication flaw (man-in-the-middle attack) occurs during protocol executions, and (C sec ) expresses that the constant S remains secret to the attacker. The negation trace(n, nil) = trace(0, y) should be understood as trace(n, nil) = trace(0, y) ⇒ true = false. Note that the above variables y and n are constrained to be instantiated by terms generated by G NF (R C ) starting respectively with the non-terminals y List and x Nat , and y is moreover constrained to be instantiated by terms generated by Bad . Note that (C auth ) and (C sec ) have the same form, only the regular tree grammar Bad differs. In general, with this approach, we can express that there is no intersection between protocol traces and bad traces for any regular set of bad traces, which makes quite a rich language of security properties.

Disproofs. The application of our procedure shows that none of the conjectures is a joinable inductive theorems of R, by induction on traces, revealing attacks on the protocol. Among the instances of the conjecture (C auth ) generated5 by application of the production rules of G, we have the instance where the variable y is replaced by nil and n is replaced by s 8 (0), denoted 8 below. We can show that this instance is a counterexample for the conjecture (C auth ), with the normalization with R presented in Figure 2, where m I = pair(A, aenc(A, pub(B)))) and m B = sent(2, B, A, enc(S, adec(A, pub(A)))) (A, B and I are arbitrary distinct constructor terms of sort Name). The normalization of Figure 2 indicates quite legibly an authentication attack on the protocol. In the first steps of the reduction, the attacker builds a message sent(1, I, B, m I ) using its initial knowledge (generated by G from the no-terminal Init), with rule (att-init) and some public constructor symbols, with rule (att-anlz). Then B reads this message and believes that it originated from A. He therefore sends to A an answer which is reduced by R C into: sent(2, B, A, m B ). Hence, the list obtained after the reduction in Figure 2 For Conjecture (C sec ), we consider now n = s 12 (0) and the reduction in Figure 3. The first steps of this figure are the same as in Figure 2. In the next steps, the attacker builds (with rules (att-init) and (att-anlz)) a fake key adec(A, pub(A)) which he uses latter in order to decipher the message m B from B and recover S. Hence, the lists obtained in Figure 3 belongs to L(G, B sec ). It means that the instance of conjecture (C sec ) are reduced to a clause trace(0, ) = trace(0, ), which leads to a case of disproof.

Shamir-Rivest-Adleman Three Pass Protocol. Another example of derivation of an attack is proposed in [START_REF] Bouhoula | Tree Automata, Implicit Induction and Explicit Destructors for Security Protocol Verification[END_REF] (see also Appendix B and Figure 6). We won't reproduce it in details here. We would just like to outline one interesting use of constraints in explicit destructor axioms in this example. Indeed, the protocol RSA 3-pass relies on a commutativity-like property for the encryption operator. In our model, it is expressed by the following rule of R C :

aenc(aenc(x, k 1 ), k 2 ) = aenc(aenc(x, k 2 ), k 1 ) k 1 > k 2 (1)
Note the addition of the ordering constraint, for termination purposes.

Towards Joinable Inductive Validation of Protocols

Let us modify the protocol rules of Section 3 in order to fix the above attacks. We add a pair(x a , x b ) along with the key K in the first message:

sent(1, x a , x b , x m ) ∈ y = true, snd(fst(k)) = x b , fst(fst(k)) = fst(x m ) ⇒ trace(s(n), y) → trace(n, sent(2, x b , fst(x m ), enc(S, k))) :: y) (DS-B')
We present below some parts of the validation of the amended version of the protocol with our procedure, i.e. the proof that the conjecture C sec is a joinable inductive theorem of the above specification. The proof is much more difficult than in the previous sections. Indeed, we need here to verify all the execution traces in order to validate the protocol (by definition of joinable inductive theorems), since R is not ground-confluent. In comparison, it is sufficient to find one erroneous trace in order to show that the protocol is flawed. The application of the procedure generates several subgoals, amongst them: y = nil y : y List ∩ Bsec y = trace(n, x :: nil) y : y List ∩ B sec , n : x Nat , x : Init x 1 ∈ y = true, . . . , x k ∈ y = true ⇒ y = trace(n, f (x 1 , . . . , x k ) :: nil) y : y List ∩ B DS sec , n : x N at Let us recall that Init is a non-terminal of a regular tree grammar generating the language of the initial knowledge of the attacker. This language contains all the ground constructor terms of sort Name and Id in our example. In the third subgoal, f denotes any public constructor symbol of arity k. In our example, k = 1 and f is pub, fst, snd, body or k = 2 and and f is pair, enc, dec, aenc, adec.

The proof of the first subgoal is immediate, but the other subgoals need more developments and the interactive addition of some lemmas in order to derive a proof. We are working on an extension of our inference system with new simplification rules in order to avoid the divergence during the validation of correct authentication protocols.

Implicit Inductive Theorem Proving procedure

We present in this section a goal-directed inductive theorem proving procedure for conditional and constrained specifications.

This procedure belongs to the family of implicit induction (in the lines of [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF]) and combines the power of two classical methods for automatic induction: explicit FCS-ARSPA'07 induction and proof by consistency [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF]. As outlined above, the procedure supports features which are generally not found in former inductive theorem proving approaches, like handling non ground-confluent rewrite systems, axioms between constructors (used here for specifying explicit destructors) or the parametrization of the specification and conjectures with given regular set of terms. A key for these characteristics is that the whole procedure is based on a constrained tree grammar, which is computed automatically from the given specification. It is used for several purposes: (i) as an induction scheme. Using a constrained tree grammar instead of a test-set like in the former procedures [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF][START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF] permits precisely to handle constrained rewrite rules between constructors, (ii) as an oracle for checking validity and redundancy at each induction steps, by reduction to an emptiness problem, (iii) in order to characterize regular sets of terms representing specific values or traces, see Section 3.

Constrained Tree Grammar for Induction

Constrained tree grammars permit an exact representation of the set of ground constructor terms irreducible by a given CTRS. For this reason, such formalisms have been studied in many works related to inductive theorem proving, see e.g. [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF]. Indeed, under some assumptions like sufficient completeness and termination for constructor axioms, they provide a finite description of the minimal Herbrand model (a set of representatives of the minimal Herbrand model is the language of ground constructor R C -normal forms in this case).

For every constructor CTRS R C , we can construct a constrained tree grammar G NF (R C ) which generates the language of ground R C -normal forms. This construction, presented in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] and exemplified in the Section 3, intuitively corresponds to the complementation and completion of a tree grammar for R Creducible terms, where every subset of non-terminals (for the complementation) is represented by the most general unifier of its elements. In a first step of our induction procedure, we construct a constrained tree grammar G = (Q, ∆). This grammar is assumed fixed in the rest of the section. For the construction of G, we start with G NF (R C ) and possibly make an intersection with one or several regular tree grammars, (see Section 3). The intersection between a constrained tree grammar and a regular tree grammar is a constrained tree grammar.

We call a constrained term t c

decorated if c = x 1 : u 1 ∧ . . . ∧ x n : u n ∧ d, {x 1 , . . . , x n } = var (t), u i ∈ Q and sort(u i ) = sort(x i ) for all i ∈ [1..n].
Some of the following inference rules invoke tests for (a) satisfiability of constraints in clauses, (b) ground irreducibility of constructor clauses and (c) joinable inductive validity of ground irreducible of constructor clauses. It is shown in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] that the properties (a) and (b) are reducible to emptiness decision for constrained tree grammars which slightly extend G NF (R C ). A similar reduction is also possible for (c), following the idea that when a clause is ground irreducible, testing joinable inductive validity amounts, by definition, at testing syntactic equality. In other terms, when a and b are ground irreducible R |= jind a = b c iff the constraint c ∧ a ≈ b is unsatisfiable, and (c) is reducible to (a), hence to emptiness decision.

Based on former decision results for tree automata with equality and disequality constraints [START_REF] Comon | Tree automata techniques and applications[END_REF], some restrictions on R C are given [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] which ensure the decidability of the three above problem. The rewrite systems described in Sections 3 and 4 fulfill these restrictions.

Simplification Rules

We present in Figure 4 the system S of simplification rules for constructor clauses. Rewriting simplifies goals with axioms. Since R may not be groundconfluent, we consider all the (one step) reductions with R. Rewrite Splitting simplifies a constrained clause which contains a subterm matching some left member of rule of R D . The inference checks moreover that all cases are covered for the application of such rules of R D , i.e. that for each ground substitution τ , the conditions and the constraints of at least one rule is true wrt τ . Partial Splitting eliminates ground reducible terms in a constrained clause C c by adding to C c the negation of constraint of some rules of R C . Therefore, the saturated application of Partial splitting and Rewriting will always lead to Deletion or to ground irreducible constructor clauses. Finally, Deletion and Validity remove respectively tautologies and clauses with unsatisfiable constraints, and ground irreducible constructor joinable inductive theorems of R. As explained in Section 5.1, the tests in the rules Deletion and Validity are discharged to a decision procedure for the emptiness of constrained tree grammars.

Subsumption `E ∪ ˘C c ¯, H (E, H) if C c is subsumed by another clause of R ∪ E ∪ H Disproof `E ∪ ˘C c ¯, H (Disproof, H) if C c

Main inference system

The main inference system I is displayed in Figure 5. Its rules apply to pairs (E, H), where E is the set of current conjectures and H is the set of inductive hypotheses (constrained clauses). The inference rules of I use the constrained tree grammar G in order to instantiate variables. The replacements are limited to variables, called induction variables, whose instantiation is needed in order to trigger a rewrite step. Definition 1. The set Indpos(f, R) of induction positions of f ∈ D is the set of non-root and non-variable positions of left-hand sides of rules of R D with the symbol f at the root position. The set Indvar (t) of induction variables of t = f (t 1 , . . . , t n ), with f ∈ D and t 1 , . . . , t n ∈ T (C, X ), is the subset of variables of var (t) occurring in t at positions of Indpos(f, R) .

Let us now describe the inference rules of I. Simplification reduces a conjecture which does not contain any induction variable using the rules of System S (Figure 4). Inductive Narrowing generates new subgoals by application of the production rules of the constrained grammar G until the obtained clause is deep enough to cover left hand side of rules of R D . Each obtained clause must be simplified by one of the rules of S (if one instance cannot be simplified, then the rule Inductive Narrowing cannot be applied). Subsumption deletes clauses redundant with axioms of R, induction hypotheses of H and other conjectures not yet proved (in E).

Soundness and Completeness

Our inference system is sound, and refutationally complete. Definition 2. We call derivation a sequence of inference steps generated by a pair of the form (E 0 , ∅), using the inference rules in I, written (E 0 , ∅)

I (E 1 , H 1 ) I • • • (E n , H n ) I • • • .
We say that a derivation is fair if the set of persistent constrained clauses (∪ i ∩ j≥i E j ) is empty or equal to Disproof or Failure. The derivation is said to be a disproof or failure, respectively, in the two last cases, and a success in the first case.

Finite success is obtained when the set of conjectures to be proved is exhausted. Infinite success is obtained when the procedure diverges, assuming fairness. When it happens, the clue is to guess some lemmas which are used to subsume or simplify the generated infinite family of subgoals, therefore stopping the divergence. This is possible in our approach, since lemmas can be used in the same way as axioms are. The proof of the following theorems can be found in the long version [START_REF] Bouhoula | Tree Automata, Implicit Induction and Explicit Destructors for Security Protocol Verification[END_REF] of this extended abstract.

Theorem 1 (Soundness of successful derivations). Let E 0 be a set of decorated constrained clauses. If there exists a successful derivation (E 0 , ∅)

I (E 1 , H 1 ) I • • • then R |= jind E 0 .
The following theorem states that the derivation of Disproof by our inference system is a correct refutation of the conjecture.

Theorem 2 (Soundness of disproof ). If a derivation starting from (E 0 , ∅) returns the pair (Disproof, H), then R |= jind E 0 .

The derivation of Failure means that we cannot conclude, however, this never happens providing the property of strongly completeness for R. A function symbol f ∈ D is sufficiently complete wrt R iff for all t 1 , . . . , t n ∈ T (C), there exists t in T (C) such that f (t 1 , . . . , t n ) --→ + R t. We say that the system R is sufficiently complete iff every defined operator f ∈ D is sufficiently complete wrt R.

Definition 3. Let f ∈ D and let: Γ 1 ⇒ f (t 1 1 , . . . , t 1 k ) → r 1 c 1 , . . . , Γ n ⇒ f (t n 1 , . . . ,
)µ 1 = . . . = f (t n 1 , . . . , t n k )µ n .
We say that f is strongly complete wrt R (see [START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF]) if f is sufficiently complete wrt R and R |= jind Γ 1 µ 1 c 1 µ 1 ∨ . . . ∨ Γ n µ n c n µ n for every subset of R as above. The system R is said strongly complete if every f ∈ D is strongly complete wrt R.

Theorem 3 (Refutational completeness). Assume that R is strongly complete and let E 0 be a set of decorated constrained clauses. If R |= jind E 0 , then all fair derivations starting from (E 0 , ∅) end up with (Disproof, H).

FCS-ARSPA'07

Conclusion

We have developed a procedure for proving joinable inductive theorems of conditional and constrained constructor based specifications which may be non confluent. This procedure is shown correct and refutationally complete, and has been applied to the verification of security properties of cryptographic protocols, both for the research of attacks or protocol validation.

A closely related first order model, also based on trace, was proposed in [START_REF] Comon | Security properties: two agents are sufficient[END_REF]. This exact model was defined in order to prove a theoretical result on the minimal number of user names required in order to prove security properties. To our knowledge, this model has not been applied in practice for protocol verification.

We are planing several development of this method for protocol verification. First, a natural case study for induction are group protocols, see e.g. [START_REF] Bundy | Attacking group protocols by refuting incorrect inductive conjectures[END_REF], with some induction on the number of participants.

Several procedures permit automatic validation of protocols described by first order specifications, e.g. [START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF], but they generally rely on over-approximating models, and are not suitable for the research of attacks, as they generate false positives. Trace based models, like the one presented here, are not approximated and hence appropriate for the search of attack, but automatic protocol validation in such models is considered as a difficult problem. The main difficulty is to generate invariants about the set of data that the attacker can not deduce. Systems like Securify [START_REF] Cortier | Proving secrecy is easy enough[END_REF] or Hermes [START_REF] Bozga | HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols[END_REF] are based on some fixed generic invariants. We would like to study the problem of the automatic generation of appropriate ad-hoc invariants, based on the theoretical framework proposed in this paper.

B Shamir-Rivest-Adleman Three Pass Protocol

We consider the same signature as in Section 3 and also the same constructor CTRS R C extended with the following commutativity-like rule for the encryption operator: aenc(aenc(x, k 1 ), k 2 ) = aenc(aenc(x, k 2 ), k 1 ) k 1 > k 2

(2)

The protocol runs between two users x a and x b in 3 pass, which are described by the following 3 CCTRS rules of R D .

trace(s(n), y) = trace n, sent(1, x a , x b , pair(x a , aenc(S, key(x a )))) :: y x a , x b : Name, x a = x b (RSA-A1) Initially, the honest user x a sends to x b a message containing a secret value S encrypted with its own public key pub(x a ). The ciphertext is sent in a pair, along with the identity of x a . After reading the message from x b , x a decrypts it with its private key inv(key(x a )), and send the result aenc(S, key(x b )). Then, B is able to decipher this message and recover S.

We consider the same rules of R D for ∈, trace and for the attacker (attinit and att-anlz) as in Section 3. We assume moreover here that the language generated by the non-terminal Init (initial knowledge of the attacker) contains the private key inv(key(I)).

Like in Section 3, we construct the constrained tree grammar G by intersection of G NF (R C ) with a regular tree grammar Bad . We consider again the non-terminal B sec which generate the set of lists containing the constant S (like in Section 3) and another non-terminal B RSA auth for authentication flaws, which generates the lists containing a message of the form sent(1, A, B, . . .) followed by a message sent(3, A, B, . . .), without a message of the form sent(2, B, A, . . .)

  This work has been partially supported by the grant INRIA-DGRSRT 06/I09.

  Inductive theorems, tautologies Let R be a terminating CCTRS. A constrained equation a = b c is called an inductive theorem of R (denoted by R |= ind a = b c ) if for all substitution σ ∈ sol (c) grounding for a and b, aσ ← --→ * R bσ, and it is called a joinable inductive theorem of R (denoted by R |= jind a = b c ) if for all substitution σ ∈ sol (c) grounding for a = b, and all R-normal forms n a , n b respectively of aσ, bσ, we have n a = n b . These notions are extended to clauses as expected. The definition of joinable inductive theorems is motivated by the applications presented in Sections 3 and 4.

Figure 1 :

 1 Figure 1: Constructor rules

Figure 2 :-trace ` 3 ,Figure 3 :

 233 Figure 3: An attack on the secrecy of S for DS protocol authentication flaw). It means that the instance of conjecture (C auth ) is reduced to a clause of the form sent(2, B, A, m B ) :: = sent(2, B, A, m B ) :: , which leads to a case of disproof.

  trace(s(n), y) → trace n, sent(1, x a , x b , pair(x a , aenc(aenc(pair(pair(x a , x b ), K), inv(pub(x a ))), pub(x b )))) :: y x a : Name, x b : Name, x a = x b (DS-A') Before sending the second message, x b checks first the pair pair(x a , x b ) sent in the ciphertext (we let k = adec(adec(snd(x m ), inv(pub(x b ))), pub(fst(x m )))):

Rewriting C c S

 c ˘D1 c , . . . , D k c īf for all i ≤ k, Di c C c where {D1 c , . . . , D k c } are all the clauses obtained by one-step rewriting with R from C c .Rewrite SplittingC c S ˘Γiσi ⇒ C[riσi]p i c ∧ ciσi ˛pi pos. of C ¯i∈[1..n] if R |= jind Γ1σ1 c ∧ c1σ1 ∨ . . . ∨ Γnσn c ∧ cnσn , C|p i > riσi and {C|p i } > mul Γiσi where the Γiσi ⇒ liσi → riσi ciσi , i ∈ [1..n],are all the instances of rules Γi ⇒ li → ri ci ∈ RD such that liσi = C|p i Partial Splitting C[lσ]p c S ˘C[rσ]p c ∧ c σ , C[lσ]p c ∧ ¬c σ īf l → r c ∈ RC, lσ > rσ, and neither c σ nor ¬c σ is a subformula of c where C c is a constructor clause. Deletion C c S ∅ if C c is a tautology or c is unsatisfiable. Validity C c S ∅ if C c is a ground irreducible constructor clause and R |= jind C c .

Figure 4 :

 4 Figure 4: System S: simplification rules

Figure 5 :

 5 Figure 5: System I: inference rules for joinable-induction

  sent(x a , x b , x) ∈ y = true ⇒ trace(s(n), y) = trace n, sent(2, x b , fst(x), aenc(snd(x), key(x b ))) :: y (RSA-B) While reading a message x from x a , x b is not able to decipher it and recover S, because he does not know the private key of A. Instead, he sends an answer obtained by encrypting again the message read with its public key key(x b ). The message sent by x b has hence the form: aenc aenc(S, key(x a )), key(x b ) which, by the rule (2) of R C is equivalent to aenc aenc(S, key(x b )), key(x a ) . sent(x a , x b , x) ∈ y = true, sent(x b , x a , x) ∈ y = true ⇒ trace(s(n), y) = trace n, sent(3, x a , x b , adec(x, inv(key(x a )))) :: y (RSA-A2)

  there exists such a term s, then t d is called reducible, otherwise it is called a normal form. A constrained term t c is ground reducible (resp. ground irreducible) by R if for every irreducible substitution σ ∈ sol (c) grounding for t, tσ is reducible (resp. irreducible) by R.The CCTRS R is terminating if there is no infinite sequence t 1 --→ R t 2 --→

	R * . . ., and R is ground-confluent if for any ground terms u, v, w ∈ T (F), v ← --R u --→ * R w, implies that v ↓ R w, and R is ground convergent if R is both ground-confluent and terminating.

  is a constructor clause and no other rule applies to C c is not a constructor clause and no other rule applies to the clause C c

	Failure	`E ∪	˘C	c ¯, H H)	(Failure,
	if C c

Note that assuming that l and r are linear is not restrictive since non linearities may be expressed as equalities between variables in c.FCS-ARSPA'07

We will not define explicitly a tree grammar for Name here, we just assume that it contains the constants A, B and I.FCS-ARSPA'07

The procedure generates all the instances which are smaller than d (R) (the maximum depth of the left-hand sides of rules of R), see Section 5.FCS-ARSPA'07

Acknowledgments. The authors wish to thank Hubert Comon-Lundh for the fruitful discussions they have had about this method and the reviewers for their useful remarks.

Appendix

A Normal form constrained tree grammar for Section 3

The constrained tree grammar G NF (R C ) for the generation of constructor normal forms contains the following sorted non terminals: pair(x 1 , x 2 ) , enc(x, y) , aenc(x, y) , inv(v) , aenc(x, inv(y)) , sent(x i , x a , x b , x) , Name,

x Key , x Msg , x List , x Bool , x Nat and x red . We assume that Name is the initial non-terminal of a regular tree grammar generating the constructor terms of sort Name. The constrained production rules of G NF (R C ) are (M represents below any non-terminal of sort Msg):

x Nat := 0 s( x Nat )

x List := nil M ::

x red := . . . y 1 ≈ y 2 x Msg := adec aenc(x, inv(y)) , M y ≈ M

x red := . . . y ≈ M

The non terminal x red generates all R C -reducible ground constructor terms, and the other n.t. generate all the ground constructor R C -normal forms. -----→ (att-anlz) trace `0, adec(aenc(S, key(I)), inv(key(I))) :: . . .

trace `0, S :: . . . Figure 6: An attack on the secrecy of S for RSA protocol in between. The conjectures are the same as in Section 3, (C auth and C sec ), with B RSA auth instead of B DS auth in (C auth ). Again, we show with our procedure that these conjectures are not joinable inductive theorems of R (by induction on traces), revealing known authentication and secrecy flaws of the protocol.

Let us consider an instance of Conjecture (C sec ) where y is replaced by nil and n is replaced by 11. The reductions in Figure 3 shows that it is a counter example and hence that the protocol has a secrecy flaw. The first part of the reduction suggests also a counter-example for Conjecture (C auth ), demonstrating an authentication flaw of the protocol.

FCS-ARSPA'07