Véronique Cortier

Antoine Dallon

Stéphanie Delaune

A small bound on the number of sessions for security protocols

Bounding the number of sessions is a long-standing problem in the context of security protocols. It is well known that even simple properties like secrecy are undecidable when an unbounded number of sessions is considered. Yet, attacks on existing protocols only require a few sessions.

In this paper, we propose a sound algorithm that computes a sufficient set of scenarios that need to be considered to detect an attack. Our approach can be applied for both reachability and equivalence properties, for protocols with standard primitives that are type-compliant (unifiable messages have the same type). Moreover, when equivalence properties are considered, else branches are disallowed, and protocols are supposed to be simple (an attacker knows from which role and session a message comes from). Since this class remains undecidable, our algorithm may return an infinite set. However, our experiments show that on most basic protocols of the literature, our algorithm computes a small number of sessions (a dozen). As a consequence, tools for a bounded number of sessions like DeepSec can then be used to conclude that a protocol is secure for an unbounded number of sessions.

I. INTRODUCTION

For several decades, decision procedures have been developed for the automatic analysis of security protocols. Various security properties can be considered. Secrecy and authentication are usually formalized as reachability properties, while anonymity, untraceability, and other privacy properties are expressed as equivalence properties. Such properties are known to be undecidable in general [START_REF] Durgin | Undecidability of bounded security protocols[END_REF]. However, if a bounded number of sessions is considered, then reachability properties as well as trace equivalence are decidable, see e.g. [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NP-complete[END_REF], [START_REF] Millen | Constraint solving for bounded-process cryptographic protocol analysis[END_REF], [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF], [START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF], [START_REF] Dawson | Automating open bisimulation checking for the spi-calculus[END_REF].

In practice, attacks exploit only a few sessions. Let us first clarify what we call sessions. A protocol defines several roles (client, server, certificate authority, etc.). Each role is a program that may be run several times, each run corresponds to a session of the role. So the number of sessions will be the total number of programs that can be run (once). Written in terms of processes, this corresponds to the total number of processes in parallel, with no replication. Up to our knowledge, extreme cases are when 5-6 sessions are needed for an attack. For example, the Triple Handshakes Attack on TLS [START_REF] Bhargavan | Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS[END_REF] requires an honest client C and an honest server S that each runs 3 subprograms, yielding 6 sessions (or even less, depending on how programs are divided). The traceability attack on electronic passports [START_REF] Chothia | A traceability attack against e-passports[END_REF] requires one honest run between the reader and the passport and then a replay against a passport, thus 3 sessions. Hence a tempting heuristic is to conclude that either an attack can be found within a few sessions, or the protocol is secure. Unfortunately, there is absolutely no formal guarantee that this is indeed the case. It is possible to construct protocols for which an arbitrary number of sessions can be needed for attacks. Hence, bounding the number of sessions is a longstanding problem. The goal is to identify criteria, achieved in practice, such that if there is an attack, then there is an attack within an a priori bounded number of sessions.

Related work. Several results have studied this question.

• Sybille Fröschle [START_REF] Fröschle | Leakiness is decidable for well-founded protocols?[END_REF] proposes a decidability result for the "leakiness" property, that guarantees that all data are either public or secret. This excludes protocols with temporary secrets. [START_REF] Fröschle | Leakiness is decidable for well-founded protocols?[END_REF] holds for typed protocols: an agent expecting a nonce or a key cannot accept a ciphertext. The considered primitives are encryption and concatenation only.

• In [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF], [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], the notion of typed protocols is relaxed to consider type-compliance, that intuitively requires that unifiable messages have the same type. While protocol agents may receive arbitrary messages, type-compliance ensures the existence of a well-typed witness when an attack exists. In [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF], [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], the notion of dependency graph is introduced with the aim to characterize how actions depend from the other ones. For protocols with an acyclic dependency graph, the number of sessions can be bounded and hence reachability and equivalence properties are decidable. This result assumes protocols to be simple (actions can be precisely identified) and else branches are disallowed. • [START_REF] Osualdo | Deciding secrecy of security protocols for an unbounded number of sessions: The case of depthbounded processes[END_REF] defines the notion of "depth-boundedness" that restricts intuitively the number of nested encryptions. It is shown that secrecy is decidable for depth-bounded protocols. As for [START_REF] Fröschle | Leakiness is decidable for well-founded protocols?[END_REF], this does not cover equivalence properties. [START_REF] Osualdo | Decidable inductive invariants for verification of cryptographic protocols with unbounded sessions[END_REF] generalizes the notion of depth-boundedness to support a wider variety of cryptographic primitives. All these results provide new decidability results: they identify classes of protocols for which secrecy (and some-times equivalence) is decidable, for an unbounded number of sessions and fresh nonces. In passing, they bound the number of sessions. However, they do not provide explicit bounds or the bounds are not practical. For example, [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF] gives a bound of 10 19 sessions for the simple Denning-Sacco protocol and the bound is even larger for more complex protocols.

Many other works have studied the analysis of security protocols in a symbolic setting, aiming at reducing the search space. Some approaches show that it is sufficient to consider typed attack traces, where messages follow some format [START_REF] Arapinis | Bounding messages for free in security protocols[END_REF], [START_REF] Chrétien | Typing messages for free in security protocols: the case of equivalence properties[END_REF], [START_REF] Hess | A typing result for stateful protocols[END_REF]. Other results reason on the origination of messages (see e.g. [START_REF] Guttman | Shapes: Surveying crypto protocol runs[END_REF]).

Contribution. Our main contribution is to show that, under assumptions similar to [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], it is possible to efficiently bound the number of sessions. Our result holds both for reachability and equivalence properties and for a generic class of equational theories that encompasses standard cryptographic primitives (symmetric and asymmetric encryption, signatures, hash). We consider the class of protocols that are type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. Type-compliance can often be achieved by simply adding a tag, that indicates at which step the message has been created. Such a tagging scheme is usually considered as a good practice since it avoids attacks and is shown to ensure type-compliance for protocols with symmetric encryption and pairing [START_REF] Chrétien | Typing messages for free in security protocols: the case of equivalence properties[END_REF]. Moreover, when equivalence properties are considered, else branches are disallowed, and protocols must also be simple, i.e. an attacker can identify from which participant and which session a message originates from.

Under these assumptions, we provide an algorithm that explores the actions of a protocol and computes a bound on the number of sessions needed for an attack. It is important to note that our assumptions do not yield a decidable class, hence our algorithm can also return that no bound could be found. On the other hand, we do compute a bound for any protocol with an acyclic graph as defined in [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], hence our algorithm covers the decidable class introduced in [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF]. Compared to [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], the major difference is that we provide a small, usable, bound where [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF] is impractical. We also provide a bound in slightly more cases but these additional cases cover contrived examples only. Actually, instead of just a bound on the number of sessions, our algorithm provides a list of scenarios that need to be considered. Each scenario corresponds to a precise number of replications of each role of the protocol, possibly truncated. For example, maybe an attack needs two replications of role B and only twice the two first steps of role A. This more precise information can be helpful when running tools for the protocol analysis.

We prove that our algorithm is correct: if there is an attack, then there is an attack covered by one of the returned scenario. The proof involves two main steps. First, we use the fact that if there is an attack, then there is a well-typed attack, that is, an attack where all the messages comply with the expected format in the protocol. This result heavily relies on a previous typing result [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], extended to else branches for reachability properties. Then, in a second step, we need to show that our algorithm explores all possible scenarios, that is, we show that a well-typed attack of minimal size (minimal length and small attacker steps) is necessarily covered by at least one of our scenarios.

Implementation. We have implemented our procedure in a tool HowMany that (i) first checks whether our assumptions, in particular type-compliance, are satisfied, (ii) then recursively computes, for each action of the protocol, how this action can be reached from other steps of the protocol. This yields the set of scenarios that need to be considered. If a loop is detected, then no bound can be found. We experimented our tool on several protocols of the literature. As already noticed in [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], they all satisfy our assumptions, possibly after tagging messages. For most protocols, HowMany can find a bound of size 3 to 55 sessions, in the worst case. For example, HowMany computes a bound of 3 sessions only for the Denning-Sacco protocol, to be compared with the previous 10 19 bound. Even in the case where 55 sessions may be needed (for the Kao-Chow protocol), HowMany actually provides finer grain information: one can either consider one scenario with 55 sessions in parallel or, instead, 385 different scenarios of at most 29 sessions each, and for which the analysis can be done independently.

Discussion. Although they do not come with termination guarantees, tools like ProVerif [START_REF] Blanchet | An automatic security protocol verifier based on resolution theorem proving (invited tutorial)[END_REF] or Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF], dedicated to the analysis of protocols for an unbounded number of sessions, can already analyze efficiently the protocols considered in our experiments. Hence, our first and main contribution is theoretical: we hope to contribute to a better understanding on the interplay between sessions and attacks. In particular, our results show that yes, for standard protocols, it is possible to find a reasonable bound on the number of sessions. Moreover, our approach allows to extend the scope of existing tools developed for a bounded number of sessions such as Avispa [START_REF] Armando | The AVISPA Tool for the automated validation of internet security protocols and applications[END_REF], Maude-NPA [START_REF] Escobar | A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties[END_REF], DeepSec [START_REF] Cheval | Deepsec: deciding equivalence properties in security protocols theory and practice[END_REF], or SAT-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF]. Despite the state-explosion issue due to the intrinsic complexity (NPcomplete) of the bounded case, a major improvement has been seen in the number of sessions that can be covered by these tools. For example, DeepSec can analyze up to 10-50 sessions for standard protocols of the literature. SAT-Equiv can even analyze up to 60-400 sessions but covers a much smaller fragment of protocols. Hence HowMany can be used as a small add-on to these tools to conclude to the security of an unbounded number of sessions when HowMany successfully computes a bound. In our experiments, SAT-Equiv was able to prove security for an unbounded number of sessions in all cases, while DeepSec faces a time out (set to 24h) in about 15% of the cases and succeeds otherwise.

All files related to the implementation and case studies are available as supplementary material in [START_REF] Cortier | A small bound on the number of sessions for security protocols[END_REF].

II. MODEL

A. Messages

As usual, messages are modeled with a term algebra. Private data, such as private keys, private randomness and nonces, are represented by a set of names N . Security protocols may also use public data, like tags, or error messages, that are represented by (public) constants of Σ 0 . Constants also model other data known from the attacker, like corrupted private keys, nonces generated by the attacker or her keys. For technical reasons (related to the typing result [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]), the attacker is also given non-atomic constants. We consider two sorts, atom and bitstring. Any name in N is of the sort atom, while Σ 0 is split as Σ 0 = Σ atom 0 Σ bitstring 0 , where the constants in Σ atom 0 are of sort atom and the constants in Σ bitstring 0 are of sort bitstring. We assume an infinite number of names in N , constants in Σ atom 0 and constants in Σ bitstring 0 , such that protocol agents can always generate fresh nonces, and the attacker can always generate new keys and create new messages. Messages (or an unknown part of them) expected by a party of a protocol are represented through variables in X . Another set W of variables is used to refer to messages learnt by the attacker. Most often, those messages result from an output. Typically, variables in X are denoted x, y, z, whereas variables in W are denoted w 1 , w 2 , . . . . Names in N are denoted n, m and k or sk when they are keys, while constants are denoted a, b, c. We refer to variables, names and constants through the generic term of data, while the word atomic or atom shall be used only for data of sort atom.

We also need to model cryptographic operations, like encryption, decryption, mac, hash function,... These operations are represented by function symbols. A signature Σ is a set of function symbols with their arity. We distinguish between three types of symbols. We consider constructor symbols like encryption, in Σ c , destructor symbols, like decryption, in Σ d , and test symbols, in Σ test , i.e. Σ = Σ c Σ d Σ test . The sets Σ d and Σ test do not contain constant symbols, i.e. function symbols of arity 0. Given a signature Σ and a set of data D, the set of terms built from Σ and D is denoted T (Σ, D). Constructor terms on D are terms in T (Σ c , D). We denote vars(u) the set of variables that occur in a term u. A term is ground if it contains no variable. Given a substitution σ, we denote dom(σ) its domain, img(σ) its image, and uσ its application to a term u. The positions of a term are defined as usual. Given a term t, the function symbol occurring at position in t is denoted root(t), and we denote St(t) the set of the subterms of t. Two terms u 1 and u 2 are unifiable when there exists a substitution σ such that u 1 σ = u 2 σ. The most general unifier between u 1 and u 2 is denoted mgu(u 1 , u 2 ).

Any constructor f comes with its sort, i.e.

f : (s 1 × . . . × s n ) → s 0
where n is the arity of f, s 0 = bitstring, and s i ∈ {atom, bitstring} for 1 ≤ i ≤ n. Given a constructor term t ∈ T (Σ c , D), p is an atomic position of t if it corresponds to a position where an atom is expected, i.e., p = p .i, t| p = f(t 1 , . . . , t n ), with f ∈ Σ c : (s 1 × . . . × s n ) → s 0 and s i = atom. We say that a constructor term t is well-sorted if t| p ∈ N X Σ atom 0 for any atomic position p of t, i.e. any subterm is of the right sort.

Example 1. Public-key encryption, signature, and pair can be modeled by considering

Σ ex = Σ ex c ∪ Σ ex d ∪ Σ ex test with: • Σ ex c = {aenc, pk, sign, vk, ok, }; • Σ ex d = {adec, getmsg, proj 1 , proj 2 }; • Σ ex test = {check}.
The symbols aenc and adec (both of arity 2) represent resp. asymmetric encryption and decryption. The symbol pk (arity 1) is the key function: pk(sk) is the public key associated to the private key sk. Signatures are modeled with the symbol sign (arity 2). We assume that the content of a signature can be extracted (symbol getmsg of arity 1). Its validity can be checked with check (arity 2). The symbol vk (arity 1) is again a key function which modeled the verification key associated to a signing key. Pairing is modeled using (arity 2), and projection functions are denoted proj 1 and proj 2 (both of arity 1). The sort of our constructors are as follows: aenc : bitstring × bitstring → bitstring pk : atom → bitstring sign : bitstring × atom → bitstring vk : atom → bitstring , : bitstring × bitstring → bitstring Consider k, ska ∈ N and ekc ∈ Σ 0 (all of sort atom), the term u 0 = aenc(sign(k, ska), pk(ekc)) is a constructor term that represents an encryption (by the public key associated to the private key ekc) of a signature. This private key is modeled using a public constant, and is therefore known to the attacker. The atomic position of u 0 are p 1 = 2.1 and p 2 = 1.2, and since ska and ekc are indeed atoms, u 0 is well-sorted.

Our main result relies on a typing result established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], and thus we need to consider a similar setting. In particular, in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], a notion of shape is introduced, whose purpose is to describe the expected pattern of a message. For example, if asymmetric encryption is represented by aenc(m, pk(k)) then it should not be applied to other keys, e.g. vk(k). Formally, to each constructor function symbol f, we associate a linear term f(u 1 , . . . , u n ) ∈ T (Σ c , X ) denoted sh f which is called the shape of f. Shapes have to be compatible, i.e. for any f(t 1 , . . . , t n ) occurring in a shape, we have that sh f = f(t 1 , . . . , t n ). A term is well-shaped if it complies with the shapes, that is, any subterm of t, heading with a constructor symbol f is an instance of the shape of f. More formally, a constructor term t ∈ T (Σ c , Σ 0 ∪ X ) is well-shaped if for any t ∈ St(t) such that root(t ) = f, we have that t = sh f σ for some substitution σ. Given D ⊆ N ∪ Σ 0 ∪ X , we denote T 0 (Σ c , D) the subset of constructor terms built over D that are well-shaped and well-sorted. Terms in T 0 (Σ c , N ∪ Σ 0 ) are called messages.

Example 2. Continuing Example 1, the shapes associated to each constructor symbol are as follows:

aenc : sh aenc = aenc(x 1 , pk(x 2 )) pk : sh pk = pk(x 2 ) sign : sh sign = sign(x 1 , x 2 ) vk : sh vk = vk(x 1 ) : sh = x 1 , x 2
It is easy to see that these shapes are compatible. The term u 0 = aenc(sign(k, ska), pk(ekc)) is well-sorted and wellshaped thus in T 0 (Σ c , N ∪ Σ 0 ), whereas aenc(k, ekc) is wellsorted but not well-shaped.

To model the effect of destructors, we use a set R of rewriting rules built from Σ.

Example 3. The properties of the primitives given in Example 1 are reflected through the following rewriting rules:

adec(aenc(x, pk(y)), y) → x getmsg(sign(x, y)) → x check(sign(x, y), vk(y)) → ok proj 1 ( x, y ) → x proj 2 ( x, y ) → y
Given a set R of rewriting rules, a term u can be rewritten in v using R if there is a position p in u, and a rewriting rule g(t 1 , ..., t n ) → t in R such that u| p = g(t 1 , . . . , t n )θ for some substitution θ, and v = u[tθ] p , i.e. u in which the subterm at position p has been replaced by tθ. Moreover, we assume that t 1 θ, . . . , t n θ as well as tθ are messages, in particular they do not contain destructor symbols. We consider sets of rewriting rules that yield convergent rewriting systems. As usual, we denote → * the reflexive-transitive closure of →, and u↓ the normal form of a term u.

An attacker builds his own messages by applying public function symbols to terms he already knows and that are available through variables in W. Formally, a computation done by the attacker is a recipe, i.e. a term in T (Σ, W Σ 0 ). Example 4. The set of rewriting rules given in Example 3 yields a convergent rewriting system. We have that:

v = getmsg(adec(u 0 , ekc)) → getmsg(sign(k, ska)) → k
Therefore, we have that v↓ = k. The term R 0 = getmsg(adec(w 1 , ekc)) with w 1 ∈ W is a recipe.

B. Protocols

Our process algebra is inspired from the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF]. Our setting allows both pattern matching on the input construct and explicit filtering using the match construct.

We assume an infinite set Ch of channels and an infinite set L of labels. We consider processes built using the following grammar:

P, P 1 , . . . , P j , Q := 0 null process | in α (c, u).P input | out α (c, u).P output | new n.P name generation | P | Q parallel | i : P phase | !P replication | new c .out(c, c ).P channel generation | match x with filtering (u 1 → P 1 | . . . | u j → P j ) where α ∈ L, u, u 1 , . . . , u k ∈ T 0 (Σ c , Σ 0 N X ), c, c ∈ Ch, n ∈ N ,
and i, j ∈ N. Given a process P , we denote fv (P ) the set of its free variables, i.e. those not bound by an input, nor by a filtering in a match construct. A protocol is a process with no free variable and with distinct labels.

Example 5. Consider the following process P :

P = in(c, x).match x with f(y) → out(c, ok) | y → out(c, error)
This process represents an agent who is waiting for a message.

If the message received is of the form f(y) (for some value of y), the constant ok will be sent. Otherwise, an error message will be emitted. The match construct is used to model conditional branching. We have that fv (P ) = ∅. Indeed, the variable x is bound by the input construct, and y (resp. y ) is bound by the filtering f(y) (resp. y ) in the match construct.

The construct in α (c, u) and out α (c, u) are the usual input and output actions, except that they are now decorated with labels α. These labels have no impact on the semantics of processes. They are used to refer to a precise action of a process and will be necessary to reason on the number of sessions needed for an attack. The construct new n.P generates a new name n and proceeds as P . The parallel composition of two processes P and Q is built as P | Q. We consider phases in our setting. They are useful to model protocols that have several phases, for example some general setup followed by the actual start of the main part of the protocol. A process i : P may only react at phase i and can be discarded once the phase is strictly greater than i.

