that Xτ σ ∈ Dy c (E e τ σ, K e τ σ) and with F σ ⊆ Dy(E e τ σ, K e τ σ) and K e τ σ∩F σ = ∅, then σ ∈ |[ t ∈ Sub(w, E, E, K) ]|

Keywords: protocoles cryptographiques, système d'inférence, protocoles de groupe, réécriture, sécurité, vérification, contraintes

Vérification de protocoles cryptographiques paramétrés à base de résolution de contraintes

Résumé : Les protocoles cryptographiques sont cruciaux pour la sécurité des transactions éléctroniques. La confiance en ces protocoles peut être améliorée par une analyse formelle de leurs propriétés de sécurité. Bien que de nombreux travaux aient été consacrés aux protocoles classiques tels que celui de Needham-Schroder, très peu s'intéressent la classe prometteuse des protocoles de groupe. Nous présentons un modèle synchrone de protocoles de groupe qui généralise les modèles classiques en incluant des listes non bornées dans les messages. Dans ce modèle étendu, nous proposons un ensemble correct et complet de règles d'inférence pour la vérification de propriétés de sécurité en présence d'un intrus actif pour une classe de protocoles bien taggés. Nous prouvons que l'application de ces règles pour un système de contraintes termine et que la forme normale obtenue peut être testée pour la satisfiabilité. Ainsi, nous présentons ici une procédure de décision pour cette classe.

Introduction

Cryptographic protocols are crucial for securing electronic transactions. They rely on cryptographic functions to ensure security properties such as secrecy or authentication. The confidence in these protocols can be increased by a formal analysis in order to verify that the security properties are met at least at the logical level, that is, even when abstracting from the cryptographic functions and considering messages as first-order terms. Verification at the logical level is nevertheless a non-trivial task since cryptographic protocols are infinite state systems and for instance the set of potential messages that can be generated by an intruder is unbounded. Recently numerous works have been dedicated to the design of automated verification tools for cryptographic protocols. Such tools are often based on model-checking, modal logics, equational reasoning, and resolution theorem-proving (see e.g., [START_REF] Weidenbach | Towards an automatic analysis of security protocols in first-order logic[END_REF][START_REF] Armando | Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning[END_REF][START_REF] Meseguer | Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols[END_REF]). Checking whether a protocol is flawed in the abstract Dolev Yao model ( [START_REF] Dolev | On the security of public key protocols[END_REF]) can often be reduced to a constraint solving problem in a term algebra (modulo an equational theory). This constraint-based approach has proved to be quite effective on standard benchmarks and has also permitted the discovery of new flaws in several protocols (see e.g., [START_REF] Basin | An On-The-Fly Model-Checker for Security Protocol Analysis[END_REF]).

However to our knowledge it has never been applied to the more challenging group protocols. In fact very few formal verification results are available for such protocols. The difficulty relates to the fact that group protocols may perform an arbitrary number of steps since the group of communicating agents is a priori unbounded. This allows one to encode easily undecidable problems.

In this work we present a synchronous model for group protocols, that can also be viewed as an extension of standard protocol models ( [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF]) to handle messages containing possibly unbounded lists. In this extended model we propose a correct and complete set of inference rules that allows one to check security properties in presence of an active intruder, for a class of so-called Well-Tagged protocols. We show that relaxing the conditions on Well-Tagged protocols leads immediately to undecidability. Our inference rules generalize the ones that are implemented in several tools for a bounded number of sessions and fixed size lists such as Cl-ATSE ( [START_REF] Turuani | The CL-Atse Protocol Analyser[END_REF]). In particular when applied to protocols with standard pair operator our inference system provides us with a decision procedure.

Related work Several works have considered protocols with unbounded number of participants and recursive steps. The formal analysis of such protocols goes up with [START_REF] Paulson | Mechanized proofs for a recursive authentication protocol[END_REF] who studied the Recursive Authentication (RA) protocol of [START_REF] Bull | The authentication protocol[END_REF] for an unbounded number of participants using Isabelle/HOL theorem prover ( [START_REF] Paulson | Isabelle: A generic theorem prover[END_REF]). However if the protocol is defective there is no automatic mechanism to find the attack.

The validation of group protocols has been investigated in the CLIQUES project ( [START_REF] Steiner | Cliques: A new approach to group key agreement[END_REF]), based on group Diffie-Hellman (A-GDH) protocols. Several analysis methods have been applied in this project, from manual to automatic ones. An interesting result in this area has been obtained by [START_REF] Pereira | Some attacks upon authenticated group key agreement protocols[END_REF] who found several attacks on the CLIQUES suite and have shown that it is impossible to design a correct authentication group key agreement protocol built on A-GDH for a number of participants greater than three ( [START_REF] Pereira | Generic insecurity of cliques-type authenticated group key agreement protocols[END_REF]). Recently, [START_REF] Kremer | Proving group protocols secure against eavesdroppers[END_REF] have developped an automata-based approximation technique to analyse this class of protocols and check the absence of flaw in presence of a passive intruder. [START_REF] Meadows | Formalizing gdoi group key management requirements in npatrl[END_REF] have adapted the NRL protocol analyser, which is based on a combination of model checking and theorem-proving techniques, to handle the GDOI's protocols. Although Diffie-Hellman exponentiation has been encoded in the tool, it was not able to rediscover Pereira-Quisquater attacks on the CLIQUES suite [START_REF] Meadows | Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives[END_REF]). [START_REF] Steel | Attacking group multicast key management protocols using CORAL[END_REF] have used Coral system to analyse an improved version of the multicast group key management protocol by Tanaka and Sato ( [START_REF] Taghdiri | A lightweight formal analysis of a multicast key management scheme[END_REF]). Two serious attacks have been found on this protocol. Coral has also discovered other attacks on Asokan-Ginzboorg protocol( [START_REF] Asokan | Key agreement in ad hoc networks[END_REF]) and Iolus protocol( [START_REF] Mittra | Iolus: A framework for scalable secure multicasting[END_REF]).

Some works have focused on the modelling of recursive computations performed by some participants (such as a server) in group protocols. [START_REF] Küsters | Automata-based analysis of recursive cryptographic protocols[END_REF] introduce tree transducers to model recursion and to allow the protocol participants to output structured messages. This work gives a decision algorithm for secrecy in the case of atomic keys and bounded message size in the Dolev Yao setting. However messages cannot be tested for equality without losing decidability. Similarly using composed keys or adding equational theories for XOR or Diffie-Hellman exponentiation in their model leads to undecidability. [START_REF] Truderung | Selecting theories and recursive protocols[END_REF] introduces a class of Horn clauses to model the recursive behavior of participants. In this model protocol participants may receive messages of unbounded sizes, send multiple messages in a single step, compare and store messages. He gives a decision procedure to check whether protocols in this model satisfy secrecy properties. His algorithm is in NEXPTIME and is based on the derivation of an exponential bound on the size of minimal attacks. Hence this nice result is rather of theoretical flavour and is not suitable for an implementation. Only atomic keys are allowed for encryption. Moreover, Truderung's model cannot model some computations such as list mapping or functional symbol mapping. Note that non-atomic keys can be handled by our verification procedure (to be presented in the following sections). [START_REF] Küsters | On the automatic analysis of recursive security protocols with xor[END_REF] extend this model to handle XOR operator. Security can then be decided for a class of recursive protocols where principals are forbidden to XOR several messages (depending on messages) received from the network. [START_REF] Kürtz | Selecting theories and nonce generation for recursive protocols[END_REF] extend the Truderung model to model freshness of nonces and keys more accurately.

The class of protocols that we study admits tagged messages. Tagging basically avoids some unifications between messages that could be exploited for attacks. Several works on protocols have considered tagging techniques on messages as ours in order to enforce decidability. But these works ( [START_REF] Blanchet | Verification of cryptographic protocols: Tagging enforces termination[END_REF][START_REF] Ramanujam | Tagging makes secrecy decidable with unbounded nonces as well[END_REF]) do not consider group protocols, or protocol with unbounded lists. Moreover in our case tagging is limited to messages that contains indexed variables, that is variables to be instanciated by items of unbounded lists. The other messages do not need to be tagged in our analysis.

Organization of the paper. We introduce in Section 2 our protocol model. We define attacks and show that their detection is undecidable. This motivates us to introduce the class of Well-Tagged protocols with autonomous keys for which we prove decidability. In Section 3, we introduce auxiliary predicates and their semantics. They are meant to express message constructibility (from intruder knowledge) and they are used to build constraint system whose satisfiability is equivalent to the existence of attacks on a protocol. In Section 4, we introduce a set of simplification rules to reduce these constraints. In Section 5, we give an algorithm for applying these rules on a constraint system modelling a protocol security problem. Completeness and correctness are proved in Section 6. Proof of termination for Protocols without mpair(, )'s is given in Section 7. Proof of termination for Well-Tagged Protocols with Autonomous Keys is given in Section 8. In Section 9, we prove satisfiability. The analysis of the the Asokan-Ginzboorg protocol by our Rules and our verification algorithm is detailed in Section 10.

Motivating Example: Synchronous Group Protocols

As a motivating and running example, we introduce the Asokan-Ginzboorg group protocol which is an application level protocol. Let the group be of size n + 1 for n ≥ 1. The protocol describes the establishment of a session key between a leader (a n ) and a random number n of participants (a i where 1 ≤ i ≤ n). Indeed, the leader starts the execution of the protocol by sending the key of encoding (e). As a response, each participant generates a symmetric key (r i ) and a contribution to the group key (s i ) and sends them encrypted under the key e. The group key would be f (s 1 , . . . , s n+1 ).

1. a n+1 → ALL : a n+1 , {e} p 2. a i → a n+1 : a i , { r i , s i } e 1 ≤ i ≤ n 3. a n+1 → a i : { s 1 , .., s n+1 } ri 1 ≤ i ≤ n 4. a i → a n+1 : a i , { s i , h(s 1 , . . . , s n+1 ) } K some i, K = f (s 1 , . . . , s n+1 )

Since here, modulo index renaming, all members of the group have identical actions, we are going to abstract them in one agent S. Thus, S is a simulator for agents a 1 , . . . , a n . Agent L simulates the leader a n+1 . This way, we obtain below a protocol with a fixed number of steps to the expense of introducing a variadic list constructor mpair( , ). This protocol is called synchronous protocol. Note that all parametric lists have the same length n. They are nested as follows:

1. L -→ S : mpair(t, l, {e} p ) 2. S -→ L : mpair(i, a i , { r i , s i } e ) 3. L -→ S : mpair(i, { mpair(j, s j ), s ′ } ri ) 4. S -→ L : mpair(i, a i , { s i , h( mpair(k, s k ), s ′ ) } f ( mpair(k,s k ),s ′ ) )

We assume that the leader L has in initial knowledge his name l (a n+1 in the initial version), the fresh public key e, the symmetric key p and two hash functions f and h (f, h ∈ H). Its contribution to the group key is noted s ′ (s n+1 in the initial version). The simulator S knows the symmetric key p, the two hash functions f and h and ∀i the identity a i , the contribution (nonce) s i and the public key r i .

The Protocol Model

We extend the protocol model [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF] in order to deal with parametric lists (whose length is the parameter). They are constructed with a new operator denoted by mpair( , ). The intuition is that a mpair message is equivalent to a list of messages built with the same pattern.

Names, Operators and Messages

Let X be a set of variables represented by capital letters. Let I be a countable set of index variables. Let -→ X be a set of symbols represented by overarrowed capital letters, disjoint from X . Let X I = {Y i s.t.

-→ Y ∈ -→ X and i ∈ I} be a countable set of (indexed) variables. Similarly, let C and -→ C be (disjoint) sets of symbols, represented by (overarrowed) lower case letters, and let C I = {c i s.t. c ∈ -→ C and i ∈ I}. Elements in C and C I are called constants. In this paper, terms can be (optionally) tagged by an index. That is, let -→ e ∈ -→ C be a symbol that we reserve for tagging operations only. Then a term is an element of T in the following language:

T s = {T } p T | {T } s T | h(T ) | T , T | mpair(I, T ) | X | X I | C | C I \{e i | i ∈ I} T = [e i , T s ] | T s with i ∈ I
where T s is by definition the set of untagged terms. The operators { } p and { } s represent asymmetric and symmetric encryptions respectively, , is a pairing operator, h is a hash function and mpair(i, t) is a symbolic representation of a list (or tuple) of terms, built from the common pattern t by iterating i along integers. The translation function defined in Section 2.4 gives the semantics of this operator. We denote by signature G the set of operators in T s . To simplify the syntax, in the following we will write t i instead of [e i , t], and call it a tagged term. We also omit the tag i of a term t i , whenever the tag i is not relevant to the discussion. We denote by T g the set of ground terms, i.e. any term t ∈ T with no variable in X or X I and no mpair symbol. Ground terms will be used to describe messages that are circulated in a protocol run. Given a term t we denote by V ar(t) (resp. Cons(t)) the set of variables (resp. constants) occuring in t. We denote by Atoms(t) the set V ar(t) ∪ Cons(t).

In order to represent a list of terms we iterate the pairing operator , . For instance to represent a, b, c, d we can use the term a, b, c, d and we shall write this term in a shorthand: a, b, c, d . However we do not assume any associativity property of pairing.

A substitution σ assigns terms to variables. A ground substitution assigns ground terms to variables. The application of σ to a term t is written tσ. These notations are extended to sets of terms E in a standard way: Eσ = {tσ|t ∈ E}. The set of subterms of t is denoted by Subterm(t). It is defined recursively as follows: If t is a variable or a constant then Subterm(t) = {t}. If t = f (t 1 , .., t n ) or t = f (t 1 , .., t n )

i with t ∈ G, then Subterm(t) = {t} ∪ ∪ n i=1 Subterm(t i ). Note that u is not considered as a subterm of u i . We denote by ≤ the subterm relation on T . We define the relation m over T × T as the smallest reflexive and transitive relation such that if t = f (t 1 , .., t n ) or t = f (t 1 , .., t n ) j with f = mpair, then for all i = 1, . . . , m we have t i m f (t 1 , .., t m ). Note that t m u implies t ≤ u.

Finally, we define two kind of Index-operations: replacements, used in the inference rules over constraints, and substitutions, used to define the solutions of constraints (See Section 3).

Definition 1 (Index-Replacement δ, Index-Substitution τ ). An Index-Replacement δ (resp. Index-Substitution τ ) is an application from I to I (resp. to non-negative integers) that is extended to indexed variables and constants with δ(X i ) = X δ(i) and δ(c i ) = c δ(i) (resp. τ (X i ) = X τ (i) and τ (c i ) = c τ (i) ) and extended to terms and sets of terms in the natural way.

We will use the notations δ i,j (resp. τ i,j ) to denote the replacement (resp. substitution) of i ∈ I by j ∈ I (resp. j ∈ N). We also use δ k i,j to denote the replacement of i ∈ I by j ∈ I and the other indexes apart from i by k ∈ I. We extend this notation to sets with δ k Q,j for some set Q ⊆ I. We define the set of indexes occuring in a term as follows:

Definition 2 (Term Indexes). Given a term t ∈ T , we denote by V ar I (t) the set of indexes in t, recursively defined as follows:

V ar I (mpair(i, t)) = V ar I (X) = V ar I (c) = ∅ with X ∈ X and c ∈ C V ar I (X i ) = V ar I (c i ) = {i} with X i ∈ X I and c i ∈ C I V ar I (f (t 1 , .., t n )) = V ar I (t 1 ) ∪ .. ∪ V ar I (t n ) otherwise V ar I (t i ) = V ar I (t) ∪ {i} Moreover, we define also the set of indexes of variables in u ∈ T as V ar X I (u) = V ar I (u) ∩ V ar I ((Subterm(u) ∩ X I ))

Protocol Specification

A protocol is given by a set of principals and a finite list of steps for each. We associate to each principal A a partially ordered finite set (W A , < W A ) steps R ι ⇒ S ι where R ι is an expected message and S ι his reply. Init and End are fixed messages used to initiate and close a protocol session. Our notion of correct execution of a protocol session (or protocol run) follows [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF].

Example 1. We return to our running example: the "synchronous version" of AG protocol with n + 1 participants (See Section 1.1). The specification of this protocol is given below:

(L, 1) Init ⇒ mpair(t, l, {e} p ) (S, 1) mpair(i, L, {E i } p ) ⇒ mpair(j, a j , { r j , s j } Ej ) (L, 2) mpair(k, a k , { R k , S k } e ) ⇒ mpair(m, { mpair(o, S o ), s ′ } Rm ) (S, 2) mpair(q, { mpair(u, s u ), S ′ } rq ) ⇒ mpair(w, a w , { s w , H( mpair(y, s y ), S ′ ) } F ( mpair(y,sy),S ′ ) ) (L, 3) mpair(x, a x , { S x , H( mpair(z, S z ), s ′ ) } F ( mpair(z,Sz),s ′ ) ) ⇒ End
The ordering on steps is:

W L = 1, 2, 3, W S = 1, 2 with 1 < W L 2, 2 < W L 3, and 1 < W S 2.

Intruder

We follow the intruder model of Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF]. The actions of the intruder are simulated by a sequence of rewrite rules on sets of messages. These rules are defined as follows. We note -→ * DY their reflexive and transitive closure.

L d ( a 1 , . . . , a n ) : a 1 , . . . , a n → a 1 , . . . , a n , a 1 , . . . , a n L d ({a} p K ) : {a} p K , K -1 → {a} p K , K -1 , a L d ({a} s K ) : {a} s K , b → {a} s K , b, a L d (t i ) : t i → t L c ( a 1 , . . . , a n ) : a 1 , . . . , a n → a 1 , . . . , a n , a 1 , . . . , a n L c ({a} p K ) : a, K → a, K, {a} p K L c ({a} s K ) : a, b → a, b, {a} s K L c (t i ) : t → t i for any i ∈ I

Attacks

We recall from [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF] the notion of derivation D of goal t from E, denoted by D t (E). We define a Non-Redundant Derivation as follows:

Definition 3 (Non-Redundant Derivation). Given a derivation D = E 0 -→ L1 . . . -→ L l E l with goal u. D is a non redundant derivation if ∀i ∀t ∈ E i , if L c (t) ∈ D then ∄L d ( ) ∈ D that
L d ( ) ∈ D that generates t if L c (t) ∈ D.
We define a predicate Dy. This predicate checks whether a message can be constructed by the intruder from some known messages.

Definition 4 (Dy, Dy c and Dy d ). Let E be a set of ground terms, K be a set of ground terms and t be a ground term such that there exists D ∈ N RD with goal t without using any term of K as a key for decryption. Then, we say that t is forged from E and we denote it by t ∈ Dy(E, K).

Moreover, if D = D ′ .L c (t) then t ∈ Dy c (E, K), otherwise t ∈ Dy d (E, K).
We interpret the mpair( , ) operator in the standard Dolev-Yao signature by defining a translation function that replaces any mpair by a sequence of pair applications. The number of such applications is given as a parameter e to the translation function. The integer represents the common length of lists of terms represented by any mpair(, ).

Definition 5 (Translation of terms). Let T DY be the set of terms without any mpair(, ). Given some integer e, the function -e from T to T DY is defined as follows:

mpair(i, t) e = τ i,1 (t) e , .., τ i,v (t)
e and f (s 1 , .., s k ) e = f (s 1 e , .., s k e ), for any f = mpair

We can now define attacks on protocols in our model, based on Dy predicate.

Definition 6 (Attack). Given a protocol P = {R ′ ı ⇒ S ′ ı |ı ∈ J}, a secret Sec and assuming the intruder has as initial knowledge S 0 , an attack is described by a ground substitution σ, an Index-Substitution τ , an integer e, and a correct execution order π : J -→ 1, . . . , k s.t. ∀i = 1, . . . , k, we have: R i τ σ e ∈ Dy(S 0 e , S 1 e τ σ, . . . , S i-1 e τ σ, ∅) Sec e ∈ Dy(S 0 e , S 1 e τ σ, . . . , S k e τ σ, ∅)

where

R i = R ′ π -1 (i) and S i = S ′ π -1 (i) .

Undecidability and Well-Tagged Protocols

Unfortunately, the insecurity problem (i.e. the existence of an attack) is undecidable in the general case. This can be shown by encoding Post Correspondance Problem (PCP) with two letters. Note that this requires only atomic keys.

Definition 7 (PCP protocol). Let J = {(α 1 , β 2 ) , .., (α p , β p )} be an instance of PCP on the alphabet {a, b}.

We define the protocol specification P (J) coding J as the following, with

C = {a, b, 0, t, u}, X = {Z}, -→ X = -→ A , -→ B , -→ X , -→
Y and only one honest participant :

1. Init ⇒ a, b, 0, { 0, 0 } t 2. mpair(i, A i , B i ) ⇒ mpair(i, { A i , B i } t ) 3. mpair(i, { X i , Y i } t ) ⇒ mpair(i, { α 1 (X i ) , β 1 (Y i ) } u ), . . . mpair(i, { α p (X i ) , β p (Y i ) } u ) 4. mpair(i, { A i , B i } u ), { Z, Z } u ⇒ Sec At
Step 1, we provide the alphabet as constants to the intruder, as well as a termination symbol 0. At Step 2, the intruder is asked to construct a list (or mpair) of pairs of words over a, b. The following of the protocol will consist in testing if each of these pairs can be obtained from an other one increased with one of the PCP words (α j , β j ). Since the initial pair of empty words represented by { 0, 0 } t , cannot be obtained this way, it is provided to the intruder separately at Step 1. We fix the intruder choice at step 2 by encrypting it with key u. Then, at Step 3 the intruder selects some of the pairs of words encrypted by t that he got at step 1 and 2, and receives each of them back extended with one of the pairs of words of the PCP instance and encrypted by u. We expect the intruder to select all of the pairs he has chosen at Step 2 minus the longest one, replaced by the pair of empty words. Finally, at Step 4 we perform two verifications: first, we test that for any pair of words chosen at Step 2, there exists an extended pair of words received at Step 3, i.e. by recursion that each pair of terms chosen at Step 2 is a concatenation of words of J, the instance of PCP from which we build this protocol; second, we test that one of the extended pair of words is a solution to PCP problem, i.e. a pair of identical words.

Theorem 1. An instance J of PCP has a solution iff P (J) has an attack on Sec.

The proof of this theorem follows from Lemmas 1 and 2.

Lemma 1. If for some integer n there is a run of P (J), then J has a solution.

Proof. According to the protocol definition, all we need to do is to backtrack recursively the creation of extended pairs at Step 2 and 3: for any term { a, b } t known by the intruder, including { A j , B j } u for any j ∈ 1..n or { Z, Z } u , there exists i ∈ 1..n and k ∈ 1..p such that a = α k (X i ) and b = β k (Y i ). Therefore, either X i = Y i = 0, or there exists i ′ ∈ 1..n such that a = α k (A i ′ ) and b = β k (B i ′ ), and the intruder knows

{ A i ′ , B i ′ } t . By iteration on A i ′ and B i ′ , starting from { Z, Z } u , and since | a, b | > | A i ′ , B i ′ |, it
appears that there exists a list [j 1 , .., j r ] of indexes in 1..p such that α j1 (α j2 (..α jr (0)..)) = β j1 (β j2 (..β jr (0)..)), i.e. α j1 ..α jr = β j1 ..β jr .

Lemma 2. If there is a solution to J, there exists n such that P (J) admits a run.

Proof. Let [j 1 , .., j r ] be a list of indexes in 1..p such that α j1 ..α jr = β j1 ..β jr . We chose n = r. We also choose the following values for variables A i , B i :

∀i ∈ 1..n -1, σ(A i ) = α ji (σ(A i+1 )) and σ(B i ) = β ji (σ(B i+1 )) σ(A n ) = α jn (0) and σ(B n ) = β jn (0)
This is the set of pairs of words chosen by the intruder at step 2. Then, at step 3 we chose :

∀i ∈ 2..n, σ(X i ) = σ(A i ) and σ(Y i ) = σ(B i ) σ(X 1 ) = σ(Y 1 ) = 0
i.e. we keep all the pairs of words chosen at step 2 except that we replace the longest (final) one, A 1 , B 1 by the pair of empty words. We can now easily pass the two tests of step 4, since :

∀i ∈ 1..n -1, ∃k ∈ 1..p, ∃j ∈ 1..n s.t. σ(A i ) = α k (σ(X j )) and σ(A i ) = β k (σ(X j )) σ(A n ) = α jn (0) and σ(B n ) = β jn (0) σ(A 1 ) = α j1 (..α jr (0)..) = β j1 (..β jr (0)..) = σ(B 1 )
Consequently, finding an attack to PCP with two letters is no more difficult than finding a run in a parameterized protocol as defined in this paper. Since finding a run is no more difficult than finding an attack (the secret can be released at the end), it follows that the insecurity problem of parameterized protocol without further restrictions is undecidable.

We will therefore introduce the class of Well-Tagged protocols for which decidability is expected. To do this, we first introduce the notion of autonomy:

Definition 8 (Autonomy). A term mpair(i, u) is autonomous when V ar I (u) ⊆ {i}. A term t ∈ T DY is autonomous if #V ar I (t) ≤ 1 and ∀t ′ < t, t ′ is autonomous. A protocol P = {R ı ⇒ S ı |ı ∈ J} is autonomous iff for all ı ∈ J, R ı and S ı are autonomous and V ar I (R ı ) = ∅ and V ar I (S ı ) = ∅.
For instance, the term t = mpair(i, mpair(j, {a i } cj )) is not autonomous. We remark that the autonomy property alone is not enough to guarantee decidability, since the PCP protocol of Definition 7 is autonomous.

