Véronique Cortier

Stéphanie Delaune

Vaishnavi Sundararajan

A decidable class of security protocols for both reachability and equivalence properties

Keywords: Security protocols, verification, privacy properties

We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be "simple", meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

Introduction

Security protocols are notoriously difficult to design and analyse. In this context, formal methods have proved their interest to help to detect automatically flaws and provide better security guarantees. For example, they have been used during the standardisation process to detect and correct flaws in the Transport Layer Security (TLS) 1.3 protocol [START_REF] Delignat-Lavaud | Implementing and proving the TLS 1.3 record layer[END_REF]. In the context of voting, the production of symbolic proofs is now a legal requirement in Switzerland [START_REF]Exigences techniques et administratives applicables au vote électronique[END_REF].

V. Cortier LORIA, CNRS, France E-mail: veronique.cortier@loria.fr (corresponding author) S. Delaune, V. Sundararajan IRISA, CNRS & Univ Rennes, France E-mail: stephanie.delaune@irisa.fr Symbolic models for security protocols abstract away how cryptographic primitives are implemented. They instead focus on the analysis of the flow of the protocols. Thanks to this level of abstraction, security analysis is amenable to automation. Several tools can now, given the abstract specification of a protocol, automatically find flaws or prove security. Examples of popular tools are ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF], Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF], 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], or Scyther [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis of security protocols[END_REF]. However, even simple security properties like confidentiality are undecidable in general [START_REF] Durgin | Undecidability of bounded security protocols[END_REF]. To retrieve decidability, one standard assumption is to bound the number of sessions, which corresponds to analysing the protocol when it is run a finite number of times. In that case, reachability properties like confidentiality and authentication properties are (co)-NP-complete [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete[END_REF]. Privacy properties like anonymity, vote secrecy or unlinkability are rather expressed as equivalence properties. For example, anonymity corresponds to the fact that an attacker should not be able to distinguish whether Alice is making a payment or Bob is making a payment. Such properties have been studied more recently but can also be shown to be decidable for a bounded number of sessions [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF][START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] for a large class of cryptographic primitives and protocols. Several tools have even been proposed to decide privacy properties for a bounded number of sessions such as SPEC [START_REF] Dawson | Automating open bisimulation checking for the spi-calculus[END_REF], APTE [START_REF] Cheval | Apte: an algorithm for proving trace equivalence[END_REF] and Akiss [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF], and Sat-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF]. However, protocols are executed a large number of times in practice (think of the number of TLS connections within a day). Some tools such as ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF] or Scyther [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis of security protocols[END_REF] can actually handle an unbounded number of sessions although they are not guaranteed to terminate. Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF] provides an automatic mode but often requires some help from the user. This is actually one of the main features of the tool: when it cannot conclude by itself, it offers an interactive mode and the possibility to state intermediary properties (lemmas). In practice, these tools work well, at least for reachability properties. So a remaining open problem for the last ten years is to characterise a decidable fragment of security protocols that captures most real protocols.

Related work.

A few decidable classes of protocols have been identified for an unbounded number of sessions. Several of them consider protocols without nonces (see e.g. [START_REF] Durgin | Undecidability of bounded security protocols[END_REF][START_REF] Comon-Lundh | New decidability results for fragments of first-order logic and application to cryptographic protocols[END_REF] for reachability properties and [START_REF] Chrétien | From security protocols to pushdown automata[END_REF][START_REF] Chrétien | Typing messages for free in security protocols: the case of equivalence properties[END_REF] for equivalence). However, protocols do use nonces in practice. If we restrict our attention to protocols with nonces, there is actually no decidability result for equivalence properties, except [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] which this paper builds upon and that we discuss later on. For reachability properties, and more precisely secrecy, Lowe [START_REF] Lowe | Towards a completeness result for model checking of security protocols[END_REF] shows decidability provided that protocols rules obey a strict format (no ciphertext forwarding for example) and assuming that agents are able to check this format when they receive messages. Typically, this result assumes that an agent can never confuse a nonce with a key, an agent name, or a ciphertext. In [START_REF] Ramanujam | Tagging makes secrecy decidable with unbounded nonces as well[END_REF], Ramanujam and Suresh obtain decidability assuming a rather severe tagging scheme, where each ciphertext has to include a fresh, shared session identifier. They do not cope with ciphertext forwarding. Dougherty and Guttman [START_REF] Dougherty | Decidability for lightweight Diffie-Hellman protocols[END_REF] have proposed a decidability result dedicated to Diffie-Hellman protocols. The result that is closest to ours is probably the one from Sybille Fröschle [START_REF] Fröschle | Leakiness is decidable for well-founded protocols?[END_REF], who has proposed a decidability result for the "leakiness" property and the class of well-founded protocols, with encryption and concatenation only (no signature nor hash). A protocol is secure w.r.t. leakiness if all data are either public or secret. In particular, it is not possible to prove security for protocols with temporary secrets, e.g. session identifiers that are not immediately revealed. Moreover, ciphertext forwarding is again prohibited and as in [START_REF] Lowe | Towards a completeness result for model checking of security protocols[END_REF] a typed model is considered.

Our result relies on a small-attack property proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. This property says that for some class of protocols, if there is an attack, then there is a welltyped attack, that is an attack where all messages comply with the expected format. This nicely restricts the search space when looking for attacks. This result was already used in [START_REF] Cortier | Efficiently deciding equivalence for standard primitives and phases[END_REF] to derive an efficient procedure for deciding trace equivalence, but for a bounded number of sessions.

Our contribution. We identify a new class of protocols with nonces, for which both reachability and trace equivalence are decidable, for an unbounded number of sessions. Our class covers all standard cryptographic primitives (deterministic and randomised symmetric and asymmetric encryptions, hashes, and signatures). Our class makes three main assumptions.

simple protocols: We assume that each role of a protocol can be written as a succession of inputs and outputs on a dedicated channel. This corresponds to the idea that each process is identified by an IP address (address of the machine) and some protocol and session identifier so that sessions cannot be mixed up. We further assume that each role has no else branch, that is, makes only positive tests (e.g. equality between a received value and a previously sent nonce). type compliance: We assume that each encrypted message of the protocol can be given an expected format (formally, a type) so that any two unifiable encrypted messages have the same format. When necessary, this can usually be enforced by tagging messages, that is, adding some tag (e.g. a number) that avoids confusion between two different messages of the protocol. This is a good practice anyway that rules out many attacks. Note that the adversary can of course deviate from the expected format. acyclic dependency graph: We associate with each protocol its dependency graph. A node of this graph corresponds to an action (input or output).

An edge corresponds to a dependency. There are two main kinds of dependencies: sequential dependencies (some action may only happen after other previous actions) and data dependencies (an input can be built using parts of messages occurring in some outputs). Our decidability result requires this dependency graph to be acyclic.

The two first conditions are easy to check and often met by protocols from the literature. Checking the last condition (acyclicity) requires the construction of the dependency graph, which can be done by applying a simple polynomial algorithm. Our experiments on a dozen of protocols of the literature show that many protocols of the literature have an acyclic graph, including for example some of the protocols embedded in the biometric passport. Interestingly, our decidability result provides an explicit bound on the number of sessions: for each protocol that falls into our class, we can bound the number of sessions that need to be considered to find an attack. This bound is however very high and currently clearly out of reach of existing tools like 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] for a bounded number of sessions. Our decidability result is established in two main steps. First, we build on the small-attack property proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. This property says that for simple and type-compliant protocols, if there is an attack, then there is a well-typed attack, that is an attack where all messages comply with the expected format. We adapt this result to our context. We introduce the notion of an honest type, for elements that only appear in key position. We show that we can always consider an attack trace that is honest-free. Such a trace does not involve any constant of honest type, even though these constants are freely available to the attacker. Then, considering the dependency graph as sketched above, we show that a well-typed execution can be mapped to a path in the graph, hence bounding the length of the execution, hence the number of sessions.

We actually prove our result first for a simple definition of dependency graph that, however, often yields to cyclic graphs. We then provide a criterion in order to soundly remove edges from the graph, hence obtaining more likely acyclicity. Our approach is flexible enough to allow further refinements of the definition of the dependency graph, if needed.

Limitations. As mentioned earlier, our result does not cope with protocols with else branches, which prevents e.g. to fully model the BAC protocol used in the passport (we cannot model the fact that the protocol sends out error messages when some checks fail). As for many other decidability results, we consider all standard cryptographic primitives but we do not allow for a general equational theory nor for operators like Exclusive Or or modular exponentiation, which are notoriously hard to verify. We are not aware of any decidability result for an unbounded number of sessions (for protocols with nonces) that would cover these aspects.

Comparison with the earlier result [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF]. We build upon an earlier result presented at CSF'15 [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] that establishes decidability of trace equivalence for protocols with symmetric encryption, with the same assumptions regarding simplicity, type-compliance, and acyclicity of the dependency graph. We extend this work to protocols with phases and to all standard primitives. This required in particular to provide a new characterisation of a sufficient set of tests for static equivalence, which in turn, yields a more subtle computation on the bound on the number of sessions. Moreover, decidability was established initially in [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] for trace equivalence only, we show how to adapt the approach to reachability.

Security protocol model

Security protocols are often modelled through a process algebra, in the spirit of the applied-pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], that defines a small abstract programming language, well suited for protocols. Our result is built upon a typing result [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] that guarantees that if there is an attack, there is a well-typed attack, hence reducing the search space. Therefore, we consider here the process algebra used in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] to established this typing result. Our decidability result covers all standard primitives. Thus, for the sake of readability, we instantiate the framework of [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] to the case of all the standard primitives while [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] consider a more general class of primitives.

Term algebra

As usual, messages are modelled by terms. Intuitively, terms are enough to represent how a message has been produced and how it can be decomposed. Private data, such as long-term and short-term keys or nonces, are represented through an infinite set of names N . Public data, i.e. any data known by the attacker, such as agent names or attacker's nonces or keys, are modelled relying on an infinite set Σ 0 of constants. Constants are all initially known to the attacker. The set of constants is infinite to allow an attacker to use an arbitrary number of nonces and keys. We also consider two sets of variables X and W. Variables in X typically refer to unknown parts of messages expected by protocol participants during the protocol execution, whereas variables in W are used to store messages learnt by the attacker so far. All these sets are assumed to be pairwise disjoint. Data are either constants, variables, or names.

Cryptographic primitives are represented by function symbols. We consider the following signature Σ = Σ c ∪ Σ d ∪ {check} where:

-Σ c = {aenc, raenc, senc, rsenc, pub, ok, sign, vk, hash} ∪ { n | n ≥ 2}, and -Σ d = {adec, radec, sdec, rsdec, getmsg} ∪ {proj n j | n ≥ 2 and 1 ≤ j ≤ n}. This signature comprises the standard primitives. Each symbol comes with an arity. The symbol aenc, of arity 2, stands for asymmetric encryption, with public key constructed using the function pub. A randomised version of asymmetric encryption is denoted raenc, of arity 3, that takes as additional argument the randomness used to compute the ciphertext. The functions adec and radec are the corresponding decryption functions (each of arity 2). Similarly, senc and rsenc denote respectively symmetric and randomised symmetric encryptions, with sdec and rsdec as corresponding decryption functions. The hash function is modelled by hash, of arity 1, while n-tuples are built using n (of arity n). Then proj n j simply retrieves the jth component of a n-tuple. Finally, signatures are expressed with sign and corresponding verification function check and verification key built using vk. While check can intuitively be seen as a destructor (it allows to inspect a signature), note that the symbol check is neither a destructor nor a constructor. This allows us to devise finer results later on, where we show that the adversary does not need to use check when computing terms (since it only yields the ok constant term).

The set of terms built from a signature F and a set of data D is denoted T (F, D). We denote vars(u) the set of variables that occur in a term u, and a term u is ground if it contains no variable. The application of a substitution σ to a term u is written uσ. We denote dom(σ) its domain and img(σ) its image. The positions of a term are defined as usual. Given a term u, we denote root(u) the function symbol occurring at position in u. The set St(u) denotes the set of subterms of u, and Cst(u) denotes the set of constants from Σ 0 occurring in u. These notations are extended as expected to sets of terms. Two terms u 1 and u 2 are unifiable if there exists a substitution σ such that u 1 σ = u 2 σ.

We consider two sorts: atom and bitstring. The elements of sort atom represents atomic data like nonces or keys while bitstring models arbitrary messages. Names in N have sort atom, whereas constants in Σ 0 contains an infinite number of constants of both sorts. Any f ∈ Σ c comes with its sorted arity:

Given D ⊆ Σ 0 ∪ N ∪ X , the set T 0 (Σ c , D) is the set of terms t ∈ T (Σ c , D)
that are well-sorted, and such that for any aenc

(u, v) ∈ St(t) (resp. raenc(u, v, r) ∈ St(t)), v = pub(v ) for some v . Terms in T 0 (Σ c , N ∪ Σ 0 ) are called messages.
Intuitively, messages are terms with atomic keys, that is, asymmetric encryption can only be used with public keys of the form pub(k) where k is an atom and symmetric encryption can only be used with keys that are atoms. Since sorts are only used to define messages, destructors do not have sort. Terms with destructors can be "ill-sorted", only messages are required to be well-sorted.