As usual, replication of processes is denoted !P . We consider a special construction to introduce a fresh public channel: new c .out(c, c ).P generates a new channel c and immediately publishes it on c. This is to allow for the generation of public channels while private channels are not considered in our setting. Finally, match x with (u 1 → P 1 | . . . | u j → P j ) will try to unify the content of x with u 1 , . . . , u j (in order) and will proceed as P i as soon as one successful unification is found for some u i . Example 6. We consider a variant of the signature-based Denning-Sacco protocol as given in [START_REF] Blanchet | Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire[END_REF]. The protocol aims at ensuring the secrecy of the key k freshly generated by agent A and sent to B relying on signature and asymmetric encryption. Informally, we have that:

A → B : aenc(sign(k, ska), pk(ekb))
As shown in [START_REF] Blanchet | Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire[END_REF], this variant is vulnerable to an attack. Indeed, a dishonest agent C may reuse a signature sign(k c , ska) sent by A to him to fool an honest agent B (see Example 7 for more details).

The two roles of A and B are represented by the following processes:

P A = new k.out α1 (c, aenc(sign(k, ska), pk(ekb))) P B = in β1 (c, aenc(sign(x, ska), pk(ekb)))
where k, ska, ekb ∈ N and x ∈ X . Then, the whole protocol is modeled by the parallel composition of these (replicated) processes, with an extra process P K that reveals public keys to the attacker, i.e.

P DS = 1 :!P A | 1 :!P B | 0 : P K with P K = out γ1 (c, pk(ekb)).out γ2 (c, vk(ska)).
Of course, we may want to consider a richer scenario involving a dishonest agent c. In this case, we can consider in addition the following processes (here ekc ∈ Σ 0 ):

P A = new k .out α 1 (c, aenc(sign(k , ska), pk(ekc))) P B = in β 1 (c, aenc(sign(x , ska), pk(ekc)))
yielding to the protocol

P DS = P DS | 1 :!P A | 1 :!P B .
Note that ekc is known to the attacker since ekc ∈ Σ 0 .

The operational semantics of a process is defined as a relation over configurations. A configuration is a tuple (P; φ; σ; i), with i ∈ N, such that:

• P is a multiset of processes.

• φ is a frame, that is a substitution with a (finite) domain dom(φ) ⊂ W, and such that img(φ) only contains messages. Intuitively, φ corresponds to messages sent on the (public) network. • σ is a substitution such that fv (P) ⊆ dom(σ), and img(σ) only contains messages. It represents the current instantiation of protocol variables. By abuse of notation, given a protocol P , we will write P for the configuration ({P }, ∅, ∅, 0).

The relation -

→ defining the operational semantics is described in Figure 1 and follows the intended semantics. Note that a process with a match is blocked if no possible match is found in the list of u i . For the sake of conciseness, we sometimes write P P instead of {P } P.

An action (or a step) is said visible when it is different from τ . The relation 1 ... n ----→ between configurations (where 1 . . . n is a sequence of actions) is defined as the transitive closure of -→. Given a sequence of visible actions tr and two configurations K and K , we write K tr = = ⇒ K when there exists a sequence 1 . . . n such that K 1... n ----→ K and tr is obtained from 1 . . . n by erasing all occurrences of τ .

Given a configuration K = (P; φ; σ; i), we denote trace(K) the set of traces defined as:

trace(K) = {(tr, φ ) | K tr = = ⇒ (P ; φ ; σ ; i )
for some configuration (P ; φ ; σ ; i )}.

Note that, by definition of trace(K), we have that trφ↓ only contains messages for any (tr, φ) ∈ trace(K).

Example 7. Continuing Example 6, we have that (tr 0 , φ 0 ) ∈ trace(P DS ) where: tr 0 = out γ1 (c, w 0 ).phase 1.out α 1 (c, w 1 ).in β1 (c, R 1 ); φ 0 = {w 0 pk(ekb), w 1 aenc(sign(k, ska), pk(ekc))}

The recipe R 1 def = aenc(adec(w 1 , ekc), w 0 ) means that the attacker decrypts the message he received (from A) and he re-encrypts it with the public-key of B. Note that R 1 φ 0 ↓ = aenc(sign(k, ska), pk(ekb)), and thus B will accept this message thinking that the key k is a secret shared with him and the agent A. However, we have that R 0 φ 0 ↓ = k meaning that this key is actually known by the attacker (with R 0 = getmsg(adec(w 1 , ekc))).

C. Equivalence

Some security properties are expressed as equivalence properties where the attacker wins if she can distinguish between two scenarios. For example, Alice is traceable if an attacker can distinguish the case where Alice is taking part several times in a protocol from the case where different users are involved.

First, we say that an attacker can distinguish between two sequences of messages φ 1 and φ 2 if she can construct a test that holds in φ 1 and not φ 2 . She can also distinguish if some evaluation (e.g. a decryption) succeeds in φ 1 and not φ 2 . Definition 1. Two frames φ 1 and φ 2 are in static inclusion, written φ 1 s φ 2 , when dom(φ 1 ) = dom(φ 2 ), and:

• for any recipe R, we have that Rφ 1 ↓ is a message implies that Rφ 2 ↓ is a message; and • for any recipes R, R such that Rφ 1 ↓, R φ 1 ↓ are messages, we have that:

Rφ 1 ↓ = R φ 1 ↓ implies Rφ 2 ↓ = R φ 2 ↓. They are in static equivalence, written φ 1 ∼ s φ 2 , if φ 1 s φ 2 and φ 2 s φ 1 .
Then we can define trace equivalence between configurations K and K : any trace of a configuration K should have a corresponding trace in K with the same visible actions and such that their frames are in static equivalence. Definition 2. A configuration K is trace included in a configuration K , written K t K , if for every (tr, φ) ∈ trace(K), there exists (tr , φ ) ∈ trace(K ) such that tr = L tr (where = L is equality without taking into account labels from L), and φ s φ . They are in trace equivalence, written

K ≈ t K , if K t K and K t K.
This notion of trace equivalence slightly differs from the original one (given e.g. in [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF]), where the frames are required IN (i : in α (c, u).P P; φ; σ; i)

in α (c,R)
-----→ (i : P P; φ; σ σ 0 ; i) where R is a recipe such that Rφ↓ is a message, and Rφ↓ = (uσ)σ 0 for σ 0 with dom(σ 0 ) = vars(uσ).

OUT

(i : out α (c, u).P P; φ; σ; i)

out α (c,w)
------→ (i : P P; φ {w uσ}; σ; i) with w a fresh variable from W, and uσ is a message. to be in static equivalence φ ∼ s φ instead of static inclusion φ s φ . Actually, these two notions of equivalence coincide for determinate protocols [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF], and in particular for the class of simple protocols that will be introduced later on (see Definition 9) when considering the case of equivalence.

NEW

III. ASSUMPTIONS

We consider two main assumptions in our setting. First, we cannot consider arbitrary primitives. Instead, we propose a generalization of decryption-encryption rules that allows us to consider all standard primitives and a few additional ones. One advantage of this generalization is not really its expressivity (we are not much more general than the standard primitives) but its flexibility. For example, encryption can be randomized, several encryption or hash functions can be considered, etc. We could consider a (long) list of decryption-like rules but this would render the proofs unnecessarily cumbersome, with dozen of cases to be considered. Our second main assumption is the fact that protocols must be type-compliant, which intuitively guarantees that each two encrypted messages of the protocol that can be unified have the same type.

A. Shaped rewriting systems

Our main result relies on the fact that, thanks to [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we can consider only some particular form of traces (well-typed). Hence we need to consider a similar setting. We consider rewriting rules that apply a symbol in Σ d Σ test on top of constructor terms that are linear, well-sorted, and well-shaped. Moreover, we strictly control the non-linearity of the rules, and we assume the standard subterm property, as recalled below. More formally, our set R is divided into two parts, i.e. R = R d R test , and for each symbol g ∈ Σ d Σ test , we assume there is exactly one rule of the form l -→ r such that:

1) l = g(t 1 , . . . , t n ) where each t i is either a variable or equal to sh root(ti) up to a bijective renaming of variables; 2) either l is a linear term, or there is a unique variable x with several occurrences in l and:

• l = g(f(t • x occurs exactly once in t jx 1 , in atomic position, and does not occur in the other t j 1 for j = j x . We denote l g -→ r g the rewriting rule in R associated to the symbol g ∈ Σ d Σ test . Then, we assume that for any g ∈ Σ test , the associated rule l g → r g is such that r g ∈ T 0 (Σ c , ∅). In this case, l g → r g is a rule of R test . When g ∈ Σ d , we assume that the associated rule g(t 1 , . . . , t n ) → r g is such that r g is a direct and strict subterm of t 1 , i.e. t 1 = f(t 1 1 , . . . , t k 1 ) with f ∈ Σ c , and r g = t j 1 for some j ∈ {1, . . . k}. In this case, l g → r g is a rule of R d .

Lastly, we assume the existence of at least one non linear rule in R. This last assumption is needed for the typing result stated and proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], and is satisfied as soon as a rewriting rule modeling e.g. symmetric (or asymmetric) encryption is present in R. A rewriting system satisfying our conditions is called a shaped rewriting system. In what follows, we only consider shaped rewriting systems.

All standard primitives such as symmetric and asymmetric encryption, signatures, mac, hash, can be modeled as shaped rewriting systems. We can also consider a few more primitives.

Example 8. The rewriting system given in Example 3 is a shaped rewriting system. We can also consider encryption schemes where 1 out of n keys suffices to decrypt, with rewriting rules of the form: adec 1 (aenc(y, pk(x), pk(x )), x) → y adec 2 (aenc(y, pk(x ), pk(x)), x) → y However, adding a rewriting rule: samekey(aenc(x 1 , pk(x)), aenc(x 2 , pk(x))) → ok allowing one to check whether two ciphertexts have been produced relying on the same key does not satisfy our requirements since the left-hand-side is not linear, and aenc(x 2 , pk(x)) is not of the form f(x).

B. Type compliance

Intuitively, types allow us to specify the expected structure of a message. Definition 3. A (structure-preserving) typing system is a pair (∆ init , δ) where ∆ init is a set of elements called initial types, and δ is a function mapping data in Σ 0 N X to types τ generated using the following grammar:

τ, τ 1 , . . . , τ n = τ 0 | f(τ 1 , . . . , τ n ) with f ∈ Σ c and τ 0 ∈ ∆ init
Then, δ is extended to constructor terms as follows:

δ(f(t 1 , . . . , t n )) = f(δ(t 1 ), . . . , δ(t n )) with f ∈ Σ c .
Example 9. We consider the typing system (∆ DS , δ DS ) generated from the set ∆ DS = {τ ska , τ ekb , τ ekc , τ k } of initial types, and such that:

• δ DS (k) = δ DS (k ) = δ DS (x) = δ DS (x ) = τ k , and • δ DS (xx) = τ xx for xx ∈ {ska, ekb, ekc}.
Consider a configuration K and a typing system (∆ init , δ), an execution K tr = = ⇒ (P; φ; σ; i) is well-typed if σ is a welltyped substitution, i.e. every variable of its domain has the same type as its image.

In [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], protocols are defined to be type-compliant if any two unifiable encrypted subterms are of the same type. "Encrypted" means any term headed by a constructor symbol that cannot be opened freely, such as encryption. Conversely, some constructors are transparent in the sense that they can be opened without any extra information, such as pairs, tuples, or lists. Formally, a constructor symbol f of arity n is transparent if there exists a term

f(R f 1 , . . . , R f n ) ∈ T (Σ, ) such that for any term t ∈ T 0 (Σ, Σ 0 N X ) such that root(t) = f, we have that f(R f 1 , . . . , R f n ){ → t}↓ = t.
We write ESt(t) for the set of encrypted subterms of t, i.e. the set of subterms that are not headed by a transparent function.

ESt(t) = {u ∈ St(t) | u is of the form f(u 1 , . . . , u n )
and f is not transparent} Since replicated processes can produce several messages with a similar structure, we define the k-unfolding unfold k (P ) of the replicated process P as a finite version of P such that each replication has been unfolded exactly k times. For instance, we have that unfold 1 (P ) is the process obtained from P by simply removing the ! operator whereas unfold 0 (P ) is the process obtained from P by removing parts of the process under a replication.

Example 10. The encrypted subterms occurring in the 2unfolding of P DS are:

• pk(ekb), vk(ska);

• sign(k i , ska), aenc(sign(k i , ska), pk(ekb));

• sign(x i , ska), aenc(sign(x i , ska), pk(ekb));

• sign(k i , ska), aenc(sign(k i , ska), pk(ekc));

• sign(x i , ska), aenc(sign(x i , ska), pk(ekc)) where indices i ∈ {1, 2} are used to distinguish names/variables coming from different unfoldings. They are given the same type: Compared to [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we have generalized the definition to the match construct (see item 2 -Definition 4). We give here an example showing that it was necessary to obtain a typing result for reachability.

δ DS (k 1 ) = δ DS (k 2 ),
Example 12. Consider the process P introduced in Example 5. Obviously, it is possible to reach out(c, ok) with the trace tr = in(c, f(a)). Assume δ(x) = δ(y) = δ(y ) = τ 0 ∈ ∆ init . As there is only one encrypted subterm in P , the typing system satisfies the first item of Definition 4. However, tr is not well-typed for P . More importantly, any trace that allows to reach out(c, ok) must unify x and f(y). Thus, it will only be well-typed if δ(x) = δ(f(y)). For a (structurepreserving) typing system, it implies that δ(x) = f(δ(y)). In particular, there is no well-typed attack trace for the typing system we have defined. Note that the condition δ(x) = f(δ(y)) is guaranteed by the second item of Definition 4.

Extending the result of [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we obtain that for any typecompliant protocol, we can restrict our attention to well-typed traces. We define tr obtained from tr by replacing any action in α (c, R) by in α (c, _), any out α (c, w) by out α (c, _), while phase i and out(c, c ) actions are left unchanged. Intuitively, we only keep the type of actions, and the channels. Of course, this theorem will have more effect when the type system is as precise as possible, for example distinguishing between several classes of constants or stating that some variables can be typed as atomic constants.

Example 13. The execution corresponding to the trace given in Example 7 is well-typed. Indeed, the resulting substitution is σ = {x → k} and we have that δ DS (x) = δ DS (k) = τ k .

IV. COMPUTATION OF A TIGHT BOUND

Our main contribution is a procedure that, given a protocol, computes a (tight) over-approximation of the number of sessions that need to be considered to find an attack. More precisely, to each trace corresponds a multiset of labels. Our procedure computes (an over-approximation of) the possible multisets of actions that can occur in minimal attack traces.

A. Dependencies

Message dependencies. One key step of our procedure consists in inspecting, for each term output by the protocol, what are the type of the terms that can be deduced from it. More formally, given a type τ , we compute a set of tuples (τ , p)#S. Intuitively, each tuple (τ , p)#S indicates that a term of type τ may be deduced, at position p, from terms of type τ , provided the attacker knows some terms whose types are contained in S (as multiset inclusion). Definition 5. Given a type τ , we define ρ(τ ) to be ρ(τ, , ∅) where ρ(τ, p, S) is recursively defined as the set {(τ, p)#S} ∪ E where E = ∅ when τ is an initial type. Otherwise, τ = f(τ 1 , . . . , τ k ) and E is defined as:

E = g( 1 , . . . , n) → rg ∈ R d θ = mgu( 1 , f(τ 1 , . . . , τ k )) i 0 ∈ {1, . . . , k} is such that rg = 1 | i 0 ρ(τ i0 , p.i 0 , S { 2 θ, . . . , n θ}) Example 14. Let τ msg def = aenc(sign(τ k , τ ska ), pk(τ ekb )).
First the element (τ msg , )#∅ is in ρ(τ msg ), and we are left to compute ρ(sign(τ k , τ ska ), 1, {τ ekb }) since the rule adec(aenc(y, pk(x)), x) → y is the only one that can be applied to extract a message from a ciphertext. Then, we have that:

ρ(sign(τ k , τ ska ), 1, {τ ekb }) = (sign(τ k , τ ska ), 1)#{τ ekb } (τ k , 1.1)#{τ ekb }
This last element represents the fact that a message of type τ k can be extracted from a signature at position 1 using the rule getmsg(sign(x, y)) → x, and this does not require additional knowledge. The set ρ(τ msg ) contains 3 elements.

In order to compute a tighter bound, we will sometimes skip the computation of some dependencies, for some marked position. A marked position of a protocol P w.r.t. a typing system (∆ 0 , δ 0 ) is a pair (α, p) where out α (c, u) is an output action occurring in P , and p is a position of the term δ 0 (u).

For the rest of this section, we will assume given a set of marked position and we will explain later on how to soundly mark positions. By default, the reader may simply assume that no position is marked.

Sequential dependencies. Another, simpler, type of dependencies is sequential dependency: some action may occur only if the previous steps of the same process have been executed. We let pred(α) be the first visible action that occurs before the action labeled by α. More formally, a process P can be seen as a tree whose nodes are actions in(c, u), out(c, u), new n, |, etc, and vertices are there to indicate the continuation of the process. For instance, a node labeled with the action "match x with" will have j sons representing the j branches of the match construct. Then, given an action of the form in α (c, u) (resp. out α (c, u )), we denote pred(α) its first predecessor that corresponds to an input/output of a message (not a channel name). We have that pred(α) = ⊥ if there is no such predecessor in the tree.

We also introduce the notion of cv-alien types, that are types that do not appear as type of the constants and variables in the protocol under study. Definition 6. Consider a protocol P and a typing system (∆ 0 , δ 0 ). A type τ h is cv-alien for P if τ h is a type alien w.r.t. the constants and variables of P , that is, τ h = δ 0 (a) for any constant/variable a ∈ Σ 0 ∪ X occurring in P .

We say that a term is cv-alien-free if it does not contain any constant from Σ 0 of cv-alien type. This notion is lifted to traces, frames, configurations and executions as expected.

We will show that the attacker may only use cv-alien-free terms since it is not useful to introduce constants whose type does not appear in the protocol.

Example 15. Continuing our running example, we have that τ ska and τ ekb are cv-alien type. Actually, we have that any type but τ k and τ ekc is a cv-alien type. Regarding τ k , this comes from the fact that δ DS (x) = δ DS (x ) = τ k (see Example 9).

B. Main procedure

We assume given a protocol P type-compliant w.r.t. a typing system. We propose a procedure, denoted dep, that, given a label α occurring in P , computes dep(α), a set of multisets of labels. Each multiset of labels represents the sessions that may be needed to reach label α.

We first introduce the operation ⊗ to compute some kind of "cartesian product" on two sets of multisets. The result is not a pair of multisets but instead we merge the two components of each pair to obtain a multiset. Formally,

{a 1 , . . . , a k } ⊗ {b 1 , . . . , b l } def = a 1 b 1 , a 1 b 2 , . . . , a 1 b l , a 2 b 1 , a 2 b 2 , . . . , a 2 b l , . . . a k b 1 , a k b 2 , . . . , a k b l
where a 1 , . . . , a k , b 1 , . . . , b l are multisets of labels. Note that given a multiset set S, we have that: S ⊗ {∅} = {∅} ⊗ S = S, and S ⊗ ∅ = ∅ ⊗ S = ∅.

We define inductively a family of functions dep i on labels and types as follows: dep i (⊥) = {∅}; and If α is an output, i > 0,

• dep 0 (α) = ∅, • dep i (α) = {{α}} ⊗ dep i-1 (pred(α)). If α is an input of type τ , i > 0, • dep 0 (α) = ∅, • dep i (α) = {{α}} ⊗ dep i-1 (pred(α)) ⊗ dep i-1 (τ ).
The definition of dep i is extended as expected to multisets:

dep i (S) = α∈S dep i (α)
When dep i is applied to a type, we need a family of auxiliary functions S i out , inductively defined as follows, i ≥ 0:

S i out (τ ) = out α (c, u) occurring in P (τ, p)#{τ 1 , . . . , τn} ∈ ρ(δ 0 (u)) (α, p) not marked dep i (α) ⊗ dep i (τ 1 ) ⊗ . . . ⊗ dep i (τ n )
Intuitively, S i out (τ ) explores all the possibilities to extract a term of type τ . Then, we define dep 0 (τ ) = ∅ when τ is a cv-alien type; dep 0 (τ ) = {∅} otherwise. The reason is that if there is an attack trace, then there is one which is well-typed and which does not involve any constant of cv-alien type. Thus, there is no need to consider this case when exploring all the possibilities to build a term having such a type, and thus dep 0 (τ ) = ∅. Otherwise, we have to consider the case where the term of type τ is a constant known by the attacker, and this does not lead to further dependencies, thus dep 0 (τ ) = {∅}. Finally, for any i > 0, we let:

• dep i (τ ) = dep 0 (τ ) ∪ S i-1 out (τ ) for an initial type τ , • dep i (τ ) = dep 0 (τ ) ∪ S i-1 out (τ ) ∪ {∅}⊗dep i-1 (τ 1 ) ⊗ . . . ⊗ dep i-1 (τ k ) for a non-initial type τ of the form f(τ 1 , . . . , τ k ).
Note that a set dep i (α) can only increase with i. More formally, for any type τ and any label α, we have that:

dep i (τ ) ⊆ dep i+1 (τ ) dep i (α) ⊆ dep i+1 (α) S i out (τ ) ⊆ S i+1 out (τ ) since A 1 ⊗ • • • ⊗ A n ⊆ B 1 ⊗ • • • ⊗ B n when A i ⊆ B i .
Hence we define dep(τ ) (resp. S out (τ )) as the limit of the

dep i (τ ) (resp. S i out (τ )), that is, dep(τ ) = ∞ i=0 dep i (τ ) S out (τ ) = ∞ i=0 S i out (τ )
We see the interest of cv-alien type in the definition of dep 0 : dep 0 (τ ) = ∅ if τ is a cv-alien type. Hence, if no term of type τ can be extracted from the outputs of the protocol (i.e.

β 2 {β 2 , β 1 , α 1 } β 1 {β 1 , α 1 } τ k {∅} α 1 {α 1 } τ ekb ∅ τ msg {α 1 } α 1 {α 1 } α 1 sign(τ k , τ ska ) ∅ . . . pk(τ ekb ) τ ekb ∅ . . . τ k τ ska ∅ τ k τ ekb α 1 τ k τ ska α 1 τ ekb τ msg pk(τ ekb ) sign(τ k , τ ska ) τ dep 0 (τ ) = ∅ pruning of the graph x Set dep(x) = {Set} . . .
does not need to be computed S out (τ ) = ∅), we have that dep(τ ) = ∅, and simplifications arise since S ⊗ ∅ = ∅.

Example 16. Continuing our running example, we may want to consider the secrecy of the key k as received by B. To encode this property, we add an action at the end of process P B , that checks whether the key can transit in clear on the network, yielding process

P + B = in β1 (c, aenc(sign(x, ska), pk(ekb))).in β2 (c, x).
We modify P DS accordingly (with P + B ), yielding P + DS . Note that, even if P + DS does not involve the dishonest agent c, the protocol features replication, and thus the question of deciding whether an action labelled β 2 is reachable is not trivial.

In order to compute dep(β 2 ), we first remark that τ ska and τ ekb are cv-alien types, as explained in Example 15. Therefore, since S out (τ ska ) = S out (τ ekb ) = ∅, we have that dep(τ ska ) = dep(τ ekb ) = ∅. Then, we have that S out (sign(τ k , τ ska )) = ∅, and thus dep(sign(τ k , τ ska )) = ∅.

We now follow the dep algorithm step by step, as illustrated in Figure 2.

dep(β 2 ) = {{β 2 }} ⊗ dep(β 1 ) ⊗ dep(τ k ) = {{β 2 , β 1 }} ⊗ dep(τ msg ) ⊗ dep(τ k )
Actually S out (τ k ) = ∅, and thus dep(τ k ) = {∅}. We have seen in Example 15 that τ k is not of cv-alien type, and thus dep 0 (τ k ) = {∅}.

We have also that:

dep(τ msg ) = {∅} ⊗ dep(sign(τ k , τ ska )) ⊗ dep(pk(τ ekb )) ∪ S out (τ msg ).
To conclude, it is sufficient to see that:

• S out (τ msg ) = dep(α 1 ) = {{α 1 }}; and • dep(sign(τ k , τ ska )) = {∅} ⊗ dep(τ k ) ⊗ dep(τ ska ) ∪ S out (sign(τ k , τ ska )) = ∅ Hence, finally, we have that dep(β 2 ) = {{β 2 , β 1 , α 1 }}.

C. Correctness of the bound

We denote Label(tr) the multiset of labels (from L) occurring in tr. The algorithm dep(α) computes an upper bound of the actions/labels that need to be considered to reach some action labeled α.

Theorem 2. Let P be a protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ). Let α be a label of P and assume (tr. , φ) ∈ trace(P ) for some tr, , φ such that Label( ) = {α}. Then there exists tr , , φ , and A ∈ dep(α) such that (tr . , φ ) ∈ trace(P ) with Label( ) = {α}; and Label(tr . ) ⊆ A.

This theorem shows that it is sufficient to consider traces with labels in dep(α) to access an action labeled by α. Secrecy can easily be encoded with such an accessibility property, introducing some special action α 0 that can be reached only if the secret is known to the attacker.

Example 17. Continuing our running example, and thanks to Theorem 2, it is sufficient to consider one instance of P A , and one instance of P + B when looking for an attack on the secrecy in P + DS . In particular, no need to unfold replications more than once, and no need to consider process P K .

Let us now consider a modified process P DS , that now includes a session between the server, the initiator, and a dishonest agent c. After applying dep recursively, we get:

dep(β 2 ) = {β 2 , β 1 , α 1 , α 1 }, {β 2 , β 1 , α 1 , α 1 , γ 1 }
In other words, to analyze secrecy of k in this richer scenario, we can restrict ourselves to two simple scenarios. The first one requires only one instance of the roles P + B , P A and P A . The second one involves half of the process P K (only the first action can be triggered), one instance of P + B , and two instances of P A (initiator role played by a with the dishonest agent c).

We prove our Theorem 2 in two main steps.

(i) We first rely on type-compliance and the typing result given in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], extended here to deal with processes with match construct. As stated in Theorem 1, this allows us to restrict our attention to well-typed traces. Actually, we further show that traces can be assumed to be cv-alien-free, and to only involve simple recipes (some constructors are applied on top of recipes that are almost destructor-only) 1 . Lastly, we show that each message of such traces can be computed as soon as possible (asap). Intuitively, recipes should refer to the earliest occurrence of a message. More formally, we have that: Definition 7. Let φ be a frame with a total ordering < on dom(φ), and m be a message such that Rφ↓ = m. We say that R is an asap recipe of m if R is minimal among the recipes {R | R φ↓ = m} for the following measure: for any two recipes R and R , we have R < R if, and only if, vars # (R) < mul vars # (R ), where vars # (R) denotes the multiset of variables occurring in R, and < mul is the multiset extension of <.

(ii) Second, our procedure dep is used to consider all the possible ways of deducing a term of a certain type τ (or reaching a specific action α). This is done by considering all the sequential dependencies, and all the message dependencies. For this, we heavily rely on the fact that our witness only involves simple recipes. We thus know the shape of these recipes, and compliance with types also imposes us some restrictions that are exploited in our procedure.

D. Marking criteria

We mainly consider two marking criteria. First, we mark any position p occurring in an output out(c, u) such that δ 0 (u)| p is a public type. Definition 8. Given a protocol P and a typing system (∆ 0 , δ 0 ). A type τ p is public if for any name n occurring in P , we have that δ 0 (n) ∈ St(τ p ).

Actually, a public type is a type for which all the terms of this type are known by the attacker from the beginning (in a well-typed cv-alien-free execution). Thus, we can safely ignore those terms when computing dep.

Second, we also mark any position p occurring in an output out(c, u) when an occurrence of u| p already occurs in the process (before the output under consideration) and it was less protected. The intuition is that an attacker who will try to deduce each term as soon as possible, will never use this output out(c, u) to extract u| p . We illustrate this second criterion through an example.

Example 18. Consider the following process:

P = in α (c, senc( req, x , k)).out β (c, senc( rep, x , k)).
We can safely mark (β, 1.2) corresponding to the term x which is protected by k.

We formally show that our two marking criteria are sound, namely that we can safely ignore marked positions in dep. In other words, we show that Theorem 2 still holds with these two criteria.

V. EXTENSION TO EQUIVALENCE PROPERTIES

We can also bound the number of sessions in case of equivalence properties. We however consider a more restricted class of protocols, without the match construct (hence without else branches) and with a simple structure: each process emits on a distinct channel. This corresponds to the case, common in practice, where sessions can be identified, for example with session identifiers. More formally, we consider the class of simple protocols. Definition 9. A simple protocol P is a protocol of the form

!new c 1 .out(c 1 , c 1 ).B 1 | . . . | !new c m .out(c m , c m ).B m | B m+1 | . . . | B m+n
where the channel names c 1 , . . . , c n , c n+1 , . . . , c n+m are pairwise distinct, and each B i with 1 ≤ i ≤ m (resp. m < i ≤ m + n) is a ground process on channel c i (resp. c i ) built using the following grammar:

B := 0 | in α (c i , u).B | out α (c i , u).B | new n.B | j : B where u ∈ T 0 (Σ c , Σ 0 ∪ N ∪ X ), α ∈ L, and j ∈ N.
Note that our definition of simple protocol assumes a fresh, distinct channel for each session. In particular, two sessions of the same process will use different channels. Hence our model does not assume that the attacker can identify an agent across different sessions, this will depend on the protocol. Therefore simple processes can still be used to model anonymity or unlinkability properties.

A. Our procedure

The computation of dep for reachability properties no longer suffices for equivalence properties. Indeed, the attacker not only may need several sessions to reach some interesting step of the protocol, but may also need to deduce auxiliary information to mount a test that allows her to distinguish between two protocols. Hence, the computation of dep will now also depend on the rewriting rules in R test .

Formally, we keep our definition of dep on labels and types and we extend it to protocols. We define:

dep(P ) = {∅} ∪ S reach (P ) ∪ S test (P ) ∪ S check (P )
where S reach , S test , and S check are given in Figure 3.

Intuitively, dep(P ) explores the different cases where trace inclusion of P in some protocol Q may fail. The first case is when some action can be reached in P but not in Q. The corresponding sets of labels are computed by S reach (P ). A second case is when some equality holds in P and not in Q. We rely here on a precise characterization of static inclusion, where we show that it is possible to consider tests of the form M = N where N only contains destructors. This case is explored by S test (P ) where the possible types of a destructoronly recipe is computed by S + out . Finally, the last relevant case is when a term can be reduced in P (according to the equational theory) and not in Q. This corresponds to S check . Note that S out coincides with S + out except that marked positions (α, p) are no longer ignored when p = . The reason is that even if a position is marked and hence the corresponding term could be obtained earlier, it may be necessary to consider the position in order to check its equality with an earlier term. In other words, when looking for a test M = N , we can no longer consider that both M , and N are asap recipes. However, we have shown that we can safely consider that at least one of them is asap, whereas the other one can be assumed to be subterm asap, meaning that all its direct subterms are asap (but not necessarily the term itself).

S reach (P ) = α∈Label(P ) dep(α) S test (P ) = τ ∈St(δ0(P )) dep(τ ) ⊗ S + out (τ ) S check (P ) = τ ∈ St(δ 0 (P )) = g(t 1 , . . . , tn) → r θ = mgu(t 1 , τ ) S out (τ ) ⊗ dep(t 2 θ) ⊗ . . . ⊗ dep(t n θ) S + out (τ ) = out α (c, u) occurring in P (τ, p)#{τ 1 , . . . , τn} ∈ ρ(δ 0 (u)) (α, p) not marked or p = dep(α) ⊗ dep(τ 1 ) ⊗ . . . ⊗ dep(τ n )

B. Correctness

When searching for an attack against an equivalence property specified as P ≈ t Q, it is sufficient to consider sessions as prescribed by dep(P ) and dep(Q).

Theorem 3. Let P be a simple protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ). Let Q be another simple protocol such that P t Q. There exists a trace (tr, φ) ∈ trace(P ) witnessing this non-inclusion such that Label(tr) ⊆ A for some A ∈ dep(P ).

The proof of this theorem follows the same lines as the one for reachability. Additional difficulties arise due to the fact that we also need to provide a bound regarding static inclusion. Considering an equality test R 1 = R 2 that witnesses non static inclusion, we show that R 1 and R 2 can be chosen with a specific shape that allows one to precisely characterize the actions that may be involved in such a test.

VI. EXPERIMENTS

We have implemented our procedure into a tool HowMany, that we run on several protocols of the literature, studying both reachability and equivalence properties. When the tool returns a list of (finite) scenarios, we can then use two existing tools, SAT-Equiv and DeepSec, developed for a bounded number of sessions, and directly conclude that security holds in the unbounded case (unless the tools find an attack). The specifications of all protocols, as well as the files to reproduce the experiments, can be found in [START_REF] Cortier | A small bound on the number of sessions for security protocols[END_REF].

A. HowMany

The function dep may return infinite sets, hence does not directly yield a terminating algorithm. Therefore, we define dep , a terminating algorithm that returns the same result than dep whenever it is finite, and returns ⊥ otherwise.

The main idea is to first decide whether a given type τ (resp. label α) is such that dep(τ ) = ∅. In this case, since ∅ is an absorbing element w.r.t. ⊗, we may conclude that, e.g.

dep(τ ) ⊗ dep(τ 1 ) ⊗ . . . ⊗ dep(τ n ) = ∅
without computing dep(τ 1 ), . . . , dep(τ n ). Once empty elements have been identified, relations can be simplified, and it is relatively easy to identify a loop and to return ⊥ to indicate that one of the resulting multisets will be infinite.

The algorithm dep has been implemented in the tool HowMany. It will either return ⊥ or a set of multisets of labels. Each element in the set corresponds to a finite scenario that needs to be analyzed. Thanks to Theorems 2 and 3, we can conclude that the protocol is secure if it is secure in all the scenarios identified by HowMany. A multiset of labels tells us the maximal number of sessions that may be involved in a minimal attack. Actually, it is even more precise than that since our algorithm gives us a list of scenarios, and each scenario corresponds to a precise number of unfolding of a replication, possibly truncated.

B. Security properties

We have considered three types of security properties, depending on the protocol under study.

The first one is weak secrecy (WSEC), a reachability property. We always consider secrecy of the key (sometimes the nonce) as received by the responder. This is done by adding an instruction of the form in α (c, k) at the end of the responder role. Then, we ask for reachability of the label α.

The second one is key privacy (KPRIV). Intuitively, a key k is secure if an attacker cannot learn any information on messages that are encrypted by k. We model this by adding at the end of the responder' role senc(m 1 , k) on the left, and senc(m 2 , k ) on the right, where k is fresh, and m 1 , m 2 are two public constants.

For these two security properties, we consider a process where each role is instantiated (arbitrarily many times) by all possible players among 2 honest agents and a dishonest one.

Lastly, we analyzed some protocols from the e-passport application, and we consider the unlinkability property (UNLINK). This property is modeled relying on phases. In a first phase, the attacker interacts with two passports and two readers possibly many times. In a second phase, the attacker interacts with either one instance of the first passport (and a reader) or the second one. The protocol is linkable if the attacker is able to distinguish between the two cases.

C. Outcome of Howmany

HowMany computes a set of scenarios, and each scenario involves several sessions of the protocol. When more than one scenario is returned, HowMany also computes a unique scenario that over-approximates all the other ones. Indeed, there is trade-off between considering multiple simple scenarios or a unique but more complex one corresponding to the overapproximation of all the simple ones. Depending on the tool and the protocol, one approach may be more efficient than the other, hence we consider both cases (multiple and unique scenarios).

On all the examples mentioned in this section, HowMany concludes in few seconds on a standard laptop but the Kao-Chow example for KPRIV, which takes around 2 min. The detailed outcome of our experiments is displayed in Table I and Table II and we further comment them below. Compared with [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF], this shows a significant improvement. For the simple Denning-Sacco protocol, in the case of reachability, [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF] yields a bound of at least 10 19 and the bound would be even larger in the other cases.

Reachability. The results regarding the weak secrecy property WSEC are reported in the right part of Table I. The table can be read as follows. For instance, for the Yahalom-Paulson protocol, HowMany states that we may either consider 25 scenarios among which the biggest one is made up of 19 sessions in parallel and 35 actions in total; or we can decide to analyze directly the more complex one which features 30 sessions in parallel for a total of 56 actions.

Equivalence. Actually, when analyzing KPRIV, we may restrict our attention to consider one inclusion. Indeed, in case P ≈ t Q, we necessarily have that P t Q since there are more equalities on P side. To study this inclusion, we only need to compute dep(P ). Regarding the property UNLINK, we focus again on one inclusion due to the symmetry of the relation under study. Moreover, we consider a simplified variant of the protocols, without else branches, since else branches are not supported by our approach.

Our experiments show that for all these protocols, a small number of sessions is sufficient, up to 55 sessions in parallel for the Kao-Chow protocol if one wishes to analyze a unique (big) scenario only. The only cases where HowMany cannot conclude are the Yahalom-Lowe protocol and the (flawed) Needham-Schroeder protocol. For several protocols such as Denning-Sacco or Wide-Mouth Frog, we even retrieve that 2-3 sessions are sufficient, which corresponds to a very simple scenario where one honest instance of each role is considered.

D. SAT-Equiv, DeepSec

Even if our first and main contribution is theoretical, our result shows that it is possible to find a reasonable bound on the number of sessions on several protocols of the literature. Actually, thanks to the recent advances of the verification : the tagged version of the protocol has been considered to ensure type-compliance. nb columns: number of scenarios returned by HowMany. "size" columns (white): maximal number of sessions involved in the multiple scenarios, and in parentheses, the number of protocol actions. "size" columns (gray): idem but for the unique, aggregated scenario given by HowMany. mult.: time for the analysis of all the multiple scenarios.

unique: time for the analysis of the unique, aggregated scenario. TO: time out (>24h). tools dedicated to a bounded number of sessions, our approach extends the scope of existing tools such as Avispa [START_REF] Armando | The AVISPA Tool for the automated validation of internet security protocols and applications[END_REF], DeepSec [START_REF] Cheval | Deepsec: deciding equivalence properties in security protocols theory and practice[END_REF], or SAT-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF] to an unbounded number of sessions. We consider two of them, namely DeepSec and SAT-Equiv, based on different verification techniques. We selected them because they are known for their efficiency, they are suitable for the class of protocols we consider in this paper, and they are able to deal with both reachability and equivalence properties.