Definition 9. (Well-Tagged protocols) A protocol P = {R ı ⇒ S ı |ı ∈ J} is Well-Tagged iff: 1. ∀ı ∈ J, ∀X i ∈ X I ∩ Subterm(R ı ) ∩ ı ′ <ı Subterm(R ı ′ ), X i is tagged; 2. ∀ı ∈ J, ∀X i ∈ X I ∩ Subterm(S ı ), X i is tagged; 3. ∀ı ∈ J, ∀t = f (s 1 , .., s k ) ∈ Subterm(R ı ∪ S ı ) with f = mpair, if ∃j = 1..k s.t. s j is tagged, then t is tagged too; 4. ∀ı ∈ J, ∀t ∈ Subterm(R ı ) tagged, ∀X i ≤ t where X i ∈ X I , X i is tagged.

P is autonomous.

In this definition, Conditions 1 and 2 state that any indexed variable of the protocol must be tagged, except for its first occurrence w.r.t. the partial step ordering. Moreover, Condition 3 (when combined with Conditions 1 and 2) states that, for any subterm t of the protocol, if an indexed variable is accessible from t by decompositions without opening any mpair, then t must be tagged. Note that as a consequence of mpair autonomy, an indexed variable X i can only appear tagged by its index (as in X i i ) or untagged. Condition 4 states that every indexed variable subterm of a tagged term of R ı is tagged.

The idea underlying the tagging of variables is to add enough information on terms in mpair so that the protocol cannot be used to test or guarantee relations between elements of the same mpair, such as ∀i = 2..n, ∃i ′ = 1..n s.t. X i = f (X i ′ ). This is precisely the kind of relations that the encoding of PCP is able to exploit. Thus, adding tags to the PCP-encoding protocol will generate a new protocol that cannot be run.

We introduce the notion of protocols with autonomous keys that will be used to prove the termination for those protocols.

Definition 10. (Protocol with Autonoumous Keys

) A protocol P = {R ı ⇒ S ı |ı ∈ J} is called with autonomous keys iff ∀ı ∈ J t ∈ Subterm(R ı ∪ S ı ) s.t t = {u} v , V ar I (v) = ∅.

Constraints for Protocol Verification

We will use a symbolic constraint system to represent all runs of a protocol given a step ordering. This system uses (universal or existential) quantifiers on index variables and includes an (implicit) universal quantification on the number n of elements in any mpair. Before defining our constraint system, some basic notions have to be introduced. For terms s, s ′ (resp. sets of terms E, E ′ ) we note s ∼ s ′ (resp. E ∼ E ′ ) if they are equal once we erase their tags.

Definition 11 (Relation L E for accessible subterms). We consider a relation on T × 2 T × 2 T × T . We write s L E t for s, t terms in T and E and L finite subsets of T . Note that this can be used for T s too. This relation is defined as the smallest relation such that:

t ∅ ∅ t ∀t ∈ T s L E t iff s ′ L ′ E ′ t ′ where s ∼ s ′ , t ∼ t ′ , E ∼ E ′ , L ∼ L ′ If {m} p k L E t then m L ′ E,k -1 t where L ′ = L ∪ {{m} p k } If {m} s b L E t then m L ′ E,b t where L ′ = L ∪ {{m} s b } If t 1 , . . . , t n L E t then ∀i ≤ n, t i L ′ E t where L ′ = L ∪ { t 1 , . . . , t n } If m L E ′ t and E ′ ⊂ E then m L E t We note u E t when u L E t for some L.
Remark that by construction, u E t implies u ∈ Subterm(t). We say that u is a subterm of t that is accessible, i.e. can be obtained from t by decompositions using keys in E. For simplicity, we note b1,..,b k instead of {b1,..,b k } . We define also the set of strict accessible terms by

s< F t (resp. s< L F t) if s F t (resp. s L F t) and s = t. Given t L F u or t < L F u), we call length of t L F u or (resp t < L F u) the number of elements of L.
Before defining constraint systems, we need to introduce the environment and elementary constraints.

Definition 12 (Environment). We call an environment a finite set of equalities X = u whose left-hand sides are variables (X ∈ X ∪ X I ). We usually denote it by E.

Definition 13 (Elementary Constraint). An elementary constraint is an expression

(t ∈ F orge(E, K)), (t = t ′ ), (t ∈ Sub(t ′ , E, E, K)), (t ∈ Sub d (t ′ , E, E, K)) or (t ∈ F orge c (E, K)) with t, t ′ ∈ T , E ⊂ T and an environment E.
An elementary constraint represents a basic relation on terms: t ∈ F orge(E, K) if the term t is derivable from the knowledge E without using any element from K as a key for decryption; t ∈ F orge c (E, K) if t is derived by composition; t ∈ Sub(t ′ , E, E, K) if t is an accessible subterm from t ′ with knowledge E with none of keys of the intermediate terms between t and t ′ in K, and this modulo replacements using equations of E; t ∈ Sub d (t ′ , E, E, K) if t is accessible by decomposition of t ′ , also modulo replacements using E; and t = t ′ if t and t ′ are equal.

Definition 14 (Negative Constraint). A negative constraint is an expression (∀i

X m = u) or (X m / ∈ F orge c (E, K)) with X m ∈ X I , u ∈ T , E, E ′ ⊂ T and i ∈ V ar I (u).
The set of solutions of a constraint S, denoted by |[ S ]| e τ where e is a value of n and τ is an Index-Substitution is a set of ground substitutions to be defined in the following. We define GS to be the set of all ground substitutions. Definition 15 (Solutions of an Elementary Constraint).

|[ t = t ′ ]| e τ = {σ ∈ GS | t e τ σ = t ′ e τ σ} |[ t ∈ F orge(E, K) ]| e τ = {σ ∈ GS | t e τ σ ∈ Dy(E e τ σ, K e τ σ)} |[ t ∈ F orge c (E, K) ]| e τ = {σ ∈ GS | t e τ σ ∈ Dy c (E e τ σ, K e τ σ)} |[ t ∈ Sub(w, E, E, K) ]| e τ = {σ ∈ GS | ∃u ∃F, L s.t. u L F w e τ, F σ ⊆ Dy(E e τ σ, K e τ σ), F σ ∩ K e τ σ = ∅, and either uσ = t e τ σ or ∃v, δ, k, τ ′ s.t               either u ∈ X , (u = v) ∈ E, δ = ∅, and τ ′ = τ or ∃ -→ Z ∈ -→ X , i, j ∈ I s.t u = Z i τ ′ , (Z j = v) ∈ E, or δ = δ k j,i , τ ⊆ τ ′ and Dom(τ ′ ) = Dom(τ ) ∪ {k, i} k, i / ∈ V
|[ X m / ∈ F orge c (E, K) ]| e τ = GS \ |[ X m ∈ F orge c (E, K) ]| e τ |[ (∀i X m = u) ]| e τ = GS \ x=1...e |[ X m = u ]| e [i←x],τ
We describe our constraint system by blocks in the following way:

Definition 17 (Constraint System). First, we define a constraints block B as a conjunction of constraints together with an environment E: B = (ctr 1 ∧ . . . ∧ ctr l , E)

We will sometimes handle blocks as set of elementary or negative constraints for ease of notations. For instance we write c ∈ B to express that the elementary constraint c is a conjunct of B.

We can now define the constraint system that we will use to represent protocol runs. Given two finite lists of index variables Q = i 1 , . . . , i k and R = j 1 , . . . , j l , we write the quantifier prefix

∀i 1 • • • ∀i k ∃j 1 • • • ∃j l in short: ∀Q ∃R.
A constraint system, denoted by S, is a disjunction of blocks with a quantifier prefix:

S = ∀Q ∃R (B 1 ∨ . . . ∨ B p )
Now, we define the set of solutions of the constraint system as follows:

Definition 18 (Solutions of the Constraint System). Consider a constraint system S, B i , for i = 1 . . . p (blocks of S) and ctr i,j , for j = 1 . . . l i (constraints of the block B i ) given in Definition 17. The set of solutions of a constraint system CS is defined inductively using the following cases:

|[ ∀i S ]| e τ = ∩ x=1,...,e |[ S ]| e [i←x],τ |[ S ]| e τ = i=1...p |[ B i ]| e τ |[ ∃i S ]| e τ = ∪ x=1,...,e |[ S ]| e [i←x],τ |[ B i ]| e τ = j=1...li |[ ctr i,j ]| e τ
The idea will be to use a constraint system based on blocks to represent all possible ways the intruder can construct a list of terms represented by an mpair. Roughly, there will be one block in the system for each way. Note also that blocks are extended to admit labeled constraints: Notation 1. (labels of constraints) A constraint ctr may be equiped with a label (ctr) m or (ctr) sm or (ctr) f to denote respectively a master constraint or a submaster constraint or a final constraint. The tow first labels allow us to keep track of the "official" formal value of some indexed or non-indexed variable. For example, we will prove that we have exactly one master constraint for every indexed variable in each block, and we will use master or sub master constraints to instanciate variables when needed; The third label will be used to prevent any further rewriting on some constraint. We introduce also the notation (ctr) to refer to labeled or non labeled constraint. The solutions of labeled constraints are the solutions of the constraints obtained by removing labels.

To simplify the use of (sub)master constraints, we group them into sets:

Definition 19 (Set of (sub)master constraints). Let S = ∀Q∃R B 1 ∨ .. ∨ B p be a constraint system, Y ∈ X , W ⊆ X and -→ X ∈ -→ X . We define M(S, -→ X ) = {ctr | ∃i (ctr) m ∈ B i and ∃j ∈ Q s.t ctr = (X j ∈ F orge c (E, K)) or ctr = (X j = u)} and ∀i SM(B i , W ) = {ctr | (ctr) sm ∈ B i , Y ∈ W and ctr = (Y = u)}. Also, SM(B i , Y ) = SM(B i , {Y }).
When S is clear from the context we omit it in M(S, -→ X ) and write simply M( -→ X ).

Normalisation of a Constraint System

In this section we present the rules applied in the normalization function over constraint systems. After applying a rule to a constraint system, the result is put in disjunctive normal form and existential quantifiers are moved up to the prefix of the system using first order logic. We introduce some definitions used to define our rules. First, we extend the blocks of constraints to include an history, that is, a sorted list of rules that have occured at some step in this block: Definition 20. (Block History) Any block B = ctr 1 ∧ ..ctr p is equiped with a sorted list of rules Hist = [r 1 , . . .] named the history of the block B denoted by Hist(B). Hist(B)(i) denotes the i th rule of the history. The block is then denoted by B = (ctr 1 ∧ ..ctr p , E, Hist), and constraint systems are extended to blocks with history.

Any rule application will implicitly update the history of the block in which it is applied. Therefore, in what follows, we will not write the history (Hist) of the block each time it is not relevant for the discussion.

We also introduce the notion of anteriority between index variables in the same block that will be used in the definition of Rule 25 and in proofs.

Definition 21 (anteriority of indexes). Let B = (ctr 1 ∧ ..ctr p , E, Hist) be a block. Let i and j be two index variables. We define the function ant(, ) from I × I to I such that ant(i, j) = i if ∃ı s.t i ∈ post(Hist(B)(ı)) and ∀ı ′ ≤ ı j / ∈ post(Hist(B)(ı ′ )).

We then define the function awake that allows to remove the label for dull constraints. This is used when a master constraint is introduced in the block or a master constraint of type F orge is changed to a new Equality master constraint.

Definition 22. (Function awake) We define the function awake as follows: awake((ctr) d ) = ctr awake((ctr) ) = (ctr) for (ctr) = (ctr) d

The function awake is extended in a natural way to constraints blocks and constraints system: Let B = ctr 1 ∧ . . . ∧ ctr m be a constraints block and S = B 1 ∨ . . . ∨ B l be a constraints system. Then: awake(B) = awake(ctr 1 ) ∧ . . . ∧ awake(ctr m ) awake(S) = awake(B 1 ) ∨ . . . ∨ awake(B l ) Finally, we define the dependency graph of a block that will be used to define the notion of accessibility of variables used in Rule 3.

Definition 23 (Dependency graph of a block). We define the dependency graph G B of a block B to be the graph where X ∪ X I is the set of nodes and we have an oriented edge from X to Y iff there is (X = u) ∈ B with Y < u. We write X ⊏ Y when there exists a path in G B from X to Y . We also note X ⊏ l Y if X ⊏ Y and l is the minimal length of a path from X to Y . Now, we present our rules system. They are organized in six groups G 1 , . . . , G 6 .

G 1 : Group of prioritary rules G 1 aims at maintaining syntactic properties over a constraint system. Any rule in this group is applied eagerly with priority higher than any other rule applicable from another group. Moreover the rules in this group are given in strictly decreasing priority order.

t = X -→ X = t where X ∈ X ∪ X I and t / ∈ X ∪ X I (1) (X = u) sm ∧ (Y = X) -→ (X = u) sm ∧ (Y = u) for X, Y ∈ X (2) X = u -→ ⊥ if there is Y < u s.t Y ⊏ X for X, Y ∈ X ∪ X I (3) ∀Q.i ∃R S ∨ (ctr ∧ B) -→ ∀Q.i ∃R awake(S) ∨ ((ctr) m ∧ awake(B)) (4)
where ctr

∈ {X i ∈ F orge c (E, K), X i = u} and B ∩ M( -→ X ) = ∅ ∀Q.i.j ∃R S ∨ ((X i ∈ F orge c (E, K)) m ∧ X j = u ∧ B) -→ ∀Q.i.j ∃R awake(S) (5) ∨(X i ∈ F orge c (E, K) ∧ (X j = u) m ∧awake(B)) (Y j = Z) ∧ X = u -→ (Y j = Z) ∧ X = uλ where Y j < u and λ = [Y j ← Z] (6) B ∧ X = u -→ B ∧ X = uλ ∧ Y j = Z where Y j < u, and λ = [Y j ← Z] (7) if for all Z ′ , E ′ we have (Y j = Z ′ ) / ∈ B B ∧ X = u -→ B ∧ (X = u) sm where SM(B, X) = ∅ (8)
Some rules handle labelling of master constraints by adding new labels or transfering existing ones. Indeed, Rule 4 labels master constraints for a vector variable -→ X ∈ -→ X in a block B when B does not contain yet a master constraint for -→ X . We note that Rule 4 is applied only once for each variable vector in a block. Rule 5 transfers master constraints labels from forge constraints to equality ones whenever possible. Intuitively, an equality constraint being more precise than a forge one, has to be favoured. Note that the index itself, i.e. i or j in Rule 5 is not relevant.

Other rules format constraints in order to get preferably variables on their left hand-side (Rule 1), or replace indexed variables by non-indexed ones (Rules 6 and 7).

Finally, Rule 8 manages submaster constraints by ensuring that if some block contains at least one equality fixing a value for a variable X, then exactly one of them is labelled as submaster constraint for X.

G 2 : Group of F orge reduction rules G 2 aims at enumerating all possible ways a term can be built by the intruder. Here, we consider a constraints block (B ′ , E).

t ∈ F orge(E, K) -→ t ∈ F orge c (E, K) ∨ w∈E t ∈ Sub(w, E, E, K) (9) t 1 , . . . , t m ∈ F orge c (E, K) -→ i=1...m t i ∈ F orge(E, K) (10)
{t} b ∈ F orge c (E, K) -→ (b ∈ F orge(E, K) ∧ t ∈ F orge(E, K)) (11) h(t) ∈ F orge c (E, K) -→ t ∈ F orge(E, K)) (12) ∀Q ∃R S ∨ (B ∧ mpair(k, t) ∈ F orge c (E, K)) -→ (13) ∀Q ∃R S ∨ (B ∧ tδ ∈ F orge(E, K)) if Hy13 ∀Q.k ′ ∃R S ∨ (B ∧ tδ k,k ′ ∈ F orge(E, K))
otherwise where k ′ fresh and Hy13 = ((mpair(k, t)

∈ F orge c (E, K) -→ tδ ∈ F orge(E, K)) ∈ Hist(B)) c ∈ F orge c (E, K) -→ ⊥, for c ∈ C ∪ C I ( 14
)
Rule 9 is a generic rule that illustrates the two possible ways for forging a term t: either by composing or by decomposing one of the knowledge. The other rules enumerate all possible ways a term can be composed by the Intruder: we have exactly one rule for decomposing each kind of operator in the signature G (Rules 10 to 13). In particular, Rule 13 operates for the mpair operator where mpair autonomy is used to justify the quantification.

G 3 : Group of Sub reduction rules G 3 is similar to G 2 , but they decompose Intruder knowledge.

t ∈ Sub(u, E, E, K) -→ (t = u) if u = {v} b and b ∈ K (15) (t = u) ∨ (t ∈ Sub d (u, E, E, K)) otherwise t ∈ Sub d ( t 1 , . . . , t m , E, E, K) -→ i=1...m (t ∈ Sub(t i , E, E, K)) (16) t ∈ Sub d ({u} s b , E, E, K) -→ t ∈ Sub(u, E, E, K) ∧ b ∈ F orge(E, K ∪ {b}) (17) t ∈ Sub d ({u} p K , E, E, K) -→ t ∈ Sub(u, E, E, K) ∧ K -1 ∈ F orge(E, K ∪ {K}) (18) t ∈ Sub d (mpair(k, u), E, E, K) -→ (t ∈ Sub(uδ, E, E, K)) if Hy19 (19) ∃k ′ (t ∈ Sub(uδ k,k ′ , E, E, K)) otherwise
where k ′ fresh and Hy19 = ((t

∈ Sub d (mpair(k, u), E, E, K) -→ t ∈ Sub(uδ, E, E, K)) ∈ Hist(B)) t ∈ Sub d (c, E, E, K) -→ ⊥, for c ∈ C ∪ C I ( 20
)
Rule 15 is a generic rule that follows precisely the intruder deduction rules: a term t is an accessible subterm of u iff t = u or there exists a direct subterm u ′ of u, derivable from u, with t being an accessible subterm of u ′ . Therefore, there exists exactly one rule for decomposing each kind of operator in G (apart from variables and constants).

G 4 : Group of simplification rules for equalities G 4 encodes unification algorithm for terms in our system, and thus, the resolution of equality constraints. Let us note t the root symbol of a term t.

u i = w i where f ∈ {{} p , {} s , , [], h} (23)
∀Q ∃R S ∨ (B ∧ (mpair(k, u) = mpair(l, w))) -→ (24) ∀Q ∃R S ∨ (B ∧ (uδ = wδ l,k δ)) if Hy24 ∀Q.k ′ ∃R S ∨ (B ∧ (uδ k,k ′ = wδ l,k ′ )) otherwise
where k ′ fresh and Hy24 = (((mpair(k, u) = mpair(l, w)) -→ (uδ = wδ l,k δ)) ∈ Hist(B))

∀Q ∃R S ∨ (B ∧ c j = c i ) -→ ∀Q ∃R S ∨ (Bδ) where c i , c j ∈ C I (25) and δ = δ i,j if j ∈ Q and δ = δ j,i if i ∈ Q and δ = δ {i,j},ant(i,j) otherwise
These rules simply consist in testing recursively the compatibility of each top operator in each term. Therefore, the only equality constraints remaining after an iteration of these rules are those assigning a value to a variable, i.e. X = u with X ∈ X ∪ X I .

G 5 : Group of interleaving rules inside a block

These rules aim at replacing variables by their value, inside one block. These rules manage the interaction between two constraints in the same block. Rules in G 5 have priority on rules in G 6 . Moreover, in G 5 , Rule 32 has weaker priority than other rules in the same group.

B ∧ (X i = u) ∧ (X i = v) -→ B ∧ (X i = u) ∧ (X i = v) ∧ u = v (26) if (B ∧ (X i = u) ∧ (X i = v) -→ B ∧ (X i = u) ∧ (X i = v) ∧ u = v) / ∈ Hist(B) (X = u) sm ∧ (X = v) -→ (X = u) sm ∧ (u = v) (27)
(X i = u) ∧ X i ∈ F orge c (E ′ , K) -→ (X i = u) ∧ u ∈ F orge c (E ′ , K) (28)
(X = u) sm ∧ X ∈ F orge c (E ′ , K) -→ (X = u) sm ∧ u ∈ F orge c (E ′ , K) (29)
(A ∈ F orge c (E, K)) ∧ A ∈ F orge c (E ′ , K) -→ (A ∈ F orge c (E, K)) (30)
where

E ⊆ E ′ and A ∈ X ∪ X I (X = w) sm ∧ t ∈ Sub d (X, E ′ , E, K) -→ (X = w) sm ∧ t ∈ Sub d (w, E ′ , E, K) (31) ∧X / ∈ F orge c (E, K) where (X = w) sm ∈ E A ∈ F orge c (E, K) ∧ t ∈ Sub d (A, E ′ , E, K) -→ ⊥ where A ∈ X ∪ X I (32)
Rule 32 says that it is not necessary to decompose a variable. While a bit more complex than expected, our semantics of Sub d (, , ,) has been defined to prevent useless actions like this, thus ensuring the validity of G 6 .

G 6 : Group of interleaving rules between different blocks G 6 generalizes G 5 by allowing variable replacements from one block to an other one. Therefore, these rules are the ones that define interactions between blocks, and solve constraints between multiple indexes of the same variable in a formal way.

Given some vector variable -→ X ∈ -→ X , we assume that M( -→ X ) = {X io = u o } o=1..p ∪{X jr ∈ F orge c (E ′ r , K r )} r=1..q . Then the rewriting rules in this group for constraints over -→ X are the following, with

δ o = δ k ′ o Q,m , k ′ o ∈ I a fresh index variable : t ∈ Sub d (X m , E ′ , E, K) -→ (Xi = u)∈E ∃k ′ t ∈ Sub d (uδ, E ′ , E, K) ∧ (X m = uδ) f (33) ∧X m / ∈ F orge c (E ′ , K)with δ = δ k ′ i,m X m ∈ F orge c (E ′ , K) -→ ((X m ∈ F orge c (E ′ , K)) d ∧ o=1...p (∀k ′ 0 X m = u o δ o )) ∨ (34) o=1...p ∃k ′ 0 u o δ o ∈ F orge c (E ′ , K) ∧ (X m = u o δ o ) f X m = v -→ r=1...q (v ∈ F orge c (E ′ r , K r )) ∧ (X m = v) d ∧ o=1...p (∀k ′ 0 X m = u o δ o ) ∨ (35) o=1...p ∃k ′ o (u o δ o = v) ∧ (X m = u o δ o ) f
The structure of these rules is essentially the same as for interleaving in only one block: Given a constraint containing a variable X i that must be replaced by its value, we enumerate a finite number of "candidate" terms representing all possible values of this variable according to the whole constraint system. These values are provided by master constraints. For instance, in Rule 33, only the case where master constraints are equality ones are taken into account since F orge ones leads to ⊥. This rule adds an (extra) equality representing the master constraint it used. It adds also negative constraints to eliminate the case of F orge master constraints.

Let B the block that we focus on for Rules 33, 34 and 35. For Rule 33, if

(t ∈ Sub d (X m , E, E, K) -→ ∃k ′ t ∈ Sub d (uδ, E ′ , E, K) ∧ (X m = uδ) f ∧ X m / ∈ F orge c (E ′ , K)) ∈ Hist(B)
, then we preserve the same index k ′ for uδ. That is, we generate the same Sub constraint that was generated before and which belongs to Hist(B). Otherwise, i.e. the constraint (t ∈ Sub d (X m , E, E, K)) was not treated with Rule 33 by the interleaving with the master constraint (X i = u), then k ′ will be a fresh index. The same reasoning is valid for Rule 34. Indeed, if the constraint (X m ∈ F orge c (E ′ , K)) was not already treated with Rule 34 by the interleaving with the master constraint (X io = u o ), then the index k ′ o is fresh. Otherwise, we preserve the same index that was generated before by Rule 34 for the constraint (X m ∈ F orge c (E ′ , K)) considering the master constraint (X io = u o ) and which belongs to Hist(B). We reason similarly for Rule 35. Indeed, if the constraint (X m = v) was already treated by Rule 35 by the interleaving with a master constraint (X io = u o ) and then

(X m = v -→ ∃k ′ o (u o δ o = v) ∧ (X m = u o δ o ) f ) ∈ Hist(B)
, we preserve the same index variable as the one generated before. Otherwise, k ′ o will be a fresh index.

Simplification rules with Tagging

We have defined our constraints simplification for untagged terms.

Nevertheless, these rules deal also with tagged terms following the definition of our signature. Indeed, for decomposition in F orge or Sub constraints, our rules behave similarly with tagged terms as for untagged terms. Moreover, for equality constraint, the constraint (X i

) i = u leads to ⊥ when u is untagged, since (X i ) i = [e i , X i ].
Besides, for replacement in F orge or Sub constraints, tagged variables behave as 'special' variable. For example, given a constraint (t ∈ Sub(X i i , E, E, K)), we search for master constraints for the vector -→ X . Then, assuming (X o = u) m is one of them, the replacement result would (t ∈ Sub((uδ) i , E, E, K)) for this master constraint. The same reasoning is valid for a F orge constraint.

Definition 24 (Solved Constraint). A solved constraint is of type:

(X i ∈ F orge c (E, K)) , X ∈ F orge c (E, K), (X i = u) , (X = u) sm , (∀j X i = u) (Y / ∈ F orge c (E, K)), where X ∈ X , Y ∈ X ∪ X I , X i ∈ X I , u ∈ T , j ∈ V ar I (u), E ⊂ T and K ⊂ T
We will prove that at each step of our algorithm, the normalized constraint system contains only solved constraints.