The properties of the cryptographic primitives are reflected through the following convergent system of rewriting rules: sdec(senc(x, y), y) → x adec(aenc(x, pub(y)), y) → x getmsg(sign(x, y)) → x rsdec(rsenc(x, y, z), y) → x radec(raenc(x, pub(y), z), y) → x check(sign(x, y), vk(y)) → ok proj n i ( x 1 , . . . , x n n ) → x i with n ≥ 2 and 1 ≤ i ≤ n A term u can be rewritten into v if there is a position p in u, and a rewriting rule g(t 1 , . . . , t n ) → t 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. As usual, we denote by → * the reflexive-transitive closure of →, and by u↓ the normal form of a term u.

An attacker builds his own messages by applying 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 1

Let u 1 = aenc(sign(k , sk a ), pub(ek c )) with k , sk a ∈ N and ek c ∈ Σ 0 . This term represents the encryption of sign(k , sk a ) (the signature of k with the signing key sk a ) with the public key pub(ek c ). Note that the private key associated to pub(ek c ) is the public constant ek c and is known to the attacker. The recipe getmsg(adec(u 1 , ek c )) models the application of the decryption algorithm on top of u 1 using the key ek c followed by the application of the algorithm that allows one to extract a message from a signature.

We need also to define the notion of key position on constructor terms. In particular, this notion will be used on messages (and types).

Given a set D of data, a position p of a constructor term u ∈ T (Σ c , D) is a key position if either p = q.1 for some q such that root(u| q ) = {pub, vk}; or p = q.2 for some q such that root(u| q ) ∈ {senc, rsenc, sign}. We will denote KP(u) the set of all key positions of a term u. We denote by K(u) the subterms of u occurring at a key position in u, i.e. K(u) = {u | u = u| p for some p ∈ KP(u)}.

Example 2 Consider the term u 1 = aenc(sign(k , sk a ), pub(ek c )) and u 2 = pub(ek c ). We have that KP(u 1 ) = {21, 12}, and KP(u 2 ) = {1}.

Process algebra

We assume an infinite set Ch = Ch 0 Ch fresh of channels used to communicate, where Ch 0 and Ch fresh are infinite and disjoint. Intuitively, channels of Ch fresh will be used to instantiate channels when they are generated during the execution of a protocol. They should not be part of a protocol specification. We also assume an infinite set L used to label input and output actions of processes. Protocols are modelled through processes built by the following grammar:

P, Q := 0 | in (c, u).P | out (c, u).P | new n.P | (P | Q) | !P | new c .out(c, c ).P | i : P where u ∈ T (Σ c , Σ 0 ∪N ∪X ), n ∈ N , c, c ∈ Ch, ∈ L, and i ∈ N.
The process 0 simply represents the null process. A process in (c, u).P will receive a message of the form u on channel c, while process out (c, u).P emits message u on channel c. Then new c .out(c, c ).P is a special construction that allows one to create a new channel c , provided it is immediately emitted on a public channel c. This way, we allow an arbitrary number of public channels but disallow private ones. Then, as usual, P | Q is the parallel composition of P and Q, while !P represents the unlimited replication of P . Finally, i : P denotes that the process P will be executed at phase i. Phases are used to model protocols that are inherently divided into several steps, such as e-voting protocols (with setup, voting, and tallying phases). They are also convenient to model several security properties expressed as a game where, e.g., the attacker is first given the opportunity to interact with the protocol, and is then given a real or random key and he has to distinguish the two cases.

We denote fv (P) the variables occurring in P that are not bound by an input and we assume w.l.o.g. that variables are bound at most once. Note that once a variable is bound by an input, it may be later used in an input as a filtering argument. For example, the variable x is bound only once in in(c, x).in(c, x). This models the fact that the process will first input any message but will then expect exactly the same one. In contrast, the variable x is bound twice in in(c, x) | in(c, x), and we will not consider such a process. We will assume instead that variables have been properly renamed. We denote phase( ) the integer corresponding to the phase at which the action labelled occurs.

Example 3 We consider a variant of the Denning-Sacco protocol with signatures as given in [START_REF] Blanchet | Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. automatic verification of security protocols: formal model and computational model[END_REF]. The protocol aims at ensuring the secrecy of the message m exchanged encrypted with the symmetric key k. This key is freshly generated by A and sent to B in the first message. It can be informally described as follows:

A → B : aenc(sign(k, priv A ), pub B ) B → A : senc(m, k)
where pub B is the public encryption key of the agent B, and priv A is the private signing key of the agent A. This is a slight variant of the original protocol proposed by Denning and Sacco in which the identity of the agents A and B appear inside the signature [START_REF] Denning | Timestamps in key distribution protocols[END_REF]. This variant is vulnerable to an attack regarding the secrecy of the key k and the message m that will be explained in Example 4.

We model this protocol in our formalism through the two processes P A and P B representing respectively the role of A and the role of B.

P A = new k. out 1 (c A , aenc(sign(k, sk a ), pub(ek b ))). in 2 (c A , senc(x A , k)) P B = in 3 (c B , aenc(sign(x B , sk a ), pub(ek b ))). new m. out 4 (c B , senc(m, x B ))
We have that k, sk a , ek b , and m are names, whereas x A and x B are variables.

The name sk a represents the signing private key of the agent a whose associated verification key is vk(sk a ), and ek b is the private encryption key of the agent b and the associated public key is pub(ek b ).

Then, the protocol is modelled by the parallel composition of these two processes P A and P B together with a process P K that models the initial knowledge of the attacker. More precisely, P K reveals the public encryption keys and the verification keys to the attacker during an initialisation phase.

P DS = 0 : P K | 1 : !new c A .out(c 1 , c A ).P A | !new c B .out(c 2 , c B ).P B where P K = out K 1 (c 0 , pub(ek b )).out K 2 (c 0 , vk(sk b )). out K 3 (c 0 , pub(ek a )).out K 4 (c 0 , vk(sk a ))
We may want to consider a different scenario taking into account the presence of a dishonest agent c. We give below the process P A that corresponds to the role A played by a with a dishonest agent c. Below, k is a name, x A a variable, and ek c is a (public) constant from Σ 0 .

P A = new k . out 1 (c A , aenc(sign(k , sk a ), pub(ek c ))). in 2 (c A , senc(x A , k )).0
The one session of the initiatior role played by a with c and one session of the responder role played by b with a is modelled by the process P DS given below.

For the sake of simplicity, we only consider one session of each role.

P DS = 0 : P K | 1 : P A | P B
Note that the decryption key ek c of the agent c is modelled as a public constant and is thus implicitly known by the attacker. We do not need to reveal it explicitly.

Semantics

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

-P is a multiset of processes (not necessarily ground); φ = {w 1 m 1 , . . . , w n m n } is a frame, i.e. a substitution where w 1 , . . . , w n are variables in W, and m 1 , . . . , m n are messages; σ is a substitution such that fv (P) ⊆ dom(σ), and img(σ) are messages.

Intuitively, P represents the processes that still remain to be executed; φ represents the sequence of messages that have been learnt so far by the attacker, σ stores the value of the variables that have already been instantiated, and i is an integer that indicates the current phase. A configuration (P; φ; σ; i) such that φ = σ = ∅ and i = 0 is called initial.

The operational semantics of a configuration are induced by the relation α -→ over configurations and is defined in Figure 1. 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 observable actions tr, and 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. two configurations K and K , we write K tr = = ⇒ K if there exists a sequence α 1 . . . α n such that K α1...αn -----→ K and tr is obtained from α 1 . . . α n by erasing all occurrences of τ and erasing all labels: out (c, w) is replaced by out(c, w) and in (c, R) is replaced by in(c, R). Labels may also be omitted when writing K α1...αn -----→ K when they are not relevant.

New

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

trace(K) = {(tr, φ ) | K tr = = ⇒ (P; φ ; σ ; i ) for some configuration (P; φ ; σ ; i )}.
Example 4 Continuing Example 3, we consider the initial configuration K 0 = (P DS ; ∅; ∅; 0). As mentioned in Example 3, this variant of the Denning-Sacco protocol is vulnerable to an attack depicted in Figure 2. The attack relies on the fact that agent A starts a session with the dishonest agent C leading the agent C to know a valid signature sign(k , priv A ) on a key k that he can deduce. Then, agent C can pretend to be A and send this signature to B encrypted with the public key of B. Agent B will then accept this message and send his private message m intended to A, encrypted with the key k since he believes that he shares this key with A (whereas this key is known by the attacker). This attack is reflected by the following sequence tr 0 : out(c 0 , w 1 ).phase 1.out(c A , w 2 ).in(c B , R 0 ).out(c B , w 3 ) where R 0 = aenc(adec(w 2 , ek c ), w 1 ) corresponds to the message manipulation done by the attacker: he decrypts the message received from A and re-encrypt it with the public key of B. This sequence of actions leads to the frame φ 0 defined as follows:

φ 0 = {w 1 pub(ek b ), w 2 aenc(sign(k , sk a ), pub(ek c )), w 3 senc(m, k )}.
We have that (tr 0 , φ 0 ) ∈ trace(K 0 ).

Trace equivalence

Privacy properties are often modelled as equivalence of processes. We first start with the notion of static equivalence. Intuitively, two frames, that is two sequences of messages, are in static equivalence when an attacker cannot tell them apart. Definition 2 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 .

Example 5 Continuing Example 4, we consider the two following frames:

-

φ 1 = {w 1 pub(ek b ), w 2 aenc(sign(k , sk a ), pub(ek c )), w 3 senc(m 1 , k )}; -φ 2 = {w 1 pub(ek b ), w 2 aenc(sign(k , sk a ), pub(ek c )), w 3 senc(m 2 , k )}
where m 1 and m 2 are public constants from Σ 0 . We have that sdec(w 3 , R k )φ 1 ↓ = m 1 φ 1 ↓ where R k = getmsg(adec(w 2 , ek c )). This equality does not hold in φ 2 , hence φ 1 and φ 2 are not in static equivalence.

We can now define equivalence over processes. Intuitively, equivalence is meant to model the fact that an attacker cannot distinguish between two processes P and Q. We consider here the notion of trace equivalence stating that any observable sequence of actions in P can also be observed in Q and viceversa and that the resulting sequences of messages are in static equivalence. Definition 3 A configuration K is trace included in a configuration K , written K t K , if for every (tr, φ) ∈ trace(K), there exist (tr , φ ) ∈ trace(K ) such that tr = tr , and φ s φ . They are in trace equivalence, written K ≈ t K , if K t K and K t K.

Assume given two configurations K and K such that K t K . A witness of this non-inclusion is a trace tr for which there exists φ such that (tr, φ) ∈ trace(K) and:

either there is no φ such that (tr, φ ) ∈ trace(K ); or φ s φ for any φ such that (tr, φ ) ∈ trace(K ). This notion of trace equivalence slightly differs from the original one introduced by Abadi and Fournet in [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. In the original definition, frames are required 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]. Intuitively, a protocol can be modelled as a determinate process if no agent makes a non deterministic choice and if all agents emit on distinguishable channels.

Definition 4 A configuration K is determinate if whenever K tr = = ⇒ K 1 and K tr = = ⇒ K 2 for
some tr, K 1 = (P 1 ; φ 1 ; σ 1 ; i 1 ), and K 2 = (P 2 ; φ 2 ; σ 2 ; i 2 ) we have that φ 1 ∼ s φ 2 .

Hence, our reduction and decidability results are applicable to standard equivalence for determinate protocols. For protocols that are not determinate, our results still hold but only apply for our own notion of trace equivalence that is slightly weaker than standard trace equivalence.

Example 6 Continuing Example 3, we consider the protocol P DS that models a role of A played by a with c, and a role of B played by b with a. To model the fact that the message m sent by B for A should remain secret, we require that even if the attacker knows two possible values for m, say m 1 and m 2 , he should not be able to distinguish which of these values has been exchanged. The corresponding processes are P 1 DS and P 2 DS which are P DS in which m has been replaced respectively by m 1 and m 2 . Then, we consider the configuration K 1 = (P 1 DS ; ∅; ∅; 0) and K 2 = (P 2 DS ; ∅; ∅; 0). We can show that K 1 t K 2 (and K 2 t K 1 ) since m is not strongly secret due to the attack depicted in Figure 2. This is exemplified by the trace tr 0 given in Example 4 which leads to the frame φ 1 (resp. φ 2 ) starting with the configuration K 1 (resp. K 2 ), i.e. (tr 0 , φ 1 ) ∈ trace(K 1 ) and (tr 0 , φ 2 ) ∈ trace(K 2 ). We have that φ 1 s φ 2 (and φ 2 s φ 1 as well) as explained in Example 5.

To avoid this attack, names of the agents should be included in the signature sent by A to B.

Simple processes

We consider a fragment of processes, the class of simple processes, similar to the one introduced in [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF]. This corresponds to protocols where each role can be seen as a sequence of inputs and outputs on a specific channel, distinct for each session. Definition 5 A simple protocol P is a ground process 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 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 ), and j ∈ N. Moreover, we assume that the channel names c 1 , . . . , c n , c n+1 , . . . , c n+m are pairwise distinct.

Example 7 Note that the processes P DS and P DS given in Example 3 are simple.

We sometime denote by P the initial configuration ({P }; ∅; ∅; 0), and we denote by Terms(P ) the set of all terms occurring in P , i.e. terms u such that out(c, u) (resp. in(c, u)) occurs in P .