DeepSec. DeepSec is based on constraint solving. As any other tool based on this approach, it suffers from a combinatorial explosion when the number of sessions increases. To tackle this issue partial-order reductions (POR) techniques that eliminate redundant interleavings have been implemented and provide a significant speedup. This is only possible for the class of determinate processes, but this assumption is actually satisfied by our case studies.

SAT-Equiv. SAT-Equiv proceeds by reduction to planning problem and SAT-formula, and is quite efficient on the specific class of protocols that it handles. This class is similar to the one considered in this paper. This approach is less impacted by the state-space explosion problem when the number of sessions increases.

We used both tools to analyze all the scenarios returned by HowMany. Even if parallelism is available in DeepSec, we do not rely on this feature, and we consider a timeout of 24h. SAT-Equiv concludes on all the scenarios and is more efficient when analyzing the unique, aggregated scenario than all the small ones. Regarding DeepSec, when more than 40 sessions are involved, the tool is not able to conclude within 24h. It is interesting to note that, contrary to SAT-Equiv, DeepSec is more efficient when analyzing many small scenarios rather than the unique aggregated one.

VII. CONCLUSION

We have proposed an algorithm that soundly bounds the number of sessions needed for an attack, both for reachability and equivalence properties. This provides some insights on why, in practice, attacks require only a small number of sessions. Note that dep(P ) may potentially be infinite. In that case, our theorem does not provide any concrete bound but may be of theoretical interest.

In our experiments, we have assumed a finite number of agents (two honest agents and a dishonest one). Agents can soundly be bounded for reachability properties [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF] and equivalence [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] when there is no else branches. Alternatively, an additional process can be considered in the model, that creates agents and keys, and distributes them to the other roles. It then remains to check whether HowMany can still bound the number of sessions in this setting. Further experiments would need to be conducted.

We could extend our approach to deal with correspondence properties, for example simple authentication properties of the form end(x) → start(x). We could indeed exploit our extension of the typing result that preserves a certain number of disequalities. An other interesting direction for future work could be to extend our class of protocols and to consider e.g. private channels. This requires first to extend the underlying typing result but seems to be doable. Regarding reachability properties, our dep algorithm will require some small adaptations. The case of equivalence properties appears to be more difficult since the addition of private channels takes us away from the class of simple protocols.

While HowMany provides a small bound in many cases (smaller than 15 sessions), the bound can be quite big in some cases. We plan to further refine our bound by identifying spurious scenarios, for example exploiting further dependencies in the case of phases. Lastly, there is a trade-off between analyzing many simple scenarios and a big one. Whereas it makes sense to put together simple scenarios when the overlap is important, we should not gather scenarios that are almost disjoint. Providing a clever way to group scenarios could simplify the security analysis.

APPENDIX A TYPING RESULTS

A. Typing result for reachability

In [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], the existence of a well-typed witness for processes which do not feature the match construction is established. This result is stated for processes without replication, and then lifted to configuration which feature replication. The way this result is proved allows one to derive an extra property regarding the shape of the resulting well-typed witness. This result (stated and proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] in a slightly different version as Theorem 3.8) is recalled below. Note that in this version, the protocol can contain new n and new c.out(c, c ) instructions (as it is not hard to add them when there is no replication).

Theorem 4. Let P be a protocol type-compliant w.r.t. (∆ 0 , δ 0 ) which does not feature replication, nor match constructions and S be a set of pairs of terms.

If P tr = = ⇒ (P; φ; σ; i), then there exists a well-typed execution P tr = = ⇒ (P; φ ; σ ; i) w.r.t. such that tr = tr. Moreover, w.l.o.g. we can assume that the substitution σ is such that uσ and vσ are not unifiable for any u = v ∈ S such that uσ and vσ are not unifiable.

Proof. (sketch of proof) The main part of the theorem (without the consideration of the set S) has been proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. Actually, it has been shown that the substitution σ is directly derived from σ as follows: We have that σ = ρ • σ S where:

• σ S = mgu(Γ) and Γ = {(u, v) | u, v ∈
ESt(P ) such that uσ = vσ}; and • ρ is a bijective renaming from variables in dom(σ) dom(mgu(Γ)) to fresh constants (in particular those constants do not occur in S). Moreover, the existence of a substitution λ whose domain is dom(λ) = dom(ρ) and which satisfies λ • σ S = σ is established.

Let u = v ∈ S. We have to establish that, if uσ and vσ are not unifiable, then uσ and vσ are not unifiable either. We proceed by contraposition: we assume that uσ and vσ are unifiable, and we want to prove that uσ and vσ are unifiable too. As uσ and vσ are unifiable, there exists γ such that (uσ )γ = (vσ )γ and since img(σ ) only contains ground terms, we actually have that:

u(σ γ) = v(σ γ).
Since ρ is a bijective renaming and fresh constants in img(ρ) does not occur in u and v, we have that:

u(σ ρ -1 γρ -1 ) = v(σ ρ -1 γρ -1 ).
This allows us to conclude that:

u(σ S γρ -1 ) = v(σ S γρ -1 ).
Then, applying λ, we obtain that:

[u(σ S γρ -1 )]λ = [v(σ S γρ -1 )]λ.
Therefore, we have that:

[(uσ S )λ](γρ -1 λ) = [(vσ S )λ](γρ -1 λ).
This allows us to conclude that uσ and vσ are unifiable. This concludes the proof.

Then, the idea is to show how relying on Theorem 4, we can establish a similar result for protocols which feature replication and match constructions. Proof. (sketch of proof) First, we make the observation that every attack trace is an attack trace against a finite execution. More formally, we have that if there exists an execution of P of length at most , then a similar execution can be done starting from unfold (P ). Conversely, any execution obtained starting from unfold (P ) can be done starting from P itself. Now, we are able to establish our typing result for reachability in presence of replication and match constructions. Assuming we have a trace tr starting from the configuration P , we have that this trace can be performed starting from P = unfold (P ) for some .

Along this execution, we consider all equalities Γ tr match coming from the execution of a match construction, i.e. Γ tr match gathers all the pair (x, u i ) corresponding to an execution of the i th branch of a match construction of the form match x with (u 1 → P 1 | . . . | u j → P j ). Then, we consider σ tr match = mgu(Γ tr match ), and we denote P the process obtained from P by replacing each match instruction match x with(u 1 → P 1 | . . . |u j → P j ) directly by its continuation P i (the one used in the execution trace tr), and we apply the substitution σ tr match . The resulting configuration P does not feature match construction anymore, and we have that ESt(P ) ⊆ ESt(P σ tr match ). Now, Theorem 4 applies on P . First, let us show that type-compliance is satisfied on configuration P . Let u 1 , u 2 ∈ ESt(P ) such that u 1 and u 2 are unifiable. Up to a bijective renaming of names and variables, we have that u 1 , u 2 ∈ ESt(unfold 2 (P )) are two unifiable terms, and thus by definition of type-compliance as stated in Definition 4, we know that δ(u 1 ) = δ(u 2 ). Thus, type-compliance is satisfied by P . Second, for S, we consider the set of all the pairs of terms corresponding to match that did not pass. In other words, for each match instruction match x with (u 1 → P 1 | . . . |u j → P j ) that executes its i th branch in tr, we add (x, u 1 ), . . . , (x, u i-1 ) in S. Theorem 4 gives us the existence of a well-typed execution P tr ==⇒ (P; φ ; σ ; i) such that tr = tr. Moreover, w.l.o.g. we can assume that the substitution σ is such that uσ and vσ are not unifable for any u = v ∈ S such that uσ = vσ were not unifiable.

Therefore, we have that P can execute tr leading to a configuration with subsitution σ tr match σ ∪ σ . Thus we have:

σ = σ tr match σ ∪ σ (1)
Both substitutions being well-typed, we have that σ tr match σ ∪ σ is well-typed too. Then, it is easy to see that this well-typed execution starting from P (a finite version of P ) can be mimicked starting from P . This concludes the proof.

B. Some extra properties

In addition to consider a well-typed witness, we want a witness that involes simple asap recipes, and the witness has also to be cv-alien-free. The first property (simple asap) is easy to establish.

We rely on the notion of forced normal form as introduced in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] and denoted u . This is the normal form obtained when applying rewrite rules as soon as the symbol in Σ d Σ test and the constructor match. Formally, we reuse the definition as stated in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]: Definition 10. Given a rewriting rule g → r g as defined in Section III-A, its associated forced rewriting rule is g → r g where g is obtained from g by keeping only the path to r g in g . Formally, g is defined as follows:

1) g = g(x 1 , . . . , x n ) when g ∈ Σ test ; 2) otherwise denoting p 0 = 1.j the unique position of g such that g | p0 = r g , we have that g is the linear term such that:

• root( g | ) = root( g | ), root( g | 1 ) = root( g | 1 )
; and g | p0 = r g ; • for any other position p of g , we have that g | p is a variable.

Note that the forced rewriting system associated to a rewriting system is well-defined. In particular, the position of r g in g is uniquely defined. In particular, the position of r g in g | 1 is uniquely defined since g | 1 is a linear term and r g contains a variable when g ∈ Σ d . Given a rewriting system R = R des R test , we define R f the set of forced rewriting rules associated to R. A term u can be rewritten to v using R f if there is a position p in u, and a rewriting rule g(t 1 , . . . , t n ) t in R f such that u| p = g(t 1 , . . . , t n )θ for some substitution θ, and v = u[tθ] p . We denote * the reflexive and transitive closure of , and u the normal form of u.

As established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] (in a slightly more general setting), we may restrict our attention to recipes in forced normal form.

Lemma 1. Let φ be a frame and u be a message deducible from φ, i.e. such that Rφ↓ = u for some R. We have that R φ↓ = u.

We say that a recipe R is almost destructor-only when R is in forced normal form and root(R| p ) ∈ Σ d ∪ W for any position p of the form 1 . . .

1 in R. A recipe R is simple when R = C[R 1 , . . . , R n ]
for some context C built using symbols in Σ c ∪Σ 0 , and each R i is almost destructor-only. Note that C can be empty, and thus an almost destructor-only recipe is also a simple recipe. Lemma 2. Let R be a recipe in forced normal form such that root(R) ∈ Σ d ∪ W, and φ be a frame such that Rφ↓ is a message. We have that R is almost destructor-only and R| p φ↓ ∈ St(φ) for any position p of the form 1 . . . 1 in R.

Proof. We show this result by structural induction on R.

Base case: We have that R ∈ W, and we easily conclude.

Induction case:

We have that R = f(R 1 , . . . , R k ) for some f ∈ Σ d , and we know that R 1 , . . . , R k are in forced normal form. Let f → r f be the rule in R associated to f, and f → r f its associated forced rewriting rule. We have that f = f(g(t 1 1 , . . . , t p 1 ), t 2 , . . . , t k ) for some g ∈ Σ c and r f = t j 1 for some j. Since Rφ↓ is a message, we know that root(R 1 φ↓) = g. Assume by contradiction that root(R 1 ) ∈ Σ c , then root(R 1 ) = g. Now, since R is in forced normal form, we know that root(R 1 ) = g. So we deduce that root(R 1 ) ∈ Σ c . Therefore, R 1 is in forced normal form, root(R 1 ) ∈ Σ d ∪ W, R 1 φ↓ is a message. We conclude relying on our induction hypothesis. Lemma 3. Let R be a recipe in forced normal form and φ be a frame such that Rφ↓ is a message. We have that R is a simple recipe.

Proof. We prove this result by structural induction on R. Base case: In case root(R) ∈ Σ d ∪ W, we conclude relying on Lemma 2.

Induction case: We have that either R ∈ Σ 0 or R = f(R 1 , . . . , R k ) for some f ∈ Σ c ∪ Σ test . In case R ∈ Σ 0 ,
we have that R is simple by definition. Otherwise, applying our induction hypothesis on R 1 , . . . , R n , we deduce that R 1 , . . . , R n are simple recipes, and thus R is simple too. It remains the case where f ∈ Σ test . Actually, this case is impossible since R is in forced normal form.

To justify marking, we have to restrict to witnesses relying on asap recipes (see Definition 7). Whenever a message is deducible, we can also find an asap recipe of the message which is also simple. Lemma 4. Let φ be a frame (with a total ordering on dom(φ)) and u be a message deducible from φ, i.e. such that Rφ↓ = u for some R. We have that there exists R a simple asap recipe such that R φ↓ = u.

Proof. We first chose among all the recipes {R | R φ↓ = u}, one that is minimal. Let R 0 be such a recipe, and then we consider R 0 . Thanks to Lemma 1, we have that R 0 is a recipe for u. Thanks to Lemma 3, we have that R 0 is imple. It is also asap since R 1 R 2 implies R 2 ≤ R 1 . This allows us to conclude.

Let Cst(u) be the set of constants from Σ 0 occurring in u. We have the following result. Lemma 5. Let φ be a frame and R be a simple recipe such that Rφ↓ is a message. We have that Cst(R) ⊆ Cst(φ) ∪ Cst(Rφ↓).

Proof. We prove this result by structural induction on R. Base case: R ∈ W ∪ Σ 0 . In such a case, the result trivially holds. Induction case: R = f(R 1 , . . . , R k ) for some f ∈ Σ c ∪ Σ d .

• Case f ∈ Σ c . In such a case, we have that Rφ↓ = f(R 1 φ↓, . . . , R k φ↓), and we easily conclude relying on our induction hypothesis. • Case f ∈ Σ d . In such a case, we have that R = g(R 1 , . . . , R k ), and thanks to Lemma 2, we know that R 1 φ↓ ∈ St(φ). Regarding R 2 , . . . , R k , we have that

Cst(R 2 φ↓) ∪ . . . ∪ Cst(R k φ↓) ⊆ Cst(R 1 φ↓).
Therefore, applying our induction hypothesis on R i that are simple, we have that:

Cst(R) = Cst(R 1 ) ∪ . . . ∪ Cst(R k ) ⊆ Cst(φ) ∪ Cst(R 1 φ↓) ∪ . . . ∪ Cst(R k φ↓)) ⊆ Cst(φ) ∪ Cst(R 1 φ↓) ⊆ Cst(φ)
This concludes the proof. Lemma 6. Let K 0 be a configuration of the form (P 0 ; φ 0 ; ∅; 0). Let σ be a mgu of terms of P 0 . We have that St(K 0 σ) ⊆ St(K 0 )σ.

Proof. We consider σ the mgu between pairs of terms occurring in St(K 0 ), and we show that St(K 0 σ) ⊆ St(K 0 )σ.

Let Γ be the set of pairs of terms such that σ = mgu(Γ). Let t ∈ St(K 0 σ) be such that t ∈ St(K 0 )σ. Therefore, we have that t ∈ St(img(σ)). As the mgu does not create variables, if t is a variable then t ∈ St(Γ) ⊆ St(K 0 ), so we assume t is not a variable.

Let σ = σδ where δ replaces any occurrence of t in img(σ) by a fresh variable x. We have that:

• uσ = vσ for any equation u = v ∈ Γ. Indeed, we know that uσ = vσ for any such u = v, and thus (uσ)δ = (vσ)δ. Since t ∈ ESt(K 0 )σ, and u, v ∈ ESt(K 0 ), we deduce that uδ = u and:

(uσ)δ = u(σδ ∪ δ) = uσ
and similarly (vσ)δ = vσ. • σ is strictly more general that σ. Indeed, we have that σ = στ considering τ = {x → t} and t is not a variable. This leads to a contradiction since σ = mgu(Γ) and concludes the proof.

We denote by Terms(φ) the set of terms occurring in img(φ). This notation is also used to denote the set of terms occurring in a trace, e.g. Terms(trφ↓) denotes the set of terms occurring in the trace trφ↓.

We are now able to state and prove a stronger version of Theorem 1 in which the resulting witness tr satisfied some additional properties.

Theorem 5. Let P be a protocol type-compliant w.r.t. (∆ 0 , δ 0 ) (which may feature replication and match constructions).

If P tr = = ⇒ (P; φ; σ; i) then there exists a well-typed execution P tr = = ⇒ (P; φ ; σ ; i) involving only simple asap recipes such that tr = tr.

Moreover, we may assume that tr and φ are cv-alien-free.

Proof. (sketch of proof)

The first part of the theorem is a direct consequence of Theorem 1. Then, the fact that we can consider simple asap recipes is an easy consequence of Lemma 4. It remains to establish that we can consider tr and φ to be cv-alien-free. We have seen in the proof of Theorem 1 (see Equation (1)) that the well-typed substitution σ is of the form σ = σ tr match σ ∪ σ where σ = ρ • σ S where:

• σ tr match is the most general unifier of Γ tr match the set of pairs (x, u i ) corresponding to match instructions that are executed along tr; • σ S is the most general unifier of Γ where:

Γ = (u, v) | u, v ∈ ESt(P σ tr match ) such that uσ = vσ
• ρ is a bijective renaming from variables in dom(σ) dom(σ S ) to some fresh constants preserving type. We have that St((P σ tr match )σ S ) ⊆ St(P σ tr match )σ S since σ S is a mgu between subterms occurring in P by Lemma 6. Then, since ρ is a renaming, we deduce that St(P σ ) ⊆ St(P σ tr match )σ . Similarly, we have that: St(P σ tr match ) ⊆ St(P )σ tr match since σ tr match is a mgu between subterms occurring in P . Therefore, we deduce that:

St(P σ ) ⊆ (St(P )σ tr match )σ = St(P )σ (2)
We now show that tr φ ↓ is cv-alien-free. Assume by contradiction that there exists a constant c h from Σ 0 of cvalien type occurring in tr φ ↓. In other words, c h occurs in an instantatiation by σ of an input or output action of the initial processes, possibly after renaming names and variables (due to some unfolding). Thus, we have that c h ∈ St(P σ ). Thanks to the property 2, we deduce that c h ∈ St(P )σ , and since c h does not occur in St(P ) (as any constant from Σ 0 of cvalien type), we deduce that there exists x ∈ St(P ) such that xσ = c h . However, this is impossible too since no variable having such a type can occur in P . This allows us to conclude that tr φ ↓ is cv-alien-free.

We have that Terms(φ ) ⊆ Terms(tr φ ↓), and thus we easily deduce that φ is cv-alien-free. Now, regarding recipes occurring in tr , we know that they are simple, and thanks to Lemma 5, we have that Cst(R) ⊆ Cst(φ )∪Cst(Rφ ↓) for any recipe R occurring in tr . We have that constants occurring in R already occur in φ or tr φ ↓, and since we have seen that no constant from Σ 0 of cv-alien type occurs in φ and tr φ↓, we are done.

APPENDIX B COMPUTATION OF THE BOUND

A. Preliminaries

We consider that a marking is appropriate if it indicates subterms that, whenever deducible in a well-typed execution, are deducible earlier in any well-typed execution. This will guarantee that it is sound to not to take into account this subterm during the computation of dep.

An almost destructor-only recipe R such that Rφ↓ is a message, intuitively tries to dig in a term u. Such a recipe deconstructs the term u to extract its subterm at position target(R) in u, where target(R) is defined as follows:

• if R is a variable w • target(R| 1 ).i 0 if root(R) = g ∈ Σ d and g(t 1 , . . . , t n ) → r g ∈ R d with t 1 | i0 = r g .
Note that the operation target defined above is well-defined for any almost destructor-only recipe.