Application to the Asokan-Ginzboorg Protocol

Consider the constraint system to normalize given in Section 10.1. We only focus on the first step of this protocol : mpair(i, L, {E i } p ) ∈ F orge(E 1 , K 1 ) where E 1 = {mpair(t, l, {e} p )}, and E = ∅.

mpair(i, L, {E i } p ) ∈ F orge(E 1 , ∅) -→ (mpair(i, L, {E i } p ) ∈ F orge c (E 1 , ∅)) ∨(mpair(i, L, {E i } p ) ∈ Sub(mpair(t, l, {e} p ), E 1 , E, ∅)) by Rule 9 -→ ∀i (( L, {E i } p ∈ F orge(E 1 , ∅)) ∨ (mpair(i, L, {E i } p ) = mpair(t, l, {e} p )) ∨(mpair(i, L, {E i } p ) ∈ Sub d (mpair(t, l, {e} p ), E 1 , E, ∅))) by Rules 13, 15 -→ ∀i ∀j (( L, {E i } p ∈ Sub(mpair(t, l, {e} p ), E 1 , E, ∅)) ∨ ( L, {E j } p = l, {e} p ) ∨(mpair(i, L, {E i } p ) ∈ Sub d ( l, {e} p , E 1 , E, ∅)) ∨ ( L, {E i } p ∈ F orge c (E 1 , ∅)))
by Rules 9, 19, 15, 22, 24

-→ ∀i ∀j ((L ∈ F orge(E 1 , ∅) ∧ {E i } p ∈ F orge(E 1 , ∅)) ∨ ((L = l) sm ∧ E j = e) ∨( L, {E i } p ∈ Sub( l, {e} p , E 1 , E, ∅))
) by Rules 10, 15, 22, 19, 16, 20, 23

-→ ∀i ∀j ((L ∈ F orge(E 1 , ∅) ∧ E i ∈ F orge(E 1 , ∅) ∧ p ∈ F orge(E 1 , {E i } p )) ∨(L ∈ F orge(E 1 , ∅) ∧ {E i } p ∈ Sub d (mpair(t, l, {e} p ), E 1 , E, ∅)) ∨((L = l) sm ∧ E i = e) ∨ ((L = l) sm ∧ E j = e))
by Rules 9, 11, 15, 22, 23, 16, 17, 20

-→ ∀i ∀j ((L ∈ F orge(E 1 , ∅) ∧ E i = e) ∨ ((L = l) sm ∧ E i = e) ∨ ((L = l) sm ∧ E j = e))
by Rules 15, 19, 16, 17, 20, 22, 23

-→ ∀i ∀j ((L ∈ F orge(E 1 , ∅) ∧ (E i = e) m ) ∨ ((L = l) sm ∧ (E i = e) m ) ∨((L = l) sm ∧ (E j = e) m )) by Rule 4

Verification of Well-Tagged Protocols

We introduce here the verification algorithm and the results that state the correctness and the completeness of the inference rules of Section 4 and decidability for protocols without mpair(, )'s and indexed variables. Given a set R of inference rules and a formula F we say that R(F ) is a closure of F by R if it is derived by a finite number of applications of rules in R and no rule can be further applied to R(F ). First of all, we define a reduction of equalities chain in an environment: Notation 2. (⌈E⌉) We note ⌈E⌉ the closure of E by the following rules:

X = Y ∧ Y = u -→ X = u ∧ Y = u X i = Y i ∧ Y j = u -→ X i = uδ k ′ Q,i ∧ Y j = u for X, Y ∈ X ∪ X I , X i , Y j ∈ X I and u / ∈ X ∪ X I .
Second, we introduce the normalisation function denoted by S → (S)  . A normalisation of a constraint system can be defined when some closures can be computed as follows using a subset of the inference rules. This normalization operates in two main phases:

Definition 25 (Normalization function). Let S be a block system. We denote by SR the whole set of inference rules except Rule 4. We assume that we can compute:

Phase 1: S 1 , a closure of S through SR except Rules 26 and 27; Labelling: S 2 , a closure of S 1 through Rules 4 and 5 only; Phase 2: S 3 , a closure of S 2 through SR. This closure is denoted by (S)  .

The Labelling step adds labels for creating master constraints (Rule 4), making sure to always favour labelling of equality constraints to a forge constraints (Rule 5). While Phases 1 and 2 are similar by the rules they use, their behaviors differ: when used in our algorithm for a step R i ⇒ S i , Phase 1 will never use any constraint interleaving rule with a master constraint M( -→ X ) with L(X) = E i-1 . This means that during Phase 1, the variables with maximum level cannot be replaced yet from a block to an other, simply because none of them have master constraints yet. However, the second phase do not have this limitation. The verification algorithm is the following:

Algorithm 1. Let P = {R ′ ı ⇒ S ′
ı |ı ∈ J} be Well-Tagged, Sec ∈ T , and S 0 ⊂ T g . 1. Guess a correct execution order π : J → 1..k.

Let

R i R ′ π -1 (i) and S i S ′ π -1 (i) ∀i ∈ 1..k. Let R k+1 Sec. 3. Let CBS 0 ∀Q ∃R ⊤, with Q = R = ∅, be the initial constraint system. 4. For i from 1 to k + 1 : (a) Assume that CBS i-1 ∀Q∃R B 1 ∨ B 2 ∨ .. ∨ B p ; (b) Let ctr i R i ∈ F orge(S 0 , S 1 , .., S i-1 , ∅); (c) Let E i = - → X M(CBS i-1 , -→ X ) and for all j = 1, ..p, X, Y ∈ X ∪X I , E i,j = ⌈E i ∪ SM(B j , X )⌉\{(X = Y )}; (d) Let CBS i ( ∀Q∃R (B 1 ∧ ctr i , E i,1 ) ∨ .. ∨ (B p ∧ ctr i , E i,p ) )  5. Test Satisfiability of CBS k+1 (return insecure iff satisfiable).
Note that sets E i , E i,j denotes respectively the set of master constraints for vector variables and the set of submaster constraints for variables of block B j , both with variables of level strictly included in E i-1 . Notation ⊤ represents true. The algorithm chooses a "possible" protocol run represented by π, and tests if after this run Sec is derivable by the intruder for some length e of mpair(, ). We test this by increasing the initial constraint system CBS 0 with each protocol step successively, and by normalising the resulting constraint system at each step. This step-by-step normalisation is required by our inference rules which assumes that master and sub-master constraints for previous steps have been already computed.

Results obtained for our inference system are the followings:

Theorem 2. The insecurity problem for Well-Tagged protocols with Autonomous Keys is decidable.

The proof of Theorem 2 follows from Lemmas 3, 4 and 5.

Lemma 3. (Correctness and Completeness of Normalization) Let CBS i and ctr i (i = 1..k + 1) be as in the verification algorithm, for some Well-Tagged protocol P . Then for all e, |[

CBS i-1 ∧ ctr i ]| e ∅ = (CBS i-1 ∧ ctr i )  e ∅ Lemma 4. (Termination of Normalization)
Algorithm 1 terminates for Well-Tagged protocols with Autonomous Keys.

Lemma 5. (Satisfiability of normalized form) When Algorithm 1 is applied to a Well-Tagged protocol P with autonomous keys, the satisfiability of the resulting normalised constraint system can be decided.

The proof of Lemma 3 is in Section 6. The proof of Lemma 4 is in Section 8. The proof of Lemma 5 is in Section 9. It is worth also to notice that our algorithm always terminates for protocols without mpair(, )'s and without index variables (See Section 7), thus showing that our procedure is an extension of protocol analysis in the basic case. Also, note that the satisfiability of CBS k+1 will be trivial to check for protocols without mpair(, ). Moreover, the satisfiability of CBS k+1 is also trivial to check in our example, the Asokan-Ginzboorg protocol.

Correctness and completeness

The aim of this section is to show that the different reduction rules preserve the set of solutions. That is, we say that a rule

F 1 → F 2 over a constraint system is complete when ∀e, |[ F 1 ]| e ∅ ⊆ |[ F 2 ]| e ∅ , and correct when ∀e, |[ F 1 ]| e ∅ ⊇ |[ F 2 ]| e ∅ .
Note also for a rule r, post(r) denotes the right hand side of r and pre(r) denotes the left hand side of r.

We first need a notion of variable level :

Definition 26 (Variable Level, Vector Level). Assuming that P , Sec, S 0 are as in Definition 6 and π is a correct execution order for the protocol, we denote by

E i = S 0 , S 1 , .., S i for any i ∈ 1..k. Let A ∈ X ∪ X I . Then, L(A) is the smallest set E i for i = 1 . . . k such that A ≤ R i+1 .
We extend the notion of level to variable vector in the following way: Let

-→ X ∈ -→ X . Then, L( -→ X ) is the smallest set E i for i = 1 . . . k such that ∃m ∈ I with E i = L(X m ).
We give some properties that are preserved by our constraint solving rules and permit us to prove the correctness and the completeness of the algorithm.

Properties of the Rules System

We show invariants that state properties satisfied by terms or constraints occuring in any constraint system derived at some step in the normalization.

Invariant 1. #V ar I (t) ≤ 1 for t ∈ T .
Invariant 1 will be used for the correctness and completeness proof of Rule 35.

Proof. Initially constraints are of the form t ∈ F orge(E, K). According to the property of mpair autonomy over P (See Definition 8), we have V ar I (t) = ∅. Thus Invariant 1 is satisfied by the initial constraints. We show that the application of any rule of SR preserves this invariant. Rules 1, 4, 5, 6 and 8 do not change any constraint then Invariant 1 remains satisfied. Rule 2 changes a constraint into another one using the same terms as for the left-hand side of the rule. Then, Invariant 1 is preserved. Rule 3 eliminates the whole block. Then, the invariant still holds. Rule 7 adds a new constraint Y j = Z to the block and this constraint satisfies the Invariant. Rule 9 transforms a constraint t ∈ F orge(E, K) to either a F orge constraint t ∈ F orge c (E, K) conserving the same t or to a Sub constraint using the two terms t and w ∈ E. By induction hypothesis we have #V ar I (t) ≤ 1. Besides, according to the property of mpair autonomy over P, we have V ar I (w) = ∅ and then #V ar I (w) = 0. Therefore, the invariant is preserved. Rule 10 decomposes the term t 1 , . . . , t m to be forged into its subterms t i , i = 1 . . . m. Since #V ar I ( t 1 , . . . , t m ) ≤ 1 (by induction hypothesis the invariant is satisfied on the block system to be rewritten), we have #V ar

I (t i ) ≤ 1 ∀i = 1 . . . m.
A similar reasoning applies to Rules 11 and 12. For Rule 13, according to the property of mpair autonomy over terms we have V ar I (t) = {k}. Thus the invariant is satisfied. Rule 14 eliminates the whole block. Then, the invariant still holds. Rule 15 transforms a Sub constraint either to another Sub constraint or Equality one while preserving the two terms t and u. The invariant is then preserved in the two cases. In Rule 16, the Sub constraint is transformed into a Sub constraint with the same term t and subterm t i of t 1 , . . . , t m . Since #V ar I ( t 1 , . . . , t m ) ≤ 1 (by induction hypothesis), we have #V ar

I (t i ) ≤ 1 ∀i = 1 . . . m.
A similar reasoning applies to Rules 17 and 18 (with addition of F orge constraint with a subterm of the initial term t).

For Rule 19, according to the property of mpair autonomy over terms we have V ar I (u) = {k}. Thus, the invariant is satisfied. Rule 20 eliminates the whole block. Then, the Invariant remains valid. Rules 21 and 22 eliminate either the constraint (⊤) or the block (⊥). Then, the invariant is preserved. Rule 23 transforms an Equality constraint with two terms t and t ′ into equality constraints with subterms of t and t ′ . Then, the invariant is preserved.

For Rule 24, according to the property of mpair autonomy over terms we have V ar I (u) = {k} and V ar I (v) = {l}. Thus, the invariant is satisfied. Rule 25 replaces an index variable by another index variable in a block. Thus, the invariant remains satisfied.

In Rules 26, 27, 28, 29, 30 and 31, the block system resulting from the rewriting has the same terms as the one that is reduced. Thus the invariant is satisfied. Rule 32 eliminates the block and the invariant obviously holds. Rules 33, 34 and 35, transforms a block system into one built with the same terms as the initial one, reduced modulo some index replacement. Thus the invariant is satisfied.

Invariant 2. We say that a constraint ctr is a constraint for X (or

X has a constraint ctr) if ctr = (X ∈ F orge c (E, K)) or ctr = (X = u). ∀X ∈ X ∪ X I , for any rule r in SR ∪ {Rule 4}, if X has a constraint in pre(r), then it has a constraint in any B with B ∈ post(r)
Invariant 2 is used in the proof of Corollaries 1 and 2.

Proof. We show that the application of any rule of SR ∪ {Rule 4} preserves Invariant 2. Rule 2 transforms a constraint for Y into another constraint for Y without elliminating the other constraints. Thus, we still have constraints for both X and Y . Rule 3 eliminates the block. Then, the invariant holds. Rules 4, 5, and 8 do not change constraints. Rule 6 transforms a constraint for X into another constraint for X without elliminating other constraints. Thus, we still have constraints for both X and Y j . Rule 7 transforms a constraint for X into another constraint for X, while adding a new constraint for Y j . We conclude that control rules satisfies the invariant. Rule 9 may add a constraint for a variable but can not eliminate ones. Thus, the invariant holds. The other rules of Group G 2 do not treat constraints for variables. Then, the invariant remains valid. Rule 15 may add a constraint for a variable but can not eliminate ones. Then, the invariant is satisfied. The other rules of Group G 3 do not treat constraints for variables. Thus, Group G 3 preserves the invariant. Rule 23 may add a constraint for a variable but can not eliminate ones. Thus, the invariant holds. The other rules of Group G 4 do not manage constraints for variables. Thus, Group G 4 preserves the invariant. Rules 26, 27, 30 and 31, do not eliminate constraints for variables. Rule 28 eliminates a constraint for X i (X i ∈ F orge c (E ′ , K)) but it remains another constraint for X i : X i = u. We reason similarly for Rule 29. Rule 32 eliminates the block. We conclude that interleaving rules inside a block preserve Invariant 2. In Rule 34, the constraint for X m :

X m ∈ F orge c (E ′ , K) would be transformed in either X m ∈ F orge c (E ′ , K) or X m = u 0 δ 0 .
Then, in both cases, we still have a constraint for X m . In Rule 35, the constraint for X m : X m = v is either preserved or transformed into another constraint : X m = u 0 δ 0 . Then, in both cases, we still have a constraint for X m . We conclude that interleaving rules between different blocks preserve Invariant 2, and therefore it is preserved by SR ∪ {Rule 4}.

Invariant 3. For a constraint (t ∈ Sub (w, E, E, K)), we have ∀X ≤ w where X ∈ X ∪ X I , L(X) ⊂ E.

Invariant 3 is used in the proof of Proposition 21.

Proof. Initially, Sub constraints are obtained from F orge ones by Rule 9. We get a constraint t ∈ Sub(w, E, E, K) where w ∈ E. Then, ∀X ≤ w and according to the notion of correct execution, and the definition of L(X), In what follows, properties and lemmas introduced are limited to the first phase of the computation of a certain CBS i .

we
Invariant 4. ∀ctr in the computation of some

CBS i at phase 1, ∀X ∈ X ∪ X I s.t L(X) = E i-1 , if ctr = t ∈ Sub (w, E, E, K) s.t X ≤ t and ∀Y ≤ w then L(Y ) ⊂ L(X).
Invariant 4 is used in the proof of Proposition 1.

Proof. Initially, constraints are F orge ones. Then, the invariant is satisfied. We prove that Invariant 4 is preserved at each application of a rule of our inference rules. The first group does not manage Sub constraints. Then, the invariant remains satisfied. Rule 9 manages a constraint t ∈ Sub(w, E, E, K) where w ∈ E. However, according to the notion of correct execution, and by definition of L(Y ), E ⊂ E i and L(Y ) ⊆ E. Thus, L(Y ) ⊂ L(X), which satisfies the invariant. The other rules of Group G 2 do not manage Sub constraints. Therefore, Group G 2 satisfies the invariant. Rules 15 transforms a Sub constraint into another Sub d constraint with the same t and u. Thus, the invariant still holds. Rule 20 eliminates the whole block. Then, the invariant remains valid. The other rules of Group G 3 decompose the term inside the Sub constraint. Then, the invariant still holds. Thus, Group G 3 satisfies the invariant. Group G 4 does not treat Sub constraints. Then, the invariant still holds. Rule 31 generates a constraint t ∈ Sub d (w, E, E, K). However, w comes from a sub-master constraint (X = w) ∈ E. By construction of the environment, L(Y ) ⊂ L(X), which satisfies the invariant. The other rules of Group G 5 do not manage Sub constraints. Then, Group G 5 satisfies the invariant. Rule 33 generates a constraint t ∈ Sub d (uδ, E ′ , E, K). However, uδ comes from a master constraint X i = u ∈ E. By construction of E, L(Y ) ⊂ L(X), which satisfies the invariant. The other rules of Group G 6 do not treat Sub constraints. Thus, Group G 6 satisfies the invariant. We conclude that Invariant 4 is satisfied by our inference rules.

Definition 27. We say that a constraint ctr ′ has type (1), (1 ′ ),(2),(2 ′ ) or (3) for a variable X if

ctr ′ = (t ∈ F orge(E, K))
where X ≤ t, (1)

or ctr ′ = (t ∈ F orge c (E, K))
where

X ≤ t, (1 ′ ) or ctr ′ = (t ∈ Sub(u, E, E, K)) where X ≤ t (2) or ctr ′ = (t ∈ Sub d (u, E, E, K)) where X ≤ t (2 ′ ) or ctr ′ = (u = v) where X ≤ u or X ≤ v (3)
Invariant 5. For any rule r in SR except Rules 26 and 27 (ie. Rules of the phase 1), ∀X ∈ X ∪ X I s.t

L(X) = E i-1 , if pre(r) contains a constraint of type (1), (1 ′ ), (2), (2 ′ ) or (3) for X then ∀B ∈ post(r), B contains a constraint of type (1), (1 ′ ), (2), (2 ′ ) or (3) for X.
Proof. Rules 3, 14, 20,22, 32 eliminate the whole block. Then the invariant is valid. Rules 1, 2, 4, 5 and 8 do not change constraints. Then, the invariant remains valid.

In Rule 6 and 7, constraints for other variables than Y j do not change. For Y j , there exists a constraint of type (3). Thus, the invariant still holds.

For Rule 9, we obtain either a constraint of type (1 ′ ) or a constraint pf type (2) for X. For Rules 10, 11, 12 and 13, the term t is decomposed. We obtain as a result, a constraint of type (1) for X. We conclude that F orge constraints validate the invariant.

For Rule 15, we obtain either a constraint of type (3) or a constraint of type (2 ′ ) for X. For Rules 16, 17, 18 and 19, the term t is decomposed. We obtain as a result, a constraint of type (2) for X. We conclude that Sub constraints validate the invariant.

In Rules 21 and 25, pre(r) does not contain a constraint of type (1), (1 ′ ),(2),(2 ′ ) or (3) for X. For Rules 23 and 24, the term t is decomposed. We obtain as a result, a constraint of type (3) for X. We conclude that Equality constraints validate the invariant. For Rule 28, (X i ∈ F orge c (E, K)) is tranformed to (u ∈ F orge c (E, K)) but it still exists a constraint of type (3) for X i which is (X i = u) . The same reason is valid for Rule 29. In Rule 30, there is a constraint of type (1 ′ ) for A. We conclude that rules for interleaving in the same block preserve the invariant. Rules 33 and 34 preserve the same constraint given in pre(r). Rule 35 uses the same terms in equality constraints. Then, it transforms a constraint of type (3) for variables in v or X m into other constraints of the same type. We conclude that rules for interleaving in different blocks preserve the invariant.

Proposition 1. At the end of Phase 1 in the computation of CBS i , for all X ∈ X ∪ X I , for all blocks B there is a constraint ctr ∈ B such that ctr = (X ∈ F orge c (E, K)) or ctr = (X = u).

Proof. We first introduce the following claim:

Claim 1. ∀ctr in the computation of some

CBS i at phase 1, ∀X ∈ X ∪ X I s.t L(X) = E i-1 , if ctr = (Y = u) and X ≤ u then L(Y ) < L(X).
Proof. We show by contradiction that if ctr = (Y = u) and

X ≤ u then L(Y ) < L(X). Let ctr = (Y = u) such that L(Y ) = L(X). Consider a derivation d = d ′ j .L j .d j such that (Y = u) ∈ post(L j ). Then, ∃l < j such that (u ′ = v ′ ) ∈ post(L l ) where Y ≤ v ′ and u ≤ u ′ and pre(L l ) = (u" = v") where u ′ < u" and v ′ < v". (u ′ = v ′
) is obtained either by transforming a Sub constraint to an Equality one by Rule 15, or by interleavings (Rule 35). Note that Rules 33 and 34 generates equality contraints bu not suitable for our case since they may not contain X since they are in E and L(X)

= E i-1 . 1. Case pre(L l ) = (u ′ ∈ Sub(v ′ , E, E, K)). Since X < u ′ , L(X) = E i-1 and we compute CBS i , according to Invariant 4, we have L(Y ) ⊂ L(X) which contradicts the hypothesis: L(Y ) = L(X). The same reasoning is valid if pre(L l ) = (v ′ ∈ Sub(u ′ , E, E, K)). 2. case L l = R 35, then pre(L l ) = (X m = u ′
) and as master constraint we have (X i = v ′ ). Since we are in the first phase, that is before labeling master or submaster constraints for variables of level

E i-1 , then L(v ′ ) ⊂ E i-1 . Since L(X) = E i-1 and Y < v ′ then L(Y ) ⊂ L(X) which is in contradiction with our hypothesis L(Y ) = L(X).
Note that at the end of Phase 1 in the computation of CBS i , we only have solved constraints (Hypothesis H 1 ). We show by contradiction that there exists a constraint ctr for X in each block of the constraint system S. Let B be a block of S such that ∄ctr ∈ B for X (Hypothesis H 2 ). According to Invariant 5, ∃ctr ′ ∈ B such that ctr ′ has type (1), (1 ′ ), (2), (2 ′ ) or (3) for X. There are five cases. In the first one, ctr ′ = (t ∈ F orge(E, K)) where X < t, otherwise (when t ∈ X ∪ X I ) ctr = ctr ′ which is in contradiction with hypothesis H 1 . Then, Rule 9 may be applied which is in contradiction with hypothesis H 1 . In the second case, ctr ′ = (t ∈ F orge c (E, K)) where X < t. Then, Rules 10, 11, 12 and 13 may be applied which is in contradiction with hypothesis H 1 . In the third case, ctr ′ = (t ∈ Sub(u, E, E, K)) where X ≤ t. Then, Rule 15 may be applied which contradicts hypothesis H 1 . In the fourth case, ctr ′ = (t ∈ Sub d (u, E, E, K)) where X ≤ t. There are two cases. In the first one, u / ∈ X ∪ X I . Then, Rules 16, 17, 18, 19 and 20 may be applied what contradicts hypothesis H 1 . In the second case, u = Y ∈ X ∪ X I . Then, according to Invariant 4, we have L(Y ) ⊂ L(X). Thus, ∃ctr 3 ∈ E such that ctr 3 = (Y ∈ F orge(E3, K ′ )) or ctr 3 = (Y = u3) (by construction of E). Therefore, Rules 31, 32 and 33 may be applied which contradicts hypothesis H 1 . In the fifth case, ctr ′ = (u = v) where X ≤ v or X ≤ u. There are two cases. In the first one, u / ∈ X ∪ X I . Then, Rules 22, 23 and 24 may be applied what contradicts hypothesis H 1 . In the second case, u ∈ X ∪ X I . If u = X then ctr ′ = ctr which contradicts hypothesis H 2 . If u = Y and X ≤ v then according to Claim 1, L(Y ) ⊂ L(X). Then, ∃ctr" ∈ E for Y and therefore Rules 27 and 35 may be applied which contradicts hypothesis H 1 .

Corollary 1. At the end of every phase, for every block B, ∀X i ∈ X I , there exists a single master constraint

(ctr) m ∈ B such that ctr = (X i ∈ F orge c (E, K)) or ctr = (X i = u).
Proof. For Phase 1 this is an immediate consequence of Proposition 1. The unicity of the master constraint is guaranteed by the condition B ∩ M( -→ X ) = ∅ of Rule 4. At the begining of Phase 2, for a block B, ∀X i ∈ X I , there exists a single constraint (ctr) m ∈ B such that ctr = (X i ∈ F orge c (E, K)) or ctr = (X i = u) since Invariant 1 is preserved by Phase 1. According to Invariant 2, our system of rules preserve constraints for X i (F orge or Equality constraints for X i ) which are potential master constraints for X i . Our rules never eliminate a master constraint for a variable. They can change a master constraint for a variable after introducing new candidate constraints (Equality constraints for the variable). This is managed by Rule 5. Rule 5 labels a new master constraint for -→ X INRIA (X j = u) while eliminating the label of the old master constraint. Thus, in that case we still have a single master constraint for -→ X .

Corollary 2. At the end of every phase, for every block B, ∀X ∈ X , there exists a constraint ctr ∈ B such that ctr = (X ∈ F orge c (E, K)) or ctr = (X = u).