Given a simple protocol P , and 1 , 2 ∈ L(P ), we say that 2 directly follows 1 in P if both actions are in sequence in the description of P , with 2 after 1 , and no other visible action in between. When some other visible actions occur between 1 and 2 , we simply say that 2 follows 1 .

Simple protocols are determinate. Actually, given K 1 and K 2 such that P tr = = ⇒ K 1 = (P 1 ; φ 1 ; σ 1 ; i 1 ) and P tr = = ⇒ K 2 = (P 2 ; φ 2 ; σ 2 ; i 2 ) for some tr, we have that φ 1 and φ 2 are equal up to some α-renaming. Thus, considering two simple protocols P and Q, a witness of non-inclusion for P t Q is a trace (tr, φ) ∈ trace(P ) such that:

either there is no φ such that that (tr, φ ) ∈ trace(Q); or in case such a φ exists, we have that φ s φ .

Why do we consider simple protocols? This assumption is very helpful to prove trace equivalence. It allows to precisely map each action of P to an action of Q thanks to the fact that given a channel name and a trace, only one process can produce this action. We could probably relax this assumption when we consider reachability properties only. However, the proofs are easier when assuming simple protocols.

First decidability results for reachability and trace equivalence

In this section, we state our first decidability result for reachability and trace equivalence. We introduce the notion of type-compliance, which intuitively enforces that messages that can be confused within a protocol must have the same type. We also define the dependency graph of a protocol, which reflects dependencies between messages of a protocol. We show that reachability properties as well as trace equivalence are both decidable for simple protocols that are type-compliant and that have an acyclic dependency graph.

Type-compliance

We consider here typing systems that preserve the structure of terms. They are defined as follows: Definition 6 A typing system is a pair (∆ 0 , δ 0 ) where ∆ 0 is a set of elements called initial types, and δ 0 is a function mapping data in Σ 0 N X to types τ generated using the following grammar:

τ, τ 1 , τ 2 = τ 0 | f(τ 1 , . . . , τ n ) with f ∈ Σ c and τ 0 ∈ ∆ 0
We further assume the existence of an infinite number of constants in Σ 0 (resp. variables in X , names in N ) of any type. Then, δ 0 is extended to constructor terms as follows:

δ 0 (f(t 1 , . . . , t n )) = f(δ 0 (t 1 ), . . . , δ 0 (t n )) with f ∈ Σ c .
A type can be seen as a term, we will assume that initial types are of sort atom, and we extend the notion of being well-sorted from terms to types.

Consider a configuration K and a typing system (∆ 0 , δ 0 ). An execution K tr = = ⇒ (P; φ; σ; i) is well-typed if σ is a well-typed substitution, i.e. every variable of its domain has the same type as its image.

Example 8 We continue our running example with simple protocols P 1 DS and P 2

DS

as defined in Example 7. We consider the typing system generated from the set T DS = {τ sk , τ skc , τ ek , τ ekc , τ k , τ m } of initial types, and the function δ DS that associates the expected type to each constant/name (δ

DS (sk a ) = δ DS (sk b ) = τ sk , δ(sk c ) = τ skc , δ DS (m) = δ DS (m 1 ) = δ DS (m 2 ) = τ m , δ DS (k ) = τ k , . . . )
, and the following types to the variables:

δ DS (x A ) = τ m , and δ DS (x B ) = τ k .
We now introduce the notion of encrypted subterms. We write ESt(t) for the set of encrypted subterms of t, i.e. the set of subterms that are not headed by a tuple operator.

ESt(t) = {u ∈ St(t) | root(u) ∈ {aenc, raenc, senc, rsenc, sign, hash, pub, vk}}
This notion is extended as expected to sets of terms, processes, frames, and initial configurations.

We will require that any two unifiable encrypted subterms appearing in the specification of a protocol have the same type. For this, we need to rename variables under replication since, intuitively, such variables are refreshed at each new session. Formally, given a simple protocol P , we define its 2-unfolding, denoted unfold 2 (P ), to be the protocol such that every occurrence of a process !Q in P is replaced by Q | Q, assuming that a type-preserving α-renaming is performed on one copy to avoid variables and names capture. Note that, in case P is replication-free, we have that unfold 2 (P ) = P . Definition 7 A simple protocol P is type-compliant w.r.t. a typing system (∆ 0 , δ 0 ) if for every t, t ∈ ESt(unfold 2 (P )) we have that: t and t unifiable implies that δ 0 (t) = δ 0 (t ).

Example 9 Consider again our running example with P 1 DS . We have that P 1 DS is type-compliant w.r.t. the typing system given in Example 8. Indeed, the encrypted subterms of P 1 DS are: -pub(ek b ), pub(ek a ), pub(ek c ), vk(sk b ), and vk(sk a ); -sign(k , sk a ) and sign(x B , sk a ); -aenc(sign(k , sk a ), pub(ek c )) and aenc(sign(x B , sk a ), pub(ek b )); -senc(x A , k ) and senc(m 1 , x B ).

It is easy to verify that each pair of unifiable encrypted subterms have the same type. To check type-compliance, we have to consider the encrypted subterms occurring in unfold 2 (P 1 DS ) but since our process P 1 DS does not contain any replication, we have that unfold 2 (P 1 DS ) = P 1 DS . On this example, type-compliance also holds when considering a more complex scenario with replication, and actually we can also consider a more refined typing system where δ DS (sk a ) = τ ska and δ DS (sk b ) = τ skb .

Honest type

We introduce the notion of honest type that will intuitively guarantee that a term of honest type is never revealed. It will typically be used for long term secret keys.

Definition 8 Consider a simple protocol P and a typing system (∆ 0 , δ 0 ). An atomic type τ h is honest for P if for any u ∈ Terms(P ), and any position p such that (uδ 0 )| p = τ h , we have that p is a key position of uδ 0 , that is, p ∈ KP(uδ 0 ); and τ h = δ 0 (a) for any constant/variable a occurring in P .

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

Intuitively, a type is honest for P if terms of that type only occur at key positions in P . Note in particular that constants occurring in a protocol have a type that cannot be honest. Indeed, constants are actually public to the attacker. Note also that terms occurring in a configuration of the form (P ; ∅; ∅; 0) are, by definition, honest-free. They may only contain names of honest type. In what follows, we will see that it is sufficient to consider honestfree traces.

Example 10 Continuing our running example, we have that the atomic types τ sk and τ ek are honest types. Indeed, we have no constant/variable having such a type occurring in P 1 DS (resp. P 2 DS ). Moreover, the only occurrence of a term having such a type in P 1 DS is indeed in key position, i.e. under a symbol pub, vk, or as a second argument of the symbol sign. Note that τ ekc can not be considered as an honest type since ek c is a constant of type τ ekc .

We can show that, in well-typed executions, names of honest type are never revealed to the attacker.

Lemma 1 Let P be a simple protocol, (∆ 0 , δ 0 ) be a typing system, and P tr = = ⇒ (P; φ; σ; i) be a well-typed execution. Let τ h be an honest type, n be a name such that δ 0 (n) = τ h . We have that Rφ↓ = n for any recipe R.

Proof Assume towards a contradiction that there exists R such that Rφ↓ = n. Thanks to Lemma 4 (this lemma is proved later on -see page 21), we know that there exists such a recipe R that is simple, and since n is a name, we have that R is a destructor-only recipe. Let w be the variable occurring at the leftmost position of R. We have that n occurs at a plaintext (extractable) position p in wφ. By construction of the frame φ, it must be the case that wφ = uσ where u is a term appearing in P in some output. Since the execution is well-typed, we know that δ 0 (wφ) = δ 0 (uσ) = δ 0 (u). This means that p corresponds to a plaintext position of δ 0 (u) and thus δ 0 (n) is not an honest type by definition.

Dependency graph

The type of a term will be used to compute on which other terms it can depend. For example, a term of composed type senc(τ 1 , τ 2 ) may be obtained by composition from a term of type τ 1 and a term of type τ 2 .

Formally, we define two functions ρ out and ρ in . The function ρ out , computes the types of the terms that can be extracted from a term of type τ while ρ in computes the set of types that could be used to build a term of type τ . More precisely, ρ in returns a set of types whereas ρ out returns a set of tuples of the form (τ, p)#(S; A) where τ is a type, p a position, and S and A are multisets of terms. Intuitively, S collects the types of symmetric keys while A collects the types of asymmetric keys.