Definition 11. Let P be a protocol. A marked position (α, p) of P w.r.t. (∆ 0 , δ 0 ) is appropriate if for any well-typed execution P tr = = ⇒ (P; φ; σ; j) for any out α (c, w) occurring in tr, for any almost destructor-only recipe R with w at its leftmost position and such that target(R) = p and Rφ↓ = m is a message, we have that R is not an asap recipe of m (considering the frame φ and the ordering induced by tr).

B. Properties of dep

Now, we show that dep satisfies the properties stated in Figure 4. These properties will be used in the following section to establish our main result. As an illustrative example, we detailed below the proof of Property 5. The other ones can be established in a similar way. Proof of Property 5. Let τ be an initial type. For any i > 0, we have that:

dep(τ ) ⊇ dep i (τ ) = dep 0 (τ ) ∪ S i-1 out (τ )
We are going to show first that dep(τ ) ⊇ dep 0 (τ ) ∪ S out (τ ). To establish this, let e ∈ dep 0 (τ ) ∪ S out (τ ). Since dep 0 (τ ) ⊆ dep(τ ), in case e ∈ dep 0 (τ ), we easily conclude. Otherwise, we have that e ∈ S out (τ ), and thus e ∈ S i out (τ ) for some i > 0 by definition of S out (τ ), and this allows us to conclude that e ∈ dep(τ ).

Conversely, let e ∈ dep(τ ). Then, we have that e ∈ dep i (τ ) for some i > 0. Hence, we have that: e ∈ dep 0 (τ )∪S i-1 out (τ ) ⊆ dep 0 (τ ) ∪ S out (τ ) which allows us to conclude.

When considering recipes for a witness of non static inclusion, we can not asume anymore that these recipes are all asap, and thus marking is not justified. However, we can assume they are subterm asap, and this is the reason why we still consider a bit of marking.

The definition of S + out (τ ) is given in Section V. In addition, we define

dep + (τ ) = dep 0 (τ )∪({∅}⊗dep(τ 1 )⊗. . .⊗dep(τ k ))∪S +
out (τ ) for any non-initial type τ such that τ = f(τ 1 , . . . , τ k ).

C. Main result

To prove our main result, we need to define ρ on terms. The definition is similar to the one for types. Definition 12. Given a term t, we define ρ(t) to be ρ(t, , ∅) where ρ(t, p, S) is recursively defined as the set {(t, p)#S}∪E where E = ∅ when t is an atom (e.g. a constant or a name). Otherwise, we have that t = f(t 1 , . . . , t k ) and E is defined as:

E = g( 1 , . . . , n ) → r g ∈ R d θ = mgu( 1 , f(t 1 , . . . , t k )) i 0 ∈ {1, . . . , k} is such that r g = 1 | i0 ρ(t i0 , p.i 0 , S { 2 θ, . . . , n θ})
In the definition, S is a multiset of terms.

Of course, there is a link between the definition of ρ on types and the one on terms. Lemma 7. Let (∆ 0 , δ 0 ) be a typing system, and u be a term. We have that:

(v, p)#S ∈ ρ(u) implies (δ 0 (v), p)#δ 0 (S) ∈ ρ(δ 0 (u)).
Proof. We establish the following result by structural induction on u.

(v, p)#S ∈ ρ(u, p 0 , S 0 ) implies (δ 0 (v), p)#δ 0 (S) ∈ ρ(δ 0 (u), p 0 , δ 0 (S 0 )).

The result is a direct consequence of this property.

Note that the implication from types to terms does not hold since the structure of a type may be finer than the structure of the term. For instance, we may have δ(c) = τ 1 , τ 2 . Lemma 8. Let φ be a frame and R be an almost destructoronly recipe such that Rφ↓ is a message. We have that (Rφ↓, target(R))#S ∈ ρ(wφ) where S = {R| p φ↓ | p = 1 . . . 1.i with i ≥ 2 and p a position in R}, and w is the variable occurring in R at its leftmost position.

Proof. We establish the following result by structural induction on R:

ρ(Rφ↓, target(R), S) ⊆ ρ(wφ)
where S = {R| p φ↓ | p = 1 . . . 1.i with i ≥ 2 and p a position in R}, and w is the variable occurring in R at its leftmost position. Note that the result stated in the lemma is a direct consequence of the property stated above.

Base case: R ∈ W. In such a case, we have that Rφ↓ = wφ. We have that target(R) = , and S = ∅. By definition, we have that ρ(wφ) = ρ(wφ, , ∅). Thus the result holds.

Induction case: root(R) ∈ Σ d . In such a case, we have that R = g(R 1 , . . . , R n ) for some g ∈ Σ d . By induction hypothesis we have that ρ((R 1 φ↓, target(R 1 ), S 1 ) ⊆ ρ(wφ) where

S 1 = R 1 | p φ↓ | p = 1 . . . 1.i with i ≥ 2 and p a position in R 1 .
We also know that t = R 1 φ↓ = f(t 1 , . . . , t k ) for some t 1 , . . . , t k and some f, and we consider the rule → r ∈ R d that is applied to lead to a message. We have that = g(f( 1 1 , . . . , 1 k ), 2 , . . . , n ), and r = 1 i0 for some i 0 ∈ {1, . . . , k}.

According to the definition of ρ(t, target(R 1 ), S 1 ), we have that it contains ρ(t i0 , target(R 1 ).i 0 , S 1 ∪ { 2 θ, . . . , n θ}) where θ = mgu( 1 , f(t 1 , . . . , t k )). Thus, we have that ρ(t i0 , target(R 1 ).i 0 , S 1 ∪ { 2 θ, . . . , n θ}) ⊆ ρ(t, target(R 1 ), S 1 ). We have that:

ρ(Rφ↓, target(R), S) = ρ(t i0 , target(R 1 ).i 0 , S 1 ∪ {R 2 φ↓, . . . , R n φ↓}) = ρ(t i0 , target(R 1 ).i 0 , S 1 ∪ { 2 θ, . . . , n θ}) ⊆ ρ(t, target(R 1 ), S 1 ) ⊆ ρ(wφ)
This allows us to conclude this case.

1) dep(⊥) = {∅}; 2) In case α is an output, we have that: dep(α) = {{α}} ⊗ dep(pred(α)).

3) In case α is an input of type τ , we have that: dep(α) = {{α}} ⊗ dep(pred(α)) ⊗ dep(τ ). 4) for any type τ , we have that

S out (τ ) = out α (c, u) occurring in P (τ, p)#{τ 1 , . . . , τ n } ∈ ρ(δ 0 (u)) (α, p) not marked dep(α) ⊗ dep(τ 1 ) ⊗ . . . ⊗ dep(τ n ) .
5) for an initial type τ , we have that dep(τ ) = dep 0 (τ ) ∪ S out (τ ); 6) for a non-initial type τ such that τ = f(τ 1 , . . . , τ k ), we have that:

dep(τ ) = dep 0 (τ ) ∪ ({∅} ⊗ dep(τ 1 ) ⊗ . . . ⊗ dep(τ k )) ∪ S out (τ )
where dep 0 (τ ) = ∅ when τ is an cv-alien type; and dep 0 (τ ) = {∅} otherwise.

• V N = {v ∈ V | ∃ r ∈ N, r → * v}; • E N = {(u, v) ∈ E | u, v ∈ V N }
where → * denotes the transitive closure of the relation induced by E.

When we consider an execution and its associated dag, we can decide to prune the dag w.r.t. a given set of nodes N , then the resulting dag corresponds also to an execution of P .

Given an execution exec and its associated dag D, we denote exec| v the execution obtained by pruning D w.r.t. the set of nodes {v}, and given a recipe R such that vars(R) = {w i1 , . . . , w i k }, we denote exec| R the execution obtained by pruning D w.r.t. {v 1 , . . . , v k } where v j is the node corresponding to the output w ij .

We denote Label(tr) (resp. Label(exec)) the multiset of labels (from L) occurring in tr (resp. exec), and given a node v of a dag (coming from an execution trace), we denote Label(v) its label.

A simple recipe is subterm asap w.r.t. φ if all its direct subterms are asap w.r.t. φ. Note that this implies that all its strict subterms are asap too.

Then, we are able to establish this key result by induction on the length of the trace.

Proposition 1. Let P be a protocol type-compliant w.r.t. some typing systems (∆ 0 , δ 0 ). We consider a well-typed and cvalien-free execution exec : P tr = = ⇒ (P; φ; σ; i) involving only simple asap recipes. We consider the dag D corresponding to this execution. We have that:

1) for any node v of D, we have that there exists a multiset A ∈ dep(Label(v)) such that Label(exec| v ) ⊆ A;

2) for any almost destructor-only receipe R which is also asap (resp. subterm asap), and cv-alien-free, and such that Rφ↓ is a message of type τ , we have that there exists a multiset A ∈ S out (τ ) (resp. S + out (τ )) such that Label(exec| R ) ⊆ A.

3) for any simple asap (resp. subterm asap), cv-alien-free recipe R such that Rφ↓ is a message of type τ , we have that there exists a multiset A ∈ dep(τ

) (resp. dep + (τ )) such that Label(exec| R ) ⊆ A.
Proof. We prove these results by induction on the length of tr.

Base case: tr is empty. In such a case, we have that there is no node v in D, and therefore item 1 trivially holds. Regarding item 2, since dom(φ) = ∅ there is no recipe satisfying the condition. Regarding item 3, we have Rφ↓ = R↓ = R, and R is cv-alien-free. We show by induction on |R| that dep(τ ) = ∅ (where τ is the type of R). In case |R| = 1, we have that either R ∈ Σ c , and thus τ = R, and ∅ ∈ dep(τ ); or R ∈ Σ 0 . In this case, we have that τ is not an cv-alien type, and thus ∅ ∈ dep(τ ). Now, in case R -f(R 1 , . . . , R n ) with f ∈ Σ c , by induction hypothesis, we have that R 1 , . . . , R n are cv-alien-free, and thus for any i ∈ {1, . . . , n}, we have that dep(τ i ) = ∅ where τ i is the type of R i . This allows us to conclude that dep(τ ) = dep(f(τ 1 , . . . , τ n )) = ∅. Therefore, we have that dep(τ ) = ∅ (resp. dep + (τ ) = ∅). We have that Label(exec| R ) = ∅, and thus the result holds.

Inductive case: tr = tr .α. We denote exec the prefix of exec corresponding to the trace tr . We distinguish several cases depending on the type of the action α.

Case of an output. We assume that tr = tr .(α : out(c, w)) or tr = tr .(α : out(c, c )), and we establish the two items. 1) Let v be a node of D. In case α does not correspond to the node v, we have that Label(exec| v ) = Label(exec | v ). Relying on our induction hypothesis, we know that there exists A ∈ dep(Label(v)) such that Label(exec | v ) ⊆ A. This allows us to conclude. Now, we assume that α corresponds to the node v.

In case pred(α) = ⊥, then dep(exec| v ) = {α} and dep(Label(v)) = {{α}}, thus the result holds. Otherwise, we have that pred(α) = α for some α , and we denote v the node corresponding to this action in our dag D. Relying on our induction hypothesis, we have that there exists

A ∈ dep(Label(v )) such that Label(exec | v ) ⊆ A .
By definition of dep, we have that dep(Label(v)) = {{α}} ⊗ dep(Label(v )), and by definition of Label, we have that Label(exec| v ) = Label(exec | v ) {α}. It is easy to see that A = A {α} satisfies the requirement. 2) Let R be an almost destructor-only recipe which is also asap (resp. subterm asap), and cv-alien-free, and such that Rφ↓ is a message of type τ . In case w ∈ vars(R), we have that Label(exec| R ) = Label(exec | R ). Relying on our induction hypothesis, we know that there exists a multiset A ∈ S out (τ ) (resp. S + out (τ )) such that Label(exec | R ) ⊆ A. This allows us to conclude. Now, we assume that w ∈ vars(R). We establish the existence of A ∈ S out (τ ) (resp. S + out (τ ) in case R is subterm asap) such that Label(exec| R ) ⊆ A. We show this result by induction on the size of the asap (resp. subtem asap) recipe R. We have that Rφ↓ is a message and R is an almost destructor-only recipe.. We denote p = target(R), w 0 the variable at the leftmost position in R (i.e. at position 1 . . . 1), and R 1 , . . . , R k the recipes at position 1 . . . 1.i with i ≥ 2 in R for any such position which is well-defined. First, we may note that, for any i ∈ {1, . . . , k}, we have that R i φ↓ is a message, R i is in forced normal form, asap and cv-alien-free, and thus, thanks to Lemma 3, we know that for any i ∈ {1, . . . , k}, R i is simple. Actually, we have that R 1 is an almost destructor-only recipe. Therefore, we can apply our induction hypothesis (item 3), and denoting τ 1 , . . . , τ k the types of R 1 φ↓, . . . , R k φ↓, we obtain that there exists A i ∈ dep(τ i ) such that Label(exec| Ri ) ⊆ A i for each i ∈ {1, . . . , k}. Applying Lemma 8 on φ and R, we have that (Rφ↓, p)#{R 1 , . . . , R k } ∈ ρ(wφ). Then, thanks to Lemma 7, we deduce that (τ, p)#{τ 1 , . . . , τ k } ∈ ρ(β) where β is the label associated to the output w 0 , and τ 1 , . . . , τ k are the types of R 1 φ↓, . . . , R k φ↓. By definition of S out (τ ), we have that:

dep(β) ⊗ dep(τ 1 ) ⊗ . . . ⊗ dep(τ k ) ∈ S out (τ ).
Note that by definition of a marked position to be appropriate, we know that (β, p) is not marked. Indeed, otherwise, this would contradict the fact that R is asap. Now, in case we only know that R is subterm asap, it remains to establish that (β, p) is not marked or p = . Assume that p = . We thus have that p = p .i 0 for some i 0 , and we therefore know that R ∈ W. We have that R = g(R 1 , . . . , R n ) for some g ∈ Σ d . We have that R 1 is cv-alien-free, target(R 1 ) = p , w 0 is the variable at the leftmost position in R 1 , and R 1 φ↓ = w 0 φ| p . Since R 1 is asap and almost destructor-only, by definition of an appropriate marking, we deduce that (β, p) is not marked. Now, relying again on our induction hypothesis, we have that there exists A 0 ∈ dep(Label(v 0 )) = dep(β) such that Label(exec| v0 ) ⊆ A 0 where v 0 is the node associated to out(c, w 0 ). Note that this has been established in item 1 above in case α = β. To conclude, it is easy to see that A = A 0 A 1 . . . A k satisfies the requirement.

3) Let R be a simple asap (resp. subterm asap) and cvalien-free recipe such that Rφ↓ is a message of type τ . In case w ∈ vars(R), we have that Label(exec| R ) = Label(exec | R ). Relying on our induction hypothesis, we know that there exists a multiset A ∈ dep(τ

) (resp. dep + (τ )) such that Label(exec | R ) ⊆ A.
This allows us to conclude. Now, we assume that w ∈ vars(R). We establish the existence of A ∈ dep(τ

) (resp. dep + (τ ) in case R is subterm asap) such that Label(exec| R ) ⊆ A.
We show this result by induction on the size of the asap (resp. subtem asap) recipe R.

In case R is an almost destructor-only recipe, we conclude relying on item 2. Note that S out (τ ) ⊆ dep(τ ) and S + out (τ ) ⊆ dep + (τ ). Thus, we now consider the case where

R = f(R 1 , . . . , R k ) (with k ≥ 1), and f ∈ Σ c or R ∈ Σ 0 .
In case R = c 0 ∈ Σ 0 , we know that τ is not cv-alien (since R is cv-alien-free), and therefore we have that ∅ ∈ dep(τ ), and dep(exec| R ) = {∅}, and the result holds. Note that dep(τ ) ⊆ dep + (τ ). Otherwise, we have that R = f(R 1 , . . . , R k ), and R 1 , . . . , R k are simple, asap, and cv-alien-free. Note that, R i not asap will contradict the fact that R is asap or subterm asap. Relying on our induction hypothesis, we have that, for each i ∈ {1, . . . , k}, there exists

A i ∈ dep(τ i ) such that Label(exec| Ri ) ⊆ A i , and we have that dep(τ 1 ) ⊗ . . . ⊗ dep(τ k ) ∈ dep(τ ) ⊆ dep + (τ ).
It is therefore easy to see that A = A 1 . . . A k satisfies the requirement.

Case of an input. Now, we assume that tr = tr .(α : in(c, R in )) and we establish the two items.

1) Let v be a node in D. In case α does not correspond to the node v, we have that Label(exec| v ) = Label(exec | v ). Relying on our induction hypothesis, we know that there exists A ∈ dep(Label(v)) such that Label(exec | v ) ⊆ A. This allows us to conclude. Now, we assume that α corresponds to the node v.

We establish the existence of

A ∈ dep(Label(v)) with Label(exec| v ) ⊆ A. In case pred(α) = ⊥, then Label(exec| v ) = Label(exec | R in ) {v}.
Applying our induction hypothesis on tr (item 3) with R in , we deduce that there exists

A 0 ∈ dep(τ ) such that Label(exec | R in ) ⊆ A 0 .
By definition, we have that {{α}} ⊗ dep(τ ) = dep(Label(v)). It is easy to see that A = A 0 {α} satisfies the requirement. Now, in case pred(α) = α for some α . We denote v the node corresponding to this action in our execution dag. Relying on our induction hypothesis, we know that there exists

A ∈ dep(Label(v )) = dep(α ) such that Label(exec | v ) ⊆ A . We have that Label(exec| v ) = Label(exec | R in ) Label(exec | v ) {v}.
Applying our induction hypothesis on tr (item 3) with R in we deduce that there exists

A 0 ∈ dep(τ ) such that Label(exec | R in ) ⊆ A 0 . By definition, we have that {{α}} ⊗ dep(α ) ⊗ dep(τ ) = dep(Label(v)).
It is easy to see that A = A 0 A {α} satisfies the requirement. 2) Let R be an almost destructor-only asap (resp. subterm asap), cv-alien-free recipe such that Rφ↓ is a message of type τ . Since α is an input, we have that

Label(exec| R ) = Label(exec | R ).
Relying on our induction hypothesis, we know that there exists a multiset A ∈ S out (τ ) (resp. S + out (τ )) such that Label(exec | R ) ⊆ A. This allows us to conclude.

3) Let R be a simple asap (resp. subterm asap), cv-alienfree recipe such that Rφ↓ is a message of type τ . Since α is an input, we have that Label(exec| R ) = Label(exec | R ). Relying on our induction hypothesis, we know that there exists a multiset A ∈ dep(τ

) (resp. dep + (τ )) such that Label(exec | R ) ⊆ A.
This allows us to conclude. This concludes the proof of this result.

D. Proof of Theorem 2

We are now able to prove our main result regarding reachability.

Theorem 2. Let P be a protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ). Let α be a label of P and assume (tr. , φ) ∈ trace(P ) for some tr, , φ such that Label( ) = {α}. Then there exists tr , , φ , and A ∈ dep(α) such that (tr . , φ ) ∈ trace(P ) with Label( ) = {α}; and Label(tr . ) ⊆ A.

Proof. By hypothesis, we have that (tr. , φ) ∈ trace(P ), and thus there is an execution exec witnessing this fact. Thanks to Theorem 5, we can assume that this execution is well-typed, and involves simple asap recipes. Moreover, we can assume that tr. and φ are cv-alien-free. Thus, this execution is cvalien-free.