Proof. The proof follows directly from Proposition 1 and Invariant 2.

Correctness and Completeness of Rules

We prove correctness and completeness of each rule of our system for an index substitution τ and a value e for n. Correctness and completeness of Rules 1, 6, 7, 21 and 22 is trivial. For Rules 4, 5 and 8, since the semantics of a constraint is the same with or without the label, and since these rules only modify labels then they are complete and correct.

Proposition 2. Rule 2 is correct and complete. Correctness and completeness of Rule 9 follows from Propositions 4 and 5 below.

Proof. σ ∈ |[ (X = u) sm ∧ (Y = X) ]| e τ iff X e τ σ = u e τ σ ∧ Y e τ σ = X e τ σ iff X e τ σ = u e τ σ ∧ Y e τ σ = u e τ σ iff σ ∈ |[ (X = u) sm ∧ (Y = u) ]|
Proposition 4. |[ B ∧ t ∈ F orge(E, K) ]| e τ ⊆ (B ∧ t ∈ F orge c (E, K)) ∨ w∈E (B ∧ t ∈ Sub(w, E, E, K)) e τ . Proof. Let σ ∈ |[ B ∧ t ∈ F orge(E, K) ]| e τ . Then, σ ∈ |[ B ]| e τ ∩ |[ t ∈ F orge(E, K) ]| e τ . But, |[ t ∈ F orge(E, K) ]| e τ = |[ t ∈ F orge c (E, K) ]| e τ ∪ (|[ t ∈ F orge(E, K) ]| e τ \|[ t ∈ F orge c (E, K) ]| e τ
). Thus, we will prove that ∃w ∈ E s.t.

σ ∈ |[ t ∈ Sub(w, E, E, K) ]| e τ if σ ∈ (|[ t ∈ F orge(E, K) ]| e τ \|[ t ∈ F orge c (E, K) ]| e τ
). We first prove some lemmas. We will prove this proposition by using the following lemma that follows from Proposition 2 from [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF]. Lemma 6. Let t ∈ Dy(E, K) and γ ∈ Dy c (E, K) be given with D γ (E) ∈ N RD. Then, there is a derivation

D ′ t (E) ∈ N RD verifying L d (γ) / ∈ D ′ .
Proof. The proof is exactly the same as mentioned in [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF] with the difference that D γ (E) is not a minimal derivation but rather a non-redundant derivation. The proof remains valid as we have no useless rules in D γ (E) since it is a non-redundant derivation. Moreover, D ′ t (E) as it is constructed in [START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is np-complete[END_REF] is a general derivation. However, according to Remark 1, there exists an equivalent non-redundant derivation for D ′ t (E). In our context, Lemma 6 says that for any term t, a set of terms E, a set of terms K and a variable X ∈ X ∪ X I , and for any e, τ and σ, if t e τ σ ∈ Dy(Eτ σ, K e τ σ) and Xτ σ ∈ Dy c (E e τ σ, K e τ σ) then there exists a derivation D ′ building t e τ σ from E e τ σ where Xτ σ is never decomposed. This can be easily generalized from singleton {X} to any set of variables instead of X. In the second case, ∃v, δ, k, τ

(1) ∃v, δ, k, τ ′ s.t k / ∈ {t, X, E}, Xτ σ = v e δτ ′ σ, vδ / ∈ X ∪ X I and σ ∈ |[ t ∈ Sub(vδ, E, E, K) ]| e τ ′ (
′ s.t k / ∈ V ar I (t, w, E), σ ∈ |[ t ∈ Sub(vδ, E, E, K) ]|
e τ ′ and uσ = v e δτ ′ σ. We can suppose that vδ / ∈ X ∪ X I . Otherwise, by Proposition 6, there exists another choice for v, δ, k, τ ′ such that either vδ / ∈ X ∪ X I or t e τ σ = vδτ σ. The last case leads to t e τ σ ∈ Dy d (E e τ σ ∪ {w e τ σ}, K e τ σ) since F σ ⊆ Dy(E e τ σ, K e τ σ) and t e τ σ Lσ F σ w e τ σ. Thus, assuming that vδ / ∈ X ∪ X I , we have two cases.

• In the first case, u = w e τ and then v e δτ σ = w e τ σ. If vδ ∈ C ∪ C I then, |v e δτ σ| = 1 which follows from the initial case of recurrence. Otherwise, ∃w ′ such that vδ = f (w ′ ) where f ∈ G.

Let F 0 = {b} if vδ = {w ′ } b and F 0 = ∅ otherwise. Note that F 0 ⊆ F . Besides, since σ ∈ |[ t ∈ Sub(vδ, E, E, K) ]|
Proposition 8. Rule 13 is correct and complete.

Proof. According to our semantics, we have :

|[ ∀Q ∃R S ∨ (B ∧ mpair(k, t) ∈ F orge(E, K)) ]| e = Q R |[ S ∨ (B ∧ mpair(k, t) ∈ F orge(E, K)) ]| e τ = Q R |[ S ]| e τ ∪ (|[ B ]| e τ ∩ |[ mpair(k, t) ∈ F orge(E, K) ]| e τ ) = Q R |[ S ]| e τ ∪ (|[ B ]| e τ ∩ |[ ∀kt ∈ F orge(E, K) ]| e τ ) (according to Lemma 9) = Q R k |[ S ]| e τ ′ ∪ (|[ B ]| e τ ′ ∩ |[ t ∈ F orge(E, K) ]| e τ ′ ) (since k fresh, τ ′ = τ.[k ← n k ]) = Q k R |[ S ]| e τ ′ ∪ (|[ B ]| e τ ′ ∩ |[ t ∈ F orge(E, K) ]| e τ ) (thanks to mpair autonomy) = Q.k R |[ S ∨ (B ∧ t ∈ F orge(E, K)) ]| e τ = |[ ∀Q.k ∃R S ∨ (B ∧ t ∈ F orge(E, K)) ]| e τ
Correctness and completeness of Rule 14 is trivial. Completeness and correctness of Rule 15 follow from Proposition 9 and Proposition 10. Thus, u L F w e τ leads to u = w e τ . We can suppose that w / ∈ X ∪ X I , otherwise u L F w leads to u< L F w. Therefore, we only have the first case of the semantic of Sub that is uσ = t e τ σ which leads to w e τ σ = t e τ σ.

• (w = {v} b or b / ∈ K). Then, we have the two cases of the semantics of Sub:

-In the first case, uσ = t e τ σ. Moreover, u L F w e τ . Then, either u < L F w e τ which leads to

σ ∈ |[ (t ∈ Sub d (w, E, E, K)) ]|
∈ K). Let σ ∈ |[ (t = w) ∨ (t ∈ Sub d (w, E, E, K)) ]| e τ .
There are two cases:

-σ ∈ |[ (t = w) ]| e τ .
We show in a similar way as the first case (w = {v} b and b

∈ K) that σ ∈ |[ (t ∈ Sub(w, E, E, K)) ]| e τ . -σ ∈ |[ (t ∈ Sub d (w, E, E, K)) ]|
Proof. Let W = |[ i=1...m (t ∈ Sub(t i , E, E, K)) ]| e τ . Let σ ∈ |[ t ∈ Sub d ( t 1 , .., t m , E, E, K) ]| e τ . Then, ∃u, ∃F, L such that u < L F t 1 , .., t m e τ , K e τ σ ∩ F σ = ∅,
F σ ⊆ Dy(E e τ σ, K e τ σ) and the two possibilities for u (the two cases of the semantics of Sub).

τ σ ∩ F σ = ∅ which leads to σ ∈ |[ t ∈ Sub d ( t 1 , .., t m , E, E, K) ]| e τ .
Proposition 12. Rules 17 and 18 are correct and complete.

Proof. First focus on Rule 17.

Let W = |[ t ∈ Sub(w, E, E, K) ∧ b ∈ F orge(E, K ∪ {b}) ]| e τ . Let σ ∈ |[ t ∈ Sub d ({w} s b , E, E, K) ]| e τ . Then, ∃u, ∃F, L s.t u < L F {w} s b e τ , K e τ σ ∩ F σ = ∅, F σ ⊆ Dy(E e τ σ, K e τ σ)
In order to prove Proposition 16, we first prove Lemma 10. Proof.

σ ∈ |[ mpair(k, u) = mpair(l, w) ]| e τ iff mpair(k, u) e τ σ = mpair(l, w) e τ σ iff τ k,1 (u) e , . . . , τ k,v (u) e τ σ = τ l,1 (w) e , . . . , τ l,v (w) e τ σ iff τ k,1 (u) e τ σ, . . . , τ k,v (u) e τ σ = τ l,1 (w) e τ σ, . . . , τ l,v (w) e τ σ iff i=1,...,e (τ k,i (u) e τ σ = τ l,i (w) e τ σ) iff i=1,...,e (τ k,i (u) e τ σ = τ k,i (wδ l,k ) e τ σ) iff i=1,...,e (u e τ τ k,i σ = wδ l,k e τ τ k,i σ) iff σ ∈ i=1,...,e |[ u = wδ l,k ]| e τ,τ k,i iff σ ∈ |[ ∀k u = wδ l,k ]| e τ
Proposition 16. Rule 24 is correct and complete.

Proof. According to our definitions, we have:

|[ ∀Q ∃R S ∨ (B ∧ (mpair(k, u) = mpair(l, w))) ]| e = Q R |[ S ∨ (B ∧ (mpair(k, u) = mpair(l, w))) ]| e τ
(where τ assigns values to Q and R)

= Q R (|[ S ]| e τ ∪ (|[ B ]| e τ ∩ |[ mpair(k, u) = mpair(l, w) ]| e τ )) = Q R (|[ S ]| e τ ∪ (|[ B ]| e τ ∩ |[ ∀k u = wδ l,k ]| e τ )) (according to Lemma 10) = Q R k (|[ S ]| e τ ′ ∪ (|[ B ]| e τ ′ ∩ |[ u = wδ l,k ]| e τ ′ )) (since k is fresh, τ ′ = τ.[k ← n k ]) = Q k R (|[ S ]| e τ ′ ∪ (|[ B ]| e τ ′ ∩ |[ u = wδ l,k ]| e τ ′ )) (thanks to mpair autonomy, V ar I (u)∩R = V ar I (w)∩R = ∅)) = Q.k R (|[ S ∨ (B ∧ (u = wδ l,k )) ]| e τ ′ ) = |[ ∀Q.k ∃R S ∨ (B ∧ (u = wδ l,k )) ]| e τ .
Proposition 17. Rule 25 is correct and complete.

Proof. This follows directly from the fact that each two constants c i and c j are different.

Proposition 18. Rules 26 and 27 are correct and complete.

Proof. Correctness of Rule 26 is trivial. For it's completeness, let σ Proof. First focus on Rule 28. According to our semantics, we have:

∈ B ∧ (X i = u) ∧ (X i = v) e τ . Then, X i τ σ = u e τ σ and X i τ σ = v e τ σ. Thus, σ ∈ B ∧ (X i = u) ∧ (X i = v) ∧ u = v
σ ∈ (X i = u) ∧ X i ∈ F orge c (E ′ , K) e τ iff σ ∈ (X i = u) e τ ∩ |[ X i ∈ F orge c (E ′ , K) ]| e τ iff X i τ σ = u e τ σ and X i τ σ ∈ Dy c (E e τ σ, K e τ σ) iff X i τ σ = u e τ σ and u e τ σ ∈ Dy c (E e τ σ, K e τ σ) iff σ ∈ (X i = u) ∧ u ∈ F orge c (E ′ , K) e τ .
Second, correctness and completeness of Rule 29 follows in a similar way. Moreover, this is trivial for Rule 30 as it follows direclty from the fact that E ⊂ E ′ and since Aτ σ ∈ Dy c (E e τ σ, K e τ σ), then Aτ σ ∈ Dy c (E ′ e τ σ, K e τ σ).

Proposition 20. Rule 31 is correct and complete.

Proof. correctness:

Let σ ∈ |[ (X = w) sm ∧ t ∈ Sub(w, E ′ , E, K) ∧ X / ∈ F orge c (E, K) ]| e τ . Let u = X, δ = ∅, τ ′ = τ . Then, uσ = Xσ = w e δτ ′ σ that leads to uσ / ∈ Dy c (E ′ e τ σ, K e τ σ), and σ ∈ |[ t ∈ Sub(wδ, E ′ , E, K) ]| e τ ′ . Moreover, u< ∅ ∅ X and ∅ ⊆ Dy(E ′ e σ, ∅), thus proving σ ∈ |[ t ∈ Sub d (X, E ′ , E, K) ]| e τ according to the definition. Completeness: let σ ∈ |[ (X = w) sm ∧ t ∈ Sub d (X, E ′ , E, K) ]| e τ where (X = w) sm ∈ E. Let u, F, L be the objects defined by u L F X, F σ ∩ K e τ σ = ∅ and F σ ⊆ Dy(E ′ e σ, K e σ) in the definition of t ∈ Sub d (X, E ′ , E, K).
Since Sub d ensures that u< L F X in case uσ = t e τ σ and since u< L F X is impossible, then we have uσ = t e τ σ and u = X. Thus, u and F validates the second case of the semantics of Sub with u ∈ X , and therefore, Since Sub d ensures that u< L F A in case uσ = t e τ σ and since u< L F A is impossible, then we have uσ = t e τ σ and u = A. Thus, u and F validates the second case of the semantics of Sub and therefore, ∃v, δ, k, τ ′ such that uσ / ∈ Dy c (E ′ e τ ′ σ, K e τ ′ σ). Nevertheless, uσ = Aσ. Then, Aσ / ∈ Dy c (E ′ e σ, K e τ ′ σ). Moreover, Aσ ∈ Dy c (E e σ, K e τ ′ σ). However, E ⊆ E ′ . Indeed, according to Invariant 3, L(A) ⊆ E ′ . Then, either

∃v, δ, k, τ ′ such that (X = v) ∈ E, δ = ∅, τ ′ = τ , k, i / ∈ {t, X, E}, X / ∈ F orge c (E, K), uσ = v e δτ ′ σ and σ ∈ |[ t ∈ Sub(vδ, E ′ , E, K) ]| e τ . However, since (X = u) sm ∈ E, then we choose v = w which lead to σ ∈ |[ (X = w) sm ∧ t ∈ Sub(w, E ′ , E, K) ∧ X / ∈ F orge c (E, K) ]|
L(A) = E or L(A) ⊆ E.
In the last case, there are two possibilities. In the first one, A ∈ F orge c (E, K) would be simplified to A ∈ F orge c (L(A), K) if at level L(A) we have A ∈ F orge c (L(A), K) as constraint for A. In the second possibility, A ∈ F orge c (E, K) would be eliminated if at level L(A) we have A = u as constraint for A. This is due to the fact that for the level L(A) we have a constraint F orge or Equality according to the Proposition 1. We conclude that E ⊆ E ′ . Therfore, Aσ / ∈ Dy c (E ′ e σ, K e τ ′ σ) and Aσ ∈ Dy c (E ′ e σ, K e τ ′ σ)

proving that σ ∈ |[ ⊥ ]| e τ . Proposition 22. Rule 33 is correct and complete. Proof. Completeness: if σ ∈ |[ t ∈ Sub d (X m , E ′ , E, K) ]| e τ , then ∃(X j = v) ∈ E, ∃k / ∈ {t, X m , E}, ∃n k s.t. τ ′ = τ.[k ← n k ], σ ∈ |[ t ∈ Sub(vδ, E ′ , E, K) ]| e τ ′ , σ ∈ |[ X m = vδ ]| e τ ′ and σ / ∈ |[ X m ∈ F orge c (E ′ , K) ]| e τ ′ , with δ = δ k j,m . To show this, let u, F, L be the u L F X m τ , F σ ∩ K e τ σ = ∅ and F σ ⊆ F orge(E ′ e τ σ, K e τ σ) from the semantics of Sub d proving that σ ∈ |[ t ∈ Sub d (X m , E ′ , E, K) ]| e τ ′ .
Note that Sub d is more restrictive than Sub in the sence that it ensures u < L F X m τ in case uσ = t e τ σ. However u < L F X m τ is impossible, so uσ = t e τ σ and u = X m τ necessarily. This means that u, F validate the second case of the semantics of Sub, and thus that ∃v, δ, k, i, j, τ

′ s.t. k, i / ∈ {t, X m , E}, Dom(τ ′ ) = Dom(τ )∪{k, i}, u = X i τ ′ , (X j = v) ∈ E, δ = δ k j,i , uσ / ∈ F orge c (E ′ e τ σ, K e τ σ), uσ = v e δτ ′ σ, and σ ∈ |[ t ∈ Sub(vδ, E ′ , E, K) ]| e τ ′ .
We remark that τ (m) = τ ′ (i) since X m τ = u = X i τ ′ , and so the proposition follows by replacing i by m.

Correctness

: if ∃(X j = v) ∈ E, ∃k / ∈ {t, X m , E}, ∃n k s.t. τ " = τ.[k ← n k ], σ ∈ |[ t ∈ Sub(vδ, E ′ , E, K) ]| e τ " , σ ∈ |[ X m = vδ ]| e τ " and σ / ∈ |[ X m ∈ F orge c (E ′ , K) ]| e τ " , with δ = δ k j,m , then σ ∈ |[ t ∈ Sub d (X m , E ′ , E, K) ]| e τ .
INRIA Assume that the precondition above is true for the objects X j , v, E, k, τ " = τ.[k ← n k ]. Let u = X m τ , thus uσ = X m τ "σ, and let i be a fresh index, δ ′ = δ k j,i , and let e . We denote by Rhs the right-hand side of Rule 35. Then we have two cases : . Moreover, thanks to corollary 1, we know that for any block in B 1 ∨ .. ∨ B s , there exists a master constraint for -→ X in this block. Besides, ∃τ " with ∀i ∈ Q τ "(i) = τ ′ (m) such that ∃j σ ∈ |[ B j ]| e τ " . Thus, σ validates at last one of the master constraints for -→ X for τ ". However, by hypothesis ∀o

τ ′ = τ ".[i ← τ (m)]. Then we have u = X i τ ′ , (X j = v) ∈ E, k, i / ∈ {t, X m , E}, uσ = v e δ ′ τ ′ σ, uσ / ∈ F orge c (E ′ e σ, K e σ) and σ ∈ |[ t ∈ Sub(vδ ′ , E ′ , E, K) ]| e τ ′ . Moreover, we have u ∅ ∅ X m τ and ∅ ⊆ F orge(E e σ, K e σ), thus proving σ ∈ |[ t ∈ Sub d (X m , E ′ , E, K) ]|
• Either ∃o = 1..p ∃n ko s.t. σ ∈ |[ X m = u o δ o ]| e τ ′ with τ ′ = τ.[k ′ o ← n ko ].
= 1..p, σ / ∈ |[ X m = u o δ o ]| e τ " . Thus, ∃r = 1..q such that σ ∈ |[ X jr ∈ F orge c (E ′ r , K r ) ]| e τ " . Since τ "(j r ) = τ ′ (m) = τ (m), it follows that σ ∈ |[ Rhs ]| e τ .
7 Termination For Protocols Without mpair's and Without Indexed Variables

This section aims at proving the termination of rules presented in Section 4 for protocols without mpair(, ) and without index variables. Note that for autonomous protocols without mpair(,s), a constraint system would contain neither quantifiers, nor indexed variables and consequently no master constraints. We first define a weight for terms, elementary constraints, blocks and constraint systems. Then, we show that each rule decreases this weight.

In order to define the weight of a term, we need to introduce some definitions:

Definition 28 (Row of a term). A row of a term t is defined as follows:

• r(X) = max{l | X ⊏ l Y , Y ∈ X } for X ∈ X • r(t) = max{r(Y ) | Y < t, Y ∈ X }
Definition 29 (Size of a term t). We define the size of a term t denoted by |t| as follows:

• |t| = 1 for t ∈ X ∪ C • |f (u 1 , .., u m )| = 1 + |u 1 | + .. + |u m | • |h(u)| = 2 + |u| for h ∈ H
We extend this definition to sets of terms by: |E| = Σ t∈E |t| for E ⊂ T . Now, we can define the weight for terms, then, for elementary constraints and finally for constraint blocks and constraint system.

Definition 30 (Weight of a term t). Let p be the size of the protocol, i.e. the sum of sizes of messages. We define the weight of a term t denoted by t as follows:

• X = p r(X) + 1 for X ∈ X • c = 1 for c ∈ C • f (u 1 , .., u m ) = 1 + u 1 + .. + u m • h(u) = 2 + u for h ∈ H
We extend this definition in the natural way to sets of terms: E = Σ t∈E t for E ⊂ T .

Definition 31 (Weight of an elementary constraint). Let st be the number of the protocol subterms. We define the weight of an elementary constraint ctr denoted by ctr as follows:

• t ∈ F orge(E, K) = st -#K, t + E + |E| + 1 • t ∈ F orge c (E, K) = st -#K, t + E + |E| • t ∈ Sub(w, E, E, K) = st -#K, t + w + |E| + 1 • t ∈ Sub d (w, E, E, K) = st -#K, t + w + |E| • t = u = 0, t + u
Definition 32 (Weight of a constraint block). Let N cE be the maximum number of Equality constraints of the form X = u where X ∈ X and N cN be the maximum number of Negative constraints of type F orge. Consider a constraint block: B = ctr 1 ∧ ..ctr l . We denote by N c B the number of of negative constraints in B, Sc B the number of submaster constraints in B and by Ec B the number of equality constraints of the form X = u (X ∈ X ) in B. We denote also the lexicographic order by and multiset by []. We define the weight of B as follows:

B = N cN -N c B , N cE -Sc B , [ ctr i ] ctri∈B , N cE -Ec B
Definition 33 (Weight of a constraint System). Consider a constraint system: S = B 1 ∧ ..B l . We define the weight of S as follows:

S = [ B i ] Bi∈S
Proposition 25. Algorithm 1 terminates for protocols without mpair(, ) and without index variables.

Proof. Proof. We prove Proposition 25 by showing that each rule of Section 4 which is related to non indexed variables decreases the weight of the whole constraint system S. That is, considering a rule r, post(r) < pre(r) . First, note that our rules do not eliminate negative constraints. Then, ∀B ∈ S, N cN -N c B either remains unchanged or decreases for the case of Rule 31. Thus, Rule 31 decreases S . Rules 3, 14, 20, 22, 32 eliminate one block of the constraint system since they lead to ⊥. Then, they decrease S . Rule 22 eliminates one constraint of a certain block of S since they lead to ⊤. Then, it decreases S . Rule 1 changes an equality constraint ctr ∈ B into another one of the form (X = u) where X ∈ X. Both the number of submaster constraints and the weight of constraints in B remain unchanged. Besides, N cE -Ec B decreases since Ec B increases. Then, B decreases and so does S . Rule 8 adds a submaster constraint to a block B ∈ S. Then, S decreases. For Rule 2, since (X = u) sm ∈ B, X > u . Indeed, u ≤ |u| * p max{r(Y )|Y <u,Y ∈X } ≤ p r(X)+1 . Then,

Y = X = Y + X > Y + u = Y = u .
Besides, the number of submaster constraints remains unchanged. Thus, S decreases.

For Rule 9, pre(R 9) > post(R 9) . Indeed, pre(R 9) = k, t

+ E + |E| + 1 and post(R 9) = [ k, t + E + |E| , k, t + w + |E| + 1 ],
where k = st -#K and w ∈ E. Moreover, Rule 9 do not change the number of submaster constraints. Then, S decreases. For Rule 10, pre(R 10) = k, 1 + t 1 + .. + t m + E + |E| and post(R 10) = [ k, t i + E + |E| + 1 ] ti< t1..tm , where k = st -#K. Moreover, Rule 10 do not change the number of submaster constraints. Then, pre(R 10) > post(R 10) . Therefore, B decreases and so does S . We show in a similar way as Rule 10 that for Rule 11, S decreases. For Rule 12, pre(R 12) > post(R 12) . Indeed, pre(R 12) = k, 2 + t + E + |E| and post(R 12) = k, 1 + t + E + |E| , where k = st -#K. Moreover, Rule 12 do not change the number of submaster constraints. Then, B decreases and so does S . For Rule 15, we have pre(R 15) = k, 1 + t + u + |E| and two cases for post(R 15). In the first one, post(R 15) = k, t + u . In the second case, post(R 15) = [ k, t + u , k, t + u + |E| ]. In both the two cases, pre(R 15) > post(R 15) . Besides, since this rule do not modify the number of submaster constraints, S decreases. We show in a similar way as Rule 10 that for Rule 16, S decreases. For Rule 17, first, pre(R 17

) = k, 1 + t + u + b + |E| where k = st -#K. Second, post(R 17) = [ k, 1 + t + u + |E| , k ′ , 1 + b + E + |E| ] where k ′ = st-#K ∪ {{u} p p }. Since k ′ < k, pre(R 17) > post(R 17) .
We show in a similar way as Rule 17 that for Rule 18, S decreases. For Rule 23, first, pre(R 23

) = k, 2 + u 1 + .. + u m + w 1 + .. + w m . Second, pre(R 23) = [ k, u i + w i ] i=1..m
where k = st -#K. Then pre(R 23) > post(R 23) and since the number of submaster constraints remains unchanged, S decreases. We show in a similar way as Rule 2 that for Rule 27 S decreases since X > u and therefore X = v > u = v . We show in a similar way as Rule 27 that for Rule 29 S decreases since X > u and therefore