Definition 9 Given a well-sorted type τ , we define ρ out (τ ) to be ρ out (τ, , ∅, ∅) where ρ out (τ, p, S, A) is recursively defined as the set {(τ, p)#(S; A)} ∪ E where E is defined as follows:

-E = ∅ when τ is an initial type or root(τ ) ∈ {pub, vk, hash};

-E = n i=1 ρ out (τ i , p.i, S, A) when τ = τ 1 , . . . , τ n ; -E = ρ out (τ 1 , p.1, S, A) when τ = sign(τ 1 , τ 2 ); -when root(τ ) ∈ {senc, rsenc}, E = ∅ if τ | 2 is an honest type, and E = ρ out (τ | 1 , p.1, S {τ | 2 }, A) otherwise; -when root(τ ) ∈ {aenc, raenc}, E = ∅ if τ | 21 is an honest type, and E = ρ out (τ | 1 , p.1, S, A {τ | 21 }) otherwise.
Example 11 Consider the types τ 1 0 = aenc(sign(τ k , τ sk ), pub(τ ekc )) and τ 2 0 = senc(τ m , τ k ), we have that:

-ρ out (τ 1 0 ) = {(τ 1 0 , )#(∅; ∅), (sign(τ k , τ sk ), 1)#(∅; τ ekc ), (τ k , 11)#(∅; τ ekc )}; -ρ out (τ 2 0 ) = {(τ 2 0 , )#(∅; ∅), (τ m , 1)#(τ k ; ∅)}.
Definition 10 Given a well-sorted type τ , we define ρ in (τ ) as follows:

case where τ is an initial type:

ρ in (τ ) = {τ }; -case where τ = f(τ 1 , . . . , τ n ) for some f ∈ Σ c : -ρ in (τ ) = {τ } if there exists 1 ≤ i ≤ n such that τ i is an honest type; -ρ in (τ ) = {τ } ∪ n i=1 ρ in (τ i ) otherwise.
Example 12 Consider the types τ 1 i = aenc(sign(τ k , τ sk ), pub(τ ek )) and τ 2 i = senc(τ m , τ k ), we have that:

-ρ in (τ 1 i ) = {τ 1 i , pub(τ ek ), sign(τ k , τ sk )}; -ρ in (τ 2 i ) = {τ 2 i , τ m , τ k }.
We can now define the dependency graph associated to a protocol.

Definition 11 Let (∆ 0 , δ 0 ) be a typing system, and P be a simple protocol. The dependency graph associated to P is a graph having L(P ) as vertices, and which are connected as follows:

1. for any action with label in P that directly follows an action with label in P , there is an edge → ; 2. for any " in : in(c, u)" and " out : out(d, v)" in P such that phase( out ) ≤ phase( in ), there is an edge in → p out if there exists τ ∈ ρ in (uδ 0 ) such that (τ, p)#(S; A) ∈ ρ out (vδ 0 ) (for some S and A); 3. for any " : out(c, u)" and " : out(d, v)" in P , there is an edge

→ p if (τ, q)#(S {τ k }; A) ∈ ρ out (uδ 0 ) or (τ, q)#(S; A {τ k }) ∈ ρ out (uδ 0 )
for some τ, q, S, A and τ k such that (τ k , p)#(S ; A ) ∈ ρ out (vδ 0 ) (for some S and A ).

Intuitively, edges of type 1 simply record that some action occurs after another one. Edges of type 2 reflect how some term u expected as input may be built from terms terms output by the protocol. These dependencies are inferred from the type of the terms. Finally, edges of type 3 are there to record when a term, intuitively a ciphertext, can be opened using key material output by the protocol.

Example 13

The dependency graph for the protocol P 1 DS defined in Example 6 w.r.t. the typing system (T DS , δ DS ) given in Example 8 is depicted in Figure 3. The vertical arrows (in blue) correspond to sequential dependencies (item 1), the arrows in red are due to item 2, and the arrow in green are due to item 3.

Intuitively, the arrows from 3 to K 1 , K 3 , and 1 mean that the input 3 may depend on the outputs K 1 , K 3 , and 3 , that is, the output term may be partially used to fill the input. The part of the output that could be used is indicated by the position p written on the arrow. Note that these dependencies are computed relying solely on types. The dependency graph for the protocol P 2 DS will be exactly the same as the one obtained for P 1 DS .

1 2 3 4 K 1 K 2 K 3 K 4 , 1 11 1 11
Fig. 3 Dependency graph for the simple protocol P 1 DS

Decidability Results

Our main result consists in showing that reachability properties and trace equivalence are decidable for protocols that are simple, type-compliant and with acyclic dependancy graphs.

Reachability.

We first establish decidability for reachability properties. This result is formally stated below and proved in Section 4

Theorem 1 Let P be a simple protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ) and with an acyclic dependency graph. Let ∈ L(P ). The problem of deciding whether is reachable in P , i.e. whether P tr = = ⇒ ({i : io (c, u).Q} ∪ P; φ; σ; i)

for some trace tr, and io ∈ {in, out} is decidable.

It is easy to encode a secrecy property as reachability of a particular action, as illustrated in the following example.

Example 14 To illustrate this result, we consider P DS which is as P DS but we add in 5 (c B , x B ) at the end of the process P B . In case 5 is reachable in P DS , it means that the value of k as received by the agent B is deducible by the attacker (and thus k is not secret). We have that:

P DS = 0 : P K | 1 : P A | P B
where P A and P B are as follows:

P A = new k . out 1 (c A , aenc(sign(k , sk a ), pub(ek c ))).
in 2 (c A , senc(x A , k )).0

P B = in 3 (c B , aenc(sign(x B , sk a ), pub(ek b ))). new m. out 4 (c B , senc(m, x B )).in 5 (c B , x B )
For the same reasons as P DS , we have that P DS is a simple protocol and it is type-compliant w.r.t. (T DS , δ DS ). The dependency graph associated to P DS is similar to the one associated to P 1 DS and contains an additional node labelled 5 with:

an additional arrow (of type 1) from 5 to 4 ; an additional arrow (of type 2) from 5 to 1 with label 11 since a value of type δ DS (x B ) = τ k can be extracted at position 11 from the term outputted at 1 .

Note that the resulting dependency graph is still acyclic, and thus this protocol/scenario falls into our decidable class.

For sake of simplicity we have considered so far a simple protocol P DS that does not feature any replication (and thus the fact that it falls into our decidable class is not surprising). However, as detailed in the following example, our result applies also considering a richer scenario.

Example 15 We now consider the scenario P ! DS which is similar to the process P DS given in Example 14 but includes replication (except for the role encoding key disclosure):

P ! DS = 0 : P K | 1 : !new c A .out(c 1 , c A ).P A | !new c B .out(c 2 , c B ).P B
We have that P ! DS is a simple protocol and is type-compliant w.r.t. (T DS , δ DS ). Since replication does not play any role in the construction of the dependency graph, the dependency graph associated to P ! DS is the same as the one for P DS . It is therefore acyclic meaning that this richer scenario falls also into our decidable class.

We consider more protocols, in an even richer scenario in Section 7.

Equivalence.

We can similarly decide trace equivalence by deciding trace inclusion.

Theorem 2 Le P be a simple protocol type-compliant w.r.t. some typing system (∆ P , δ P ) and with an acyclic dependency graph. Let Q be another simple protocol. The problem of deciding whether P is trace included in Q is decidable.

Section 5 is dedicated to the proof of Theorem 2.

Example 16

We have that P 1 DS and P 2 DS are simple protocol type-compliant w.r.t. (T DS , δ DS ) (see Example 9), and we have seen that the dependency graph associated to P 1 DS is acyclic (see Example 13). Thus this protocol/scenario falls into our decidable class.

Again, for sake of simplicity we have considered so far a simple protocol P 1 DS that does not feature any replication but our result applies for a richer scenario with replicated processes.

Decidability result for reachability

The main ingredient of the proof of Theorem 1 is to show that an execution trace corresponds to a path in the dependency graph. This is not true for all traces but for well-typed traces where the recipes used by the adversary follow certain conditions. The goal of this section is to introduce these conditions and show that they can be fulfilled. Part of the results established in this section will also be used for the proof of Theorem 2 on equivalence.

Well-typed traces involving only simple recipes

To establish our decidability result, we first show that we can consider welltyped executions involving only simple recipes. Simple recipes are recipes that are of the form destructors over constructors. Definition 12 We say that a recipe is simple if there exist destructor-only recipes R 1 , . . . , R k , i.e. recipes in

T (Σ d , W ∪ Σ 0 ) Σ 0 , and a context C made of constructors, i.e. function symbols in Σ c ∪ Σ 0 , such that R = C[R 1 , . . . , R k ].
When we consider a simple recipe R of the form C[R 1 , . . . , R k ], we implicitly refer to the decomposition expressed above meaning that R 1 , . . . , R k are the maximal destructor-only recipes occurring in R. As formally stated in the next lemma, destructor-only recipes may only deduce a subterm of the initial frame.

Lemma 2 Let φ be a frame, and R be a destructor-only recipe such that Rφ↓ is a message. We have that Rφ↓ ∈ St(φ).

Proof We prove this result by structural induction on R.

Base case: R ∈ W. In such a case, the result trivially holds. Induction case. In such a case, we have that

-either R = g(R 1 , R 2 ) with g ∈ {sdec, rsdec, adec, radec}; -or R = g(R 1 ) with g ∈ {getmsg} ∪ {proj j n | n ≥ 2 and 1 ≤ j ≤ n}.
In both cases, we know that R 1 is a destructor-only recipe, and thus, by induction hypothesis, we have that R 1 φ↓ ∈ St(φ). Actually, we have that Rφ↓ ∈ St(R 1 φ↓). Therefore, we have that Rφ↓ ∈ St(φ).

As in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we introduce the notion of forced normal form, denoted u . It intuitively corresponds to applying the rewriting rules even when some equalities are not satisfied, e.g. decrypting even with the wrong key. The idea is to pre-compute what can be deduced at best using the real rewriting system. We give below the rules R f associated to the rewriting system given in Section 2. sdec(senc(x, y 1 ), y 2 )

x adec(aenc(x, y 1 ), y 2 )

x getmsg(sign(x, y 1 ))

x rsdec(rsenc(x, y 1 , y 2 ), y 3 ) x radec(raenc(x, y 1 , y 2 ), y 3 )

x check(x, y) ok

proj n i ( x 1 , . . . , x n n ) x i with n ≥ 2 and 1 ≤ i ≤ n
A term u can be rewritten in v using the R f if there exists a position p in u, and a rewriting rule g(t 1 , . . . , t n ) t such that u| p = g(t 1 , . . . , t n )θ for some substitution θ, and v = u[tθ] p . As usual, we denote * the reflexive and transitive closure of . For example, sdec(senc(a, k), k ) a but sdec(aenc(a, pub(k)), k ) a. The forced rewriting system allows more rewriting steps than the original system. Nevertheless, the following lemma (stated and proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]) ensures that if R can be used to obtain a message then R computes the same message.

Lemma 3 [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] Let φ be a frame, R be a recipe such that Rφ↓ is a message, and R be such that R R . We have that R is a recipe and R φ↓ = Rφ↓.

We show that we can always chose simple recipes, simply by considering recipes in forced normal form. This result is similar to the one established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] but for a slightly different notion of simple terms (because [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] considers a more general equational theory).

Lemma 4 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 and R is a simple recipe.

Proof Let R be a recipe such that Rφ↓ = u. Thanks to Lemma 3, we have that R φ↓ = u. We now prove that R = R is simple by structural induction on R . Base case: R ∈ W ∪ Σ 0 . In both cases, it is easy to see that R is indeed simple. Induction case: R = f(R 1 , . . . , R k ) for some f ∈ Σ and R 1 , . . . , R k are in forced normal form. We distinguish two cases:

-Case f ∈ Σ c . Applying our induction hypothesis on R i (1 ≤ i ≤ k), we easily conclude. -Case f ∈ Σ d ∪ {check}.
Note that the case where f = check is impossible since R is in forced normal form. Now assume that f = adec, and thus R = adec(R 1 , R 2 ). As R φ↓ is a message, R 1 φ↓ and R 2 φ↓ are messages.

Applying our induction hypothesis, we know that both R 1 and R 2 are simple. As R 2 φ↓ is an atomic message, we know that R 2 is either destructoronly or a constant. Assume that R 1 = g(R 1 , . . . , R n ) for some g ∈ Σ c . As R φ↓ is a message, we have that g = aenc contradicting the fact that R is in forced normal form. Thus R 1 is destructor-only, and therefore R is simple. The other cases can be done in a similar way.

Interestingly, simple recipes do not use spurious constants: all constants that appear in a simple recipe R remain in the deduced message unless they already appear in the initial frame.

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

-either R = g(R 1 , R 2 ) with g ∈ {sdec, rsdec, adec, radec}; -or R = g(R 1
) with g ∈ {getmsg} ∪ {proj j n | n ≥ 2 and 1 ≤ j ≤ n}. In both cases, we know that R 1 is a destructor-only recipe, and thus, by Lemma 2, we have that R 1 φ↓ ∈ St(φ). Regarding R 2 , when it exists, we have that R 2 φ↓ ∈ St(R 1 φ↓). Therefore, applying our induction hypothesis on both R 1 and R 2 that are simple, we have that:

Cst(R) = Cst(R 1 ) ∪ Cst(R 2 ) ⊆ Cst(φ) ∪ Cst(R 1 φ↓) ∪ Cst(R 2 φ↓) = Cst(φ)
This concludes the proof.