We consider the dag D corresponding to this execution, and we denote v the node corresponding to the action . Thanks to Proposition 1 (item 1), we have that there exists a multiset A ∈ dep(Label(v)) such that Label(exec| v ) ⊆ A. Note that Label(v) = Label( ) = {α}, and thus if we denote tr the trace underlying the execution exec| v , we have that tr = tr . for some tr and such that Label( ) = {α}. Moreover, we have that (tr . , φ ) ∈ trace(P ) for some φ (indeed by definition of exec| v we keep all the dependencies, and thus exec| v is an execution of P ). Thus, we deduce the existence of tr , , φ , and A ∈ dep(α) such that (tr . , φ ) ∈ trace(P ) with Label( ) = {α}, and Label(tr . ) ⊆ A.

E. Marking criteria

We now establish the following result regarding terms with a public type (see Definition 8).

Lemma 9. Let P be a protocol, (∆ 0 , δ 0 ) be a typing system, and u be a term having a public type. Let P tr = = ⇒ (P; φ; σ; i) be a well-typed execution such that Rφ↓ = u for some recipe R, then u ∈ T (Σ c , Σ 0 ).

Proof. Let τ p be the type of u. To show the result, we establish that each leaf of u is either a constant in Σ 0 or a constant in Σ c . Let l be a leaf of u. We have that l is either a name or a constant. In case l is a constant, we are done. Otherwise, we have that l ∈ N , and we have that δ 0 (l) ∈ St(τ p ). Since Rφ↓ = u for some recipe R, we have that l occurs somewhere in φ, and thus a name n such that δ 0 (n) = δ 0 (l) occurs in P . Therefore, we have that δ 0 (n) ∈ St(τ p ) for some name n occurring in P . This contradicts the fact that τ p is a public type, and allows us to conclude the proof.

We conclude that marking a position that has a public type is appropriate.

Lemma 10. Let (α, p) be a marked position of a protocol P w.r.t. a typing system (∆ 0 , δ 0 ). Let u be the term such that out α (c, u) occurs in P . If δ 0 (u)| p has a public type then (α, p) is appropriate.

Proof. We consider a well-typed execution P tr = = ⇒ (P; φ; σ; i) and out α (c, w) occurring in tr. Let R be a recipe in forced normal form such that root(R) ∈ Σ d ∪W with w at its leftmost position, and such that target(R) = p and Rφ↓ = m is a message. By definition of target(R), we have that Rφ↓ = wφ| p , and since we are considering a well-typed execution, we know that δ 0 (wφ| p ) = δ 0 (wφ)| p has public type. Thus, we have that wφ| p ∈ T (Σ c , Σ 0 ) thanks to Lemma 9, and therefore R (which contains w) is not an asap recipe for Rφ↓ = m = wφ| p .

Our second criterion is a precedence criterion. We extend the criterion proposed in [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF], [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF] in order to make it applicable in presence of match constructions.

Example 19. Consider the following process P modelling a simple challenge response exchange relying on a match construction:

P = in α (c, y).match y with senc( req, x , k) → out β (c, senc( rep, x , k))
Type-compliance is satisfied considering δ 0 (y) = δ 0 (senc( req, x , k)). Clearly, we have that (β, 1.2) is an appropriate marked position, Indeed, extracting the value corresponding to x from the output β is actually useless since this value was accessible before through the input α under the exact same protection (here the key k). Any asap recipe will favour the use of the recipe used in input rather than the one which digs into the output.

Given a protocol P , we say that the action labeled β follows the action labeled α in P if β is sequentially after α, i.e. in case α is an output, we have that out α (c, •).Q is a subprocess of P and β occurs in Q. Given an action labeled α occurring in a protocol P , we denote by σ α match the mgu of all the equations u = v corresponding to an instruction match u with v → _ encountered from the root of P to its action labeled α. Note that for a protocol P that does not feature match construction, we have that σ α match = ∅ for any label α occurring in it. Example 20. Going back to Example 19, we have that β follows α in P , and σ β match = {y → senc( req, x , k)}. The inclusion S ⊆ # S denotes the fact that for any element e ∈ S, the multiplicity of e in S is smaller than the multiplicity of e in S .

Lemma 11. Let (β, p) be a marked position of a protocol P w.r.t. a typing system (∆ 0 , δ 0 ) and α a label of an action in P involving term v such that:

• out β (c, u) follows the action α in P ; • ((uσ β match )| p , p)#S ∈ ρ(uσ β match ) for some S; • ((uσ β match )| p , q)#S ∈ ρ(vσ β match )
for some q, S such that S ⊆ # S. We have that (β, p.p ) is appropriate for any p such that δ 0 (u)| p.p is well-defined.

Proof. We consider a well-typed execution P tr = = ⇒ (P; φ; σ; i) and out β (c, w) occurring in tr. Let R be a recipe in forced normal form such that root(R) ∈ Σ d ∪W with w at its leftmost position, and such that target(R) = p.p and Rφ↓ is a message. By definition of target(R), we have that Rφ↓ = wφ| p.p . In order to conclude, we want to show that R is not an asap recipe for Rφ↓ = wφ| p.p .

Let η = 1 . . . 1 be a sequence of 1 and R 0 = R| η be such that target(R 0 ) = p. We have that R 0 φ↓ = wφ| p , and we denote by {R 1 key , . . . , R j key } the multiset of recipes occurring at position of the form η.k with k ≥ 2 in R 0 .

According to our hypothesis, we know that there exist in α (_, R in ) (resp. out α (_, w )) occurring before out β (c, w) in tr, and a substitution τ such that wφ = uσ β match τ and R in φ↓ = vσ β match τ in case α corresponds to an input (resp. w φ = vσ β match τ in case α corresponds to an output). We know that p is a position that exists in uσ β match and similarly the position q exists in vσ β match . Moreover, thanks to our hypothesis, we have that (vσ β match )| q = (uσ β match )| p . Thus, we have that R in φ↓| q = wφ| p in case α corresponds to an input (resp. w φ| q = wφ| p in case α corresponds to an output). Now, reusing some elements of the multiset {R 1 key , ..., R j key }, we can build a recipe starting from R in (resp. w ) and adding destructors in order to extract the subterm at position q in R in φ↓ (resp. w φ) using elements of the multiset {R 1 key , ..., R j key }. We denote R 0 such a recipe. We have that R 0 is smaller than R 0 since we replace one occurrence of w (the one occurring at the leftmost position in R 0 ) by a smaller recipe (R in or w ), and regarding recipes occurring at position 1...1.k with k ≥ 2 in R 0 , they form a submultiset of those occurring at position 1...1.k with k ≥ 2 in R 0 . Note that R 0 φ↓ = R 0 φ↓ = wφ| p . Thus, we have that R 0 is not an asap recipe for wφ| p (R 0 being smaller), and therefore R (recipe which contains R 0 as a subterm) is not an asap recipe for Rφ↓ = wφ| p.p . Indeed R[R 0 ] η is smaller than R 0 and deduce the same term wφ| p.p .

C TERMINATION

In the previous sections, we considered a mathematical function dep. This function maps labels and types on sets of multisets. It may happen that the multisets are infinite, and in this case it becomes impossible to bound the number of sessions. The purpose of this section is to define a terminating algorithm dep , which computes the function dep whenever its result is finite, and which returns ⊥ when it is infinite.

For the sake of clarity, we remark the equations satisfied by dep can be rewritten as:

dep(α) = A(α) ∪ i B(α) ⊗ ⊗ ki j=0 dep(β j i )
where α is a label or a type, A(α) and B(α) are sets depending only on α (without any call to dep) and β j i are labels or types. More precisely, A(α) ∈ {∅; {∅}} for any label and type α (and A(α) = dep 0 (α)), B(α) = {{α}} for any label α, and B(τ ) = {∅} for any type τ . Those definitions can be rewritten as:

dep(α) = A(α) ∪ B(α) ⊗ i ⊗ ki j=0 dep(β j i )
Later on, it will be convenient to consider

next(α) = {β j i | ∀i, j}.
Example 21. For example, when τ is an initial type, we have:

dep(τ ) = dep 0 (τ ) ∪ out α (c, u) occurring in P (τ, p)#{τ 1 , . . . , τ n } ∈ ρ(δ 0 (u)) (α, p) not marked dep(α)⊗dep(τ 1 )⊗. . .⊗dep(τ n )
We have A(τ ) = dep 0 (τ ), and if we denote {β 1 i , . . . , β ki i | i} the set of the α, τ 1 , . . . , τ n such that out α (c, u) occurs in P , (τ, p)#{τ 1 , . . . , τ n } ∈ ρ(δ 0 (u)), (α, p) is not marked, and B(τ ) = {∅} we have:

dep(τ ) = A(τ ) ∪ [B(τ ) ⊗ i ⊗ ki j=0 dep(β j i )]
A path of labels and types is a sequence α 1 . . . . .α n where each α i is a type or a label. We denote |p| the length of the path p (number of types or labels occuring in p). Our goal is to define a practical dep that terminates and computes dep, but before doing that we need to identify all the labels and types α such that dep(α) = ∅.

It remains to prove that if dep (α, ) = ⊥, dep(α) is infinite. It is quite intuitive to remark that any ⊥ returned by dep corresponds to a loop in the computation of dep. However, the converse is not always true, as some of those loops can result in an empty result. To prove the converse of Proposition 3, we need to define loops that do not result in ∅. To do that, we introduce next as next (α) = {β j i ∈ next(α) | ∀k, Empty(β k i , ) = False}, that is those elements in next(α) that occur in a nonempty product dep(

β 1 i ) ⊗ • • • ⊗ dep(β ki i ) = ∅.
We can also remark that the definitions of dep and dep can be rewritten with β j i ∈ next (α) as:

dep(α) = A(α) ∪ B(α) ⊗ i dep(β j i )
and (when α / ∈ p and Empty(α, ∅) = False):

dep (α, p) = A(α) ∪ B(α) ⊗ i dep (β j i , p.α)
Now, we can prove that each step of the computation of dep is non-decreasing in some way.

Lemma 18. If β ∈ next (α) for some types or labels α and β, there is a set

E(α.β) = ∅ such that E(α.β) ⊗ dep(β) ⊆ dep(α).
Proof. If β ∈ next (α), there is an equation:

dep(α) = A(α) ∪ B(α) ⊗ i ⊗ ki j=0 dep(β j i )
where β is among the β j i , say β = β 0 0 . Then we have:

dep(α) = A(α) ∪ B(α)⊗ [ i>0 (⊗ ki j=0 dep(β j i ))] ∪ [dep(β) ⊗ (⊗ k0 j=1 dep(β j 0 ))]
If we write E(α.β) = B(α) ⊗ (⊗ k0 j=1 dep(β j 0 )), we have E(α.β) ⊗ dep(β) ⊆ dep(α). As the only types or labels τ such that dep(τ ) = ∅ are those such that Empty(τ, ) = True by Proposition 2, and as they do not occur in the equation by definition of next , we have that E(α.β) = ∅.

When E(α.β) = {∅}, we have only proved that dep(α) = dep(β), which is not very helpful (recall that ultimately, we want to prove that a cycle in the computation means that the result must be infinite). Thus, we want to know exactly when this occurs. Lemma 19. If τ is a label or a type, and β a type or a label, E(τ.β) = {∅} only if τ is a type and:

• either β is a type τ , and τ is a direct subtype of τ ;

• or β is an output label.

Proof. If E(τ.β) = {∅}, then it means that:

{∅} = E(τ.β) = B(τ ) ⊗ ⊗ k j=1 dep(β j )
for some β 1 , . . . β k . Thus in particular B(τ ) = {∅} which means that τ is a type (as we have B(α) = {α} for any label α and B(τ ) = {∅} for any type τ ). So the associated equation is either (if τ is an initial type):

dep(τ ) = dep 0 (τ ) ∪ out γ (c, u) occurring in P (τ, p)#{τ 1 , . . . , τ n } ∈ ρ(δ 0 (u)) (γ, p) not marked dep(γ)⊗dep(τ 1 )⊗. . .⊗dep(τ n ) or (if τ = f(τ 1 , . . . , τ n )): dep(τ ) =dep 0 (τ ) ∪ ({∅} ⊗ dep(τ 1 ) ⊗ • • • ⊗ dep(τ n )) ∪ out γ (c, u) occurring in P (τ, p)#{τ 1 , . . . , τ n } ∈ ρ(δ 0 (u)) (γ, p) not marked dep(γ) ⊗ dep(τ 1 ) ⊗ . . . ⊗ dep(τ n )
We have that dep(β) occurs in a product ⊗ where all the other elements (denoted above as β j 0 ) satisfy dep(β j 0 ) = {∅}. But for the label γ of an output, we have dep(γ) = ({γ} ⊗ D) ∪ C for some sets of multisets C = ∅, D = ∅. Thus dep(γ) = {∅}. So β does not appear in a product where there is a label of an output. So either β is a direct subtype of τ , or β is itself the label of the output.

We can extend inductively E to paths through E(α.β.p) = E(α.β) ⊗ E(β.p) for any labels or types α, β ∈ next (α) and any path p = p 1 . . . . .p k where p 1 ∈ next (β) and p i+1 ∈ next(p i ) for each i with 1 ≤ i < k. We are now ready to prove the main theorem of this section. Theorem 6. Let α be a label or a type. Let p be a path of label and types. Then, dep (α, ) terminates. Moreover, dep (α, ) = ⊥ iff dep(α) is finite, and in this case dep(α, ) = dep(α).

Proof. The termination of dep has been proved when dep has been defined. It follows directly from the finiteness of the set of labels and types. The case where dep(α, ) = ⊥ has been handled by Proposition 3.

It remains to prove that, when dep (α, ) = ⊥, the set dep(α) is infinite. Let α be a label or a type. Assume that dep (α, ) = ⊥. Then there is a minimal path p and a β such that dep (α, ) has called dep (β, p) = ⊥ with β occuring in p (only the calls to dep on an already-explored type or label can create ⊥ elements).

By Lemma 18 (applied inductively), we have that dep(α) = E(α.p.β) ⊗ dep(β). Moreover, as β occurs inside p, we can write p = p 1 .β.p 2 and by Lemma 18 (applied inductively):

E(β.p 2 .β) ⊗ dep(β) ⊆ dep(β)
We have to prove that E(β.p 2 .β) = {∅}. It will prove that dep(β) contains an infinite multiset. It is sufficient to prove that there are two successive elements e 1 .e 2 in the sequence β.p 2 .β, such that E(e 1 .e 2 ) = {∅}. Assume toward contradiction that there are no such two successive elements in β.p 2 .β. By Lemma 19, it means that for any e 1 .e 2 in β.p 2 .β, we have that e 1 is a type τ , and: However, either e 2 = β (it is the last element of the sequence), or (it is not the last element) there is an element e 3 such that e 2 .e 3 occurs in β.p 2 .β. In the second case, e 2 is a type. In the first case, e 2 = β, which is a type as it is the first element of the sequence. So in both cases, e 2 is a type, and we deduce it is a direct subtype of e 1 . Thus β.p 2 .β is a sequence where each element is a direct subtype of the previous one. It implies that β is a strict subtype of itself, which is a contradiction. Thus, there are two successive elements e 1 .e 2 in β.p 2 .β such that E(e 1 .e 2 ) = {∅}. It implies that dep(β) contains an infinite element, and thus as dep(α) = E(α.p ⊥ (α)) ⊗ dep(β), that α contains an infinite element. It is the result we wanted to prove.

D THE CASE OF EQUIVALENCE

Regarding the class of protocols, we consider protocols without else branches and we consider processes in simple form. This corresponds to protocols that do not feature match constructions. The main reason for this restriction is the fact that despite our effort, we do not succeed to establish a typing result with else branch. Thus, this result for equivalence only deal with protocols without else branch. Since we are considering protocols without else branch, we can directly built on top of the typing result stated and proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF].

Then, following the proof done in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we establish our small bound in 2 main steps:

1) We first show that if P is not trace included in Q then there exists a witness of non inclusion that is well-typed, cv-alien-free, and involves only simple asap recipes. 2) We then compute a bound regarding the size of a welltyped attack of minimal size. We need for that to establish a new characterization regarding static inclusion.

A. A well-tped witness

As for the reachability case, we first show that we can focus on witnesses of non trace inclusion that have a particular form. A similar result has already been established in [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF] considering a fixed set of primitives. The sketch of proof given below follows the exact same lines. Theorem 7. Let K P be an initial configuration type-compliant w.r.t. (∆ 0 , δ 0 ) and K Q be another configuration. We have that K P t K Q if, and only if, there exists a well-typed execution K P tr = = ⇒ (P; φ; σ; i) involving only simple asap recipes witnessing this fact. Moreover, we may assume that tr and φ are cv-alien-free.

Proof. The first part of this theorem is actually a consequence of the typing result that has been established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] (Theorem 3.9). Indeed, let K P , and K Q be two configurations as described in the theorem, and consider a witness tr of non-inclusion of minimal length. Thanks to Theorem 3.9 ( [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]), we know that there exists a well-typed execution K P tr = = ⇒ (P; φ; σ; i) witnessing this non-inclusion and we have that tr and tr have the same length. It thus remains to establish that we can consider such an execution which only involves simple asap recipes, and that we can assume that tr, and φ are cv-alien-free.

We first establish that we can consider a witness involving simple asap recipes. We denote i 0 the first step in the execution that involves a recipe that is not a simple asap one. In case such a i 0 does not exist, we are done. Otherwise, we consider a well-typed witness of non-inclusion such that |tr| -i 0 is minimal. We have that the i 0 th step is an input of the form in(c, R) and R is not simple asap. Let tr i0 be the prefix of tr until the i 0 th step. We denote φ i0 the frame such that (tr i0 , φ i0 ) ∈ trace(K P ), and ψ i0 the frame such that (tr i0 , ψ i0 ) ∈ trace(K Q ). Note that these frames are uniquely defined as we consider simple protocols.

Let R be a simple asap recipe such that R φ i0 ↓ = Rφ i0 ↓. Note that such a recipe exists thanks to Lemma 4. Since we consider a witness of non-inclusion of minimal length, we know that φ i0 s ψ i0 , and thus we have that Rψ i0 ↓ = R ψ i0 ↓. We consider the trace tr which is equal to tr replacing at the i 0 th step, the recipe R with the recipe R . We obtain a witness of non-inclusion which contradicts the minimality of the trace tr. Hence, we are done, and we can consider that K P tr = = ⇒ (P; φ; σ; i) is a well-typed execution involving only simple asap recipes witnessing the non-inclusion.

It remains to establish that we can assume that tr and φ are cv-alien-free. Actually, considering K P tr = = ⇒ K P = (P; φ; σ; i) a witness of non-inclusion, according to Proposition 5.4 stated and proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we know that the well-typed substitution σ is such that σ = σ S ρ where:

• σ S is the most general unifier (denoted mgu) of Γ = {(u, v) | u, v ∈ ESt(K 0 ) such that uσ = vσ}; and • ρ is a bijective renaming from variables in dom(σ) dom(σ S ) to some fresh constants preserving type. We have that St(K P σ S ) ⊆ St(K P )σ S since σ S is a mgu between subterms occurring in K P by Lemma 6. Then, since ρ is a renaming, we deduce that St(K P σ) ⊆ St(K P )σ.