X ∈ F orge c (E ′ , K) > u ∈ F orge c (E ′ , K) .
Rule 30 eliminates one constraint. Then, S decreases.

Termination for Protocols with Autonomous keys

The aim of this section is to prove the termination for our inference system. For this, we need some definitions of index variables.

Definition 34. (Index Variables) V ar I (t) the set of indexes of t V ar Q I (t) the set of universal indexes of t V ar R I (t) the set of existential indexes of t V ar X ,R

I (t) = Xi m t V ar R I (X i ) where X i ∈ X I V ar C,R I (t) = ci m t V ar R I (c i ) where c i ∈ C I
Then, we introduce some invariants in Section 8.1 that are used in the proofs of termination. The aim of Section 8.2 is to prove that the set of indexes generated by our inference system is bounded. Once the set of possible indexes to be generated is fixed, we can prove the termination for protocols with autonomous keys by defining a weight for terms, constraints, a constraints block and a system constraint as it is given in Section 8.3.

Invariants

Invariant 6. For a constraint (t ∈ Sub(t ′ , E, E, K)) where

∃X i ≤ t ′ we have ∀u ≤ t ′ s.t X i m u, u is tagged. For a constraint (u = v) where ∃X i < u, Y j < v s.t X i , Y j ∈ X I , we have X i or Y j is tagged. Moreover, if X i m u and Y j m v then i = j.
This invariant will be used in the proof of Invariant 7, Invariant 8 and Proposition 27.

Proof. The first group manages equality constraints that satisfy the invariant. Indeed, Rule 3 eliminates the whole block. Then, the invariant is valid. Rules 6 and 7 transform equality rules and generate new ones.

Nevertheless, these constraints do not fit the shape of constraints defined in Invariant 6, i.e. having two indexed variables in the two terms forming the equality. The rest or rules of the group G 1 does not modify constraints since they only manage labelling. Thus, the invariant is satisfied. Rules of the group G 2 manage F orge constraints. Only Rule 9 generates a Sub constraint: (t ∈ Sub(w, E, E, K)) where w ∈ E. However, according to the second condition of the definition of well-tagged protocols (See Definition 9), w is tagged. Besides, according to the third condition of the same definition, each subterm of w having an indexed variable as a subterm without crossing mpair operator is tagged. Thus, if ∃X i ≤ t ′ then ∀u ≤ t ′ s.t X i m u, u is tagged, and then, the invariant follows. The other rules do not generate neither equality constraintes, nor Sub ones. Then, the invariant still holds. The Rule 15 of the group G 3 transforms a Sub constraint into either a Sub d constraint or an equality one. The Sub d constraint has the same u, and then, the invariant is still satisfied. The equality constraint is of the form (t = u) where u is the term of the Sub constraint. However, by induction hypothesis, if ∃X i ≤ u then ∀v ≤ u s.t X i m v, v is tagged. Then, the first condition of the invariant for the constraint (t = u) is satisfied. Moreover, if X i m u and Y j m t, then u is tagged since X i is tagged and according to the third condition of the definition 9. Thus, t has to be tagged with the same tag as u. Thus, i = j. The other rules of the group G 3 transform a Sub d constraint into new Sub constraints while decomposing the term inside the Sub d constraint. However, the invariant is satisfied for the constraint (t ∈ Sub d (u, E, E, K)) for the term u then it still holds for a subterm u ′ of u (u ′ ≤ u). Indeed, if ∃X i ≤ u ′ then, X i ≤ u. However, by induction hypothesis, ∀v ≤ u s.t X i m v, v is tagged. Therefore, ∀v ≤ u ′ ≤ u s.t X i m v, v is tagged. We conclude that all the rules of the group G 3 satisfy the invariant. Rules of the group G 4 manage equality constraints. Rule 21 eliminates the constraint. Rule 22 eliminates the whole block. Rule 25 replaces an index by another one in all the block. Thus, these rules satisfy the invariant. Rule 23 decomposes an equality constraint of two terms (u = v) into an equality constraint of two subterms

(u ′ = v ′ ) where u ′ ≤ u and v ′ ≤ v. Thus, if ∃X i < u ′ , Y j < v ′ then ∃X i < u, Y j < v.
However, by induction hypothesis, X i or Y j is tagged. Moreover, if X i m u ′ and Y j m v ′ then, X i m u and Y j m v, and therefore, i = j. Rule 24 decomposes an equality constraint of two terms (mpair(k, u) = mpair(l, w)) into an equality constraint of two subterms (u = wδ l,k ). If ∃X i < u < mpair(k, u), Y j < wδ l,k < mpair(k, w) s.t X i , Y j ∈ X I , then, X i or Y j is tagged by induction hypothesis. Besides, V ar I (u) ⊆ {k} and V ar I (wδ l,k ) ⊆ {k}. Thus, if X i m u and Y j m wδ l,k then i = k = j. Rule 26 of the group G 5 generates an equality constraint (u = v). Suppose Y j < u and Z k < v. By induction hypothesis, for the constraint (X i = u), Y j is tagged. In a similar way, Z k is tagged. Then, the first condition of the invariant is satisfied. Suppose now that Y j m u and Z k m v. By induction hypothesis, for the constraint (X i = u), we have i = j. In a similar way, for the constraint (X i = v), we have i = k. Thus, j = k. Therefore, the second condition of the invariant is satisfied. For Rule 27, the equality constraint generated (u = v) can not have X i ≤ u or Y j ≤ v by priority of Rules 6 and 7 replacing indexed variables by non indexed ones. In a similar way, Rule 31 can not generate a constraint (t ∈ Sub d (w, E, E, K)) having indexed variables in w. Rules 28, 29 and 30 do not modify equality constraints. Rule 32 eliminates the whole block. Therefore, the invariant is valid for all the rules of the group G 5 . The Rule 33 of the group G 6 generates a constraint (t ∈ Sub d (uδ, E, E, K)). However, u comes from a master constraint: (X i = u). By induction hypothesis, if ∃Y j < u then Y j is tagged. Moreover, since u is a term of the protocol, according to the third condition of Definition 9, ∀u ′ ≤ u s.t Y j m u ′ , u ′ is tagged. Then, the Sub constraint generated satisfies the invariant. Rule 34 does not generate neither Sub constraints nor non final equality ones Then, the invariant still holds. Rule 35 generates an equality constraint (u o δ o = v). Suppose that ∃Y j and Z k s.t Y j < u o δ o and Z k < v. By induction hypothesis for the constraint (X m = v), we have Z k is tagged. Then, the first condition of the invariant is satisfied. Suppose now that Y j m u o δ o and Z k m v. By induction hypothesis for the constraint (X m = v), we have m = k. By induction hypothesis for the constraint (X o = u o ), where Y l < u o we have o = l. Then, V ar I (u o δ o ) ⊆ {m} which leads to j = m. Thus, j = k and therefore the invariant holds for Rule 35.

Invariant 7. For a constraint of the form (t ∈ F orge c (E, K)), (t ∈ F orge(E, K)), (t ∈ Sub(u, E, E, K)), or (t ∈ Sub d (u, E, E, K)), where ∃X i m t, we have V ar I (t) ⊂ Q. For a non final constraint of the form u = v where ∃Y j and Z k s.t Y j m u and Z k m v, we have j, k ∈ Q. This invariant will be used in the proof of Invariant 8, Proposition 27, Proposition 28, Lemma 11 and Proposition 31.

Proof. Rules of the group G 1 do not generate new constraints of the form F orge or Sub or equality constraints of the form defined in Invariant 7. Then, the invariant still holds.

Rule 9 of the group G 2 generates from a F orge constraint either a F orge c constraint or a Sub constraint with the same term t in both cases. However, by induction hypothesis, V ar I (t) ⊂ Q. Then, the invariant is satisfied. Rules 10, 11 and 12 transform a constraint t ∈ F orge c (E, K) into another constraint (t ′ ∈ F orge(E, K)) where t ′ m t. However, V ar I (t ′ ) ⊆ V ar I (t) and V ar I (t) ⊂ Q. Thus, V ar I (t) ⊂ Q which satisfies the invariant. Rule 13 generates a new constraint (t ∈ F orge(E, K)) where V ar I (t) ⊂ {k} and k ∈ Q. Thus, the invariant is valid. Rule 14 eliminates the block. Thus, the group G 2 validates the invariant. Rule 15 transforms a Sub constraint into either a Sub d constraint preserving the same t or an equality constraint. For the new Sub d constraint, by induction hypothesis we have V ar I (t) ⊂ Q which satisfies the invariant. For an equality constraint (t = u), suppose that ∃X i , Y j s.t X i m t and Y j m u. According to Invariant 6 for the constraint (t = u) we have i = j. However, by induction hypothesis, V ar I (t) ⊂ Q. Since we only replace an universal index by another universal index, we have i, j ∈ Q. Rules 16 and 19 transform a Sub constraint into another one while preserving the same t. However, by induction hypothesis, V ar I (t) ⊂ Q. Then, the invariant is satisfied. Rules 17 and 18 generate from a Sub constraint a Sub d constraint with the same t and a new constraint F orge for forging the key b. For the new constraint Sub d , by induction hypothesis, we have V ar I (t) ⊂ Q which satisfies the invariant. For the F orge constraint, b is a key. According to the restriction of autonomous keys, we have V ar I (b) = ∅, which satisfies the invariant. Rule 20 eliminates the block. Thus, the group G 3 satisfies the invariant. Rule 21 of the group G 4 eliminates a constraint. Rule 22 eliminates the block. Rule 23 transfoms an equality constraint

(u = v) into a new one (u ′ = v ′ ) where u ′ m u et v ′ m v. Then, if ∃X i , Y j s.t X i m u ′ and Y j m v ′ , then X i m u
and Y j m v. However, by induction hypothesis, i, j ∈ Q which satisfies the invariant. Rule 21 transforms an equality constraint into another constraint (u = wδ l,k ) where V ar I (u) = V ar I (v) ⊆ {k} and k ∈ Q, which satisfies the invariant. Thus, the group G 4 satisfies the invariant. Rule 26 generates a new constraint (u = v). Suppose that ∃Z k , Y j s.t Z k m u and Y j m v. By induction hypothesis for the constraint (X i = u), we have i, k ∈ Q. By induction hypothesis for the constraint (X i = v), we have i, j ∈ Q. Then, j, k ∈ Q, which satisfies the invariant. Rule 27 generates an equality constraint (u = v). However, u and v comes from constraints (X = u) and (X = v). Then, ∄X i s.t X i m u or X i m v by priority of Rules 6 et 7. In a similar way, Rule 29 does not generate a constraint (u ∈ F orge c (E, K)) where X i m u. Thus, Rules 27 and 29 satisfy the invariant. Rule 28 generates a new constraint (u ∈ F orge c (E, K)). Suppose that ∃Y j s.t Y j m u. However, u comes from the constraint X i = u. According to Invariant 6, i = j. Moreover, by induction hypothesis, we have i ∈ Q and therefore j ∈ Q, which satisfies the invariant. Rule 30 does not generate new constraints. Rule 31 generates a new Sub constraint while preserving the same t. Rule 32 eliminates the block. Thus, the group G 5 validates the invariant. Rule 33 generates a new Sub constraint but preserving the same t. Then, the invariant still holds. Rule 34 generates a new constraint (u o δ o ∈ F orge c (E ′ , K)). Suppose that ∃Y j s.t Y j m u o δ o . However, according to Invariant 6 applied to the master constraint (X o = u o ) taking into account δ o , we have j = m. Moreover, by induction hypothesis applied to the constraint (X m ∈ F orge c (E ′ , K)), we have m ∈ Q, which satisfies the invariant. Rule 35 generates two new constraints. The first constraint is (v ∈ F orge c (E ′ r , K r )). Suppose that ∃Y j s.t Y j m v. According to the induction hypothesis applied to the constraint (X m = v), we have m, j ∈ Q, which satisfies the invariant. The second constraint generated is (u o δ o = v). Suppose that ∃Y j , Z k s.t Y j m v and Z k m u o δ o . However, by induction hypothesis applied to both the master constraint (X o = u o ) taking into account δ o and the constraint (X m = v), we have m, j, k ∈ Q which satisfies the invariant. Thus, the group G 6 validates the invariant.

Invariant 8. For a constraint (u = v), where X i m u and c j m v, then i and j can not be both existential indexes.

Proof. Groups G 1 and G 2 do not generate new equality constraints of the form (u = v) where ∃X i ∈ X I and c j ∈ C I s.t X i m u and c j m v. Thus, the invariant still holds. For the group G 3 , only Rule 15 can generate an equality constraint (t = u) from a constraint (t ∈ Sub(u, E, E, K)). Suppose that ∃X i ∈ X I and c j ∈ C I s.t i, j ∈ R and either (X i m u and c j m t) or (X i m t and c j m u). In the first case, i.e. (X i m u and c j m t), according to Invariant 6, X i is tagged. According to the third condition of Definition 9, u is also tagged. Thus, v has to be tagged with the same tag as u and then i = j, which contradicts our hypothesis. In the second case, i.e. X i m t and c j m u, according to the Invariant 7, we have i ∈ Q which contradicts the hypothesis: i ∈ R. Thus, for the two cases, i and j can not be both existentials. Rule 21 eliminates a constraint. Rule 22 eliminates the whole block. Rule 25 replaces an index by another one. Nevertheless, it can not replace an universal index by an existential one. Thus, these three rules of the group G 4 satisfy the invariant. Rule 23 decomposes an equality constraint between two terms (u = v) into another equality contraint between two subterms ((u ′ = v ′ ) with u ′ < m u and v ′ < m v) without generating indexes. By induction hypothesis, if ∃X i ∈ X I and c j ∈ C I s.t X i m u ′ < m u and c j m v ′ < m v then i and j can not be both existential. Rule 24 generates new equality constraint (u = wδ l,k ) with V ar I (u) = V ar I (wδ l,k ) ⊆ {k} which satisfies the invariant. Rule 26 of the group G 5 generates an equality constraint (u = v). Suppose that ∃Z k ∈ X I and c j ∈ C I s.t k, j ∈ R, Z k m u and c j m v. Nevertheless, according the invariant 6 applied to the constraint (X i = u), we have i = k. However, according to the induction hypothesis for the constraint (X i = v), i and j can not be both existential. Thus, k and j can not be both existential which satisfies the invariant. Rule 27 generates an equality constraint (u = v). However, u and v come from constraints (X = u) and (X = v). The, ∄X i s.t X i m u or X i m v by priority of Rules 6 and 7. Thus, Rule 27 satisfies the invariant. The other rules of the group G 5 do not generate new equality constraints. Thus, the group G 5 satisfies the Invariant 8. Rules 33 and 34 of the group G 6 do not generate new not final equality constraints. Thus, the invariant is Moreover, by induction hypothesis for the constraint (X m = v), m and j can not be both existential. Then, k and j can not be both existential, which satisfies the invariant. In the second case, i.e. Z k m v and c j m u o δ o , according to the invariant 6 for the constraint (X m = v), we have m = k. However, by induction hypothesis for the master constraint (X o = u o ) taking into account δ o , we have m and j can not be both existential and then k and j can not be both existential, which satisfies the invariant. Thus, in both cases, the invariant is valid.

Invariant 9. For a constraint t ∈ Sub(u, E, E, K) or t ∈ Sub d (u, E, E, K) where V ar R I (u) = {i} we have either i is fresh and (ant(i, j) = j if V ar C,R I (t) = j ∈ R) or i ∈ V ar R I (E) .
This invariant is used for the proof of Invariant 10, Proposition 27 and Proposition 28.

Proof. we show that the different rules of our inference sytem satisfy the invariant. Rules of the first group does not generate Sub constraints. Then, the invariant holds. Rule 9 generates a constraint (t ∈ Sub(w, E, E, K)) where w ∈ E. and then, V ar I (w) = ∅. The other rules of the second group do not generate Sub constraints. Thus, the invariant is satisfied. Rule 15 transforms a Sub constraint into a Sub d constraint while preserving the same u. Then, the invariant still holds. Rules 16, 17, 18 transform a constraint (t ∈ Sub d (u, E, E, K)) into one single constraint (t ∈ Sub(u ′ , E, E, K)) where u ′ m u. If V ar R I (u ′ ) = {i} then, V ar R I (u) = {i}. However, by induction hypothesis, either i is fresh and (ant(i, j) = j if V ar C,R I (t) = j ∈ R) or i ∈ V ar R I (E) which satisfies the invariant. For Rule 19, there are two cases. In the first one, it generates a new Sub constraint with fresh index variable k and thus if V ar C,R I (t) = j ∈ R then ant(i, j) = j. Therefore, the invariant is satisfied. In the second case, it generates an old constraint that exists in Hist(B). Then, by induction hypothesis, the invariant is satisfied. Rule 20 eliminates the whole block. We conclude that the third group satisfies the invariant. Rules of the fourth group do not generate Sub constraints. Only Rule 25 may generate a new Sub constraint with a new existential index inside the Sub. In this case we have (t ∈ Sub(u, E, E, K)) or (t ∈ Sub d (u, E, E, K)) where V ar R I (u) = {i}. We must have also in the block (c i = c k ) where i, k ∈ R in order to have a constraint of the form (t ∈ Sub(u ′ , E, E, K)) or (t ∈ Sub d (u ′ , E, E, K)) where V ar R I (u ′ ) = {k}. However, by induction hypothesis, either i is fresh and (ant(i, j) (w,E,E,K)). However, w comes from a sub master constraint. Then, V ar R I (w) ∈ V ar R I (E) which satisfies the invariant. Only Rule 33 generate a Sub d constraint. There are two cases. In the first one, it generates a new Sub d constraint with fresh index variable k ′ and then (ant(i, j) = j if V ar C,R I (t) = j ∈ R). Thus, the invariant is satisfied. In the second case, it generates an old constraint that already exists in Hist(B). Then, by induction hypothesis, the invariant is satisfied.

= j if V ar C,R I (t) = j ∈ R) or i ∈ V ar R I (E). If i is fresh, then it is contradictory with (c i = c k ) in the block. If i ∈ V ar R I (E), then ant(i, j) = {k} if k ∈ E and ant(i, k) = {i} otherwise. In these two cases, we have V ar R I (u ′ ) ∈ V ar R I (E)

Bound on Indexes Generated by the Inference System

The aim of this section is to bound the set of possible indexes generated by our inference system. For this, we consider a derivation i.e a successive application of our rules on a constraint system. In this derivation, the number of application of labelling rules and modification of sub-master constraints, i.e. Rules 4, 5 and 8 is bounded. We consider a derivation where there is not modification or labelling of sub-master constraints (E is then fixed for all rules). Indexes in E are the most anterior indexes. The aim of this section is then to bound the set of indexes generated by our inference system throught this derivation. Theorem 3. The set of indexes generated by our inference system is bounded.

Proof. We first define this set of indexes useful for the proof:

Definition 35. Let: V 1 = V ar C,R I ({t|t ∈ F orge(E, K) ∨ t ∈ F orge c (E, K) ∨ t ∈ Sub(u, E, E, K) ∨ t ∈ Sub d (u, E, E, K) ∈ B}) V 2 = V ar R I ({u|t ∈ Sub(u, E, E, K) ∨ t ∈ Sub d (u, E, E, K) ∈ B and ∃X i s.t X i m t}) V 3 = V ar C,R I ({v|u = v ∨ v = u ∈ B and ∃X s.t X m u and X ∈ X ∪ X I }) V 4 = V ar R I (E) Then, V = V 1 ∪ V 2 ∪ V 3 ∪ V 4 .
Then, the proof of Theorem 3 is structured as follows: We bound first the set of universal indexes generated by our inference system (See Proposition 26). Then, we bound the set of existential indexes generated by our inference system. First, considering a constraint (t ∈ Sub(v, E, E, K)), while fixing t (by the condition X i m t), we bound the set of existential indexes generated by our inference system inside a Sub (in v). For this, we bound first the set of existential indexes indexing variables inside a Sub (See Proposition 27). Once this set is bounded, we bound the set of existential indexes indexing constants inside a Sub (See Proposition 28) permetting then to bound the set of existential indexes inside a Sub. Then, we bound the set of existential indexes in V defined in Definition 35 (See Proposition 29). We can after bound the set of existential indexes in u for constraints of the form (t ∈ Sub(u, E, E, K)) without any restrictions over the term t (See Proposition 30). Once the of existential indexes for F orge and Sub constraints is bounded, we bound existential indexes for equality constraints (See Proposition 31 and Proposition 32).

Thus, the proof of Theorem 3 follows from the following propositions:

Proposition 26. The set of universal indexes generated by our inference system is bounded.

Proposition 27. V ar X ,R I ({v s.t (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) ∈ B and ∃X i m t}) ∪ V ar R I (E) is bounded. Proposition 28. V ar C,R I ({v | (t ∈ Sub(v, E, E, K)) ∨ (t ∈ Sub d (v, E, E, K)) ∈ B
and ∃X i m t)} has a bound. Proposition 29. The set of indexes in V (defined in Definition 35) is bounded.

Proposition 30. V ar R I ({u | t ∈ Sub(u, E, E, K) ∨ t ∈ Sub d (u, E, E, K) ∈ B}) is bounded. Proposition 31. V ar X ,R I ({u | (v = u) ∨ (u = v) ∈ B}) is bounded. Proposition 32. V ar C,R I ({u | (v = u) ∨ (u = v) ∈ B}) is bounded.
The dependency between these propositions is illustrated by Figure8.2. Before proving the propositions above, we need to prove the following invariant:

Invariant 10. For a non final or dull constraint (u = v) where V ar C,R I (u) = {i} and V ar C,R I (v) = {j}, we have ant(i, j) ∈ V where V is defined in Definition 35. This invariant will be used in Invariant 11, Proposition 31 and Proposition 32.

Proof. Rules of the first group and the second group do not generate constraints of the form defined in Invariant 10. Then, the Invariant is satisfied.

Only Rule 15 generate an equality constraint (u = v) from a constraint (u ∈ Sub(v, E, E, K)) where V ar C,R I (u) = {i} and V ar C,R I (v) = {j}. However, according to Invariant 9, either j is fresh and ant(i, j) = i or j ∈ V ar R I (E). There are then two cases. In the first case, j is fresh and ant(i, j) = i. However, i ∈ V since i ∈ V 1 . Thus, ant(i, j) ∈ V and the invariant is satisfied. In the second case, j ∈ V ar R I (E). Then, ant(i, j) = i if i ∈ V ar R I (E) and ant(i, j) = j otherwise. In both cases, ant(i, j) ∈ V and the invariant follows. The same reasoning is valid when the constraint

(v ∈ Sub(u, E, E, K)) is transformed into a constraint (u = v).
Rule 21 eliminates the constraint. Rule 22 eliminates the whole block. Rule 23 decomposes an equality between two terms into an equality between two subterms while preserving the same indexes. Then, th invariant still holds. Rule 24 generates an equality constraint (u = v) where V ar I (u) = V ar I (v). Then, the invariant remains satisfied. Rule 25 replace an index by another in the whole block. It may lead to a generation of a new constraint (u = v ′ ) from a constraint (u = v) where V ar I (v) = {j}, V ar I (v ′ ) = {k}, V ar I (u) = {i} and i, j, k ∈ R. We must then have the constraint (c j = c k ) in the block. Then, we have ant(j, k) = k. We distinguish two cases concerning the constraint (u = v ′ ). In the first one, ant(i, k) = k. However, by induction hypothesis for the constraint (c j = c k ) and since ant(j, k) = k, we have k ∈ V which satisfies the invariant. In the second case, ant(i, k) = i. However, ant(j, k) = k. Then ant(i, j) = i and therefore by induction hypothesis for the constraint (u = v) we have i ∈ V which satisfies the invariant. Thus, in both cases, the invariant still holds.

Only Rules 26 and 27 of the fifth group may generate new constraints of the form (u = v). However, u and v belongs to constraints of the form (X i = u) or the form (X = u) whose existential indexes are already counted in V . Thus,, Group G 5 satisfies the invariant.

Only Rule 35 may generate a new equality constraint of the form (

u o δ o = v). Suppose V ar C,R I (u o δ o ) = {i} and V ar C,R I (v) = {j}.
There are two cases. In the first one, it generates a new equality constraint (u o δ o = v) with fresh index variable i and then ant(i, j) = j. However, j ∈ V 3 . Then, ant(i, j) ∈ V . Thus, the invariant is satisfied. In the second case, it generates an old constraint that already exists in Hist(B). Then, by induction hypothesis, the invariant is satisfied. Proposition 26. The set of universal indexes generated by our inference system is bounded. This proposition will be used in the proof of Theorem 3, Proposition 28 and Lemma 11.

Proof. There are only two rules that may generate universal indexes in constraints, i.e. Rules 13 and 24. Then, the number of universal indexes is bounded by the number of constraints of the form (mpair(i, t) ∈ F orge c (E, K)) and (mpair(j, u) = mpair(k, v)).

The number of constraints of the form (mpair(i, t) ∈ F orge c (E, K)) is bounded by (the number of mpairs * the number of different E * the number of different K). Let st the number of subterms of the protocol. The number of mpairs is bounded by st. The number of different E is bounded by 2 st since terms in E have not indexes outside mpairs according to the restriction of Well-Tagged protocols (See Definition 9). The number of different K is bounded by 2 keys which is bounded by 2 st since keys have not indexes outside mpairs according to the restriction of autonmous keys (See Definition 10).

The number of constraints of the form (mpair(j, u) = mpair(k, v)) is bounded by (the number of mpairs * the number of mpairs) which is bounded by (st * st). We conclude that the number of universal indexes is bounded.