A key step for decidability is that we can consider only well-typed traces thanks to [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. We state here this result and show in addition that it is enough to consider simple, honest-free recipes. When restricting ourselves to welltyped traces, we still preserve the general form of the trace. Formally, tr is obtained from tr by replacing any action in(c, R) by in(c, ), and keeping the other visible actions, i.e. out(c, w), out(c, c ) and the phase instruction, unchanged.

Theorem 3 Let K 0 be an initial configuration type-compliant w.r.t. (∆ 0 , δ 0 ) such that K 0 tr = = ⇒ (P; φ; σ; i). We have that there exists a well-typed execution K 0 tr = = ⇒ (P; φ ; σ ; i) involving only simple recipes such that tr = tr, and tr as well as φ are honest-free.

Proof Most of the theorem is a direct consequence of the typing result that has been established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. Then, the fact that we can consider simple recipes is an easy consequence of Lemma 4. It remains to establish that we can consider tr and φ to be honest-free.

According to Proposition 4.11 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.

In Lemma 4.10 of [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], it has been shown that ESt(K 0 σ S ) ⊆ ESt(K 0 )σ S , and since ρ is a renaming, we have that:

ESt(K 0 σ ) ⊆ ESt(K 0 )σ (1)
We now show that tr φ ↓ is honest-free. Assume by contradiction that there exists a constant c h of honest type occurring in tr φ ↓. In other words, c h occurs in an instantiation by σ of an input or output action of the initial processes, possibly after renaming names and variables (when unfolding replication). Thus the constant c h must occur in K 0 σ .

By definition of being an honest type, c h can only occur in key position in K 0 σ . This means that there exists either f(u, c h ) ∈ ESt(K 0 σ ) with f ∈ {senc, rsenc, sign}, or pub(c h ) ∈ ESt(K 0 σ ). Thanks to (1), we deduce that there exists either

f(u , v ) ∈ ESt(K 0 ) such that f(u , v )σ = f(u, c h ), or pub(v ) ∈ ESt(K 0 ) such that pub(v )σ = pub(c h ).
This implies that v is either a variable of honest type, or the constant c h , and both are forbidden according to the definition of honest type. This allows us to conclude that tr φ ↓ is honest-free.

We have that Terms(φ ) ⊆ Terms(tr φ ↓), and thus we easily deduce that φ is honest-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 of honest type occurs in φ and tr φ↓, we are done.

Exploiting the dependency graph

We are almost ready to show that any (well-typed, simple, honest-free) trace can be mapped to a path of the dependency graph. For this, we define ρ out and ρ in on terms. Intuitively, ρ in computes how a term can be built by an attacker.

Definition 13 Given a well-sorted term t and a typing system (∆ 0 , δ 0 ), we define ρ in (t) as follows:

case where t is atomic: ρ in (t) = {t}; case where t = f(t 1 , . . . , t n ) for some f ∈ Σ c :

ρ in (t) = {t} if there exists 1 ≤ i ≤ n such that t i has an honest type; ρ in (t) = {t} ∪ n i=1 ρ in (t i ) otherwise. Lemma 6 Let K 0 be an initial configuration, (∆ 0 , δ 0 ) be a typing system, and K 0 tr = = ⇒ (P; φ; σ; i) be a well-typed honest-free execution involving only simple recipes. In particular, no constant of honest type occurs in tr and φ.

Let R = C[R 1 , . . . , R n ] be a simple recipe such that Rφ↓ is a message and R is honest-free. We have that R i φ↓ ∈ ρ in (Rφ↓) for all i ∈ {1, . . . , n}.

Proof We establish the result by structural induction on C. Base case: C is the empty context or a constant. In such a case, the result trivially holds. Induction case. We have that C = f(C 1 , . . . , C k ) for some f ∈ Σ c . In such a case, we have that Rφ↓ = f(t 1 , . . . , t k ), and we have recipes, namely R 1 , . . . , R k , allowing one to deduce t 1 , . . . , t k . First, assume that there exists i ∈ {1, . . . , k} such that t i has an honest type. In such a case, t i is atomic, and actually t i is neither a constant (otherwise, an honest constant would occur in R or in φ), nor a name (by Lemma 1). Thus, we know that no t i has an honest type. Thus, by definition of ρ in (Rφ↓), we have that

ρ in (Rφ↓) = {Rφ↓} ∪ ρ in (t 1 ) ∪ . . . ∪ ρ in (t k ) Applying our induction hypothesis on R i = C i [R 1 , . . . , R n ] with 1 ≤ i ≤ k, we have that for any j ∈ {1, . . . , n}, R j φ↓ ∈ ρ in (C i [R 1 , . . . , R n ]φ↓) = ρ in (t i ).
Therefore, we have that R i φ↓ ∈ ρ in (Rφ↓) for any i ∈ {1, . . . , n}.

We now define ρ out on terms. It intuitively computes which terms can be deduced from a term t, tracking respectively the symmetric and asymmetric keys needed for that.

Definition 14 Given a well-sorted term t and a typing system (∆ 0 , δ 0 ), we define ρ out (t) to be ρ out (t, , ∅, ∅) where ρ out (t, p, S, A) is recursively defined as the set {(t, p)#(S; A)} ∪ E where E is defined as follows: A destructor-only recipe R intuitively tries to decrypt and project one 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:

-E = ∅ when t is atomic or root(t) ∈ {pub, vk, hash}; -E = n i=1 ρ out (t i , p.i, S, A) when t = t 1 , . . . ,
     if R is a variable w target(R| 1 ).1 if root(R) ∈ {proj n 1 | n ≥ 2} ∪ {getmsg, sdec, rsdec, adec, radec} target(R| 1 ).i if root(R) = proj n
i for some n ≥ 2 and some i ∈ {2, . . . , n}

For a destructor-only recipe R with a variable w at its leftmost leaf, target(R) is the position of the subterm computed by R inside wφ. Note that, thanks to Lemma 2, we know that the result of normalising R must be a subterm of wφ, since R is destructor-only and applied to w. We show that, if Rφ↓ is a message, then it was indeed computed by ρ out (wφ).

Lemma 7 Let K 0 be an initial configuration, (∆ 0 , δ 0 ) be a typing system, and K 0 tr = = ⇒ (P; φ; σ; i) be a well-typed honest-free execution involving only simple recipes. Let R be a destructor-only recipe with the variable w at its leftmost position such that Rφ↓ is a message. We have that (Rφ↓, target(R))#(S, A) ∈ ρ out (wφ). Moreover R| 2 φ↓ ∈ S (resp R| 2 φ↓ ∈ A) when root(R) = sdec or rsdec (resp. adec or radec).

Proof We establish this result by structural induction on R. Base case: R = w. Indeed, we have that (wφ, )#(∅; ∅) ∈ ρ out (wφ).

Induction case. In this case, we have that:

either R = g(R 1 , R 2 ) with g ∈ {sdec, rsdec, adec, radec}; or R = g(R 1 ) with g ∈ {getmsg} ∪ {proj j n | n ≥ 2 and 1 ≤ j ≤ n}. From now on, consider the case where g = adec. By induction hypothesis, we have that (R 1 φ↓, target(R 1 ))#(S 1 ; A 1 ) ∈ ρ out (wφ) for some A 1 and S 1 . We also know that t = R 1 φ↓ = aenc(t 1 , pub(a)) for some t 1 and some atom a. First, we note that t| 21 = a does not have an honest type. Indeed, this case is impossible since a is necessarily a name occurring in φ and a name with an honest type is not deducible (Lemma 1). Therefore, according to the definition of ρ out , we have that ρ out (t 1 , target(R 1 ).1, S 1 , A 1 {a}) ⊆ ρ out (wφ). Thus, we have that (t 1 , target(R 1 ).1)#(S 1 ; A 1 {a}) ∈ ρ out (wφ), i.e. (Rφ↓, target(R))#(S; A) ∈ ρ out (wφ) for some S and some A. Moreover, we have R| 2 φ↓ = R 2 φ↓ = a in A and root(R) = adec. This concludes this case, and the other cases can be handled in a similar way.

Of course, we can link the definitions of ρ in and ρ out on types and the ones on terms. Lemma 8 Let (∆ 0 , δ 0 ) be a typing system and u be a well-sorted term. We have that:

v ∈ ρ in (u) implies δ 0 (v) ∈ ρ in (δ 0 (u)); and -(v, p)#(S; A) ∈ ρ out (u) implies (δ 0 (v), p)#(δ 0 (S); δ 0 (A)) ∈ ρ out (δ 0 (u)).

Proof Regarding the first result about ρ in , it can be easily proven by structural induction on u. To establish the second result about ρ out , we prove the following result by structural induction on u: (v, p)#(S; A) ∈ ρ out (u, p 0 , S 0 , A 0 ) implies (δ 0 (v), p)#(δ 0 (S); δ 0 (A)) ∈ ρ out (δ 0 (u), p 0 , δ 0 (S 0 ), δ 0 (A 0 )).

The result is a direct consequence of this property.

Note that the converse implications (from types to terms) do not hold: the structure of the type may be finer that the structure of the corresponding term, e.g. δ(x) = τ 1 , τ 2 .

Any dependency arising in an execution of a protocol can be mapped to its dependency graph.

Proposition 1 Let P be a simple protocol, (∆ 0 , δ 0 ) be a typing system, and P tr -→ (P; φ; σ; j 0 ) be a well-typed honest-free execution involving only simple recipes.

For any pair of actions in in (d, C[R 1 , . . . , R k ])/out out (c, w) occurring in tr with w ∈ vars(R i0 ) (1 ≤ i 0 ≤ k), we have that: in → 0 out → * out is a path in the dependency graph associated to P where 0 out is the label associated to w 0 , the handle occurring at the leftmost position in R i0 . Moreover, the length of the path from 0 out to out is equal to the number of occurrences of 2 in p (the position at which w occurs in R i0 ).

Proof Let R = C[R 1 , . . . , R k ].
Note that since w ∈ vars(R), we have that phase( out ) ≤ phase( in ). The execution being honest-free, we have that no constant of honest type occurs in tr. Let i 0 ∈ {1, . . . , k} be such that w occurs in R i0 , and let p be a position at which w occurs in R i0 . We show the result by induction on the number of occurrences of 2 in p.

1. Base case: p is a possibly empty sequence of 1. In this case, we have that w occurs at the leftmost position of R i0 . Applying Lemma 7, we have that (R i0 φ↓, target(R i0 ))#(S; A) ∈ ρ out (wφ). Then, thanks to Lemma 6, we have that R i0 φ↓ ∈ ρ in (Rφ↓). We rely on Lemma 8 to transfer these relations on types and we conclude the existence of an edge in → target(Ri 0 ) out of type 2 in the dependency graph. 2. Induction case: p = p 0 .2.1 . . . 1 with a possibly empty sequence of 1 at the end. Applying Lemma 7 on R i0 | p0 and denoting w p0 the variable occurring at its leftmost position, we have that:

(R i0 | p0 φ↓, target(R i0 | p0 ))#(S; A) ∈ ρ out (w p0 )
for some S and A such that R i0 | p0.2 φ↓ ∈ S (resp. A) when root(R i0 | p0 ) = sdec or rsdec (resp. adec or radec). Applying Lemma 7 on R i0 | p0.2 (note that the variable occurring at its leftmost position is w), we have that

(R i0 | p0.2 φ↓, target(R i0 | p0.2 ))#(S ; A ) ∈ ρ out (w)
for some S and A . We rely on Lemma 8 to transfer these relations on types and we conclude to the existence of an edge out → target(Ri 0 |p 0 .2 ) out of type 3 in the dependency graph -where out is the label associated to w p0 . By induction hypothesis, we have that: in → + out since w p0 occurs at position p 0 .1 . . . 1 in R i0 and this position contains less occurrences of 2 than p 0 .2.1 . . . 1. This gives us the expected result.

out 1 (c A , w 2 ) in 3 (c B , R 0 ) out 4 (c B , w 3 ) out K 1 (c 0 , w 1 )
Fig. 4 Execution graph associated to tr 0 for the simple protocol P DS

Bounding the length of a minimal witness

Given a trace (tr, φ) of a simple protocol P , we can represent it as a dag D (directed acyclic graph) whose vertices are input/output actions of tr, and edges represent sequential dependencies and data dependencies. Note that such a dag can be computed simply from tr. Indeed, for simple protocols, sequential dependencies may be inferred from the channel names occurring in tr, and data dependencies are inferred from input recipes occurring in tr.

Our ultimate goal is to bound the length of a trace tr witnessing the existence of an attack. We first define the notion of execution graph.

Definition 15 Let P be a simple protocol. The execution graph associated to an execution ex starting from P is a directed acyclic graph whose vertices are the actions of ex of the form in (c, R) and out (c, w), and whose edges denoted →, are defined as follows:

there is an edge from an action a 2 with label 2 to an other action a 1 with label 1 if both actions are on the same channel, and 2 directly follows 1 in P ; there is an edge from in (c, R) to an action out (c , w) if w ∈ vars(R).

We note that for a simple protocol P , the execution graph associated to a trace (tr, φ) ∈ trace(P ) is unique. The actions of the form out(c, c ) with c a channel name are not part of the execution graph.

Example 17

The execution graph associated to the trace (tr 0 , φ 0 ) ∈ trace(K 0 ) given in Example 4 is depicted in Figure 4. Remember that

tr 0 = out(c 0 , w 1 ).phase 1.out(c A , w 2 ).in(c B , R 0 ).out(c B , w 3 )
where R 0 = aenc(adec(w 2 , ek c ), w 1 ).

Given a directed acyclic graph D, the width of D, denoted width(D), is the maximum outgoing degree of any vertex of D. The depth of D, denoted depth(D), is the length of the longest path in D, and we denote nbroot(D) its number of roots, i.e. vertices with no ingoing edge. Lemma 9 Let (∆ 0 , δ 0 ) be a typing system and P be a simple protocol whose associated dependency graph G is acyclic. Let P tr -→ (P; φ; σ; i 0 ) be a welltyped honest-free execution involving only simple recipes, and D its associated execution graph. We have that:

depth(D) ≤ depth(G).
Proof We denote ρ the function which associates to an action a occurring in tr, its label ∈ L(P ). Given an arrow a → b between two actions of the execution graph D, we show that ρ(a) → + ρ(b) in the dependency graph G. By definition, this arrow either corresponds to a sequential dependency or corresponds to a data dependency. In case of a sequential dependency, the same arrow exists in the dependency graph. In case of a data dependency, Proposition 1 ensures that ρ(a) → + ρ(b). This allows us to conclude. Given P a simple protocol which is type-compliant w.r.t. some typing system (∆ 0 , δ 0 ), we consider the sizes induced by the types that appear in input and output actions of the protocol. Let u denote the size of u. Then we define:

in P = max{ uδ 0 | in(c, u) occurs in P for some c}; -out P = max{ uδ 0 | out(c, u) occurs in P for some c}.

We show that the width of the execution graph of a trace of P can be bounded depending on the size of the types appearing in P .

Lemma 10 Let (∆ 0 , δ 0 ) be a typing system, and P be a simple protocol whose associated dependency graph G is acyclic. Let P tr -→ (P; φ; σ; i 0 ) be a welltyped honest-free execution involving only simple recipes, and D its associated execution graph. We have that:

width(D) ≤ 1 + out P depth(G) × in P .
Proof Any node has at most one sequential predecessor. Now, in case of an input, we have to take into account data dependencies. We know that the involved recipe R is of the form C[R 1 , . . . , R k ] with R i (1 ≤ i ≤ k) destructoronly and k ≤ in P since C is at most of size in P . Moreover, thanks to Proposition 1, we have that, for any i ∈ {1, . . . , k}, the maximal number of occurrences of 2 in any sequence in pos(R i ) (the positions of R i ) is bounded by depth(G).

To conclude, it remains to show that we can bound the number of variables occurring in such recipes. Let S be the set of all destructor-only recipes R such that any sequence in pos(R) (the positions of R) contains at most occurrences of 2. We aim at bounding nb = M ax{#{w ∈ vars(R)} | R ∈ S }. Clearly, for = 0, we have that nb = 1. Moreover, nb +1 can be bound by out P × nb since the number of consecutive 1 in a path is bounded by out P , the maximal size of a term to which the recipe can be applied. Therefore, each R i involves no more than out P depth(G) variables, and this allows us to conclude.

To establish our result, we show that pruning an execution graph w.r.t. a set of nodes still yields a valid trace for P . This notion of pruning preserves all sequential and data dependencies and is formally defined as follows.

Definition 16 Given an execution graph D = (V, E) and a set R ⊆ V , we define the pruning D R = (V R , E R ) of D w.r.t. R as follows:

-V R = {v ∈ V | r → * v for some r ∈ R}; -E R = {(u, v) ∈ E | u, v ∈ V R }
where → * denotes the transitive closure of the relation induced by E.

Let P be a simple protocol and D the execution graph associated to a given trace tr. We note that the pruning of D w.r.t. some nodes still corresponds to an execution of P . The underlying trace tr is actually a subtrace of tr. More formally, we have the following result.

Lemma 11 Let P be a simple protocol, (tr, φ) ∈ trace(P ) and D the execution graph of tr w.r.t. P . Let R = {v 1 , . . . , v p } be a set of nodes of D and D R the pruning of D w.r.t. R. Then, there exists (tr R , φ R ) ∈ trace(P ) such that:

-D R is the execution graph of tr R w.r.t. P ; -tr R is a subtrace of tr, and φ R is a subframe of φ.

Proof The execution graph captures all the dependencies, and thus the closure of D R ensures that any action occurring in tr R has the needed predecessors.

Finally, we can bound the number of nodes of an execution graph (for well chosen executions), hence decide reachability.

Theorem 1 Let P be a simple protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ) and with an acyclic dependency graph. Let ∈ L(P ). The problem of deciding whether is reachable in P , i.e. whether P tr = = ⇒ ({i : io (c, u).Q} ∪ P; φ; σ; i) for some trace tr, and io ∈ {in, out} is decidable.

Proof To establish this result, we show that there is a trace witnessing this fact whose execution graph D = (V, E) is such that:

#V ≤ (2 + out P depth(G) × in P ) depth(G)+1 .
First, thanks to Theorem 3, we can consider that there is a trace (tr, φ) witnessing that is reachable that is well-typed, simple, and honest-free. Then, we consider the execution graph D associated to this trace (tr, φ). We know that one node (at least) is labelled with io (c, ). Let D be the execution graph corresponding to the pruning of D w.r.t. such a node. Thanks to Lemma 11, we have that D = (V , E ) is an execution graph corresponding to an execution leading to the action io (c, ). Moreover, we have that:

#V ≤ 1 + width(D ) + width(D ) 2 + . . . + width(D ) depth(D ) ≤ max(2, width(D )) depth(D )+1 .
Thanks to Lemma 9 and Lemma 10, we deduce that:

#V ≤ (2 + out P depth(G) × in P ) depth(G)+1 .
All these results together yield the expected bound on the number of vertices of the execution graph D of the trace (tr, φ). This, in turn, bounds the length of the trace tr but does not take into account the actions out(c, c ) since they do not appear in the execution graph. In other words, we have bounded the number of sessions that involve at least one visible action that is not an output on a channel. Actually, actions of the form out(c, c ) are unnecessary (except possibly one) if they are not followed by some actions on the channel c . Thus, this gives us a bound on the number of sessions involved in an attack trace. Since reachability for a bounded number of sessions is known to be decidable [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete[END_REF], this allows us to conclude.

Alternatively, we could also directly bound the total size of a minimal witness tr. To do so, we would need to show that we can bound the size of recipes as well. This would allow us to conclude the proof without relying on the decidability of reachability for a bounded number of sessions. We see on this very simple example that the bound on the number of sessions is huge and way beyond the reach of existing tools. There is however clearly room for improvements. In particular, we could improve our bound by exploiting the fact our witness is well-typed.

Decidability result for equivalence

The goal of this section is to provide the main ingredients of the proof of Theorem 2, that states that trace inclusion is decidable for well-typed protocols that have an acyclic dependency graph. The proof follows a similar structure than the reachability case.

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, honest-free, and involves only simple recipes. 2. We already know from the reachability case that any such well-typed, honest-free, simple trace can be mapped to a path in the dependency graph. 3. This allows us to compute a bound on the length of such a witness of non inclusion, hence deciding trace inclusion. To compute this bound in the case of equivalence, we provide a new characterisation of static inclusion, following the approach of [START_REF] Chrétien | Typing messages for free in security protocols[END_REF].

Well-typed witnesses involving simple recipes

As for the reachability case, we first show that we can focus on witnesses of non trace inclusion that have a particular form.

Theorem 4 Let K P be an initial configuration type-compliant w.r.t. (∆ P , δ P ) 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; φ; σ P ; i P ) involving only simple recipes witnessing this fact. Moreover, we may assume that tr and φ are honestfree.

Proof The existence of a well-typed witness of non-inclusion is a direct consequence of the typing result that has been established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. Then, it remains to justify the fact that we can consider such a witness with simple recipes. To establish this, we consider a well-typed execution K P tr = = ⇒ (P; φ; σ P ; i P ) witnessing this non-inclusion of minimal length, and we denote tr the trace obtained from tr by replacing any recipe R occurring in it by a simple recipe R deducing the exact same term as Rφ↓ (such a recipe exists according to Lemma 4). Our aim is to show that tr is still a witness of non-inclusion.

In case |tr| = 0, we have that tr = tr and thus the result trivially holds. We consider tr = tr .α, and a well-typed execution corresponding to this minimal witness of non-inclusion: K P tr = = ⇒ (P ; φ ; σ P ; i P ) α = = ⇒ (P; φ; σ P ; i P ).

Note that K P tr = = ⇒ (P ; φ ; σ P ; i P ) α = = ⇒ (P; φ; σ P ; i P ) by definition of tr which is computed w.r.t. φ. Since tr is minimal and |tr | < |tr|, we know that there

exists K = (Q ; ψ ; σ Q ; i Q ) such that K Q tr = = ⇒ K
and φ s ψ . Such a configuration K is not necessarily unique. We denote K 1 , . . . , K k the configurations that satisfy this requirement, and we denote ψ 1 , . . . , ψ k their associated frame. For each configuration K i (with its associated frame ψ i ), we have that: for any recipe R occurring in tr , we have that Rφ ↓ = Rφ ↓, and thus Rψ i ↓ = Rψ i ↓. Therefore, we have that tr can be executed from K Q and leads to the exact same configuration K i as before with frame ψ i . In other words, the configurations K 1 , . . . , K k are still reachable starting from K Q when executing tr .

In case tr is a witness of non-inclusion, we are done. Now, assume that tr passes in K Q , i.e. α can be executed from K i (for some i) and the resulting frame ψ i is such that φ s ψ i . In case α = α, then this means that tr passes in K Q and the resulting frame ψ i is such that φ s ψ i . This contradicts the fact that tr is a witness of non-inclusion. Otherwise, we have that α = in(c, R), and α = in(c, R). Since φ s ψ i , and Rφ ↓ = Rφ ↓, we deduce that Rψ i ↓ = Rψ i ↓. Therefore, the fact that tr passes in K Q leading to frame ψ such that φ s ψ implies that tr also passes in K Q and leads to the exact same frame ψ. This contradicts the fact that tr is a witness of non-inclusion.

It remains to establish that we can assume tr and φ to be honest-free.

Actually, considering K P tr = = ⇒ K P a witness of non-inclusion with underlying substitution σ P , 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 σ P is such that σ P = σ S ρ where:

-σ S is the most general unifier (denoted mgu) of Γ = {(u, v) | u, v ∈
ESt(K 0 ) such that uσ P = vσ P }; and ρ is a bijective renaming from variables in dom(σ P ) dom(σ S ) to some fresh constants preserving type.

In order to conclude, we apply the same reasoning as in the case of reachability, as done at the end of Theorem 3.

Exploiting the dependency graph

Thanks to Proposition 1, we know that any well-typed, simple, and honest-free trace can be mapped to a path of the dependency graph. There is nothing to add in the case of trace inclusion.

Bounding the length of a minimal witness

The last step of the proof of Theorem 2 consists in bounding the size of a (minimal) witness of trace inclusion, that is well-typed, simple, and honest-free. We use a similar technique as in the reachability case, exploiting the dependency graph. However, in case non-inclusion is due to a non static inclusion, pruning the execution w.r.t. a single node is not sufficient. We first establish a bound on the number of nodes involved in a witness of non-inclusion. For this, we have to characterise the form of the test involved in such a witness. We use for that the alternative definition of static inclusion already introduced in [START_REF] Cortier | Efficiently deciding equivalence for standard primitives and phases[END_REF].

Definition 17 Let φ, ψ be such that dom(φ) = dom(ψ). We write φ simple s ψ if:

1. For each destructor-only recipe R such that Rφ↓ is a (resp. atomic) message, Rψ↓ is a (resp. atomic) message. 2. For each simple recipe R and destructor-only recipe R such that Rφ↓, R φ↓ are messages and Rφ↓ = R φ↓, we have that Rψ↓ = R ψ↓.

3. For each destructor-only recipes R, R , if Rφ↓ = sign(t, s), and R φ↓ = vk(s) for some term t and atom s, then Rψ↓ = sign(t , s ), and R ψ↓ = vk(s ) for some term t and atom s . 4. For each destructor-only recipe R, such that Rφ↓ = pub(s) for atom s, Rψ↓ = pub(s ) for some atom s .

As established in [START_REF] Cortier | Efficiently deciding equivalence for standard primitives and phases[END_REF] for a slightly different set of primitives, this notion of static inclusion is equivalent to the original one.

Lemma 12 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 2 are straightforward. Given two recipes R and R satisfying the assumptions of item 3, we have check(R, R ) = ok for φ hence for ψ, hence the result. Then given a recipe R satisfying the assumptions of item 4, we have that aenc(ok, R) is a message in φ, hence in ψ, hence the result. Thus, we only consider the other implication. To establish the other implication, we consider another alternative definition of static inclusion, denoted s . This notion is the same than the one given in Definition 17 but considering arbitrary recipes instead of simple/destructor-only 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 R and R 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 alreasoningady been transferred from φ to ψ. We consider the following measure µ where |R| is simply the size of R, i.e. the number of function symbols occurring in it. We 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 normal form w.r.t.

. Consider R such that R R . We have that R φ↓ is a message (Lemma 3). By induction hypothesis R ψ↓ is a message too. It remains to show that Rψ↓ is a message. Actually, we have that

R = C[adec(aenc(R 1 , R 2 ), R 3 )] and R = C[R 1 ]
(other cases are similar). Since Rφ↓ is a message, we know that R 2 φ↓ = pub(R 3 )φ↓. By induction hypothesis R 2 ψ↓ = pub(R 3 )ψ↓, and this allows us to conclude.

-Case where R is in normal form w.r.t. . In this case, we know that R is simple (Lemma 4), i.e.

R = C[R 1 , . . . , R k ],
where C is a constructor context and R i are destructor-only recipes. If C is empty, then R is destructor-only.

We conclude by relying on our hypothesis. Otherwise R = f(R 1 , . . . , R n ). By induction hypothesis, we know that R i ψ↓ is a message (1 ≤ i ≤ n). We have to prove that C[R 1 , . . . , R k ]ψ↓ = f(R 1 , . . . , R n )ψ↓ is a message. We have atomic messages at key positions (thanks to our induction hypothesis).

In case f = aenc (resp. f = raenc) and thus n = 2, we have to ensure that R 2 ψ↓ is of the form pub(s). This is given by item 4 of Definition 17.

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φ↓ and Rψ↓ are messages, we deduce that R φ↓ = Rφ↓ and R ψ↓ = Rψ↓.

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 ψ↓. -Otherwise, thanks to Lemma 4, 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 destructor- only recipes. If neither C nor C is empty (that is, neither R nor R is destructor-only) then root(R) = root(R )
, and thus we conclude relying on our induction hypothesis. Otherwise, we conclude relying on our hypothesis that φ simple s ψ.

The test T is of the form R = R such that R and R are recipes, Rφ↓ = sign(t, s), and R φ↓ = vk(s) for some term t and some atom s.

-Case R (resp. R ) is not in normal form w.r.t. . R (resp. R ) is a smaller recipe than R (resp. R ). By Lemma 3, R φ↓ = Rφ↓ (resp. R φ↓ = R φ↓). So R , R (resp. R, R
) gives us a smaller test than R, R . By induction hypothesis we get that R ψ↓ = sign(t , s ) and R ψ↓ = vk(s ) for some term t and atom s . We already considered the case where Rφ↓ is a message, so we can assume Rψ↓ is a message. Then we deduce that Rψ↓ = R ψ↓ by Lemma 3, and concluding this case. -Otherwise, thanks to Lemma 4, we know that R and R are both simple recipes. In case they are both destructor-only recipes we conclude relying on our hypothesis. Otherwise, assume first R = sign(R 1 , R 2 ). In such a case, we have that the test vk(R 2 ) = R is smaller than R = R , and it holds in φ, and thus it can be transferred from φ to ψ by induction hypothesis. Moreover, R 2 ψ↓ is an atom by induction hypothesis. Hence, we have that Rψ↓ = sign(R 1 ψ↓, R 2 ψ↓), and R ψ↓ = vk(R 2 ψ↓). Hence, the result. Now, assume that R is destructor-only and R is not, i.e. R = vk(R 1 ). Since R 1 φ↓ is an atomic message, R 1 is destructor only, and thus sign(getmsg(R), R 1 ) is simple. We know that sign(getmsg(R), R 1 ) = R holds in φ. By hypothesis, it also holds in ψ. This allows us to conclude that Rψ↓ = sign(t , s ) with R 1 ψ↓ = s . Hence, the result.

The test T is a recipe R such that Rφ↓ = pub(s) for some atom s.

-Case R is not in forced normal form, we have that R is a smaller recipe than R. By Lemma 3, R φ↓ = Rφ↓. So by induction hypothesis R ψ↓ = pub(s) for some atom s. We have already proved that, as Rφ↓ is a message, Rψ↓ is a message. So by Lemma 3, R ψ↓ = Rψ↓ = pub(s). -Case R is a simple recipe. In case R is a destructor-only recipe, we conclude relying on our hypothesis. Otherwise R = pub(R 1 ) and R 1 φ↓ is an atom, thus R 1 is destructor-only. We conclude that R 1 ψ↓ is an atom too relying on our induction hypothesis, and thus Rψ↓ = pub(s ) for some atom s .

We use this new characterisation of static inclusion to bound the size of a minimal witness.

Lemma 13 Let P be a simple protocol type-compliant w.r.t. some typing system (∆ P , δ P ), and let G be its associated dependency graph which is supposed to be acyclic. Let Q be another simple protocol such that P Q. Let (tr, φ) be a witness of non-inclusion which is well-typed and with minimal length. We have that:

nbroot(D) ≤ 2 × (1 + out P ) depth(G)+1
where D is the execution graph associated to (tr, φ) w.r.t. P .

Proof Thanks to Theorem 4, we know the existence of a well-typed witness of non-inclusion, and we choose one having a minimal length. We denote D the execution graph associated to (tr, φ) w.r.t. P . We distinguish two 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 D the resulting execution graph and (tr 0 , φ 0 ) the corresponding trace of P (the one mentioned in Lemma 11). 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 R α 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, we are done since nbroot(D) = nbroot(D ) = 1. 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 non-inclusion, and its associated execution graph D is such that nbroot(D ) = 0 (such a graph is empty).

There exists ψ such that (tr, ψ) ∈ trace(Q) but φ s ψ. From Lemma 12, we can consider distinguishing tests that satisfy Definition 17. We now compute a bound b on the number of distinct variables that may occur in such a test.

-In case the test involved one (resp. two) destructor-only recipe(s), following the proof of Lemma 10, we can show that a destructor-only recipe contains at most out P depth(G) variables, and this leads us to the bound b = 2 × out P depth(G) . -In case the test involved a simple recipe R. Since we know that Rφ↓ = R φ↓ with R destructor-only, and (tr, φ) is a well-typed witness of noninclusion, we deduce that

R = C[R 1 , . . . , R k ] with k ≤ R φ↓ ≤ out P .
Therefore, we deduce that such a simple recipe involved at most (1 + out P ) depth(G) × out P distinct variables, and this leads us to the bound b = (1 + out P ) depth(G)+1 .

Let W be the set of all the variables occurring in the test witnessing the noninclusion. We have seen that #W ≤ b. We consider the actions of tr labelled with out(c, w) with w ∈ W, and we prune D w.r.t. this set of actions. Let D be the resulting execution graph. We obtain (tr 0 , φ 0 ) ∈ trace(P ) (by Lemma 11). Note that the definition of pruning does not depend on the underlying protocol, and thus, since (tr, ψ) ∈ trace(Q), we have also that D is the execution graph of tr 0 w.r.t. Q, and ψ 0 is a subframe of ψ. Actually, we have that there exists W such that W ⊆ W , φ 0 = φ| W , and ψ 0 = ψ| W . This allows us to ensure that (tr 0 , φ 0 ) with execution graph D is still a witness of non-inclusion which satisfies our requirements.

We can now conclude that trace inclusion is decidable.

Theorem 2 Le P be a simple protocol type-compliant w.r.t. some typing system (∆ P , δ P ) and with an acyclic dependency graph. Let Q be another simple protocol. The problem of deciding whether P is trace included in Q is decidable.

Proof Let G be the dependency graph associated to P . To establish this result, we show that there is a trace (tr, φ) ∈ trace(P ) witnessing this fact whose execution graph D = (V, E) is such that:

#V ≤ 2(1 + out P ) depth(G)+1 × (2 + out P depth(G) × in P ) depth(G)+1 .
First, thanks to Theorem 4, we consider a well-typed witness (tr, φ) of noninclusion which is also honest-free and that only involve simple recipes, and we consider one of minimal length. Thanks to Lemma 13, we know that:

nbroot(D) ≤ 2(1 + out P ) depth(G)+1
where D is the execution graph associated to (tr, φ) w.r.t. P .

We aim at bounding the number of vertices in D. Actually, we have that:

#V ≤ nbroot(D)(1 + width(D) + width(D) 2 + . . . + width(D) depth(D) ) ≤ nbroot(D) × max(2, width(D)) depth(D)+1
Thanks to Lemma 9 and Lemma 10, we know that:

width(D) ≤ 1 + out P depth(G) × in P , and

-depth(D) ≤ depth(G).
All these results together yield the expected bound on the number of vertices of the execution graph D of the trace (tr, φ). This, in turn, bounds the length of the trace tr up to the actions out(c, c ) since they do not appear in the execution graph. As for the reachability case, this gives us a bound on the number of sessions. Hence it is sufficient to decide trace equivalence for a bounded number of sessions, which is known to be decidable [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF][START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF].

6 An improved version of our decidability result Unfortunately, our initial definition of dependency graph often yields to cyclic graphs (actually, in most cases!). Hence we devise a refined dependency graph such that our results still hold. The idea is to mark some positions of output actions of a protocol P and disallow arrows that point to such positions. Recall that many arrows of the dependency graph aim at identifying, for each input action, which output actions could be used to build the input message. We show that it is sound to remove arrows that points to marked positions, as long as we know that terms appearing at such positions in an output can already be deduced from earlier messages. Such a marking is then called appropriate. We provide two simple syntactic criteria that, when satisfied, guarantees that a marking is appropriate.

Simple asap recipes

To show that our results still hold for our refined notion of dependency graph, we will first show that we can consider executions where recipes are not only simple but also asap, that is, to build a message, a recipe should use messages that have been introduced as early as possible.

Definition 18 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 , it is the case that R < R if vars # (R) < mul vars # (R ), where vars # (R) denotes the multiset of variables occurring in R, and < mul is the multiset extension of <.

Example 19 Consider the frame φ = {w 1 k, k , w 2 k}. Then the recipe w 2 allows to deduce k since w 2 φ↓ = k but is not asap. Instead proj 1 (w 1 ) is an asap recipe of k.

Whenever a message is deducible, we can also find a simple and asap recipe of the message.

Lemma 14 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 simple and asap such that R φ↓ = u.

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

We show that, for both reachability and equivalence, we can consider witnesses that are well-typed, honest-free, and that involve simple and asap recipes.

Theorem 5 Let K 0 be an initial configuration type-compliant w.r.t. (∆ 0 , δ 0 ).

If K 0 tr = = ⇒ (P; φ; σ; i) then there exists a well-typed execution K 0 tr = = ⇒ (P; φ ; σ ; i) involving only simple asap recipes such that tr = tr. Moreover, we may assume that tr and φ are honest-free.

Proof This theorem is a consequence of the typing result that has been established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], and can be established following the same lines as the proof of Theorem 3. To justify the fact that we can consider simple asap recipes, we rely on Lemma 14 (instead of Lemma 4). Then, it remains to justify that tr and φ are honest-free, and the proof is similar to one of Theorem 3.

Theorem 6 Let K P be an initial configuration type-compliant w.r.t. (∆ P , δ P ) 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; φ; σ P ; i P ) involving only simple asap recipes witnessing this fact. Moreover, we may assume that tr and φ are honest-free.