In order to conclude, we apply the same reasoning as in the case of reachability, as done e.g. at the end of Theorem 5. We first show that trφ↓ is cv-alien-free. Assume by contradiction that there exists a constant c h from Σ 0 of cvalien type occurring in trφ↓. In other words, c h occurs in an instantatiation by σ of an input or output action of the initial processes, possibly after renaming names and variables (due to some unfolding). Thus, we have that c h ∈ St(K P σ). Thanks to the inclusion St(K P σ) ⊆ St(K P )σ, we deduce that c h ∈ St(K P )σ, and since c h does not occur in St(K P ) (as any constant from Σ 0 of cv-alien type), we deduce that there exists x ∈ St(K P ) such that xσ = c h . However, this is impossible too since no variable having such a type can occur in K P . This allows us to conclude that trφ↓ is cv-alien-free.

We have that Terms(φ) ⊆ Terms(trφ↓), and thus we easily deduce that φ is cv-alien-free. Now, regarding recipes occurring in tr, we know that they are simple, and thanks to Lemma 5, we have that Cst(R) ⊆ Cst(φ) ∪ Cst(Rφ↓) for any recipe R occurring in tr. We have that constants occurring in R already occur in φ or trφ↓, and since we have seen that no constant from Σ 0 of cv-alien type occurs in φ and trφ↓, we are done.

B. Bounding the length of a minimal witness

We have to explain how to bound the size of a (minimal) witness of trace inclusion, that is well-typed, cv-alien-free, and that only involve simple asap recipes. One additional difficulty is to establish a bound regarding static inclusion. For this, we characterize the form of the test involved in such a witness, and we rely on an alternative definition of static inclusion. Definition 14. Let φ, ψ be such that dom(φ) = dom(ψ). We write φ simple s ψ if: This notion of static inclusion is equivalent to the original one.

Lemma 20. Let φ and ψ be two frames having the same domain. We have that:

φ s ψ ⇔ φ simple s ψ.
Proof. It is easy to see that φ s ψ ⇒ φ simple s ψ. Indeed, item 1 and item 3 are straightforward. Note that atomicity can be ckecked using the non-linear rule we have at our disposal. Given recipes R 1 , . . . , R n satisfying the assumptions of item 4, we have g(R 1 , . . . , , R n ) being a message is a test that holds φ, and thus it also holds for ψ thanks to our hypothesis, hence the result. Then, given a recipe R satisfying the assumptions of item 2, we can easily build a recipe R applying f on top of R such that Rφ↓ is a message. By hypothesis, we have that Rψ↓ is a message too, and thus R ψ↓ = C[x 1 , . . . , x n ]θ since to be a message Rψ↓ has to be compliant with the shape of f. Thus, we only consider the other implication. To establish the other implication, we consider another alternative definition of static inclusion, denoted by s . This notion is the same than the one given in Definition 14 but considering arbitrary recipes instead of simple/almost destructor-only/asap/subterm asap recipes. Clearly, we have that φ s ψ ⇒ φ s ψ, and thus to conclude, it remains to establish φ simple s ψ ⇒ φ s ψ.

So, we now assume φ simple s ψ and we show φ s ψ by induction on the size of the tests, i.e. the recipes involved in the test. More precisely, given an arbitrary test T that holds in φ w.r.t. the notion s , we show that T also holds in ψ assuming that any test smaller than T have already been transferred from φ to ψ. Given a test T , we denote R 1 , . . . , R n the recipes that are used in that test T . We consider the measure µ(T ) = (M, n) where:

1) M is the multiset of variables occurring in recipes R 1 , . . . R n but we do not count recipes that are asap and simple;

2) n = |R 1 | + . . . + |R n | where |R| is simply the size of R,
i.e. the number of function symbols occurring in it. We consider the lexicographic ordering. We now show that the four items of the definition of s are satisfied.

The test T is a recipe R such that Rφ↓ is a message (resp. atomic message).

• Case where R is not in forced normal form. Consider R such that R R . We assume that the rewriting step has been done at the innermost position p in R. We have that R φ↓ is a message (Lemma 1). By induction hypothesis R ψ↓ is a message too. It remains to show that Rψ↓ is a message. To show this, we will show that the same rewriting rule applies at root position on R| p φ and R| p ψ. We have that R| p = g(R 1 , . . . , R n ) for some g ∈ Σ test ∪ Σ d . Since Rφ↓ is a message, we know that R| p φ↓ = g(R 1 φ↓, . . . , R n φ↓)↓ is a message too, and we know that a rewriting has occurred at root position, and thus atomicity conditions and equality conditions imposed by the rule were satisfied. In order to conclude, we apply the induction hypothesis (item 4) on recipes R 1 , . . . , R n , we deduce that the same rewriting rule can be applied on the ψ side, and this allows us to conclude.

• Case where R is in normal form w.r.t. . Thanks to Lemma 3, we know that R is simple. Either R is almost destructor-only or R = C[R 1 , . . . , R k ] with C a nonempty context built using symbols in Σ c , and R 1 , . . . , R k almost destructor-only for any 1 ≤ i ≤ k. In the latter case, we easily conclude relying on our induction hypothesis (item 1 and also item 2 for the shape restriction) applied on R 1 , . . . , R k . In the former case, we know that R is almost destructor-only. We first assume that R is not subterm asap, meaning that there exists 1 ≤ i ≤ k such that R i is not asap. Let R i be the asap recipe w.r.t. φ allowing us to deduce R i φ↓. We have that (R i = R i )φ↓, i.e. the test R i = R i holds in φ, and relying on our induction hypothesis, we deduce that R i = R i holds in ψ. Consider the recipe R = R[R i ] i . We deduce that R = R holds in ψ. Applying our induction hypothesis on R , we deduce that R ψ↓ is a message which is atomic in case R φ↓ is atomic, and thus we deduce that Rψ↓ is a message which is atomic in case Rφ↓ is atomic too. Now, we asssume that R is subterm asap. First, in case R is asap, we are done. Thus, we know that R is an almost destructor-only recipe which is subterm asap but not asap. Let R be a simple asap recipe w.r.t. φ such that R = R holds in φ. Thus by hypothesis we have that R = R which holds in φ also holds in ψ. Then, applying our induction hypothesis on R (item 1), we deduce that R ψ↓ is a message (which is atomic in case R φ↓ is atomic), and thus we easily conclude that Rψ↓ is a message which is atomic in case Rφ↓ is atomic too. , we have that R = R holds in ψ. We have that the test R is compliant with shape C[x 1 , . . . , x n ] in φ, and thus by induction hypothesis R is compliant with shapre C[x 1 , . . . , x n ] in ψ, and thus this also holds for R. This allows us to conclude.

The test T is of the form R = R such that R and R are recipes, Rφ↓, R φ↓ are messages, and Rφ↓ = R φ↓.

• Case R (resp. R ) is not in normal form w.r.t. . Let R = R . Since Rφ↓ is a message, we deduce that R φ↓ = Rφ↓ (Lemma 1). We have shown that Rψ↓ is a message, and thus R ψ↓ = Rψ↓ thanks to Lemma 1.

We have that R φ↓ = Rφ↓ = R φ↓. Relying on our induction hypothesis applied on the test R = R , we deduce that R ψ↓ = R ψ↓, and thus Rψ↓ = R ψ↓. We have that R| i0 = R i0 holds in φ, and relying on our induction hypothesis, we deduce that R| i0 = R i0 holds in ψ. Consider R = R[R i0 ] i0 . We deduce that R = R holds in ψ. Relying on our induction hypothesis applied on R = R which holds in φ, we deduce that R = R holds in ψ, and this allows us to conclude that R = R holds in ψ. Now, we can assume that R is subterm asap.

Regarding the recipe R , we have that R = f(R 1 , . . . , R ). We would like to show that R is subterm asap. Indeed, assume w.l.o.g. that R 1 is not asap and let R 1 be an asap recipe w.r.t. φ. We have that R 1 = R 1 holds in φ, and relying on our induction hypothesis, we have that R 1 = R 1 holds in ψ. Consider R = f(R 1 , . . . , R ). We have that R = R holds in φ and ψ. Thus, we have that R = R holds in φ and relying on our induction hypothesis, we deduce that R = R holds in ψ. This allows us to conclude that R = R holds in ψ. Now, it remains to show that R or R is asap. Assume w.l.o.g. that both are not asap. Let R be an asap recipe w.r.t. φ such that R φ↓ = Rφ↓ = R φ↓. Relying on our induction hypothesis, we can transfer the tests R = R and R = R that both holds in φ, and thus we deduce that these tests also hold in ψ, and thus we conclude that R = R holds in ψ.

The test T is of the form (R 1 , . . . , R n ) such that R 1 , . . . , R n are recipes, (R 1 φ↓, . . . , R n φ↓) = (t 1 , . . . , t n )θ for some θ and a rule g(t 1 , . . . , t n ) → r ∈ R test ∪ R d .

• Case R 1 (resp. R 2 , . . . , R n ) is not in normal form w.r.t.

. Let R 1 = R 1 . Since R 1 φ↓ is a message, we deduce that R 1 φ↓ = R 1 φ↓ (Lemma 1). We have shown that R 1 ψ↓ is a message too, and thus thanks to Lemma 1, we have that R 1 ψ↓ = R 1 ψ↓. Relying on our induction hypothesis applied on the test R 1 , R 2 , . . . , R n , we deduce that the test R 1 , R 2 , . . . , R n holds in ψ, and thus we conclude that the test R 1 , R 2 , . . . , R n holds in ψ.

• Otherwise, as in the previous cases, thanks to Lemma 3, we know that R 1 , . . . , R n are simple. In case, one of them is not asap, e.g. R i , we can consider R i an asap simple recipe such that R 1 = R 1 holds in φ, and thus in ψ relying on our induction hypothesis (item 3 we have already proved), and this allows us to conclude. Thus, we can now assume that R 1 , . . . , R n are simple and asap. In case R 1 is almost destructor-only, we conclude relying on our hypothesis. Otherwise, we have that R 1 = f(R 1 1 , . . . , R k 1 ) for some f ∈ Σ c . We distinguish two cases.

Case 1: = g(t 1 , . . . , t n ) is linear. We thus only have to ensure that, for each 1 ≤ i ≤ n such that t i is not a variable, R i ψ↓ complies with the shape of sh root(ti) knowing that it is the case for R i φ↓. This is actually an easy consequence of our induction hypothesis. Note that item 2 has already been proved, and thus we can rely on it even if our measure has not strictly decreased.Therefore, we are done for this case.

Case 2: = g(t 1 , . . . , t n ) is not a linear term. In such a case, we necessarily have that t 1 = f(t 1 1 , . . . , t k 1 ) for some f ∈ Σ c . We know that t 1 is linear and contains exactly one occurrence of the non-linear variable x. Let j ∈ {1, . . . , k} be such that x occurs in t j 1 . By hypothesis we have that: {x} ⊆ {t j 1 , t 2 , . . . , t n } ⊆ {x} ∪ {h(x) | h ∈ Σ c } Let R x be a recipe among {R j 1 , R 2 , . . . , R n } such that the term t x among {t j 1 , t 2 , . . . , t n } associated to it is the variable x. By hypothesis, we know that there exists u (of sort atom) such that:

for all p such that | p = x, we have that g(f(R 1 1 φ↓, . . . , R k 1 φ↓), R 2 φ↓, . . . , R n φ↓)| p = u. To conclude, it remains to show that there exists v (of sort atom) such that:

for all p such that | p = x, we have that g(f(R 1 1 ψ↓, . . . , R k 1 ψ↓), R 2 ψ↓, . . . , R n ψ↓)| p = v. It is easy to see that using R x (almost destructor-only and asap recipe) or h(R x ) (simple and subterm asap recipe), we can transfer the required equalities from φ to ψ. For instance, assume that t 2 = h(x), and also that root(R 2 ) = h. We know that R 2 is almost destructor-only and asap. Consider the test h(R x ) = R 2 . We have that it holds in φ, and thus by hypothesis it also holds in ψ. A similar reasoning allows us to conclude for each occurrence of x in , and this allows us to conclude.

We are now able to prove our main theorem regarding trace equivalence.

Theorem 3. Let P be a simple protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ). Let Q be another simple protocol such that P t Q. There exists a trace (tr, φ) ∈ trace(P ) witnessing this non-inclusion such that Label(tr) ⊆ A for some A ∈ dep(P ).

Proof. Thanks to Theorem 7, we know the existence of a well-typed, cv-alien-free witness of non-inclusion which only involves simple asap recipes. We choose one having a minimal length. We denote D the execution graph associated to the execution exec corresponding to this witness (tr, φ) w.r.t. P .

Relying on the fact that P and Q are simple protocols, we distinguish the two following cases.

There does not exist ψ such that (tr, ψ) ∈ trace(Q). In such a case, we have that tr = tr • . This last action is necessarily a visible action. In case, it corresponds to an input (resp. output) of a message (not a channel name), then we prune D w.r.t. this single action. We denote exec the resulting execution, D its execution graph, and (tr 0 , φ 0 ) the corresponding trace of P . Actually, by definition of pruning, we have that tr 0 = tr 0 • where tr 0 is the trace obtained by pruning D w.r.t. the set of nodes N corresponding to all the dependencies of . We have that tr 0 passes in P and also in Q by minimality of the witness tr. Assume now that tr 0 . does not pass in Q. Then, we have built a smaller witness of non inclusion (contradiction), unless D = D . In the latter case, let v be the node corresponding to the action . We are done since, thanks to Proposition 1, we have that Label(exec| v ) ⊆ A for some A ∈ dep(Label(v)). Since D = D, we have that exec = exec| v = exec. Moreover, by definition of dep(P ), we have that dep(Label(v)) ⊆ dep(P ), and this allows us to conclude in the case where D = D .

Otherwise, we have that tr 0 . passes in Q meaning that is available after the execution of tr 0 and we can show that this action is still there after the execution of tr . Thus, contradiction.

In case, this last action corresponds to an output of a channel name then we have that out(c, c ) is available in P and not in Q, and due to the form of our processes (they are simple), we have that (tr, φ) = (out(c, c ), ∅) is a witness of noninclusion that satisfies our requirement.

There exists ψ such that (tr, ψ) ∈ trace(Q) but φ s ψ. From Lemma 20, we can consider distinguishing tests that satisfy Definition 14. Let W ⊆ W be the set of variables involved in such a test. In case exec| W is indeed smaller in length than exec, then to conclude, it remains to establish that exec| W is indeed a witness of non-inclusion. We have that exec| W is an execution of P (since we keep all the necessary dependencies), and since we are considering simple protocols, we know that the corresponding trace tr leads to a frame φ such that φ = φ| W . Similarly, we have that tr can be executed starting from Q and this leads to a frame ψ such that ψ = ψ| W . The witness of non-inclusion we considered is therefore still valid on this smaller witness, and this allows us to conclude in case exec| W = exec. Now, we assume that exec| W = exec, and we show that the result holds, i.e. there exists A ∈ dep(P ) such that Label(exec) ⊆ A. We distinguish several cases depending on the form of the test.

1) There exists an almost destructor-only and asap recipe R such that Rφ↓ is a (resp. atomic) message. Thanks to Lemma 2, we have that Rφ↓ ∈ St(φ). Then, thanks to Lemma 5, we have that Cst(R) ⊆ Cst(φ) ∪ Cst(Rφ↓), and thus Cst(R) ⊆ Cst(φ), and since φ is cv-alien-free, we have that R is cv-alien-free too. Thanks to Proposition 1, we know that there exists A ∈ S out (τ ) such that Label(exec| R ) ⊆ A where τ = δ 0 (Rφ↓). We have seen that Rφ↓ ∈ St(φ), and since we are considernig welltyped execution, we have that τ ∈ St(δ 0 (P )). Since there exists A ∈ S out (τ ), we have that dep(τ ) = ∅. Moreover, we have that S out (τ ) ⊆ S + out (τ ), and thus we deduce that A ∈ S out (τ ) implies that there exists A ∈ S test (P ) such that A ⊆ A .

2) There exists C[x 1 , . . . , x n ] a strict/direct substerm of a shape sh f with f ∈ Σ c , and an almost destructor-only and asap recipe R such that Rφ↓ is a message of the form C[x 1 θ, . . . , x n θ]. The reasoning is similar to the one done in the previous item. We have that there exists A ∈ dep(P ) such that Label(exec| R ) = Label(exec) ⊆ A.

3) There exist a simple recipe R and an almost destructoronly recipe R such that Rφ↓ = R φ↓ (is a message).

In addition, one recipe is asap, and the other is subterm asap w.r.t. φ. Thanks to Lemma 2, we have that Rφ↓ = R φ↓ ∈ St(φ). Then, thanks to Lemma 5, and since φ is cv-alien-free, we have that both R and R are cv-alienfree. Let τ = δ 0 (Rφ↓). We have seen that Rφ↓ ∈ St(φ), and since we are considernig well-typed execution, we have that τ ∈ St(δ 0 (P )).

First, we assume that R is asap and R is only subterm asap. Thanks to Proposition 1, we know that:

• there exists A ∈ dep(τ ) such that Label(exec| R ) ⊆ A; and • there exists A ∈ S + out (τ ) such that Label(exec| R ) ⊆ A . Therefore, we deduce that there exists A 0 ∈ dep(τ ) ⊗ § + out (τ ) such that Label(exec| {R,R } ) ⊆ A 0 . We thus have that A 0 ∈ S test (P ) and this allows us to conclude. Now, we assume that R is subterm asap, and R is asap. Thanks to Proposition 1, we know that:

• there exists A ∈ S out (τ ) such that Label(exec| R ) ⊆ A; and • there exists A ∈ dep + (τ ) such that Label(exec| R ) ⊆ A . Therefore, we deduce that there exists A 0 ∈ dep + (τ ) ⊗ S out (τ ) such that Label(exec| {R,R } ) ⊆ A 0 . Actually, we have that:

dep + (τ ) ⊗ S out (τ ) = dep 0 (τ ) ∪ S + out (τ ) ⊗ S out (τ ) = dep 0 (τ ) ⊗ S out (τ ) ∪ S + out (τ ) ⊗ S out (τ ) ⊆ dep(τ ) ⊗ S + out (τ )
We thus have that there exists A 0 ∈ S test (P ) such that Label(exec) = Label(exec| {R,R } ) ⊆ A 0 . 4) There exists a rule g(t 1 , . . . , t n ) → r ∈ R test ∪ R d , an almost destructor-only and asap recipe R 1 , and some simple asap recipes R 2 , . . . , R n such that R 1 φ↓, . . . , R n φ↓ are messages and (R 1 φ↓, . . . , R n φ↓) = (t 1 , . . . , t n )θ for some θ. Thanks to Lemma 2, we have that R 1 φ↓ ∈ St(φ).

Then, thanks to Lemma 5, and since φ is cv-alien-free, we have that R 1 is cv-alien-free. This allows us to deduce that R 2 φ↓, . . . R n φ↓ are also cv-alien-free since those terms only involve constants occurring in R 1 φ↓ or in l = g(t 1 , . . . , t n ) (left-hand side of a rewriting rule). In this latter case, those constants are constants from Σ c and do not have an cv-alien-type by definition of cv-alien-type. Let τ = δ 0 (R 1 φ↓). We have seen that R 1 φ↓ ∈ St(φ), and since we are considering well-typed execution, we have that τ ∈ St(δ 0 (P )). For any i ∈ {2, . . . , n}, we have that δ(t i θ) = t i δ 0 (θ). Let τ i = t i δ 0 (θ) for any i ∈ {2, . . . , n}.

Thanks to Proposition 1, we know that:

• there exists A 1 ∈ S out (τ ) such that Label(exec| R1 ) ⊆ A 1 ; and • for any i ∈ {2, . . . , n}, there exists A i ∈ dep(τ i ) such that Label(exec| Ri ) ⊆ A i . Therefore, we deduce that there exists A ∈ S check (P ) such that Label(exec) = Label(exec| W ) ⊆ A. Let W be the set of all the variables occurring in the test witnessing the non-inclusion. We have seen that there exists A ∈ dep(P ) such that Label(exec) = Label(exec| W ) ⊆ A, and this allows us to conclude.

Fig. 1 .

 1 Fig. 1. Semantics for processes

Theorem 1 .

 1 Let P be a protocol type-compliant w.r.t. (∆ 0 , δ 0 ). If P tr = = ⇒ (P; φ; σ; i) then there exists a well-typed execution P tr = = ⇒ (P; φ ; σ ; i) such that tr = tr.

Fig. 2 .

 2 Fig. 2. Computation of dep(β 2 ).

Fig. 3 .

 3 Fig. 3. Definitions of S reach , Stest, and S check .

Theorem 1 .

 1 Let P be a protocol type-compliant w.r.t. (∆ 0 , δ 0 ). If P tr = = ⇒ (P; φ; σ; i) then there exists a well-typed execution P tr = = ⇒ (P; φ ; σ ; i) such that tr = tr.

Fig. 4 .

 4 Fig. 4. Properties of dep

  is the smallest index such that xσ and u j0 σ unify and σ 0 = mgu(xσ, u j0 σ).

			(i : new n.P P; φ; σ; i)	τ -→	(i : P { m / n } P; φ; σ; i)
						where m ∈ N is a fresh name.
	NULL		(i : 0 P; φ; σ; i)	τ -→	(P; φ; σ; i)
	PAR		(i : (P | Q) P; φ; σ; i)	τ -→	(i : P i : Q P; φ; σ; i)
	REP		(i :!P P; φ; σ; i)	τ -→	(i : P	i :!P P; φ; σ; i)
				with P a copy of P where bound variables are renamed.
	OUT-CH	(i : new c .out(c, c ).P P; φ; σ; i)	out(c,c ) -----→ (i : P { c / c } P; φ; σ; i)
						where c is a fresh channel name.
	MATCH ({i : match x with (u 1 → P 1 | . . . | u j → P j )} P; φ; σ; i)	τ -→	(i : P j0 P; φ; σ σ 0 ; i)
	where j 0 MOVE	(P; φ; σ; i)	phase i ----→ (P; φ; σ; i )	with i > i.
	PHASE	(i : i : P P; φ; σ; i)	τ -→	(i : P P; φ; σ; i)
	CLEAN	(i : P P; φ; σ; i )	τ -→	(P; φ; σ; i )	when i > i.

etc

  Definition 4. A protocol P is type-compliant w.r.t. a typing system (∆ init , δ) if• for every t, t ∈ ESt(unfold 2 (P )) we have that t and t unifiable implies that δ(t) = δ(t ). • for every construction match x with (u 1 → P 1 | . . . | u j → P j ) occurring in P , we have that δ(x) = δ(u 1 ) = . . . = δ(u j ). Continuing our running example, we have that P DS (and P DS as well) is type-compliant w.r.t. (T DS , δ DS ) given in Example 9. Indeed, since k i , k i , and x i , x i (with

	Example 11. i ∈ {1, 2}) are given the same type, we have that any two
	unifiable encrypted subterms occurring in unfold 2 (P DS ) (those
	terms are listed in Example 10) have the same type.

1 )

 1 For each almost destructor-only and asap recipe R such that Rφ↓ is a (resp. atomic) message, Rψ↓ is a (resp. atomic) message. 2) For each C[x 1 , . . . , x n ] a strict/direct subterm of a shape sh f with f ∈ Σ c , for each almost destructoronly and asap recipe R such that Rφ↓ is a message. If Rφ↓ = C[x 1 , . . . , x n ]θ for some θ, then Rψ↓ = C[x 1 , . . . , x n ]θ for some θ . 3) For each simple recipe R and each almost destructoronly recipe R such that Rφ↓, R φ↓ are messages, if Rφ↓ = R φ↓, then we have that Rψ↓ = R ψ↓. Actually, we can assume in addition that one recipe is asap, and the other one is subterm asap w.r.t. φ. 4) For each rule g(t 1 , . . . , t n ) → r in R test ∪ R d , for each almost destructor-only and asap recipe R 1 , and simple asap recipes R 2 , . . . , R

n such that R 1 φ↓, . . . , R n φ↓ are messages, if (R 1 φ↓, . . . , R n φ↓) = (t 1 , . . . , t n )θ for some θ, then (R 1 ψ↓, . . . , R n ψ↓) = (t 1 , . . . , t n )θ for some θ .

  The test T is of the form R such that R is a recipe,Rφ↓ = C[x 1 , . . . , x n ]θ where C[x 1 , . . . , x n ] is a strict direct subterm of a shape sh f . • Case R is not in normal form w.r.t. . Let R = R .Since Rφ↓ is a message, we deduce that R φ↓ = Rφ↓ (Lemma 1). We have already seen (item 1) that Rψ↓ is a message too and thus we have that R ψ↓ = Rψ↓. Since R holds in φ, i.e. Rφ↓ = C[x 1 , . . . , x n ]θ for some θ, we have that R holds in φ, i.e. R φ↓ = C[x 1 , . . . , x n ]θ for the same θ. Relying on our induction hypothesis applied on test R we deduce that the test R holds in ψ, i.e. R ψ↓ = C[x 1 , . . . , x

n ]θ for some θ , and thus we conclude that R holds in ψ, i.e. Rψ↓ = C[x 1 , . . . , x n ]θ .

• Otherwise, as in the previous case, thanks to Lemma 3, we deduce that R is a simple recipe. In case

R = f(R 1 , . . . , R n ) for some f ∈ Σ c , then we have that C = f(C 1 , . . . , C n ). Applying our induction hypothesis on each R i with term C i [_]

which is also a strict direct subterm of a shape, we have that R i φ↓ = C i [x 1 , . . . , x n ]θ, and thus we deduce that R i ψ↓ = C i [x 1 , . . . , x n ]θ i for each i, and since a subterm of a shape is a linear term, we get the result by considering θ the union of the θ i . Otherwise, we have that R is an almost destructor-only recipe. As in the previous case (see the test T is a recipe R such that Rφ↓ is a message -item 2), we can show that R is subterm asap. In case R is asap, we are done. Thus, it remains the case where R is subterm asap but not asap. We know that there exists an asap simple recipe R w.r.t. φ such that R = R holds in φ. By hypothesis, we know that φ simple s ψ, and thus by definition of simple s

•

  Otherwise, as in the previous cases, thanks to Lemma 3, we know that R and R are simple, i.e.R = C[R 1 , . . . , R k ] and R = C [R 1 , . . . , R ],where C, C are constructor contexts and R i (1 ≤ i ≤ k) as well as R j (1 ≤ j ≤ ) are almost destructor-only recipes. If neither C nor C is empty (that is, neither R nor R is almost destructor-only) then root(R) = root(R ), and thus we conclude relying on our induction hypothesis applied on direct subterms of R and R . Otherwise, we assume w.l.o.g. that R is an almost destructor-only recipe, and R is simple. In case R is not subterm asap, it means that there exists 1 ≤ i 0 ≤ k such that R| i0 is not asap. Let R i0 be an asap recipe w.r.t. φ such that R| i0 φ↓ = R i0 φ↓.

The research leading to these results has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No 714955-POPSTAR), as well as from the French National Research Agency (ANR) under the project TECAP, and the Chaire IA ASAP.

A formal defintion is given in Appendix

• either e 2 is a type τ , and τ is a direct subtype of τ ;• or e 2 is an output label.

A. How to compute the empty dependencies We start with an example showing that this task it is not obvious.

Example 22. Let P = new s.in α (c, s).out β (c, s). We have that dep(δ 0 (s)) = ∅. Indeed, consider the equations for dep (note that δ 0 (s) is a cv-alien type as there are no variables or constants in P ) with i > 0.

We have that dep i-1 (⊥) = {∅} and that dep 0 (δ 0 (s)) = dep 0 (α) = dep 0 (β) = ∅. Thus, dep i (δ 0 (s)) = ∅ for each i. We can check that it is a solution of the following equation (resulting from the defining equations above).

dep(δ 0 (s)) = {{β}} ⊗ {{α}} ⊗ dep(δ 0 (s))

It confirms that it is a correct solution. So, there is a type δ 0 (s) such that the recursive calls defined by the equations loop, but dep(δ 0 (s)) = ∅.

To find the labels and types α such that dep(α) = ∅, we define the algorithm Empty. This algorithm takes (α, p) as input, where α is a label or type and p is a path (actually a sequence of labels), and returns b ∈ {True, False}. Intuitively, Empty(α, p) is used to know if dep(α) is empty. We also define auxiliary functions Paths and m(α, p). We want to prove that Empty(α, p) tells if dep(α) = ∅. Paths(α, ) represents the set of paths explored during the execution of Empty(α, ) while m(α, p) is the number of remaining (inductive) steps required to reach a result. They are defined as: Empty(β j i , p.α) for β j i ∈ next(α), set E as E = {p.α} ∪ ∪ i,j (Paths(β j i , p.α)). Empty(α, p) returns b, Paths(α, p) returns E, and m(α, p) = 1 + max i,j (m(β j i , p.α)). Note that, as there are only a finite number of labels and types, and as the paths cannot contain twice the same label and type, those algorithms terminate. Note that all elements of Paths(α, p) are of length at least 1. We prove the following lemma.

Lemma 12. For any label or type α and any path p, we have Empty(α, p) = True iff dep i (α) = ∅ for any i ≤ m(α, p).

Proof. We do the proof by induction on m(α, p).

Base case. If m(α, p) = 0, then either dep 0 (α) = A(α) = ∅, and in this case Empty(α, p) = False, or A(α) = ∅ and thus dep 0 (α) = ∅ and Empty(α, p) = True. It proves the base case.

Inductive case. Let n be an integer. Assume that the result is true for any α, p such that m(α, p) ≤ n. Let α, p be such that m(α, p) = n + 1. Then (as m(α, p) = n + 1 > 0):

for β j i ∈ next(α) and we have (as

But B(α) = ∅, so dep n+1 (α) = ∅ if the following formula φ evaluates as True.

Thus formula (3) evaluates as True iff φ evaluates as True. Thus dep n+1 (α) = ∅ iff Empty(α, p) = True. As dep i (α) ⊆ dep n+1 (α) for any i ≤ n + 1, it concludes the proof.

Lemma 13. Let α be a label or type. If p ∈ Paths(α, ) then for any prefix q = of p we have q ∈ Paths(α, ).

Proof. We prove the following result by induction on m(α, p 0 ): if p ∈ Paths(α, p 0 ), then p = p 0 .α.q, and for any prefix q of q, we have p 0 .α.q ∈ Paths(α, p 0 ).

Base case. Assume m(α, p 0 ) = 0. Then Paths(α, p 0 ) = {p 0 .α}. Let p ∈ Paths(α, p 0 ). We have p = p 0 .α (so q = ). For any prefix q of q, we have q = and p 0 .α.q = p ∈ Paths(α, p 0 ). Inductive case. Assume the result is true for any α, p 0 such that m(α, p 0 ) ≤ n. Let α, p 0 be such that m(α, p 0 ) = n + 1 > 0. So we have that Paths(α, p 0 ) = {p 0 .α} ∪ ∪ i,j Paths(β j i , p 0 .α) for β j i ∈ next(α). Let p ∈ Paths(α, p 0 ). Either p = p 0 .α, and the proof of the base case applies; or p ∈ Paths(β j i , p 0 .α) for some β j i ∈ next(α). We have that m(β j i , p 0 .α) < m(α, p 0 ) = n + 1 thus m(β j i , p 0 .α) ≤ n and induction hypothesis applies. So p = p 0 .α.β j i .q and for any prefix q of q, we have: p = p 0 .α.β j i .q ∈ Paths(β j i , p 0 .α) Let q be a prefix of β j i .q. Either q = β j i .q and we get: p = p 0 .α.q ∈ Paths(β j i , p 0 .α) ⊆ Paths(α, p 0 ) Or q = and p = p 0 .α which has been handled before. This concludes the inductive case.

If we apply the above result to p ∈ Paths(α, ), we get that p = α.q and that for any prefix q of q, α.q ∈ Paths(α, p 0 ). As α is a prefix of any non-empty prefix of p, we get the result.

The following lemma aims to help us proving that there Empty has the expected property of indicating the empty results. However, it is not always true: for example, Empty(α, α) = True just by definition of Empty, and even if dep(α) = ∅. So, we have to restrict ourselves to paths that actually occur inside a computation, that is elements of Paths(α, ). But even for those paths, it might be that Empty(α, ) = True, but that Empty(α, p) = False for some path p, as examplified below. Thus, we have to handle the case where Empty(α, p) is true, but some other computations will make that Empty(α, ) is false, or more generally Empty(α, q) = False for some prefix q of p. This is done by possible conclusion (b) in the following lemma. This possible conclusion will be impossible anyway when the lemma is called in Proposition 2 with p = . Lemma 14. Let α be a label or a type. Let p.β ∈ Paths(α, ). If Empty(β, p) = True, then (a) dep(β) = ∅ or (b) p = p 0 .γ.p 1 for some p 0 , γ, p 1 such that Empty(γ, p 0 ) = False.

Proof. First, we prove the following result by induction on Inductive case. Let k 0 be such that the result is true for k 0 . Assume toward contradiction that the result is not true for k 0 + 1. We can consider a minimal k such that there is a p.β ∈ Paths(α, ) for which k + |p| = k 0 + 1, Empty(β, p) = True but dep k (β) = ∅ and there is no p 0 , γ, p 1 such that p = p 0 .γ.p 1 and Empty(γ, p 0 ) = False. We consider the cases in the computation of Empty(β, p). gives us a contradiction as p 0 = q 0 .γ.q 1 implies that p = q 0 .γ.q 1 .p 1 , and we have Empty(γ, q 0 ) = False; or Empty(β, p 0 ) = False and there is a contradiction.

By hypothesis, we have Empty(β, p) = True. Assume that one of the Empty(β j i , p.β) = True and has property (b), that is there is a γ, a p 0 and a p 1 such that p.β = p 0 .γ.p 1 and Empty(γ, p 0 ) = False. We know that (γ, p 0 ) = (β, p) as Empty(β, p) = True. So p = p 0 .γ.p 1 and p 1 = p 1 .β, so we get property (b) which is a contradiction. So from now we can assume ( ) that for each β j i ∈ next(β), either Empty(β j i , p.β) = False or property (b) is false. We also have (as k > 0 and A(α) = ∅):

But by minimality of k and by our assumption ( ), for each β j i such that Empty(β j i , p.β) = True, we have that

As Empty(β, p) = True, we have that for each i there exists a j such that Empty(β j i , p.β) = True. It implies that for each i there exists a j such that dep(β j i ) = ∅ and thus that φ is true, so dep k (β) = ∅. It concludes the proof of the inductive case. Now remark that dep(β) = ∪ k dep k (β) so case (a) rewrites as dep(β) = ∅ as it is true for any k 0 .

We prove the expected result that the Empty algorithm determines the α such that dep(α) = ∅.

B. How to compute dep in practice (dep )

In this section, we define algorithm dep and we prove it coincides with dep. More precisely, dep always terminates, and it returns either ⊥ when dep contains an infinite multiset; or the same result as dep when it is a finite set of finite multisets. Algorithm dep uses Empty to avoid looping on empty dependencies.

Algorithm dep .: We define two operators ⊗ and ∪ such that:

Intuitively, ⊥ represents a set that has an infinite multiset as an element.

Then, for α a label or a type, we define dep (α, p) and m (α, p) as:

Empty(α, ) = False; • Otherwise, as:

and m (α, p) = 1 + max i,j m (β j i , p.α). The computation of dep terminates as there are only a finite number of labels and types, so the length of the paths p is bounded (there can be no repetition in p). Moreover, if dep (α, ∅) = ⊥, it is finite and each of the multisets included in dep (α, ∅) are finite as they are computed in a finite number of steps.

Our goal is to prove that dep (α, ∅) = dep(α) if dep(α) is finite, and dep (α, ∅) = ⊥ if dep(α) is infinite (for any type or label α).

Lemma 15. For any label or type α, for any path p, if dep (α, p) = ∅ then Empty(α, p) = True.

Proof. We prove the result by induction on m(α, p).

Inductive case. We assume that the result is true for any m(α, p) ≤ n and we want to prove it is true for m(α, p) = n+1. Let α, p be such that m(α, p) = n+1 > 0. By definition of m(α, p), we know that (with next(β) = {β j i | i, j}): Empty(α, p) = ∧ i ∨ j Empty(β j i , p.β) Moreover, as dep (α, p) = ∅, we have either α ∈ p and Empty(α, p) = True (which is the result); or:

As dep (α, p) = ∅, A(α) = ∅, and:

Empty(α, p) = ∧ i ∨ j Empty(β j i , p.β) For each i, j, we have that m(β j i , p.β) < m(α, p) = n + 1. Therefore induction hypothesis applies and for each dep (β j i , p.α) = ∅ we have Empty(β j i , p.α) = True. As dep (α, p) = ∅, for each i there is a j such that dep (β j i , p.α) = ∅. Thus for each i there is a j such that Empty(β j i , p.α) = True. It implies that Empty(α, p) = True.

From this, we can deduce the following lemma. Lemma 17. If p is a suffix of q, then m (α, p) ≥ m (α, q). Proof. We do the proof by induction on m (α, p). If m (α, p) = 0, then either Empty(α, ) = True or α ∈ p and thus α ∈ q. Thus m (α, q) = 0 in both cases. Now, assume the result is true for any α, p such that m (α, p) ≤ k for some k ≥ 0. Let α, p such that m (α, p) = k + 1 and q such that p is a suffix of q. As m (α, p) = k + 1 > 1, we have m (α, p) = 1 + max i,j m (β j i , p.α). Either m (α, q) = 0 and thus m (α, q) ≤ m (α, p) or m (α, q) > 0 and m (α, q) = 1+max i,j m (β j i , q.α). We have that m (β j i , p.α) ≤ k for each i, j, and p.α is a suffix of q.α so induction hypothesis applies and m (β j i , p.α) ≥ m (β j i , q.α) for each i, j. We conclude that m (α, q) ≤ m (α, p). We have m (β j i , α.p) < m (α, p) = k + 1 for every i, j by definition of m . So induction hypothesis applies and for any i, j, dep (β j i , p.α) = dep(β j i ) if dep (β j i , p.α) = ⊥. As dep (α, p) = ⊥, for each i 0 , j 0 such that dep (β j0 i0 , p.α) = ⊥, there must be a j 1 such that dep (β j1 i0 , p.α) = ∅. As ∅ = ⊥, it implies by induction hypothesis that dep(β j1 i0 ) = ∅ and thus that ⊗ j dep(β j i0 ) = ∅. We deduce: ⊗ j dep(β j i0 ) = ⊗ j dep (β j i0 , p.α)

Given i 1 such that there is no j 0 such that dep (β j i0 , p.α) = ⊥, we also have (as the factors are equal): ⊗ j dep(β j i1 ) = ⊗ j dep (β j i1 , p.α)

Thus we deduce dep(α) = dep (α, p). It concludes the inductive case.

Conclusion.

We have proved that for any α,p such that dep (α, p) = ⊥, we have dep (α, p) = dep(α). The result is the case where p = .