Proposition 27. V ar X ,R I ({v s.t (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) ∈ B and ∃X i m t}) ∪ V ar R I (E) is bounded.
This proposition will be used for the proof of Proposition 28 and Theorem 3.

Proof. Rule 19 generates a bounded set of indexes. Indeed, let st the number of subterms of the protocol. Then, the number of existential indexes in v from constraints (t

∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K))
is bounded by the number of constraints of this form which is bounded by: (the number of possible terms t * the number of different E * the number of different K) * the number of existential indexes in v fixing the other parameters. However, ∃X i m t and according to Invariant 7, i ∈ Q. Then, the number of indexes in t is bounded. Let b 1 this bound. Thus, the number of possible terms t is bounded by 2 b1 * st . Besides, the number of different E is bounded by 2 st since terms in E have not indexes outside mpairs according to the restriction of Well-Tagged protocols (See Definition 9). Moreover, the number of different K is bounded by 2 keys which is bounded by 2 st since keys have not indexes outside mpairs according to the restriction of autonmous keys (See Definition 10). Then, fixing t, E, K and E (which is fixed by the hypothesis on the derivation chosen), the number of new existential indexes in v generating by Rule 19 is the number of mpairs which is bounded by st.

We now prove Proposition 27 by proving the following invariant:

V ar X ,R I ({v s.t (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) ∈ B and ∃X i m t})∪V ar R
I (E) is stable or decreases by our inference system except Rule 19. We denote by V the set of indexes defined in Proposition 27. We recall that in the derivation that we consider, E is fixed. Then, V ar R I (E) is fixed. Rules of the group G 1 does not generate Sub constraints. Then, the invariant is valid. Rule 9 of the group G 2 generates a constraint (t ∈ Sub(w, E, E, K)) with w ∈ E. Then, V ar I (w) = ∅, which satisfies the invariant. The other rules of the group G 2 do not generate Sub constraints. Thus, the group G 2 satisfies the invariant. Rule 15 transforms a Sub constraint into either an other Sub d constraint while preserving the same u and then V is stable or an equality constraint and then V may decrease. Rules 16, 17 and 18 transform a Sub d constraint into a Sub constraint while decomposing the term inside a Sub without generating new indexes. Then, V remains stable or decreases. Rule 20 eliminates the whole block, then V remains stable or decreases. Rules of the group G 4 do not generate new Sub constraints. Besides, Rule 25 does not replace an universel index by an existential one. The only case where Rule 25 may generate new index inside a Sub is to transform a E,E,K)) where V ar I (v ′ ) = {j} and j ∈ R by a replacement thanks to the application of Rule 25 to the constraint (c i = c j ). However, according to Invariant 9, i is fresh or i ∈ V ar R I (E). The first case (i is fresh) is contradictory with the existence of (c i = c j ). In the second case (i ∈ V ar R I (E)), the only way to replace i by j is to have ant(i, j) = {j}. Since i ∈ V ar R I (E), this case is only possible if j ∈ V ar R I (E). Thus, V remains stable or decreases. Rule 31 generates a constraint (t ∈ Sub d (w, E, E, K)). Suppose that ∃X i s.t X i m w and i ∈ R. However, this is contradictary with the fact that X i comes from the constraint (X = w) by priority of Rules 6 and 7. The other rules of the group G 5 do not generate Sub constraints. Then, V remains stable. Rule 33 generates a constraint (t ∈ Sub d (uδ, E, E, K)). Suppose that ∃Y j s.t Y j m uδ and j ∈ R. However, according to Invariant 6 for the master constraint taking into account δ, we have j = m and then V remains stable. The other rules of the group G 6 do not generate new Sub constraints. Thus, V remains stable.