Proof This theoroem is a consequence of the typing result that has been established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], and can be established following the same lines as the proof of Theorem 4. To justify the fact that we can consider simple asap recipes, we rely on Lemma 14 (instead of Lemma 4). Then, it remains to justify that tr and φ are honest-free, and the proof is similar to the one of Theorem 4.

Marking (semantic criterion) and refined dependency graph

We first devise a general (semantic) criterion in order to mark some output actions of a protocol and remove accordingly some of the edges of the dependency graph.

Definition 19 A marked position of a simple 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). A marking of P w.r.t. (∆ 0 , δ 0 ) is a set of marked positions of P .

We consider that a marking strategy is appropriate for our dependency graph 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 remove arrows pointing to marked positions.

Definition 20 Let P be a simple 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 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).

Deciding whether a marked position is appropriate is not an easy task. We will provide some syntactic criteria in the following section. Relying on this notion of marking, we are now able to define our notion of refined dependency graph associated to an initial configuration K 0 . It is simply obtained by removing arrows pointing to marked positions.

Definition 21 Let (∆ 0 , δ 0 ) be a typing system, P be a simple protocol, and M be a marking of P w.r.t. (∆ 0 , δ 0 ). The refined dependency graph associated to P and M is obtained from the dependency graph of P by simply removing any arrow of the form → p for which ( , p) ∈ M.

We can again link dependencies arising in executions of a protocol to its refined dependency graphs. More precisely, we show that any dependency arising in an execution can be mapped to a path in the (refined) dependency graph provided that the underlying execution is well-typed, honest-free, and that it involves simple and asap recipes.

Proposition 2 Let (∆ 0 , δ 0 ) be a typing system, P be a simple protocol with M an appropriate marking, (∆ 0 , δ 0 ) be a typing system, and P tr = = ⇒ (P; φ; σ; j 0 ) be a well-typed honest-free execution involving simple asap recipes.

For any pair of actions in in (d, C[R 1 , . . . , R k ])/out out (c, w) occurring in tr with w ∈ vars(R i0 ) (1 ≤ i 0 ≤ k), we have that: in → 0 out → * out in the refined dependency graph associated to P where 0 out is the label associated to w 0 , the handle occurring at the leftmost position in R i0 . Moreover, the length of the path from 0 out to out is equal to the number of occurrences of 2 in p (the position at which w occurs in R i0 ).

Proof The proof is similar to the one performed to establish Proposition 1. We follow the same reasoning but we now have to justify in addition that the arrow we consider is not removed by marking. We perform the proof by induction on the number of occurrences of 2 in p (the position at which w occurs in R i0 .

1. Following the proof of Proposition 1, we conclude the existence of an edge in → target(Ri 0 ) out of type 2 in the dependency graph. Now, we have to justify that this edge is still present in the refined dependency graph. Assume by contradiction that it is not the case, i.e. ( out , target(R i0 )) ∈ M. Since M is appropriate, we easily deduce that R i0 is not an asap recipe of R i0 φ↓, and thus R (occurring in tr) is not asap. This leads to a contradiction.

2. Following the proof of Proposition 1, we conclude the existence of an edge out → target(Ri 0 |p 0 .2) out of type 3 in the dependency graph -where out is the label associated to w p0 . Now, we have to justify that this edge is still present in the refined dependency graph. Assume by contradiction that it is not the case, i.e. ( out , target(R i0 )) ∈ M. Since M is appropriate, we easily deduce that R i0 | p0.2 is not an asap recipe of R i0 | p0.2 φ↓, and thus R (occurring in tr) is not asap. This leads to a contradiction.

We obtain the expected result.

Marking -syntactic criteria

We can use any marking that is appropriate. However, checking that a particular marking is appropriate is far from easy and is actually very likely undecidable. So instead, we provide two syntactic criteria that allow to mark a position and we prove that such a marking is appropriate.

Our first criterion allows us to remove arrows towards terms having a public type. This notion is defined below.

Definition 22 Given a simple 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 ).

The intuition is that, in a well-typed execution, terms having a public type are terms built using public constants only, and are thus deducible from the beginning of the execution. This is formally established in the following lemma.

Lemma 15 Let P be a simple 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. In order to establish that u ∈ T (Σ c , Σ 0 ), we show that each leaf of u ∈ Σ 0 ∪ {ok}. Consider an arbitrary leaf a of u. We have that a is either a name or a constant. In case a ∈ Σ 0 , then we are done. Now assume that a ∈ N , and thus we have that δ 0 (a) ∈ St(τ p ). Since Rφ↓ = u for some recipe R, we have that a occurs somewhere in φ and thus a name n such that δ 0 (n) = δ 0 (a) occurs in P . Therefore we have that δ 0 (n) ∈ St(τ p ) for some name n occurring in P . This is impossible by definition of being a public type, and this allows us to conclude.

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

Lemma 16 Let ( , p) be a marked position of a simple 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 destructor-only recipe 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 15, and therefore R (which contains w) is not an asap recipe for Rφ↓ = m = wφ| p .

Example 20 Going back to our running example, we may decide to declare τ skc as a public type. Indeed, there is no name in P 1 DS having such a type. However, this will not change the resulting dependency graph as no term having such a public type is extractable from an output of the protocol.

Our second criterion is a precedence criterion: a position p of an output action can be safely marked if there exists a previous action such that the term at position p in can always be accessed in with a smaller set of keys. We use this criterion to obtain acyclic graphs for several protocols such as the Needham-Schroeder symmetric key protocol, as explained in the next section.

Lemma 17 Let ( , p) be a marked position of a simple protocol P w.r.t. a typing system (∆ 0 , δ 0 ) such that there exists an action labelled in P with:

out (c, u) follows the action involving term v in P ; -(u| p , p)#(S; A) ∈ ρ out (u) for some S and some A; -(u| p , q)#(S ; A ) ∈ ρ out (v) for some q, S and A such that S ⊆ mul S and A ⊆ mul A.

We have that ( , p.p ) is appropriate for any p such that δ 0 (u)| p.p is welldefined.

Intuitively, the sets S and A represent the keys needed to access u| p following the path p, while the sets S and A represent the keys needed to access u| p in v following the path q. Hence, if action precedes action and if u| p can be accessed more easily in action than in action (using only keys of S ∪ A rather than keys in S ∪ A), then it is not longer necessary to take into account what can be built from action at position p.

Proof We consider a well-typed execution P tr = = ⇒ (P; φ; σ; i) and an action out (c, w) occurring in tr. Let R be a destructor-only recipe 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 R 0 be R| 1...1 such that target(R 0 ) = p. We have that R 0 φ↓ = wφ| p , and we denote by R 1 key , . . . , R j key recipes occurring at position of the form 1 . . . 1.2 in R 0 . According to our hypothesis, we know that in ( , R in ) (resp. out ( , w )) occurs before out (c, w) in tr with R in φ↓| q = wφ| p in case corresponds to an input (resp. w φ| q = wφ| p in case corresponds to an output). Moreover, 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 } at key positions. 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.2 in R 0 , they form a submultiset of those occurring at position 1 . . . 1.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 , and therefore R (recipe which contains R 0 ) is not an asap recipe for Rφ↓ = wφ| p.p .

Our syntactic criteria are easy to check and it would be also easy to automate the marking of a graph following these two criteria.

Main results

It remains to conclude that we can decide reachability and trace equivalence whenever the refined dependency graph is acyclic. Thanks to Proposition 2 that ensures that a minimal well-typed, honest-free, simple and asap trace can be mapped to the refined dependency graph, the remaining proof can be adapted in a straightforward way.