constraint (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) where V ar I (v) = {i} and i ∈ R into a constraint (t ∈ Sub(v ′ , E, E, K)) or (t ∈ Sub d (v ′ ,
Proposition 28. V ar C,R I ({v | (t ∈ Sub(v, E, E, K)) ∨ (t ∈ Sub d (v, E, E, K)) ∈ B and ∃X i m t)} has a bound.
This proposition will be used for the proof of Theorem 3, Lemma 11, Invariant 11 and Proposition 30.

Proof. We recall that we consider a derivation where we have E fixed. Then, let b 2 be the number of constraints of E and id = V ar R I (E). Then, let st the number of subterms of the protocol. The number of existential indexes in v from constraints (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) is bounded by the number of constraints of this form which is bounded by: (the number of possible terms t * the number of different E * the number of different K) * the number of existential indexes in v fixing the other parameters.

However, ∃X i m t and according to Invariant 7, i ∈ Q. Then, the number of indexes in t is bounded. Let b 1 this bound. Thus, the number of possible terms t is bounded by 2 b1 * st . Besides, the number of different E is bounded by 2 st since terms in E have not indexes outside mpairs according to the restriction of Well-Tagged protocols (See Definition 9). Moreover, the number of different K is bounded by 2 keys which is bounded by 2 st since keys have not indexes outside mpairs according to the restriction of autonmous keys (See Definition 10).

Fixing t, E, E and K for the constraint (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) there are four possible rules that may generate existential indexes in v, i.e. Rules 19, 31, 33 and 25. Then, we distinguish four cases depending on the rule that leads to the generation of an existential index.

In the first case, i.e. Rule 19 is the rule that generates a new existential index. The number of possible existential indexes in v is the number of mpairs which is bounded by st.

In the second case, i.e. Rule 31 is the rule that generates a new existential index. Then, the number of possible existential indexes in v is the number of constraints of the form (X = v) sm which is bounded by b 2 .

In the third case, i.e. Rule 33 is the rule that generates a new existential index. Since we generate only one existential index by indexed variable and by master constraint for this variable, the number of possible existential indexes in v is the number possible replacement which is bounded by (the number of indexed variables * the number of master constraints). The number of master constraints is bounded by b 2 . The number of indexed variables is bounded by (the number of vectors * the number of indexes inside the Sub for indexed variables). The number of vectors is fixed from the specification of the protocol. The number of indexes inside the constraint Sub is the sum of the number of universal indexes which is bounded in Proposition 26 and the number of existential indexes (for indexed variables) which is bounded in Proposition 27. Thus, the number of existential indexes in v generated by Rule 33 is bounded.

In the fourth case, i.e. Rule 25 is the rule that generates a new existential index inside the Sub. This is only possible when it transforms a constraint (t E,E,K)) where V ar I (v ′ ) = {j} and j ∈ R by a replacement thanks to the application of Rule 25 to the constraint (c i = c j ).

∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) where V ar I (v) = {i} and i ∈ R into a constraint (t ∈ Sub(v ′ , E, E, K)) or (t ∈ Sub d (v ′ ,
However, according to Invariant 9, i is fresh or i ∈ V ar R I (E). The first case (i is fresh) is contradictory with the existence of (c i = c j ). In the second case (i ∈ V ar R I (E)), the only way to replace i by j is to have ant(i, j) = {j}. Since i ∈ V ar R I (E), this case is only possible if j ∈ V ar R I (E). Then, the number of indexes generated inside the Sub in this case is bounded by id.

Proposition 29. The set of indexes in V (defined in Definition 35) is bounded. This proposition will be used for the proof of Proposition 31 and Proposition 32.

Proof. The proof is a direct consequence of the following Invariant 11 and the following Lemma 11. Lemma 11. The set of indexes in V (defined in Definition 35) generated by the following rules: Rule 19 for a constraint

(t ∈ Sub d (u, E, E, K)) when ∃Z j m t; Rule 33 for a constraint (t ∈ Sub d (X m , E, E, K)) when ∃Z j m t; Rule 34; Rule 35 for a constraint (X m = v) when ∃Z m m v. is bounded.
Proof. Rule 19 generates a new constraint t ∈ Sub(uδ, E, E, K) that may contain a new existential index in uδ. However, since ∃Z j m t and according to Proposition 28 and Proposition 27, the set of existential indexes that may be generated by Rule 19 is bounded. In the same way, Rule 33 may generate a new existential index inside the constraint Sub, but that are bounded according to both Proposition 28 and Proposition 27. Rule 34 may generate new existential indexes in the constraint u o δ o ∈ F orge(E ′ , K). However the set of these indexes is bounded. Indeed, the number of existential indexes in u o δ o is bounded by the number of constraints of the form u o δ o ∈ F orge(E ′ , K) which is bounded by: (the number of different K * the number of different E ′ * the number of existential indexes in u o δ o fixing E ′ and K).

However, the number of different E is bounded by 2 st since terms in E have not indexes outside mpairs according to the restriction of Well-Tagged protocols (See Definition 9). Besides, the number of different K is bounded by 2 keys which is bounded by 2 st since keys have not indexes outside mpairs according to the restriction of autonmous keys (See Definition 10).

Moreover, the number of existential indexes in u o δ o fixing E ′ and K is the number of possible replacements which is bounded by (the number of indexed variable in F orge constraints * the number of master constraints) since we have exactly one fresh index per indexed variable per master constraint. The number of master constraints is bounded by the number of constraints in E which is fixed. The number of indexed variables in F orge constraints is bounded by (the number of vectors * the number of indexes in variables for F orge constraints). However, according to Invariant 7, these indexes are universal. Then, according to Proposition 26, the set of universal indexes is bounded. Besides, the number of vectors is fixed from the specification of the protocol. For Rule 35, considering a constraint (X m = v) and since ∃Z m m v, we have m ∈ Q according to Invariant 7. Then, for this rule, we have existential indexes only in u o δ o . Therefore, the number of fresh indexes generated by this rule is bounded by the number of constraints of the form (u o δ o = v) which is bounded by ((st * the set of universal indexes) * the set of existential indexes in u o δ o fixing v). However, the set of universal indexes is bounded according to Proposition 26. Besides, the set of existential indexes in u o δ o fixing v is bounded by (the number of indexed variables in equality constraints * the number of master constraints) since we have exactly one fresh index per indexed variable in equality constraint per master constraint. However, the number of master constraints is bounded by the number of constraints in E which is fixed. Moreover, the number of indexed variables in equality constraints of the form (X m = v) is bounded by (the number of vectors * the number of indexes in variables for these equality constraints). Since m ∈ Q and the number of vectors is fixed and according to Proposition 26, this number of indexed variables is bounded. We conlude that the set of indexes in V generated by these rules is bounded.

Invariant 11. V is stable or decreases by application of our inference system except: Rule 19 for a constraint (t ∈ Sub d (u, E, E, K)) when ∃Z j m t;

Rule 33 for a constraint (t ∈ Sub d (X m , E, E, K)) when ∃Z j m t;

Rule 34; Rule 35 for a constraint (X m = v) when ∃Z m m v.

Proof. V 4 is always stable by hypothesis on the chosen derivation. V 2 is bounded according to Proposition 27 and Proposition 28. Then, in this proof, we consider this bound and show that, for each rule of our inference system, the possible indexes that we may generate in V 1 and V 3 exist always either in V 2 and V 4 that are fixed or in V 1 and V 3 before the application of the rule. Rules of the group G 1 do not generate new F orge or Sub constraints, then V 1 remains stable. Moreover, rules of this group do not generate new equality constraints u = v with ∃X i , Y j ∈ X I s.t X i m u and Y j m v. Thus, V remains stable or decreases by the group G 1 . Rules of the group G 2 do not generate equality constraints, then V 3 remains stable. Rule 9 transforms a F orge constraint either into a F orge constraint or a Sub constraint with the same t in both cases. Then, V 1 remains stable. Rule 13 generates a new constraint (t ∈ F orge(E, K)) with V ar I (t) ⊆ {k} and k ∈ Q. Then, V 1 remains stable. Rule 14 eliminates the whole block. The other rules of the group G 2 transform a constraint (t ∈ F orge c (E, K)) into a constraint (t ′ ∈ F orge(E, K)) with mpair(t ′ , t) without generating new indexes. Then, V 1 remains stable. Thus, V is stable by the group G 2 . Rule 15 transforms a constraint (t ∈ Sub(u, E, E, K)) into either another Sub d constraint with the same t and then V 1 remains stable or an equality constraint (t = u). Suppose that ∃X i s.t X i m t or X i m u. We distinguish two cases. In the first one, X i m t. Suppose that ∃c j s.t c j m u and j ∈ R. However, j already belongs to V 2 . Thus, V 2 ∪ V 3 remains stable and then V is stable. In the second case, X i m u. Suppose that ∃c j s.t c j m t and j ∈ R. However, j already belongs to V 1 . Thus, V 1 ∪ V 3 remains stable and then V is stable. Rule 16 transforms a Sub d constraint into another Sub constraint while preserving the same t but decomposing the term inside the Sub without generating new indexes. Then, V 1 remains stable. There are not new equality constraint. Thus, V 3 remains stable and then V remains stable. Rule 17 transforms a Sub d constraint into a Sub conctraint preserving the same t and generating a F orge constraint. The last constraint (the F orge one) uses a key b. According to Definition 10 of autonomous keys, V ar I (b) = ∅. Thus, V 1 remains stable and then V remains stable. The reasoning is the same for Rule 18. Rule 19 is applied when ∄Z j m t and then V 2 does not change for this rule. V 1 remains stable since the rule preserve the same t. Rule 20 eliminates the block. Thus, V remains stable by the group G 3 Rule 21 eliminates the constraint. Rule 22 eliminates the whole block. Then, V remains stable or decreases. Rule 23 decomposes an equality constraint without generating new indexes. Then, V 3 remains stable. It does not generate other new constraints. Then, V is stable. Rule 24 generates new equality constraint (u = wδ l,k ) where V ar I (u) = wδ l,k ⊆ {k} and k ∈ Q. Thus, V 3 remains stable and then V is stable. Therefore, V remains stable by the group G 4 . Rule 25 replace an index by another one which may lead to the generation of a new index for V . In this case, we must have in the block a constraint (c i = c j ) where i, j ∈ R, i ∈ V , j / ∈ V and ant(i, j) = j. However, according to Invariant 10 for the constraint (c i = c j ), ant(i, j) ∈ V which contradicts the fact that j / ∈ V . Thus, V is stable by Rule 25. Rule 26 generates a new equality constraint (u = v). If ∃c j s.t j ∈ R and c j m u or c j m v, then j belongs either to the constraint (X i = u) or (X i = v) and then V 3 does not change. The same reasoning is valid for Rule 27. Rule 29 can add an index to V 1 . Nevertheless, this index comes from a sub-master constraint which is already computed in V 4 . Then, V remains stable. The same reasoning is valid for Rule 31. Rule 30 does not generate new constraints. Rule 32 eliminates the whole block. Thus, V remains stable or decreases by the group G 5 Rule 33 is authorized only if ∄Z j s.t Z j m t. Then, V 2 does not change. Moreover, this rule generates a new Sub constraint from a Sub d constraint preserving the same t. Then, V 1 is stable. Rule 35 is only authorized when (X m = v) and ∄Z m s.t Z m m v. Then, suppose this rule generates an equality constraint (u o δ o = v) that may add an index to V 3 , i.e. ∃Z m , c j s.t j ∈ R and Z m m u o δ o . Then, j is already computed in V 3 thanks to the constraint (X m = v). Thus, V 3 remains stable. In the same way, the existential index that may be generated by the addition of the constraint (v ∈ F orge c (E ′ r , K r )) is already computed in V 3 thanks to the constraint (X m = v). Thus, V 1 ∪ V 3 remains stable. Therefore, V is stable or decreases by the group G 6 . We conclude that the set of indexes in V is bounded.

Proposition 30. V ar R I ({u | t ∈ Sub(u, E, E, K) ∨ t ∈ Sub d (u, E, E, K) ∈ B}) is bounded.
This proposition will be used for the proof of Theorem 3, Proposition 31 and Proposition 32.

Proof. Considering a constraint of the form (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)), since V ar I (t) is now bounded thanks to Proposition 29, we follow the same proof as the one of Proposition 27 in order to prove that V ar X ,R I ({v s.t (t ∈ Sub(v, E, E, K)) or (t ∈ Sub d (v, E, E, K)) ∈ B and ∃X i m t}) ∪ V ar R I (E) is bounded. Then, we follow the same proof as the one of Proposition 28 in order to prove that V ar C,R I ({v

| (t ∈ Sub(v, E, E, K)) ∨ (t ∈ Sub d (v, E, E, K)) ∈ B)} is bounded. We conclude that V ar R I ({u | t ∈ Sub(u, E, E, K) ∨ t ∈ Sub d (u, E, E, K) ∈ B}) is bounded. Proposition 31. V ar X ,R I ({u | (v = u) ∨ (u = v) ∈ B}) is bounded.
This Proposition will be used for the proof of Theorem 3 and Proposition 32.

Proof. We prove Proposition 32 by proving the following invariant:

V ar X ,R I ({u | (v = u) ∨ (u = v) ∈ B}
) is stable or increases by a set of indexes which is already bounded. The first group does not generate new equality constraint with new indexes. Rules of the second group do not manage equality constraints. Then, the invariant is satisfied by G 1 and G 2 . The only rule of the third group that may generate an equality constraint is Rule 15. However, the possible existential indexes that may be in this equality constraint already belong to the Sub equality. Then, the set of these indexes is bounded according to Proposition 29 and Proposition 30 and thus, the invariant still holds. Rule 21 eliminates the constraint. Rule 22 eliminates the whole block. If Rule 24 generates a new index, then it would be an universal one. Thus, for these rules, the invariant is still satisfied. Rule 23 decomposes an equality constraint between two terms into another equality constraint between two subterms while preserving the same index variables. Then, the set of existential indexes remains stable and the invariant still holds. Rule 25 replaces an index by another using the constraint (c i = c j ). However, according to Invariant 10, ant(i, j) ∈ V . Then, even if Rule 25 lead to the generation of a new index in other equality constraints, then, this index belongs to a set which is already bounded since this index is in V and V is bounded according to Proposition 29. Thus, the invariant still holds. Only Rules 26 and 27 of the fifth group may generate new equality constraints. However, the possible indexes in these constraints already belongs to equality constraints in the left side of rules. Then, the set of indexes is stable and therefore the invariant is satisfied. Only Rule 35 of the sixth group may generate new equality constraints: (u o δ o = v). If ∃Z j s.t j ∈ R and Z j m v, then according to Invariant 7, j, m ∈ Q which is contradictory with j ∈ R. The same reason is valid for the case where ∃Z j s.t j ∈ R and Z j m u o δ o since u o belongs to tha master constraint (X io = u o ). Then, the invariant still holds.

Proposition 32. V ar C,R I ({u | (v = u) ∨ (u = v) ∈ B}) is bounded.
Proof. We prove Proposition 32 by proving the following invariant:

V ar C,R I ({u | (v = u) ∨ (u = v) ∈ B}
) is stable or increases by a set of indexes that is already bounded. We only focus on equality constraints (v = u) that do not contain indexed variables.

If ∃X i s.t X i m u or X i m v then V ar C,R I ({u | (v = u) ∨ (u = v) ∈ B})
according to Proposition 29. Suppose then that (v = u) does not contain indexed variables.

The first group does not generate new equality constraint with new indexes. Rules of the second group do not manage equality constraints. Then, the invariant is satisfied by G 1 and G 2 . The only rule of the third group that may generate an equality constraint is Rule 15. However, the possible existential indexes that may be in this equality constraint already belong to the Sub equality. Then, the set of these indexes is bounded according to Proposition 29 and Proposition 30 and thus, the invariant still holds. Rule 21 eliminates the constraint. Rule 22 eliminates the whole block. If Rule 24 generates a new index, then it would be an universal one. Thus, for these rules, the invariant is still satisfied. Rule 23 decomposes an equality constraint between two terms into another equality constraint between two subterms while preserving the same index variables. Then, the set of existential indexes remains stable and the invariant still holds. Rule 25 replaces an index by another using the constraint (c i = c j ). However, according to Invariant 10, ant(i, j) ∈ V . Then, even if Rule 25 lead to the generation of a new index in other equality constraints, then, this index belongs to a set which is already bounded since this index is in V and V is bounded according to Proposition 29. Thus, the invariant still holds. Only Rules 26 and 27 of the fifth group may generate new equality constraints. However, the possible indexes in these constraints already belongs to equality constraints in the left side of rules. Then, the set of indexes is stable and therefore the invariant is satisfied. Only Rule 35 of the sixth group may generate new equality constraints: (u o δ o = v). If ∃c j s.t j ∈ R and c j m v, then it was already counted since this index belongs to the constraint (X m = v) and according to Proposition 31, the set of such indexes is bounded. If ∃c j s.t j ∈ R and c j m u o δ o , then we have a fresh index per indexed variable per master constraint. Thus, the number of possible existential indexes generated this way is bounded by (the number of indexed variable * the number master constraint). However, the number of master constraints is bounded by the number of constraints in E which is fixed. Besides, the number of indexed variables is bounded by (the number of vectors * the number of indexes in varibales in equality constraints). However, the number of vectors is defined by the specification of the protocol. Moreover, the number of indexes in variables in equality constraints is the sum of universal indexes and the existential ones. The set of universal indexes is bounded according to Proposition 26. The set of existential ones is bounded according to Proposition 31. We conclude that the invariant is satisfied by Rule 35.

Termination For Protocols with Autonomous Keys

We first define a weight for terms, elementary constraints, blocks and constraint systems. Then, we show that each rule decreases this weight.

In order to define the weight of a term, we need to introduce some definitions:

Definition 36 (Row of a term). A row of a term t is defined as follows:

• r(X) = max{l | X ⊏ l Y , Y ∈ X ∪ X I } for X ∈ X ∪ X I • r(t) = max{r(Y ) | Y < t, Y ∈ X ∪ X I } For a variable X ∈ X ∪ X I , If ∄Y ∈ X ∪ X I , s.t X ⊏ Y , then, r(X) = 0.
Definition 37 (Size of a term t). We define the size of a term t denoted by |t| as follows:

Definition 41 (Weight of a constraint System). Consider a constraint system: S = B 1 ∧ ..B l . We define the weight of S as follows:

S = [ B i ] Bi∈S
Proposition 34. Algorithm 1 terminates for protocols with autonomous keys.

Proof. We prove Proposition 34 by showing that each rule of our inference system decreases the weight of the whole constraint system S. That is, considering a rule r, we show that post(r) < pre(r) . We denote always the block treated by these rules B. First, Rule 26 decreases the size of the block for which it is applied since it decreases N a -N R B . Then, Rules 3, 14, 20, 22, 32 eliminate one block of the constraint system since they lead to ⊥. Thus, they decrease S . Moreover, Rules 21, 25 and 30 eliminate a constraint from the block treated B since they lead to ⊤. Then, B decreases. Rule 1 changes an equality constraint ctr ∈ B into another one of the form (X = u) where X ∈ X ∪ X I . The only parameter that changes for the weight of B is Ec B which increases and then N cE -Ec B decreases. Then, B decreases and so does S .

For Rule 2, we have

X > u since X = u ∈ B. Indeed, u ≤ |u| * p max{r(Y )|Y <u,Y ∈X ∪X I } ≤ p r(X)+1 . Then, Y = X = Y + X > Y + u = Y = u . Thus, Y = X > Y = u
and therefore B decreases and so does S .

Rule 4 adds a new master constraint and changes only dull constraints. Then, the only parameter that changes for the weight of B is either N cEF -M Ec B or N cEF -M F c B . Then, B decreases and so does S .

Rule 5 transforms a master constraint of the form F orge to a master equality constraint. Then, it increases N cEF -M F c B but decreases N cEF -M Ec B . Then, B decreases and so does S .

For Rule 6, we have uλ < u where λ = [Y j ← Z]. Indeed, since Y j = Z ∈ B, we have r(Z) < r(Y j ) which leads to Z < Y j . Then, X = uλ < X = u and therefore B decreases.

For Rule7, we reason similarly to Rule 6 to prove that X = uλ < X = u . Moreover, Y j = Z < X = u . Indeed, Y j < u. then, Y j < u . Besides, Z is a fresh variable and since X = u ∈ B then r(Z) < r(X). Thus, Z < X and therefore Y j = Z < X = u . We conclude that B decreases since the other parameters do not change.

Rule 8 adds a submaster constraint to the block B. Then, N cE -Sc B decreases and therefore B decreases.

For Rule 9, pre(R 9) > post(R 9) . Indeed, pre(R 9) = k, t + E + |E| + 1 and post(R 9 We show in a similar way as Rule 10 that for Rule 16, B decreases. For Rule 17, first, pre(R 17

) = k, 1 + t + u + b + |E| where k = st-#K. Second, post(R 17) = [ k, 1 + t + u + |E| , k ′ , 1 + b + E + |E| ] where k ′ = st-#K ∪ {{u} p p }. Since k ′ < k, pre(R 17) > post(R 17) .
We For Rule 24, pre(R 24) > post(R 24) . Indeed, pre(R 24) = k, 4 + uδ + wδ l,k δ . Moreover, post(R 24) = k, uδ + wδ l,k δ . Then, since the other parameters of the weight of B do not change, B decreases.

We show in a similar way as Rule 2 that for Rule 27 B decreases since X > u and therefore

X = v > u = v .
We show in a similar way as Rule 27 that for Rule 28 B decreases since X i = u ∈ B and then X i > u and therefore X i ∈ F orge c (E ′ , K) > u ∈ F orge c (E ′ , K) . The same proof is valid for Rule 29.

For Rule 31, since

X = w ∈ B, X > w . Then, t ∈ Sub d (X, E ′ , E, K) > t ∈ Sub d (w, E ′ , E, K) . Besides,

Checking Satisfiability

Let F = ∀Q∃R B 1 ∨ .. ∨ B p be a normalized constraint system as created by our decision algorithm. We choose two index variables q and r, fixed for all the following, that we will use as replacement for index in Q or R respectively. We rewrite here the definitions given earlier and give precise the application of rules E1 and E2. First, let us define patterns of a term and a constraint system : Definition 42. We say that u is a pattern of v for index variable i, denoted u ≪ i v, iff u m v and V ar I (v) ⊂ {i} or there exists mpair(k, t) m v such that u ≪ i tδ k,i .

Definition 43. Given a constraint system F = ∀Q∃R B 1 ∨ .. ∨ B p , let δq be δ Q,R→q and δr be δ Q,R→r . We denote by P att(F ) the set of all patterns in F defined by : P att(F ) = u | ∃v ∈ T in F s.t. u / ∈ X I , V ar X I (u) ⊆ {q} and u ≪ q v δq or u ≪ r v δr Second, we choose an order on P att(F ), denoted ⊳ and fixed for all the following. For any u ∈ T , we denote by u δ the higher term in P att(F ) between u δq and u δr w.r.t ⊳. Also, we define two extra deduction rules E1 and E2 ensuring that our system always uses the lower patterns w.r.t ⊳ with higher priority:

(X m = u) → u ′ ⊳u δ ∃k. (X m = u ′ δ k q,m ) ∧ v⊳u ′ ∀k ′ .X m = vδ k ′ q,m ∧ u ′ δ k q,m = u (E1) (X m ∈ F orge c (E, K)) → u ′ ∈P att(F ) ∃k. (X m = u ′ δ k q,m ) ∧ v⊳u ′ ∀k ′ .X m = vδ k ′ q,m ∧ u ′ δ k q,m ∈ F orge c (E, K) (E2) ∨(X m ∈ F orge c (E, K)) ∧ v∈P att(F ) ∀k ′ .X m = vδ k ′ q,m
To prevent cycles, the rule E1 cannot be used if the block already contains v⊳u δ ∀k ′ .X m = vδ k ′ q,m , and the rule E2 cannot be used if the block already contains v∈P att(F ) ∀k ′ .X m = vδ k ′ q,m . Moreover, E1 and E2 implicitly update the environment E of each block in the constraint system by recomputing them the same way as in Algorithm 1, except that only variables present in some F orge c (E, K) in F can get values in E. This way, we can normalize again any constraint system computed by E1 or E2 using the phase 2 of the normalization from definition 25. That is, we denote by ↓ Ext the application of as many rules E1 and E2 as possible (minimum one), followed by the phase 2 of the normalization. However, the normalisation may create new constraints for which we need E1 and E2 again, and thus, we need to iterate ↓ Ext . Hopefully, we remark that :

Lemma 12. P att(F ) = P att(F ↓ Ext ), and

|[ F ]| e ∅ = F ↓ Ext e ∅ .
Proof. This follows directly from the definition of patterns, which includes subterms, and from the rules which always extract subterms, i.e. nothing else than subterms of patterns can appear during the normalization. More precisely, P att(F ) is stable by application of any rule since :

• Implicit reformation rules have no effect on patterns;

• Prioritary rules do not create new patterns;

• Forge, Sub or equality reduction rules : create new constraints with only patterns inherited from previous ones;

• Interleaving rules : do not create new patterns;

• E1 and E2 rules : do not create new patterns.

which shows the stability of P att(..). Moreover, the rules E1 and E2 naturally preserves the semantics, since it creates disjunctions based on an exhaustive enumeration of all possible values of X m . Details are similar to the correction and completeness of the block interleaving rules. This proves the lemma.

Proposition 35. If ↓ Ext iterated on CBS k+1 terminates, then there exists e max computable such that :

∀e ≥ e max , |[ CBS k+1 ]| e ∅ = |[ CBS k+1 ]| emax ∅ Proof.
As above, let F = ∀Q∃R B 1 ∨ .. ∨ B p be a normalized constraint system as created by our decision algorithm, i.e. F = CBS k+1 , and let q and r be the two index variables fixed at the beginig of this section.

Using lemma 12 and hypothesis on ↓ Ext , we can iterate ↓ Ext until a constraint system on which no E1 or E2 rule can be applied, that is, a system where :

• Any constraint (X m = u) comes with v⊳u δ ∀k ′ .X m = vδ k ′ q,m in the same block;

• Any constraint (X m ∈ F orge c (E, K)) comes with v∈P att(F ) ∀k ′ .X m = vδ k ′ q,m in the same block.

Let F ′ be this constraint system obtained from F by iteration of ↓ Ext .

Third, we transform F ′ into a system where we choosed values for any variable under a forge constraint. Let c be a ground term in E 0 , i.e a fixed message that the intruder knows from the start. Let d = (X=u) ∈F ′ Depth(u) be the sum of all depth of equalities in F ′ . Note that d is bounded by the size of

F ′ . For any -→ X ∈ -→ X we choose a ground term b-→ X = c, .., c such that ∀ -→ X , -→ Y , b-→ X = b-→ Y . Now, for any -→ X ∈ -→ X let t-→ X = .. b-→ X c .. c be the term of depth (d + 1). Note that by construction, ∀ -→ X , -→ Y , t-→ X = t-→ Y and ∀ -→ X ,
t-→ X ∈ DY c (E 0 , ∅). Now, let F ′′ be the closure of F ′ by :

(X i ∈ F orge c (E)) → X i = t-→ X (E3) Lemma 13. If ∃σ ∈ |[ F ′ ]| e ∅ then ∃σ ′ ∈ |[ F ′′ ]| e ∅ .
Proof. Here, we do not guaranty that any solution of F ′ is preserved, but only that at last one survives. That is, let σ

∈ |[ F ′ ]| e ∅ with F ′ = ∀Q∃R B 1 ∨ .. ∨ B p . We define σ ′ such that : • ∀X ∈ X , σ ′ (X) = σ(X); • ∀ -→ X ∈ -→ X , ∀s ∈ {1.
.e}, if ∃u ∈ P att(F ′ ), ∃τ with τ (q) = s such that σ(X s ) = σ(uτ ) and u minimal w.r.t ⊳, then σ ′ (X s ) = σ ′ (uτ ); Note that u is single by minimality w.r.t ⊳ and because V ar X I (u) ⊆ {q}.

• ∀ -→ X ∈ -→ X , ∀s ∈ {1..e}, if ∀u ∈ P att(F ′ ), ∀τ with τ (q) = s, we have σ(X s ) = σ(uτ ), then σ ′ (X s ) = t-→ X . We show that σ ′ ∈ |[ F ′′ ]| e ∅ : Thanks to σ ∈ |[ F ′ ]| e ∅ , we know that ∀τ Q , ∃τ ⊇ τ Q , ∃i ∈ {1..p}, ∀ctr ∈ B i σ ∈ |[ ctr ]| e τ .
We examine all possible constraints ctr :

• If ctr = (X = u) sm or ctr = (X ∈ F orge c (E, K)), then σ ′ ∈ |[ ctr ]| e τ since σ ′ (X) = σ(X); • If ctr = (X m = u) , then thanks to the definition of F ′ , we have also σ ∈ v⊳u δ ∀k ′ .X m = vδ k ′ q,m e τ .
Therefore, u ′ = u δq or u ′ = u δr , with V ar X I (u ′ ) ⊆ {q}, is a pattern u ′ ∈ P att(F ). Moreover, it is the minimal pattern w.r.t ⊳ (since V ar X I (u) ⊆ {m}) such that σ(X m τ ) = σ(u ′ τ ′ ) with τ ′ (q) = τ (m), τ ′ (r) = τ (k) and k ∈ V ar I (u)\V ar X I (u) if non-empty. Thus, u ′ matches the second point in the definition of σ

′ , i.e. σ ′ (X m τ ) = σ ′ (u ′ τ ′ ) = σ ′ (uτ ) and σ ′ ∈ |[ ctr ]| e τ . • If ctr = (X m ∈ F orge c (E, K)) , then again thanks to the definition of F ′ , we have σ ∈ v∈P att(F ) ∀k ′ .X m = vδ k ′ q,m e τ . Therefore, σ ′ (X m τ ) = t-→ X and thus, σ ′ ∈ X m = t-→ X e τ .
• If ctr = (∀k X m = u), we prove by recurrence a more general property of σ and σ ′ . We do this in two steps :

Claim 2. ∀u ∈ P att(F ), ∀τ , ∀ -→ Z , t-→ Z = σ ′ (uτ )
Proof. We know that the value of some X s through σ ′ is a pattern using only variables indexed by s. Therefore, we have only two cases : either there exists some t-→ Y subterm of σ ′ (uτ ), and thus Depth(σ ′ (uτ )) > d+1 since u / ∈ X I , or there is no such t-→ X subterm of σ ′ (uτ ), and thus Depth(σ ′ (uτ )) ≤ d since the same patterns cannot appear twice in the same branch of σ ′ (uτ ) without creating a cycle. In both cases Depth(σ ′ (uτ )) = d + 1 which proves the claim.

Claim 3. ∀w, v ∈ P att(F ) ∪ X I with u = wδ r,r ′ , ∀τ if σ(uτ ) = σ(vτ ) then σ ′ (uτ ) = σ ′ (vτ ).
Proof. Assume that the property is true for Depth(u) + Depth(v) < n, n integer. Let u and v be two terms as above with Depth(u) + Depth(v) = n. We have cases depending of the structure of u and v :

-If u = f ({u i }) and v = g({v j }) then either f = g and thus σ ′ (uτ ) = σ ′ (vτ ), or f = g and ∃i σ(u i τ ) = σ(v i τ ) with Depth(u i ) + Depth(v i ) < n, i.e. σ ′ (u i τ ) = σ ′ (v i τ ) and thus σ ′ (uτ ) = σ ′ (vτ ).
This case includes constants, i.e. f of g with no parameter.

-If u = Y q and v = Z q with σ ′ (Y q τ ) = σ ′ (u ′ τ ) and σ ′ (Z q τ ) = σ ′ (v ′ τ ), it means that σ(Y q τ ) = σ(u ′ τ ) and σ(Z q τ ′ ) = σ(v ′ τ ), with σ(u ′ τ ) = σ(v ′ τ ). Thus, similarly as in the case above, we have σ ′ (u ′ τ ) = σ ′ (v ′ τ ) and thus σ ′ (uτ ) = σ ′ (vτ ).

-If u = Y q and v = Z q with σ ′ (Y q τ ) = t-→ Y and σ ′ (Z q τ ) = t-→ Z , then t-→ Y = t-→ Z and thus σ ′ (Y q τ ) = σ ′ (Z q τ ). Note that u = v is impossible.

-If u = Y q and v / ∈ X I with σ ′ (Y q τ ) = t-→ Y , then thanks to claim 2 above we have σ ′ (Y q τ ) = t-→ Y = σ ′ (vτ ). The same holds with u and v reversed.

-If u = Y q and v = Z q with σ ′ (Y q τ ) = t-→ Y and σ ′ (Z q τ ) = σ ′ (v ′ τ ), then thanks to claim 2 again we have σ ′ (Y q τ ) = t-→ Y = σ ′ (v ′ τ ).
This proves the claim.

Consequently, since ctr = (∀k

X m = u) we have σ(X m τ ′ ) = σ(uτ ′ ) with any τ ′ ⊇ τ such that Dom(τ ′ ) = Dom(τ ) ∪ {k}, and thus thanks to claim 2, σ ′ (X m τ ′ ) = σ ′ (uτ ′ ) i.e. σ ′ ∈ |[ ctr ]| e τ . • If ctr = (X m / ∈ F orge c (E)), assuming X = u ∈ X ∪ X I | V ar X I (
′ (uτ ) ∈ DY (E ′ σ ′ , K e τ σ ′ ) s.t. no term in t-→ X - → X ∈ - → X is decomposed, with E ′ = E ∪ t-→ X . Then ∀t knowledge in d, ∃v ∈ P att(F ) ∪ X ∃τ ′ s.t. t = σ ′ (vτ ′ ).
Moreover, replacing each t by σ(vτ ′ ) and E ′ by E ′′ = E ∪ {σ(X s ) | ∀w ∈ P att(F ), ∀τ ′ , σ(X s ) = σ(wτ ′ )} in d maintains the validity of each rule's application.

Proof. We uses the structure of any minimal derivation, i.e. that any decomposed term is a subterm of the initial knowledge, and that any composed term is a subterm of either the goal or a decomposed term (otherwise there would be useles rules in the derivation). Knowing this, we remark that :

-Let L = L d (σ ′ (wτ ′ )) ∈ d such that w ∈ P att(F ) ∪ X . Let t be the term generated by L. Then either w = f ({w i }), and thus ∃i such that t = σ ′ (w i τ ′ ), i.e. ∃w ′ ∈ P att(F ) ∪ X ∃τ ′′ such that t = σ ′ (w ′ τ ′′ ), since subterm of patterns are patterns too. Note that τ ′′ = τ ′ unless f is an mpair; Or w ∈ X ∪ X I , and thus ∀ -→ X , σ ′ (wτ ′ ) = t-→ X since such terms cannot be decomposed in d. Therefore, ∃v ∈ P att(F ) ∃τ ′′ such that σ ′ (wτ ′ ) = σ ′ (vτ ′′ ), and since v / ∈ X ∪ X I we can repeat the same reasonning as with w = f ({w i }).

-Let L = L c (σ ′ (wτ ′ )) ∈ d such that w ∈ P att(F ) ∪ X . Let {t i } be the set of terms used by L to generate σ ′ (wτ ′ ). Then either w = f ({w i }), and thus ∀i ∃w ′ i ∈ P att(F ) ∪ X ∃τ ′′ i such that t i = σ ′ (w ′ i τ ′′ i ); Or w ∈ X ∪ X I with ∃v ∈ P att(F ) ∃τ ′′ such that σ ′ (wτ ′ ) = σ ′ (vτ ′′ ), and thus the same reasoning as for w = f ({w i }) applies; Note that w ∈ X ∪ X I with ∃ -→ X such that σ ′ (wτ ′ ) = t-→ X is impossible by minimality, since each t-→ X is already in E ′ . Therefore, the first part of the claim follows by iteration of these two steps on the structure of d, starting from Eσ or σ ′ (uτ ). Moreover, we remark that all the patterns we chosed for knowledges in d validates the subterm property for each rule, modulo renaming of index variables: that is, a decomposition rule generates a term with a pattern that is a subterm of the pattern of it's argument, module index renaming, and reversly for composition rules. Therefore, replacing σ ′ by σ cannot change the validity of each rule's application, provided that the values of variables with no pattern are still available in the initial knowledge (i.e. E ′′ replacing E ′ ), which proves the claim.

We uses this claim on ctr = (X m / ∈ F orge c (E, K)), i.e. assume that σ ′ (X m τ ) ∈ DY c (Eσ ′ , K e τ σ ′ ) despites the fact that σ(X m τ ) / ∈ DY c (Eσ, K e τ σ). Then there exists a derivation d defined as in Claim 4 with , since X i = t-→ X is strictly more restrictive than X i ∈ F orge c (E). Therefore, we have the following property :

E ′ = E ∪ t-→ X , since ∀ -→ X t-→ X ∈
|[ F ′ ]| e ∅ = ∅ iff |[ F ′′ ]| e ∅ = ∅
and thus, it is enough to check the satisfiability of F ′′ instead of F ′ . However, F ′′ has a very interesting property that will allow us to bound e with equivalent satisfiability. That is :

∀σ ∈ |[ F ′′ ]| e ∅ , ∀s ∈ {1..e} , ∀ -→ X ∈
-→ X , either σ(X s ) = t-→ X (P 1) or ∃u ∈ P att(F ) ∃τ with τ (q) = s s.t. σ(X s ) = σ(uτ ) Note that this structure comes from rules E1, E2 and E3. From now on, let us fix some σ ∈ |[ F ′′ ]| e ∅ (assuming there exists one), some pattern u Xs ∈ P att(F ) ∪ {t-→ X } and τ Xs such that τ Xs (q) = s and σ(X s ) = σ(u Xs τ Xs ), according to P 1. We remark that since P att(F ) and -→ X are finite, i.e. bounded by a function in the size of the protocol specification, there exists necessarily only a bounded number of possible choices for {u Xs }-→ X ∈ - → X , independently of s. Let e 1 be this bound. Moreover, for each X s there is also only a bounded number of set of knowledges E from F ′′ and keys K such that σ(X s ) ∈ DY c (Eσ, Kσ). Let e 2 be this bound. We write e max = e 1 × e 2 × # -→ X . Naturally, if e > e max then there exists s = s ′ such that {u Xs }-→ X ∈ -

→ X = u X s ′ - → X ∈ - →
X and ∀ ( ∈ F orge c (E, K)) in F ′′ , ∀ -→ X , σ(X s ) ∈ DY c (Eσ, Kσ) iff σ(X s ′ ) ∈ DY c (Eσ, Kσ). We will use this to prove that there is no need to search for attacks with e > e max , i. Proof. Let s, s ′ be as defined above, i.e. s.t. {u Xs }-→ X ∈ - → X = u X s ′ - → X ∈ -→ X and ∀ ( ∈ F orge c (E, K)) in F ′′ , ∀ -→ X , σ(X s ) ∈ DY c (Eσ, Kσ) iff σ(X s ′ ) ∈ DY c (Eσ, Kσ). We remark that equality of patterns do not imply equality of values w.r.t σ since index of constrants may change. However, equality of patterns will be sufficient to guaranty that at indexes s and s ′ , variables validate the same unequalities. Thus, we will "remove" the index s ′ from σ and show that s can effectively replace s ′ in any case. That is, with γ replacing any c v by c v-1 if v > s ′ , and replacing any c s ′ by c s , c ∈ -→ C , let σ ′ be defined as :

• ∀i < s ′ , ∀ -→ X ∈ -→ X , σ ′ (X i ) = γ(σ(X i )); • ∀i ≥ s ′ , ∀ -→ X ∈ -→ X , σ ′ (X i ) = γ(σ(X i+1
));

• ∀X ∈ X , σ ′ (X) = γ(σ(X)).

Assuming that F ′′ = ∀Q∃R B 1 ∨ .. ∨ B p , let τ ′ Q be any index substitution from Q to {1..e -1}. Thus, let τ Q be the index substitution from Q to {1..e} such that :

• ∀i ∈ Q, if τ ′ Q (i) < s ′ then τ Q (i) = τ ′ Q (i), otherwise τ Q (i) = τ ′ Q (i) + 1.
i.e. we "insert" a blank column at index s ′ . Now, by definition of σ, ∃τ ⊇ τ Q such that σ ∈ |[ B 1 ∨ .. ∨ B p ]| e τ . Thus, we define τ ′ ⊇ τ ′ Q such that :

• ∀r ∈ R, if τ (r) < s ′ then τ ′ (r) = τ (r); if τ (r) = s ′ then τ ′ (r) = s; otherwise τ ′ (r) = τ (r) -1.

i.e. we "remove" the column at index s ′ . We must prove that σ -If τ (m) = s ′ and V ar X I (u) = {m}, then σ ′ (X m τ ′ ) = γ(σ(X s )). Since X s and X s ′ share the same pattern for σ, and since σ validates ctr, this pattern is necessarily u, i.e. γ(σ(X s )) = γ(σ(u[m ← s])) = σ ′ (uτ ′ ); -If τ (m) = s ′ and V ar X I (u) = {j} = {m}, then as above σ ′ (X m τ ′ ) = γ(σ(X s )), and X s and X s ′ share the same pattern u. Thus, σ(X s ) = σ(u[j ← τ (j)]). Now, either τ (j) = s ′ and thus γ(σ(uτ )) = σ ′ (uτ ′ ), or τ (j) = s ′ and thus γ(σ(uτ )) = σ ′ (u[j ← s]) = σ ′ (uτ ′ ). In both cases, σ ′ (X s ) = γ(σ(X s )) = σ ′ (uτ ′ ), and thus, σ ′ ∈ |[ ctr ]| e τ ′ .

• If ctr = X m = t-→ X , then σ ′ (X m τ ′ ) = γ(σ(X m τ )) = γ(t-→ X ) = t-→ X since X s and X s ′ share the same pattern, and in this case this pattern is t-→ X . Thus, σ • If ctr = (X m / ∈ F orge c (E, K)), then by assumption on s and s ′ we know that σ(X s ) and σ(X s ′ ) are both in ∈ DY c (E ′ σ, Kσ) or none is, for any ( ∈ F orge c (E ′ , K)) in F ′′ , i.e. including E. Thus, σ ′ (X m τ ′ ) / ∈ DY c (Eσ ′ , Kσ 10 Analysing Asokan-Ginzboorg

We have checked two scenarii of the synchronous version of the Asokan-Ginzboorg protocol (AG protocol). Although this version of the AG protocol has not autonomous keys, the analysis of the two scenarii terminates and gives two results. In the first one, we consider a 'normal' execution of a single session. We show that this execution is secure against a secrecy attack on the group key. In the second scenario, we consider two parallel sessions. We have found an authentication attack. Note that for these scenarii, although the version of the protocol does not only consider autonomous keys, the analysis terminates.

10.1 First Scenario: Asokan-Ginzboorg with a Single Session Consider a single session of the tagged version of Asokan-Ginzboorg, specified as follows:

(L, 1) Init ⇒ mpair(t, l, {e} p ) (S, 1) mpair(i, L, {E i } p ) ⇒ mpair(j, ( a j , ({ r j , s j } (Ej ) j ) j ) j ) (L, 2) mpair(k, ( a k , ({ R k , S k } (e) k ) k ) k ) ⇒ mpair(m, ({ mpair(o, (S o ) o ), s ′ } (Rm) m ) m ) (S, 2) mpair(q, ({ mpair(u, (s u ) u ), S ′ } (rq) q ) q ) ⇒ mpair(w, a w , { (s w ) w , H( mpair(y, (s y ) y ), S ′ ) } F ( mpair(y,(sy) y ),S ′ ) ) (L, 3) mpair(x, a x , { (S x ) x , H( mpair(z, (S z ) z ), s ′ ) } F ( mpair(z,(Sz) z ),s ′ ) ) ⇒ End

The ordering on steps is: W = 1, 2, 3, W S = 1, 2 with 1 < W L 2, 2 < W L 3, and 1 < W S 2. The execution that we focus on is the following: (L, 1), (S, 1), (L, 2), (S, 2), (L, 3) . The property we want to check is the secrecy of the group key: Sec = F ( mpair(z, (S z ) z ), s ′ ). Then, the constraint system S that we have to solve is specified below:

(step 1) mpair(i, L, {E i } p ) ∈ F orge(E 1 , ∅) (step 2) mpair(k, ( a k , ({ R k , S k } (e) k ) k ) k ) ∈ F orge(E 2 , ∅) (step 3) mpair(q, ({ mpair(u, (s u ) u ), S ′ } (rq) q ) q ) ∈ F orge(E 3 , ∅) (step 4) mpair(x, a x , { (S x ) x , H( mpair(z, (S z ) z ), s ′ ) } F ( mpair(z,(Sz) z ),s ′ ) ) ∈ F orge(E 4 , ∅) (step 5) Sec ∈ F orge(E 5 , ∅)

where E i are defined as follows:

E 1 = {mpair(t, l, {e} p )} E 2 = E 1 ∪ {mpair(j, ( a j , ({ r j , s j } (Ej ) j ) j ) j )} E 3 = E 2 ∪ {mpair(m, ({ mpair(o, (S o ) o ), s ′ } (Rm) m ) m )} E 4 = E 3 ∪ {mpair(w, a w , { (s w ) w , H( mpair(y, (s y ) y ), S ′ ) } F ( mpair(y,(sy) y ),S ′ ) )} E 5 = E 4

The normalisation of S\{step 5} by our rules system gives the system below. Note that this system is not put in the disjunctive form to avoid redundancy.

(S\{step 5})  = ∀i, j, k, k 2 , q, o, q 1 , o 1 , x, z, z 1 , z 2 , z 3 , z 4 , z 5 by witness and request. Then, the constraint system S that we have to solve is specified below:

(step 1) mpair(i, L, {E i } p ) ∈ F orge(E 2 , ∅) (step 2) mpair(i, L ′ , {E ′ i } p ) ∈ F orge(E 3 , ∅) (step 3) mpair(k, ( a k , ({ R k , S k } (e) k ) k ) k ) ∈ F orge(E 4 , ∅) (step 4) mpair(k, ( a k , ({ R ′ k , S ′ k } (e2) k ) k ) k ) ∈ F orge(E 5 , ∅) (step 5) mpair(q, ({ mpair(u, (s u ) u ), S ′ } (rq) q ) q ) ∈ F orge(E 6 , ∅) (step 6) mpair(q, ({ mpair(u, (s ′ u ) u ), S" } (r ′ q ) q ) q ) ∈ F orge(E 7 , ∅) (step 7) mpair(x, a x , { (S x ) x , H( mpair(z, (S z ) z ), s ′ ) } F ( mpair(z,(Sz) z ),s ′ ) ) ∈ F orge(E 8 , ∅) (step 8) mpair(x, a x , { (S ′

x ) x , H( mpair(z, (S ′ z ) z ), s" ) } F ( mpair(z,(S ′ z ) z ),s" ) ) ∈ F orge(E 9 , ∅) where E i are defined as follows:

E 2 = {mpair(t, l, {e} p ), mpair(t, l2, {e2} p )} E 3 = E 2 ∪ {mpair(j, ( a j , ({ r j , s j } (Ej ) j ) j ) j )} E 4 = E 3 ∪ {mpair(j, ( a j , ({ r ′ j , s ′ j } (E ′ j ) j ) j ) j )} E 5 = E 4 ∪ {mpair(m, ({ mpair(o, (S o ) o ), s ′ } (Rm) m ) m )} E 6 = E 5 ∪ {mpair(m, ({ mpair(o, (S ′ o ) o ), s" } (R ′ m ) m ) m )} E 7 = E 6 ∪ {mpair(w, a w , { (s w ) w , H( mpair(y, (s y ) y ), S ′ ) } F ( mpair(y,(sy) y ),S ′ ) )} E 8 = E 7 ∪ {mpair(w, a w , { (s ′ w ) w , H( mpair(y, (s ′ y ) y ), S" ) } F ( mpair(y,(s ′ y ) y ),S" ) )} E 9 = E 8

We normalise S by our rules system. We just focus on a single block of the normalized system:

(L ∈ F orge c (E 2 , ∅) ∧ L ′ ∈ F orge c (E 3 , ∅) ∧ (E i1 = e2) m ∧ (E ′ i4 = e) m ∧ (R k1 = r ′ k1 ) m ∧ (S k1 = s ′ k1 ) m ∧ (E ′ j1 = e) f ∧ (R ′ k2 = r k2 ) f ∧ (S ′ k2 = s k2 ) f ∧ (E j2 = e2) f ∧ (R ′ q1 = r q1 ) f ∧ (S ′ = s") sm ∧ (S ′ o1 = s o1 ) f ∧ (R q2 = r ′ q2 ) f ∧ (S" = s ′ ) sm ∧ (S o2 = s ′ o2 ) f ∧ (S x1 = s ′ x1 ) f ∧ (S y1 = s ′ y1 ) f ∧ (S ′ x2 = s x2
) f ∧ (S ′ z1 = s z1 ) f ∧witness((L, , 1), (S, , 1), f s, mpair(o, (S o ) o ), s ′ ) ∧witness((L, , 2), (S, , 2), s s, mpair(o, (S ′ o ) o ), s" ) ∧request((S, , 1), (L, , 1), f s, mpair(u, (s u ) u ), S ′ ) ∧request((S, , 2), (L, , 2), s s, mpair(u, (s ′ u ) u ), S" )) Index variables in this block are quantified in S by: ∀i 1 , ∀i 4 , ∀k 1 , ∀k 2 , ∀q 1 , ∀q 2 , ∀o 1 , ∀o 2 , ∀x 1 , ∀x 2 , ∀y 1 , ∀z 1 , ∃j 1 , ∃j 2 This block corresponds to an authentication attack on f s . Indeed, the solution σ of this block gives the value s ′ o to S o . Thus, the request for f s gives a value different from the one of the corresponding witness. The same raison is valid for s s .

Conclusion and Further Works

We have proposed an extension of the constraint-based approach in symbolic protocol verification in order to handle a class of protocols (the Well-Tagged ones with Autonomous Keys) which admit unbounded lists in messages. This class can be used to model in particular interesting group protocols. We have proposed a decision procedure for Well-Tagged protocols with Autonomous Keys. We have studied the Asokan-Ginzboorg protocol with keys having index variables outside mpair's. We showed that the analysis of this protocol terminates. Thus, we conjecture termination for a larger class than Well-Tagged protocols where the restriction of autonomous keys is weakened to include at least this protocol.

c

  = c -→ ⊤ where c ∈ C ∪ C I (21) t = t ′ -→ ⊥ where { t, t′ } ⊂ C ∪ C I ∪ G and t = t′ (22) f (u 1 , .., u m ) = f (w 1 , .., w m ) -→ i=1...m

  Proposition 3. Rule 3 is correct and complete. Proof. Let B be a block with (X = u) ∈ B, Y < u, and Y ⊏ X in B. Then, ∀τ , ∀e, ∀σ ∈ |[ B ]| e τ , we have Y e τ σ < X e τ σ thanks to Y ⊏ X and Y e τ σ < X e τ σ thanks to Y < u and (X = u) ∈ B. This is impossible, and therefore, |[ B ]| e τ = |[ ⊥ ]| e τ

Proof.

  We proceed by recurrence over |w e τ σ|. Base case: |w e τ σ| = 1. Then, either w ∈ C ∪ C I or w ∈ X ∪ X I . If w ∈ C ∪ C I , then, w e τ σ = t e τ σ. Thus, t e τ σ ∈ Dy d (E e τ σ ∪ {w e τ σ}, K e τ σ). If w = X ∈ X ∪ X I , and since σ ∈ |[ t ∈ Sub(w, E, E, K) ]| e τ , then, according to Proposition 6, we have either (1) or (2) where:

  2) t e τ σ = Xτ σ If (1) then vδ ∈ C ∪ C I since |v e δτ ′ σ| = |w e τ σ| = 1. However, v e δτ ′ σ = t e τ ′ σ and t e τ ′ σ = t e τ σ since k, i / ∈ V ar I (t) and Dom(τ ′ ) = Dom(τ ) ∪ {k, i} (by definition of the semantics of Sub). Therefore, t e τ σ ∈ Dy d (E e τ σ ∪ {w e τ σ}, K e τ σ) since v e δτ σ = t e τ σ = w e τ σ. If (2) then since w = X, we have t e τ σ ∈ Dy d (E e τ σ ∪ {w e τ σ}, K e τ σ). Induction step: Assume Lemma 8 is true for term of size strictly smaller than |w e τ σ|. Since σ ∈ |[ t ∈ Sub(w, E, E, K) ]| e τ , we have ∃u ∃F, L such that u L F w e τ , K e τ σ ∩ F σ = ∅, F σ ⊆ Dy(E e τ σ, K e τ σ) and u,F validate one of the two cases in the definition of Sub constraint solutions: In the first case, uσ = t e τ σ and uσ Lσ F σ w e τ σ since u L F w e τ (by iteration over u following the definition of ). Moreover, we have F σ ⊆ Dy(E e τ σ, K e τ σ), which leads to t e τ σ ∈ Dy d (E e τ σ ∪ {w e τ σ}, K e τ σ).

Proposition 9 .

 9 Rule 15 is complete. Proof. Let σ ∈ |[ t ∈ Sub(w, E, E, K) ]| e τ and W = |[ (t = w) ∨ (t ∈ Sub d (w, E, E, K)) ]| e τ . We show that either σ ∈ |[ (t = w) ]| e τ if w = {v} b and b ∈ K or σ ∈ W otherwise. We know that ∃u, ∃F, L such that u L F w e τ , K e τ σ ∩ F σ = ∅, F σ ⊆ Dy(E e τ σ, K e τ σ) and the two cases of the semantics of the Sub. We distinguish two cases depending whether (w = {v} b and b ∈ K) or not: • (w = {v} b and b ∈ K). By definition of < , we have w e τ ∈ L and b e ∈ F , However, K e τ σ ∩ F σ = ∅.

eτ

  or u = w e τ . In the last case, we have uσ = w e τ σ. However, uσ = t e τ σ. Then, w e τ σ = t e τ σ which leads to σ ∈ |[ (t = w) ]| e τ . Thus, for both cases, σ ∈ W . -The second case is the same for the semantics of Sub or Sub d . Therefore σ ∈ W since σ ∈ |[ t ∈ Sub d (w, E, E, K) ]| e τ . Thus Rule 15 is complete. Proposition 10. Rule 15 is correct. Proof. There are two cases whether (w = {v} b and b ∈ K) or not: • Suppose (w = {v} b and b ∈ K). Let σ ∈ |[ (t = w) ]| e τ . Then, w e τ σ = t e τ σ. Let u = w e τ . We have u ∅ ∅ w e τ , ∅ ⊆ Dy(E e τ σ, ∅) and uσ = w e τ σ = t e τ σ. Thus, σ ∈ |[ (t ∈ Sub(w, E, E, K)) ]| e τ . • Suppose (w = {v} b or b /

eτ.

  By definition of Sub d (the same as Sub with the difference that u < L F w e τ if uσ = t e τ σ) and since if u < L F w e τ then we have u L F w e τ , then σ ∈ |[ (t ∈ Sub(w, E, E, K)) ]| e τ . Thus Rule 15 is correct. Proposition 11. Rule 16 is correct and complete.

Lemma 10 .

 10 |[ mpair(k, u) = mpair(l, w) ]| e τ = |[ ∀k u = wδ l,k ]| e τ

eτ

  since u e τ σ = v e τ σ. Also, correctness and completeness of Rule 27 is similar as Rule 26.Proposition 19. Rules 28, 29 and 30 are correct and complete.

  Proposition 21. Rule 32 is correct and complete.Proof. Correctness of Rule 32 is trivial, so we focus on completeness.Let σ ∈ |[ A ∈ F orge c (E, K) ∧ t ∈ Sub d (A, E ′ , E, K) ]| e τ .Let u, F be such that u L F A and F σ ⊆ Dy(E ′ e σ, K e σ).

•

  Proposition 23. Rule 34 is correct and complete.Proof. We first focus on completeness, i.e. assume that σ ∈ |[ X m ∈ F orge c (E ′ , K) ]| e τ , and assume we have M( -→ X ) defined as in Rule 34. We denote by Rhs the right-hand side of Rule 34. Then we have two cases : Either ∃o = 1..p ∃n ko s.t. σ ∈ |[ X m = u o δ o ]| e τ ′ with τ ′ = τ.[k ′ o ← n ko ]. Then, we have u o e δ o τ ′ σ = X m τ ′ σ which leads to u o e δ o τ ′ σ ∈ Dy c (E ′ e σ, K e σ) and thus, σ ∈ |[ Rhs ]| e τ ; • Or there exists no such o, i.e. ∀o = 1..p, ∀n ko , σ / ∈ |[ X m = u o δ o ]| e τ ′ with τ ′ = τ.[k ′ o ← n ko ] i.e. u o e δ o τ ′ σ = X m τ ′ σ,and thus σ ∈ o=1..p ∀k ′ o X m = u o δ o e τ . Then, σ ∈ |[ Rhs ]| e τ ; Second, for the correctness let Rhs be the right-hand side of Rule 34, and assume M( -→ X ) defined as in the rule. Assume also that σ ∈ |[ Rhs ]| e τ because the second part of Rhs is validated (otherwise, the proposition is trivial). It means that ∃o = 1..p, ∃n ko s.t. u o e δ o τ ′ ∈ Dy c (E ′ e σ, K e σ) andX m τ ′ σ = u o e δ o τ ′ σ with τ ′ = τ.[k ′ o ← n ko ]. It follows that X m τ σ ∈ Dy c (E ′ e σ, K e σ) since X m τ = X m τ ′ .Proposition 24. Rule 35 is correct and complete. Proof. Correctness of Rule 35 is trivial. For completeness, assume that σ ∈ |[ X m = v ]| e τ , i.e. X m τ σ = v e τ σ, and M( -→ X ) according to the definitions of Rule 35. Let us write F = (∀Q∃R B 1 ∨ .. ∨ B s ) the whole formula in which Rule 35 is used, and assume that σ ∈ |[ F ]|

  Then, we have u o e δ o τ ′ σ = v e τ ′ σ which leads to σ ∈ |[ Rhs ]| e τ ; • Or there exists no such o, i.e. ∀o = 1..p, ∀n ko , σ / ∈ |[ X m = u o δ o ]| e τ ′ with τ ′ = τ.[k ′ o ← n ko ] i.e. u o e δ o τ ′ σ = X m τ ′ σ, and thus σ ∈ o=1..p ∀k ′ o X m = u o δ o e τ

  satisfied. Rule 35 generates a new equality constraint (u o δ o = v). Suppose that ∃Z k ∈ X I and c j ∈ C I s.t and either Z k m u o δ o and c j m v, or Z k m v and c j m u o δ o . In the first case, i.e. Z k m u o δ o and c j m v, according to Invariant 6 applied to the master constraint (X o = u o ) taking into account δ o , we have k = m.

Figure 8 .

 8 Figure 8.2 details the dependency between the different propositions and invariants.

  ) = [ k, t + E + |E| , k, t + w + |E| + 1 ], where k = st -#K and w ∈ E and therefore w < E . Moreover, Rule 9 do not change the other parameters of the weight of B. Then, B decreases. For Rule 10, pre(R 10) = k, 1 + t 1 + .. + t m + E + |E| where k = st-#K. Moreover, post(R 10) = [ k, t i + E + |E| + 1 ] ti< t1..tm . Then, pre(R 10) > post(R 10) . Besides, Rule 10 do not change the other parameters of the weight of B. Then, B decreases. We show in a similar way as Rule 10 that for Rule 11, B decreases. For Rule 12, pre(R 12) > post(R 12) . Indeed, pre(R 12) = k, 2 + t + E + |E| and post(R 12) = k, 1 + t + E + |E| , where k = st -#K. Moreover, Rule 12 do not change the other parameters of the weight of B. Then, B decreases. We show in a similar way as Rule 13 that for Rule 12, B decreases. For Rule 15, we have pre(R 15) = k, 1 + t + u + |E| and two cases for post(R 15): either post(R 15) = k, t + u or post(R 15) = [ k, t + u , k, t + u + |E| ]. In both cases, pre(R 15) > post(R 15) . Besides, since this rule do not change the other parameters of the weight of B. Then, B decreases.

For

  Rule 23, first, pre(R 23) = k, 2 + u 1 + .. + u m + w 1 + .. + w m . Second, post(R 23) = [ k, u i + w i ] i=1..m where k = st-#K. Then pre(R 23) > post(R 23) and since the other parameters of the weight of B do not change, B decreases.

  this rule do not change the other parameters of the weight of B. Then, B decreases. Rule 33 adds a new final constraint to the block treated B which decreases N cEF -F c B . Then, B decreases. Rule 34 either adds a negative constraint to the bloc treated B or adds a final constraint to B. In both cases, B decreases. In a similar way, Rule 35 decreases B .

  u) ⊆ {q} , we prove two more generic properties by iteration: Claim 4. ∀u ∈ P att(F ), ∀τ , let d be (one of ) the minimal derivation proving σ

  DY c (Eσ ′ , K e τ σ ′ ), and thus d holds the same properties. Therefore, there exists a (valid) derivation d ′ obtained from d as described above, starting from E ′′ σ, with goal σ(uτ ), and with the same structure as d i.e. finishing by a composition rule. Moreover, E ′′ \E contains only terms that that can be forged with (non-redundant) derivations finishing by a composition rule, too. Therefore, it follows that σ(X m τ ) ∈ DY c (Eσ, K e τ σ), thus contradicting σ(X m τ ) / ∈ DY c (Eσ, K e τ σ). Consequently, the hypothesis was false, i.e.σ ′ (X m τ ) / ∈ DY c (Eσ ′ , K e τ σ ′ ) and thus, σ ′ ∈ |[ ctr ]| e τ .Since there are no other kind of constraint in a normalized constraint system, this proves the lemma, i.e. σ ′ ∈ |[ F ′′ ]| e ∅ . Moreover, we remark that naturally, if σ ′ ∈ |[ F ′′ ]| e ∅ then σ ′ ∈ |[ F ′ ]| e ∅

  e. : Lemma 14. If e > e max and σ ∈ |[ F ′′ ]| e ∅ , then ∃σ ′ ∈ |[ F ′′ ]| e-1 ∅ .

  ′ ∈ |[ B 1 ∨ .. ∨ B p ]| e τ ′ . However, ∃i ∈ {1..p} such that σ ∈ |[ B i ]| e τ , thus ∀ctr ∈ B i , σ ∈ |[ ctr ]| e τ .As usual, we have different cases depending on ctr :• If ctr = (X = u) sm or ctr = (X ∈ F orge c (E, K)), then σ ′ ∈ |[ ctr ]| e τ ′ since σ ′ (X) = σ(X); • If ctr = (X m = u) , then : -If τ (m) = s ′ and V ar X I (u) = {j} with τ (j) = s ′ , then σ ′ (X m τ ′ ) = γ(σ(X m τ )) = γ(σ(uτ )) = σ ′ (uτ ′ )since any indexed variable in u must have m as index, and ∀ -→ Y , σ ′ (Y m τ ′ ) = γ(σ(Y m τ )) since τ (m) = s ′ ; This includes j = m;

-

  ′ ∈ |[ ctr ]| e τ ′ ; • If ctr = (∀k X m = u), then : -If τ (m) = s ′ , then ∀v ∈ {1..e}, σ ′ (X m τ ′ ) = γ(σ(X m τ )) = γ(σ(uτ [k ← v])), and thus ∀v ∈ {1..e -1}, σ ′ (X m τ ′ ) = σ ′ (uτ ′ [k ← v]); If τ (m) = s ′ , then as above ∀v ∈ {1..e}, σ(X s ′ ) = σ(X m τ ) = σ(uτ [k ← v]). However, X s and X s ′ share the same patterns, and for both of them this is the minimal one w.r.t ⊳. Thus, u is not the pattern of X s , i.e. ∀v ∈ {1..e}, σ(X s ) = σ(uτ[k ← v]). It follows that ∀v ∈ {1..e -1}, σ ′ (X m τ ′ ) = σ ′ (uτ ′ [k ← v]), i.e. σ ′ ∈ |[ ctr ]| e τ ′ .

  ′ ) and σ ′ ∈ |[ ctr ]| e τ ′ .Since these are the only constraints available in F ′′ , it follows that, as expected,σ ′ ∈ |[ B i ]| e τ ′ . Therefore, for any τ ′ Q from Q to {1..e -1}, we could find τ ′ ⊇ τ ′ Q from Q ∪ R to {1..e -1} such that σ ′ ∈ |[ B i ]| e τ ′ , thus proving that σ ′ ∈ |[ F ′′ ]| e-1∅ . This ends the proof of the lemma.

  This claim shows naturally by iteration that |[ F ′′ ]| e ∅ has a solution with e > e max if and only if |[ F ′′ ]| emax ∅ has a solution. And since for any e, |[ F ′′ ]| e ∅ has a solution if and only if |[ F ]| e ∅ has a solution, this proves the property.

  ∈ F orge c (E 1 , ∅) ∧ (E i = e) m ) ∨ ((L = mpair(t, l, {e} p )) sm ∧ (E i = e) m ) ∨((L = l, {e} p ) sm ∧ (E i = e) m ) ∨ ((L = l) sm ∧ (E i = e) m ) ∨((L = {e} p ) sm ∧ (E i = e) m ) ∨ ((L = l) sm ∧ (E j = e) m ))

  have L(X) ⊂ E. We only focus on rules treating Sub constraints. Rule 15 transforms a constraint t ∈ Sub(u, E, E, K) into a constraint t ∈ Sub d (u, E, E, K) without modifying neither u nor E. Then, Invariant 3 remains satisfied. In Rule 16, since the invariant is satisfied for t 1 , . . . , t m and E, then it remains satisfied for a subterm of t 1 , . . . , t m : t i and E. The same reasoning is valid for Rules 17, 18 and 19. Rules 20 and 32 eliminate the whole block, then, the invariant remains valid. Rule 32 eliminates the whole block. Then, Invariant 3 is satisfied. In Rule 31, we get a Sub constraint t ∈ Sub(w, E ′ , E, K) where w is given by the constraint X = w which belongs to E. However, by construction of E, L(w) ⊂ E ′ . Finally, for Rule 33, we reason similarly to Rule 31.

  Moreover, since t i < ∅ t 1 , .., t m , then t i e τ <

	such that u L F t i	e τ <	t1,..,tm	e τ
	and K	e			t1,..,tm ∅	e τ	t 1 , .., t m	e τ . Then, u < L∪{ t1,..,tm F	e τ }	t 1 , .., t m	e τ

Then ∃i = 1 . . . m. ∅ t 1 , .., t m e τ since u < L F t 1 , .., t m e τ . Thus, σ ∈ W . Let σ ∈ W . Let i = 1 . . . m such that σ ∈ |[ (t ∈ Sub(t i , E, E, K)) ]| e τ . Then, ∃u, ∃F, L such that u L F t i e τ , K e τ σ ∩ F σ = ∅, F σ ⊆ Dy(E e τ σ, K e τ σ)

and the two possibilities for u (the two cases of the semantics of Sub).

  which satisfies the invariant. Only Rule 31 generatse a Sub d constraint: (t ∈ Sub d

  show in a similar way as Rule 17 that for Rule 18, S decreases. For Rule 19, first, pre(R 19) = k, 2 + t + uδ + |E| where k = st -#K. Second, post(R 19) = k, 1 + t + uδ + |E| . Then, pre(R 19) > post(R 19) . Since this rule do not change the other parameters of the weight of B. Then, B decreases.

RR n°6712

Chridi & Turuani & Rusinowitch

We extend this definition to sets of terms by: |E| = Σ t∈E |t| for E ⊂ T . Now, we can define the weight for terms, then, for elementary constraints and finally for constraint blocks and constraint system.

Definition 38 (Weight of a term t). Let p be the size of the protocol, i.e. the sum of sizes of messages. We define the weight of a term t denoted by t as follows:

We extend this definition to sets of terms in the following way:

Definition 39 (Weight of an elementary constraint). Let st be the number of the protocol subterms. We define the weight of an elementary constraint ctr denoted by ctr as follows:

Before defining the weight of a constraint block, we first prove this proposition:

Proposition 33. The number of application of Rule 26 is bounded.

Proof. Rule 26 is applied once for each pair of constraints of the form X i = u and X i = v (thanks to Hyp26). However, according to Theorem 3, the set of indexes generated by our inference system is bounded. Then, the number of pairs of constraints for the same variable X i is bounded. Thus, the number of application of Rule 26 is bounded.

Definition 40 (Weight of a constraint block). We recall that, according to Theorem 3, the set of indexes generated by our inference system is bounded. Then, let N a be the maximum number of application of Rule 26 (See Proposition 33, this number is bounded). Let N cE be the maximum number of Equality constraints of the form X = u where X ∈ X , N cEF be the maximum number of constraints of the form X = u or X ∈ F orge c (E, K) where X ∈ X ∪ X I and N cN be the maximum number of Negative constraints of type F orge or equality.

Consider a constraint block: B = ctr 1 ∧ ..ctr l . We denote by F c B the number of final constraints in B, N c B the number of of negative constraints in B, Sc B the number of submaster constraints in B, M Ec B the number of master equality constraints in B, M F c B the number of master constraints in B of the type F orge, Ec B the number of equality constraints of the form X = u (X ∈ X ∪ X I ) in B and N R B the number of application of Rule 26. We denote also the lexicographic order by and the multiset by []. We define the weight of B as follows:

If we try to normalize the last step step 5 leads to :

The interleaving between F ( mpair(z, (S z ) z ), s ′ ) ∈ Sub d (S ′ , E 5 , E, ∅) with each block obtained above leads to ⊥ since in each block, the submaster constraint for S ′ is S ′ = s ′ . In the same way, the interleaving between F ( mpair(z, (S z ) z ), s ′ ) ∈ Sub d ((S o2 ) o2 , E 5 , E, ∅) and the master constraint for S o in each block leads to ⊥ since the "value" of S o is a constant s o . Thus, we conclude that an execution of Asokan-Ginzboorg with a single session is secure against a secrecy attack.

Second Scenario: Asokan-Ginzboorg with Two Parallel Sessions

Consider two parallel sessions. In the two following specifications (A, i, j) denotes the step i of the participant A in the session j. (L, , 1) (resp (L, , 2)) denotes the leader of the first session (resp second session) and (S, , 1) (resp (S, , 2)) denotes the similator of the first session (resp second session). The specification of the first session is given below:

(L, 1, 1) Init ⇒ mpair(t, l, {e} p ) (S, 1, 1) mpair(i, L, {E i } p ) ⇒ mpair(j, ( a j , ({ r j , s j } (Ej ) j ) j ) j ) (L, 2, 1) mpair(k, ( a k ,

∧witness((L, , 1), (S, , 1), f s, mpair(o, (S o ) o ), s ′ ) (S, 2, 1) mpair(q, ({ mpair(u, (s u ) u ), S ′ } (rq) q ) q ) ⇒ mpair(w, a w , { (s w ) w , H( mpair(y, (s y ) y ), S ′ ) } F ( mpair(y,(sy) y ),S ′ ) ) ∧request((S, , 1), (L, , 1), f s, mpair(u, (s u ) u ), S ′ ) (L, 3, 1) mpair(x, a x , { (S x ) x , H( mpair(z, (S z ) z ), s ′ ) } F ( mpair(z,(Sz) z ),s ′ ) ) ⇒ End

The specification of the second session is given below:

w , H( mpair(y, (s ′ y ) y ), S" ) } F ( mpair(y,(s ′ y ) y ),S" ) ) ∧request((S, , 2), (L, , 2), s s, mpair(u, (s ′ u ) u ), S" ) (L, 3, 2) mpair(x, a x , { (S ′ x ) x , H( mpair(z, (S ′ z ) z ), s" ) } F ( mpair(z,(S ′ z ) z ),s" ) ) ⇒ End Steps are ordered as follow: W L = 1, 2, 3, W S = 1, 2 with 1 < W L 2, 2 < W L 3, and 1 < W S 2 for each session. We consider the following execution: (L, 1, 1), (L, 1, 2), (S, 1, 1), (S, 1, 2), (L, 2, 1), (L, 2, 2), (S, 2, 1), (S, 2, 2), (L, 3, 1), (S, 3, 2). The property we want to check is the authentication of the group key in each session which is defined in the two specification below