First, we have the analog of Lemma 9 and Lemma 10, that is, we can bound the depth and width of the refined dependency graph of a minimal well-typed, honest-free, simple and asap trace, thanks to Proposition 2.

Lemma 18 Let (∆ 0 , δ 0 ) be a typing system and P be a simple protocol whose associated refined dependency graph G is acyclic. Let P tr = = ⇒ (P; φ; σ; i 0 ) be a well-typed honest-free execution involving simple asap recipes, and D its associated execution graph. We have that:

depth(D) ≤ depth(G).
Lemma 19 Let (∆ 0 , δ 0 ) be a typing system, and P be a simple protocol whose associated refined dependency graph G is acyclic. Let P tr = = ⇒ (P; φ; σ; i 0 ) be a well-typed honest-free execution involving simple asap recipes, and D its associated execution graph. We have that:

width(D) ≤ 1 + out P depth(G) × in P .
Decidability of reachability and trace equivalence then follow.

Theorem 7 Let P be a simple protocol type-compliant w.r.t. some typing system (∆ 0 , δ 0 ) and with an acyclic refined dependency graph. Let ∈ L(P ). The problem of deciding whether is reachable in P , i.e. whether P tr = = ⇒ ({i : io (c, u).Q} ∪ P; φ; σ; i)

for some trace tr, and io ∈ {in, out} is decidable.

Proof The proof follows the same lines than the proof of Theorem 1. Theorem 5 ensures the existence of a witness that only involves asap recipes. Then, we rely on Lemma 18 and Lemma 19 to establish the bound leading to the decidability result.

Theorem 8 Le P be a simple protocol type-compliant w.r.t. some typing system (∆ P , δ P ) and with an acyclic refined dependency graph. Let Q be another simple protocol. The problem of deciding whether P is trace included in Q is decidable.

Proof The proof follows the same lines than the proof of Theorem 2. Theorem 6 ensures the existence of a witness that only involves asap recipes. Then, we rely on Lemma 18 and Lemma 19 to establish the bound leading to the decidability result. Note that Lemma 13 still applies and does not need to be adapted.

Case studies

We have considered several protocols of the literature, to study whether our decidability result applies to them or not. More precisely, we have checked whether their dependency graph is acyclic or not and checked whether they are type-compliant.

Properties

We have considered two main security properties depending on the protocol. The first one is strong secrecy: a nonce or a key n is strongly secret if an attacker cannot learn any information about n. Following the game-based approach used in computational models, this has been modelled [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] as follows.

Even if the attacker knows the possible values for n, say a or b, she should not be able to distinguish whether the value a or the value b is exchanged, even if a and b are public. If P models a protocol, this is formally expressed as

P (a/n) ≈ t P (b/n).
For example, we have modelled strong secrecy of our running example in Example 6. However, strong secrecy is too strong to define the security of a key k, as soon as the key is used to encrypt. Indeed, imagine that the key k is used to encrypt some message m, that is, the message senc(m, k) is sent at some point. Then requiring strong secrecy of k would require at least that an attacker cannot distinguish between senc(m, a) and senc(m, b) where a and b are public values, that is, it would require that:

{w 1 senc(m, a)} ∼ s {w 1 senc(m, b)}.
But these frames can be distinguished with the test senc(sdec(w 1 , a), a) = w 1 .

Therefore, the security of such a key is expressed as key privacy. Intuitively, a key k is secure if an attacker cannot learn any information on messages that are encrypted by k. This can be intuitively modelled as:

{w 1 senc(a, k)} ∼ s {w 1 senc(b, k)}.
Moreover, the key k should be indistinguishable from a fresh key. In particular, the attacker should not be able to detect if the same key is used to encrypt all messages or if a fresh key is used each time. These two properties are encoded in a single equivalence, by requiring trace equivalence of P and Q where P represents the protocol that additionally sends senc(a, k) and Q represents the protocol that additionally sends senc(b, k ) where k is a fresh key.

Protocols and scenarios

We have considered a dozen of protocols of the literature, that use symmetric or asymmetric encryption, and possibly signatures. We do not recall the protocols here since most of them are standard and their description can be found in the literature, except for the passport case (see next section). For each protocol, we have considered a scenario where each role is instantiated by all possible players among 2 honest agents a and b and a dishonest one c. For example, if RoleInit(x, y) represents one session of the initiator role, where agent x talks to agent y, then we consider RoleInit(a, b), RoleInit(b, a), RoleInit(a, c), and RoleInit(b, c). We do not consider the cases where a dishonest agent communicates with other agents since this can already be simulated by the attacker. And we proceed similarly for the other roles of the protocols. Public-key protocols typically include two roles (initiator and responder) while symmetric key usually also involve a server. This corresponds to a total of 8 processes in the asymmetric case (4 for RoleInit, 4 for RoleResp, the role of the responder) and 14 processes in the symmetric case (4 for RoleInit, 4 for RoleResp, and 6 for RoleS, the role of the server). Then each of the processes is considered under replication. In other words, we consider the protocols with an unbounded number of sessions of each role, but with only two honest agents and one dishonest agent. In order to consider an unbounded number of agent names, we would need to model a more complex protocol with key generation, which may go beyond our class. An alternative approach is to rely in [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] that shows how to bound the number of agents, at the price of considering slightly more agents (2 honest and 2 dishonest agents) as well as some additional scenarios when an agent talks to itself.

Passport protocols

We describe the three less standard protocols that we have considered, namely the Basic Access Control (BAC) protocol, the Passive Authentication protocol (PA), and the Active Authentication protocols (AA). The three protocols are part of the protocol suite embedded in the biometric passport [START_REF]PKI for machine readable travel[END_REF]. They are run to authenticate the passport (and the passport holder, thanks to biometric data) to the reader. We present here the core protocols, as described in [START_REF] Hirschi | Description of some case studies[END_REF]. Basic Access Control. The BAC protocol aims at exchanging a session key between the Reader (R) and the Passport (P ), used in subsequent communications. It assumes that the reader and the passport already share an encryption key k e and a MAC key k m , that the reader derives from a seed read optically on the first page of the passport. At the end of the exchange, the reader and the passport share two session keys k R and k P that are used to derive an encryption session key ksenc and a MAC session key kmac. Actually, the passport additionally sends error messages when it receives ill-formed messages (for example if the MAC check fails). However, due to the restriction of our model (no else branch), we do not model this part of the protocol. We analyse unlinkability of the BAC protocol. Unlinkability intuitively says that an attacker, having seen a session from Alice and a session from Bob, should then not be able to distinguish Alice from Bob. This is modelled thanks to phases. In a first phase, the attacker interacts with two passports and two readers. In a second phase, the attacker interacts with either the first passport (and a reader) or the second one and she should not be able to distinguish the two cases.

Passive Authentication. The protocol assumes that the reader and the passport have just run BAC and share an encryption key ksenc and a MAC key kmac. In this protocol, the passport sends some biometric data dgp to the reader, authenticated by a certificate (the data have been signed by an authority, with signing key skds). R → P : senc(read, ksenc), hash(senc(read, ksenc), kmac) P → R : senc(datap, ksenc), hash(senc(datap, ksenc), kmac)

where datap = dgp, sign(hash(dgp), skds).

As for the BAC protocol, we analyse unlinkability.

Active Authentication. The active authentication protocol works similarly to the passive authentication protocol but prevents cloning the passport by copying a valid certificate. It assumes that the reader knows the verification key vk(sk P ) of the passport. The protocol authenticates the reader through a challenge-response mechanism where the protocol must sign a challenge r generated by the reader. The nonce n generated by the passport is used to model a randomised signature scheme.

R → P : senc((init, r), ksenc), hash(senc((init, r), ksenc), kmac) P → R : senc(sign((n, r), sk P ), ksenc), hash(senc(sign((n, r), sk P ), ksenc), kmac)

As for the BAC protocol, we analyse unlinkability.

Outcome

Since building a dependency graph may be cumbersome and error-prone, we have written a small program to compute the dependency graph of a protocol given its specification and a marking provided by the user. The program also checks that the marking complies with our definition and that type-compliance is satisfied. Note that a marking could actually be derived automatically following our two syntactic criteria but for simplicity, we did not implement this feature. The specifications of all protocols considered here, together with their associated dependency graph, can be found at [START_REF] Cortier | A decidable class of security protocols for both reachability and equivalence properties[END_REF].

The results of our study are displayed in Table 1. For each protocol, we indicate whether the resulting graph is acyclic. The fourth column of the table indicates whether we used the public type criterion whereas the fifth column indicates whether we used the precedence criterion. We note that all the obtained graphs are indeed acyclic with two exceptions: the Yahalom-Lowe and Needham-Schroeder protocols. The Needham-Schroeder protocol admits an attack and thes discovered cycle corresponds to the attack (although insecure protocols may also have an acyclic graph). The reasons of the cyclicity of the graph corresponding to Yahalom-Lowe are more subtle. The security of the protocol partly relies on the secrecy of a nonce N b that is first sent encrypted under a long-term key K bs for which we have strong secrecy guarantees and then later sent encrypted under the session key K ab . Our type system cannot exclude that N b gets revealed at this last step, and is maybe reused in an earlier step, hence creating a cycle.

Our result assumes type-compliance: whenever two encrypted subterms can be unified, they have the same type. For protocols that do not enjoy this property, type-compliance can be retrieved by adding a tag (e.g. a number) in each encryption, which is a good design practice as it avoids message confusion. The second column of the table indicates whether we needed to tag the protocol.

Note that in each case where the resulting graph is acyclic, we can compute a bound on the number of sessions that needs to be analysed, hence reducing decidability of equivalence to the bounded case.

Conclusion

We have identified a novel decidable fragment of security protocols for both reachability and trace equivalence. Most of standard protocols used as library of examples for automatic tools fall into our class. However, we have considered only relatively simple protocols. As further work, we should explore whether industrial-scale protocols fall into our class like TLS 1.3 or 5G protocols. This is probably not the case due to the fact that we do not handle else branches. To tackle this issue, we would first need to extend [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] to else branches, that is, showing that whenever there is an attack, there is also a well-typed attack in the presence of else branches.

An interesting feature of our approach is that, for each protocol of our class, we can compute an explicit bound on the number of sessions that need to be considered. This bound is still quite high but thanks to the recent progress of tools like 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], we can hope that it will be possible to analyse protocols of our class (hence for an unbounded number of sessions) with automatic tools, that decide security for a bounded number of sessions. In particular, it was shown in [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF] that about a hundred of sessions can now be analysed automatically with SAT-Equiv, for some relatively small protocols of the literature. We believe that we can further refine the computation on the bound on the number of sessions in order to match a bound that tools can reach. To provide a tighter bound, we could for example distinguish when we need a full session or only the first steps of some role, guided by the dependency graph. This would probably require to further refine the dependency graph.

Also, in order to cover a larger class of protocols, one approach is to show that we can soundly remove some additional arrows of the dependency graph. One first step would be to provide additional syntactic criteria for appropriate markings.

Fig. 1 Fig. 2

 12 Fig. 1 Semantics of our process algebra

Example 18 1 DS= in P 1 DS= 6

 18116 Continuing Example 13, the dependency graph G for the protocol P 1 DS is of depth depth(G) = 4. We have out P , hence the number of vertices of the execution graph is bounded by (2 + 6 5 ) 5 , hence more than 10 19 .

1 .

 1 If T is a recipe (message/atomic message/public key), then µ(T ) = |R| 2. If T is made of two recipes R and R (equality test/signature test), then µ(T ) = |R| + |R |.

R

  → P : getChall P → R : n P R → P : senc((n R , n P , k R ), k e ), hash(senc((n R , n P , k R ), k e ), k m ) P → R : senc((n P , n R , k P ), k e ), hash(senc((n P , n R , k P ), k e ), k m )

  t n ; -E = ρ out (t 1 , p.1, S, A) when t = sign(t 1 , t 2 ); when root(t) ∈ {senc, rsenc}, E = ∅ if t| 2 has an honest type, and E = ρ out (t 1 , p.1, S {t| 2 }, A) otherwise; when root(t) ∈ {aenc, raenc}, E = ∅ if t| 21 has an honest type, and E = ρ

out (t 1 , p.1, S, A {t| 21 }) otherwise.

Table 1

 1 Acyclicity of the dependancy graphs of protocols of the literature.

		tagged property	public types	precedence	acyclicity
	Symmetric protocols
	Denning-Sacco		Kpriv	#
	Needham-Schroeder		Kpriv	#	#
	Otway-Rees	#	Ssec	#	#
	Wide-Mouth-Frog	#	Ssec	#
	Kao-Chow (variant)	#	Kpriv	#	#
	Yahalom-Paulson	#	Kpriv	#	#
	Yahalom-Lowe	#	Kpriv	#
	Asymmetric protocols
	Running example		Ssec
	Denning-Sacco with signature		Kpriv	#
	Needham-Schroeder	#	Ssec	#
	Needham-Schroeder-Lowe	#	Ssec	#
	Passport
	BAC	#	Unlink
	Passive Authentication		Unlink
	Active Authentication		Unlink
	Ssec: strong secrecy	Kpriv: key privacy

Acknowledgements The research leading to these results has received funding from the European Research Council under the European Union's horizon 2020 research and innovation program (ERC grant agreement n • 714955-POPSTAR and ERC grant agreement n • 645865-SPOOC), as well as from the French National Research Agency (ANR) under the project TECAP.