Véronique Cortier

Antoine Dallon

Stéphanie Delaune

Efficiently deciding equivalence for standard primitives and phases

Privacy properties like anonymity or untraceability are now well identified, desirable goals of many security protocols. Such properties are typically stated as equivalence properties. However, automatically checking equivalence of protocols often yields efficiency issues. We propose an efficient algorithm, based on graph planning and SATsolving. It can decide equivalence for a bounded number of sessions, for protocols with standard cryptographic primitives and phases (often necessary to specify privacy properties), provided protocols are well-typed, that is encrypted messages cannot be confused. The resulting implementation, SAT-Equiv, demonstrates a significant speed-up w.r.t. other existing tools that decide equivalence, covering typically more than 100 sessions. Combined with a previous result, SAT-Equiv can now be used to prove security, for some protocols, for an unbounded number of sessions.

Introduction

Security protocols are notoriously difficult to design. A common good practice is to formally analyse protocols using symbolic techniques, in order to spot flaws possibly before their deployment (e.g. TLS 1.3 [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1.3[END_REF][START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF], an avionic protocol [START_REF] Blanchet | Symbolic and computational mechanized verification of the arinc823 avionic protocols[END_REF]). These symbolic techniques are mature for reachability properties like confidentiality or authentication. More recently, this approach has been extended to privacy properties, such as vote secrecy, anonymity, untraceability, or unlinkability. These properties are expressed through equivalences. For example, in the case of biometric passports, an attacker should not be able to distinguish whether she is in contact with Alice's passport or Bob's passport.

Recently, a new tool, SAT-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], has been proposed to decide such equivalence properties for security protocols, for a bounded number of sessions. It is based on a standard model-checking approach, namely graph planning [START_REF] Blum | Fast planning through planning graph analysis[END_REF][START_REF] Kautz | Planning as satisfiability[END_REF] and SAT-solving. Intuitively, protocols executions are over-approximated as a graph planning problem, which allows to consider several possible interleavings in parallel, allowing the analysis of dozen of sessions of a protocol in a few seconds. However, this result is limited to a very small set of primitives, namely symmetric encryption and concatenation.

Our contributions. Building upon this novel approach, we enrich SAT-Equiv in order to cover protocols using asymmetric primitives and/or phases. As for the original SAT-Equiv, we assume a non confusion property: encrypted messages should not be confused, a condition automatically checked by our tool and which can be enforced e.g. through appropriate labelling.

First, we extend SAT-Equiv to cover all standard primitives: symmetric and asymmetric encryption, signatures, and hashes. Since graph planning is a bounded model-checking technique, SAT-Equiv relies on a small model property, that bounds the size of messages. More precisely, [START_REF] Chrétien | Typing messages for free in security protocols: the case of equivalence properties[END_REF] guarantees that if there is an attack, then there is a well-typed attack, where messages follow a fix format. This result has been recently extended to standard primitives [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. The straightforward extension of SAT-Equiv to standard primitives however yields severe efficiency issues. Indeed, unlike the symmetric encryption case, checking whether two sequences of messages are equivalent (i.e. in static equivalence) may require complex tests where the attacker construct messages (that is, hash or asymmetrically encrypt messages). We therefore provide a precise characterisation of the set of tests that need to be considered when checking for static equivalence. This characterisation is of independent interest and could be used in other contexts. We also extend SAT-Equiv to consider protocols with phases, which are useful to model game-based properties.

Our extension of SAT-Equiv now provably terminates. In [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], termination can be guaranteed by checking that any state of the planning graph is indeed reachable, which requires to query a SAT-solver at each step. While this provides termination in theory, this yields a non practical algorithm and has not been implemented. Instead, we exhibit a bound on the maximal length of the smallest attack (bounding the attacker steps as well). It is therefore sufficient to stop the construction of the graph planning once this bound has been reached, enforcing termination for free (no computation overhead).

Finally, we have considerably revisited and improved the original implementation of SAT-Equiv. This significant speedup now allows for security proofs for an unbounded number of sessions. Indeed, [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] shows decidability of equivalence, for an unbounded number of sessions, for protocols with an acyclic dependency graph. The notion of dependency graph is introduced in [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] and intuitively captures how the input/output actions of the protocol may use messages from other steps of the protocol. As a corollary, [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] induces a bound on the number of sessions that needs to be considered for an attack, which depends on the size and structure of the graph. This bound can be rather large (50 to 100 sessions, even on small examples) but SAT-Equiv is now able to reach such bounds. These novelties are implemented in an extension of SAT-Equiv and compared with the other tools of the literature, namely Spec [START_REF] Dawson | Automating open bisimulation checking for the spi-calculus[END_REF], Akiss [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF] and the very recent DeepSec [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] tool. Our experiments show that SAT-Equiv is much faster on all the examples, allowing to reach typically more than 100 sessions. As an application, we consider two protocols, Denning-Sacco and Needham-Schroeder symmetric keys, shown to have acyclic dependency graphs in [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF]. Considering the necessary number of sessions as induced by [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF], we establish trace equivalence for these two protocols, for an unbounded number of sessions.

The tool source, the example files as well as all the proofs are available in [1].

Related work. There are two main families of tools to analyse equivalence properties on security protocols. Some tools prove equivalence for an arbitrary number of sessions, that is, no matter how often a protocol is used. The main tools in this category are ProVerif [START_REF] Blanchet | Automated Verification of Selected Equivalences for Security Protocols[END_REF], Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF], Maude-NPA [START_REF] Escobar | A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties[END_REF], Type-Eq [START_REF] Cortier | A type system for privacy properties[END_REF]. Maude-NPA often suffers from termination issues when used for equivalence properties. Type-Eq [START_REF] Cortier | A type system for privacy properties[END_REF][START_REF] Cortier | Equivalence properties by typing in cryptographic branching protocols[END_REF] is a sound (but incomplete) type-checker for equivalence properties that has good performance. It requires that protocols have a similar structure. ProVerif and Tamarin work well in practice. They actually prove a stronger notion of equivalence, diff-equivalence, that also requires that the two considered protocols have a very similar structure. Moreover, equivalence properties are undecidablein general for an unbounded number of sessions. Therefore, ProVerif may not terminate and Tamarin may need some user guidance.

A second approach consists in deciding equivalence, for a bounded number of sessions. Spec [START_REF] Dawson | Automating open bisimulation checking for the spi-calculus[END_REF] is one of the first tool that decides equivalence of security protocols but it does not scale well when the number of sessions grows (it can typically handle up to three sessions for small protocols). DeepSec [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] is a very recent tool that builds upon Akiss [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF] and Apte [START_REF] Cheval | Apte: an algorithm for proving trace equivalence[END_REF]. All these tools analyse symbolic executions and typically have to consider all possible interleavings between the roles of the protocol, which often raises efficiency issues.

Model

Protocols are modeled through a process algebra, in the spirit of the applied-pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. We consider here the model used in [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF][START_REF] Chrétien | Typing messages for free in security protocols[END_REF].

Term algebra

As usual, messages are modeled by terms. Private data are represented through an infinite set N of names used to model e.g. keys or nonces. We consider an infinite set C 0 of constants to represent public data such as agent names or attacker's nonces or keys. We consider also two sets of variables X and W. Variables in X model arbitrary data expected by the protocol, while variables in W are used to store messages learnt by the attacker. A data is either a constant, a variable, or a name. Cryptograhic primitives are represented by function symbols. We consider the signature Σ parameterised by n ≥ 2:

-Σ c = {senc, aenc, hash, pub, sign, vk, ok}

∪ { k | 2 ≤ k ≤ n}; -Σ d = {sdec, adec, getmsg} ∪ {proj k j | 2 ≤ k ≤ n and 1 ≤ j ≤ k}; and -Σ = Σ c ∪ Σ d ∪ {check}.
The symbols senc, aenc, sdec, and adec of arity 2 are used to model resp. symmetric and asymmetric encryption. We also consider signature sign and hash function hash. Concatenation of messages is modeled through tuple operators together with their projection functions. For example, m 1 , m 2 , m 3 3 represents the concatenation of the three messages m 1 , m 2 , and m 3 . It is syntactically different from the nested pairs m 1 , m 2 , m 3 2 2 . These two representations correspond to different implementation choices. We distinguish between constructors in Σ c and destructors in Σ d . The symbol check of arity 2, that corresponds to the verification of a signature, is neither a destructor nor a constructor. The set of terms built from a signature F and a set of data D is denoted T (Σ, D). Given a term u, we denote St(u) the set of its subterms, vars(u) the set of its variables, and root(u) its root symbol. A term 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. Two terms u 1 and u 2 are unifiable when there exists a substitution σ such that u 1 σ = u 2 σ.

We consider two sorts: atom and bitstring. The sort atom represents atomic data like nonces or keys while bitstring models arbitrary messages. Names in N and constants in C 0 have sort atom. Any f ∈ Σ c comes with its sorted arity: → bitstring pub : atom → bitstring vk : atom → bitstring hash : bitstring → bitstring

Given D ⊆ C 0 ⊎ X , the set T 0 (Σ c , D) is the set of terms t in T (Σ c , D) such that (i) for any term pub(u) (resp. vk(u)) in St(t), u is of sort atom; (ii) for any aenc(u, v) ∈ St(t), v = pub(v ′ ) for some v ′ . Terms in T 0 (Σ c , N ⊎ C 0 ) are called messages.
Intuitively, messages are terms with atomic keys.

The properties of the cryptographic primitives are reflected through the following convergent rewriting rules. sdec(senc(x, y), y) → x adec(aenc(x, pub(y)), y) → x getmsg(sign(x, y)) → x check(sign(x, y), vk(y)) → ok proj k j ( x 1 , . . . , x k k ) → x j with 2 ≤ k ≤ n and 1 ≤ j ≤ k 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, in particular they do not contain destructor symbols. As usual, we denote → * the reflexivetransitive closure of →, and u↓ the normal form of a term u.

An attacker builds his own messages by applying public function symbols to terms he already knows and that are available through variables in W. Formally, a computation done by the attacker is a recipe, i.e. a term in T (Σ, W ⊎ C 0 ).

Process algebra

We consider processes that may receive and send messages. We assume that each process communicates on a dedicated public channel. In practice, ip adresses and sessions identifiers are typically used to desambiguate which message is adressed to who and for which session. Of course, these channels may be freely manipulated by the attacker. Since we consider equivalence properties, distinct (public) channels provide more abilities for the adversary to distinguish between protocols. Formally, given a set Ch of channels, we consider the fragment of simple processes without replication built on basic processes as defined e.g. in [START_REF] Cheval | Deciding equivalencebased properties using constraint solving[END_REF]. Definition 1. A basic processes is defined as follows:

P, Q := 0 | in(c, u 1 ).P | out(c, u 2 ).P | i:P with u 1 , u 2 ∈ T 0 (Σ c , C 0 ⊎N ⊎X ), c ∈ Ch,
and increasing phase numbers. A simple process is a multiset of basic processes on pairwise distinct channels. A protocol is a simple process such that all its variables are in the scope of an input.

The process 0 does nothing and we often omit it. The process "in(c, u 1 ).P " expects a message m of the form u 1 on channel c and then behaves like P σ where σ is a substitution such that m = u 1 σ. Note that checking whether a received message has the expected form is done through pattern-matching instead of explicit tests. The process "out(c, u 2 ).P " emits u 2 on c, and then behaves like P . Our calculus also has a phase instruction, in the spirit of [START_REF] Blanchet | Automated Verification of Selected Equivalences for Security Protocols[END_REF], denoted i:P . This instruction is useful to model security requirements, for example in case the attacker interacts with the protocol before being given some secret.

Example 1. As an illustrative example, we consider a simplified version of the Denning-Sacco protocol which is a key distribution protocol relying on asymmetric encryption and signature. Informally, the protocol is as follows.

A → B : aenc(sign( A, B, K ab , prv(A)), pub(B))

The agents A and B aim at authenticating each other and establishing a fresh session key K ab . We model this protocol in our formalism through the simple process P DS = {P A ; P B } where P A = out(c A , aenc(sign( a, b, k ab 3 , sk a ), pub(sk b ))).0 and P B = in(c B , aenc(sign( a, b, x 3 , sk a ), pub(sk b ))).0 where sk a , sk b , and k ab are names, a and b are constants, and x is a variable.

The operational semantics of a process is defined using a relation over configurations. A configuration is a tuple (P; φ; σ; i) with i ∈ N and 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 dom(σ) = fv (P), 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, and σ stores the value of the variables that have already been instantiated. We write P instead of 0:P and P ⊎ P instead of {P } ⊎ P. Given a protocol P, we also often write P instead of (P; ∅; ∅; 0). The operational semantics is induced by the relation α -→ over configurations defined in Figure 1. For example, the In rule defines how messages can be input on a (public) channel: the adversary may 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.

Move

(P; φ; σ; i)

phase i ′ ----→ (P; φ; σ; i ′ ) with i ′ > i.

Phase

(i ′ :i ′′ :P ∪ P; φ; σ; i) τ --→ (i ′′ :P ∪ P; φ; σ; i) Fig. 1. Semantics for processes send any message, provided she can construct it through a recipe R applied on her previous knowledge φ. Note that only messages can be received (and sent).

The relation tr -→ between configurations (where tr is a possibly empty sequence of actions) is defined in the usual way. Given a configuration K, we write:

trace(K) = {(tr, φ) | K tr -→ (P ′ ; φ; σ; i) for some configuration (P ′ ; φ; σ; i)}.
Example 2. Continuing Example 1, let K DS = ({P A ; P B ; P B ′ }; φ 0 ; ∅; 0) where P B ′ models an additional session of the role B obtained by simply renaming c B and x with c ′ B and x ′ . The frame φ 0 = {w a ⊲ vk(sk a ), w b ⊲ pub(sk b )} models the fact that the attacker initially knows the public key of b and the verification key of a. We consider a simple scenario without dishonest participant. The trace tr 0 = out(c A , w 1 ).in(c B , w 1 ).in(c ′ B , w 1 ) is executable from K DS , and yields φ = φ 0 ⊎ {w 1 ⊲ aenc(sign( a, b, k ab 3 , sk a ), pub(sk b ))}, i.e. (tr 0 , φ) ∈ trace(K DS ).

Type-compliance

We present here our main assumption on protocols. Intuitively, we assume that ciphertexts cannot be confused, and we rely for this on a notion of typing system. Definition 2. A typing system is a pair (T init , δ) where T init is a set of elements called initial types, and δ is a function mapping data in C 0 ⊎ N ⊎ X to types τ :

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

δ(f(t 1 , . . . , t n )) = f(δ(t 1 ), . . . , δ(t n )) with f ∈ Σ c .
A configuration is type-compliant if two unifiable encrypted subterms have the same type. We write ESt(t) for the set of encrypted subterms of t, i.e.

ESt(t) = {u ∈ St(t) | u is of the form f(u 1 , . . . , u n ) and f = i }. Definition 3. A configuration K is type-compliant w.r.t. a typing system (T init , δ) if for every t, t ′ ∈ ESt(K) we have that t and t ′ unifiable implies that δ(t) = δ(t ′ ).
Example 3. Continuing our running example, we consider the typing system generated from T DS = {τ a , τ b , τ k , τ sk } of initial types, and the function δ DS that associates the expected type to each constant/name (δ DS (a) = τ a , δ DS (k ab ) = τ k , etc), and such that δ DS (x) = δ DS (x ′ ) = τ k . We have that K DS is type-compliant w.r.t. (T DS , δ DS ): unifiable encrypted subterms occurring in the configuration have the same type since δ DS (x) = δ DS (x ′ ) = δ DS (k ab ).

Type-compliant protocols have the property that, when looking for attacks, it is sufficient to consider well-typed execution. Formally, an execution K tr -→ (P; φ; σ; i) is well-typed w.r.t. a typing system (T init , δ), if σ is a well-typed substitution, i.e. every variable of its domain has the same type as its image.

Trace equivalence

Many privacy properties such as vote-privacy or untraceability are expressed as trace equivalence [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF][START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF]. Intuitively, two configurations are trace equivalent if an attacker cannot tell with which of the two configurations he is interacting. We first introduce a notion of equivalence (actually, inclusion) between frames. Definition 4. 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 message implies that Rφ 2 ↓ is message; -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 ↓.
Intuitively, φ 1 is included in φ 2 if any recipe producing a message in φ 1 also produces a message in φ 2 and if any equality satisfied in φ 1 is also satisfied in φ 2 .

Example 4. We consider

φ 1 = φ ⊎ {w 2 ⊲ senc(m 1 , k ab ), w ′ 2 ⊲ senc(m 1 , k ab )}, and φ 2 = φ ⊎ {w 2 ⊲ senc(m 2 , k), w ′ 2 ⊲ senc(m 2 , k ′ )} where m 1 , m 2 ∈ C 0 . We have that w 2 φ 1 ↓ = w ′
2 φ 1 ↓ whereas this equality does not hold in φ 2 . Hence φ 1 ⊑ s φ 2 . Trace inclusion is the active counterpart of static inclusion. Two configurations are in trace inclusion if, however the attacker behaves, the resulting sequences of messages observed by the attacker are in static inclusion. Definition 5. Let K and K ′ be two configurations. We have that K ⊑ t K ′ , if for every (tr, φ) ∈ trace(K), there exists (tr, φ ′ ) ∈ trace(K ′ ) such that φ ⊑ s φ ′ .

We easily derive a notion of trace equivalence: two configurations K and K ′ are trace equivalence, denoted K ≈ t K ′ , if K ⊑ t K ′ and K ′ ⊑ t K. This notion of trace equivalence slightly differs from the one used in e.g. [START_REF] Chrétien | Typing messages for free in security protocols: the case of equivalence properties[END_REF] but they actually coincide on the class of protocols we consider in this paper [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF].

Example 5. To model the secrecy of the key k ab , we define strong secrecy of k ab by requiring that k ab is indistinguishable from a fresh value. Formally, we consider P 1 B (resp. P 1 B ′ ) obtained by replacing the process 0 with 1:out(c B , senc(m 1 , x))

(resp. 1:out(c ′ B , senc(m 1 , x ′ ))).
On the other side of the equivalence, we consider P

From static inclusion to planning

The overall objective of this paper is to provide a practical algorithm for deciding trace inclusion (and thus trace equivalence) relying on graph planning and SAT solving. We start here by explaining how to build a planning problem to two frames such that the planning problem has a solution if, and only if, the two corresponding frames are not in static inclusion.

Planning problems

We first recall the definition of a planning problem, slightly simplified from [START_REF] Compagna | SAT-based Model-Checking of Security Protocols[END_REF]. Intuitively, a planning system defines a transition system from sets of facts to sets of facts. New facts may be produced and some old facts may be deleted. Given a rule r ∈ Rule of the form Pre -→ Add; Del, we denote Pre(r) = Pre, Add(r) = Add, and Del(r) = Del. If S ⊆ F act are such that Pre(r) ⊆ S, then we say that the rule is applicable in S, denoted S r -→ S ′ , and the state S ′ = (S Del) ∪ Add is the state resulting from the application of r to S. We allow some rules to be applied in parallel when no facts are deleted. Given S ⊆ F act, and a set of rules {r 1 , . . . , r k } such that Del(r i ) = ∅ and Pre(r i ) ⊆ S for any i ∈ {1, . . . , k}, {r 1 , . . . , r k } is applicable in S, denoted S {r1,...,r k } ------→ S ′ , and the state S ′ = k i=1 Add(r i ) ∪ S is the state resulting from the application of {r 1 , . . . , r k } to S.

A planning path from S 0 ⊆ F act to S n ⊆ F act is a sequence r 1 , . . . , r n made of rules or sets of rules in Rule such that S 0 r1 -→ S 1 r2 -→ . . . S n-1 rn -→ S n for some stated S 1 , . . . , S n-1 ⊆ F act. A planning problem for a system Θ = F act, Init, Rule is a pair Π = Θ, S f where S f ⊆ F represents the target facts. A solution to Π = Θ, S f , called a plan, is a planning path from Init to a state S n such that S f ⊆ S n .

A transition S {r1,...,r k } ------→ S ′ can be mimicked by S r1 -→ S 1 r2 -→ . . . r k -→ S ′ , thus the possibility of applying set of rules in a single step does not change the set of reachable states from a given state S. However, this allows us to consider plans of smaller length and will be useful later on to derive a tight bound and ensure the termination of our algorithm.

In this section, we explain the translation of static inclusion into a planning problem. We consider an (infinite) set F act 0 of facts that represent the attacker's knowledge, i.e. formulas of the form att(u P , u Q ) where u P and u Q are messages, plus a special symbol bad. Intuitively, att(u P , u Q ) represents the fact that the attacker knows u P in the "left" frame, while he knows u Q in the "right" one.

Attacker analysis rules

Following [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], we first describe the planning rules that correspond to the analysis part of the attacker behaviours. We start by describing a set of abstract rules R Ana that we instantiated later on, yielding a (concrete) planning system. att( x 1 , . . . , x k k , y 1 , . . . , y k k ) -→ att(x i , y i ) with i ≤ k att(senc(x 1 , x 2 ), senc(y 1 , y 2 )), att(x 2 , y 2 ) -→ att(x 1 , y 1 ) att(aenc(x 1 , pub(x 2 )), aenc(y 1 , pub(y 2 ))), att(x 2 , y 2 ) -→ att(x 1 , y 1 ) att(sign(x 1 , x 2 ), sign(y 1 , y 2 )) -→ att(x 1 , y 1 ) These rules correspond to the attacker's ability to project, decrypt, and retrieve messages from their signature. There is no Del since the attacker never forgets. Given a rule r ∈ R Ana , we explain how to compute its concretization.

Concrete + (r). The positive concretizations of r consist of instantiating r such that the resulting terms are messages. More formally, we have:

Concrete + (r) = {rσ | σ substitution such that rσ only involve messages.} Concrete -(r). We say that a sequence of facts att(u 1 , v 1 ), . . . , att(u k , v k ) leftunifies with a sequence att(u

′ 1 , v ′ 1 ), . . . , att(u ′ k , v ′ k ) if there exists σ such that u ′ 1 σ = u 1 , . . . , u ′ k σ = u k (
and symmetrically for right-unification). Given an abstract attacker rule r = Pre -→ Add, we define Concrete -(r) as the set containing f 1 , . . . , f k -→ bad for any sequence of facts f 1 , . . . , f k ∈ F act such that f 1 , . . . , f k left-unifies with Pre, whereas f 1 , . . . , f k does not right-unify with Pre.

Example 6. The negative concretizations of the abstract rule corresponding to asymmetric decryption are all the concrete rules of the form att(aenc(u 1 , pub(u 2 )), v), att(u 2 , v ′ ) -→ bad where u 1 , u 2 , v, v ′ , aenc(u 1 , pub(u 2 )) are messages, whereas adec(v, v ′ )↓ is not.

Static inclusion

According Definition 4, to break static inclusion, an attacker may build new terms (using both analysis and synthesis rules) but also check for equalities and computation failures. To encode static inclusion using planning in an efficient way, we need to strictly control the terms that an attacker has to synthetise.

We say that R is destructor-

only if R ∈ T (Σ d , C 0 ∪ W). It is simple if there exist destructor-only recipes R 1 , . . . , R k , and a context C made of constructors such that R = C[R 1 , . . . , R k ].
Definition 7. 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 ′ .

We write φ ⊑ simple + s ψ when the test described at item 2 is only performed when

(i) either R is destructor-only; (ii) or root(R) ∈ {senc}∪{ k | 2 ≤ k ≤ n}, and root(R ′ ) = adec.
This notion of static inclusion is equivalent to the original one.

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

φ ⊑ s ψ ⇔ φ ⊑ simple s ψ ⇔ φ ⊑ simple + s ψ.
From this new characterisation of static inclusion ⊑ simple s , we derive the planning rules that capture all the cases of failures.

R atom fail = {att(u, v) -→ bad | u is an atom but v is not} R pub fail = {att(pub(u), v) -→ bad | v is not of the form pub(v ′ )} R check fail = att(sign(u 1 , u 2 ), v 1 ) att(vk(u 2 ), v 2 ) -→ bad | check(v 1 , v 2 )↓ is not a message R test fail =    att(u 1 , v 1 ), . . . , att(u k , v k ) att(C[u 1 , . . . , u k ], v) -→ bad | C is a constructor context, C[u 1 , . . . , u k ] ∈ St(φ) ∪ C 0 v = C[v 1 , . . . , v k ].
   Actually, not all subterms of St(φ) need to be considered. Therefore, we consider an optimised version that captures only the terms that may not be reconstructed from their subterms. Formally, St opti (t) is defined as follows.

-

St opti ( t 1 , t 2 ) = St opti (t 1 ) ∪ St opti (t 2 ); -St opti (senc(t 1 , t 2 )) = St opti (t 1 ); -St opti (aenc(t 1 , t 2 )) = {aenc(t 1 , t 2 )} ∪ (St opti (t 1 ) {t 1 }) -St opti (sign(t 1 , t 2 )) = {sign(t 1 , t 2 ) ∪ St opti (t 1 ); -St opti (f(t)) = {f(t)} with f ∈ {hash, pub, vk}.
Thanks to the fact that ⊑ simple + s is equivalent to static inclusion, we may only consider simple recipes which evaluation yields a term in St opti (φ).

Lemma 2. Let φ be a frame, R = C[R 1 , . . . , R k ] be a simple recipe such that root(R) ∈ {senc} ∪ { k | 2 ≤ k ≤ n},
and R ′ be a destructor-only recipe such that root(R ′ ) = adec. Assume that Rφ↓ and R ′ φ↓ are both messages such that Rφ↓ = R ′ φ↓. We have that either C is the empty context, or Rφ↓ ∈ St opti (φ)∪C 0 .

Therefore, R test fail can be replaced by the following (smaller) set of rules:

R test1 fail = {att(u 1 , v 1 ), att(u 1 , v 2 ) -→ bad | v 1 = v 2 } R test2 fail = {att(u 1 , v 1 ), . . . , att(u k , v k ), att(C[u 1 , . . . , u k ], v) -→ bad | C is a non-empty constructor context, C[u 1 , . . . , u k ] ∈ St opti (φ) ∪ C 0 , and v = C[v 1 , . . . , v k ].}
Let φ and ψ be two frames with dom(φ) = dom(ψ) and built using constants from C ⊆ C 0 . The set of facts associated to φ and ψ is defined as follows:

Fact C (φ, ψ) = {att(a, a) | a ∈ C} ∪ {att(wφ, wψ) | w ∈ dom(φ)}
Two frames are in static inclusion if, and only if, the corresponding planning system has no solution. Actually, when the frames are not in static inclusion, we provide a bound on the length of the (minimal) plan witnessing this fact.

Proposition 1. Let φ and ψ be two frames with dom(φ) = dom(ψ), and Θ = F act 0 , Fact C0 (φ, ψ), R where

R = Concrete(R Ana ) ∪ R test1 fail ∪ R test2 fail ∪ R atom fail ∪ R check fail ∪ R pub fail . Let Π = Θ, {bad} .
We have that φ ⊑ s ψ if, and only if, Π has a solution of length at most (N + 1) × depth(φ) + 1 where N is the number of names n occurring in φ at a key position, i.e. such that n (resp. pub(n)) occurs in key position of an encryption in φ.

Intuitively, once all needed keys are derived, the minimal plan witnessing non-inclusion contains at most depth(φ) rules where depth(φ) is the maximal depth of a term occurring φ. Then we may need depth(φ) rule to derive each deducible key, hence the bound.

From trace inclusion to planning

We are now ready for the active case. Given two configurations, we show how to build a planning problem such that the planning problem has a solution if, and only if, the two corresponding configurations are not in trace inclusion.

In several places of this section, we will consider three special constants, namely c ⋆ 0 and c ⋆ 1 of sort atom, and c ⋆ + of sort bitstring. These three constants have a special type, denoted τ ⋆ .

Abstract protocol rules

We first define the abstract rules describing the protocol behaviour. We denote C P (resp. C Q ) the constants from C 0 occurring in P (resp. Q), For simplicity we assume that variables of P and Q are disjoint. In addition to the facts of the form att(u, v) used to represent attacker's knowledge, we also consider:

facts of the form Phase(i) with i ∈ N to represent phases; and facts of the form St(P, Q) = state c P,Q (id P , id Q ) where P , Q are two basic processes on channel c, and id P (resp. id Q ) is the identity substitution of domain fv (P ) (resp. fv (Q)).

Therefore, in this section, we consider the infinite set of facts F act 0 that consists of all the ground facts of this form, plus the special symbol bad.

To deal with phases, we mimic the Phase rule by considering basic processes in normal form w.r.t. the rule i:j:P -→ j:P . Then, the transformation Rule(P ; Q) from basic processes (in normal form) to abstract planning rules is defined by Rule(P ; Q) = ∅ when P = i:0, and otherwise: 1. Case output: i.e. if P = i:out(c, u).P ′ .

-

{St(P, Q), Phase(i) -→ att(u, v), St(P ′ , Q ′ ); St(P, Q)} ∪ Rule(i:P ′ ; i:Q ′ ) when if Q = i:out(c, v).Q ′ -{St(P, Q), Phase(i) -→ att(u, c ⋆ 0 ), bad} otherwise. 2.
Case input: i.e. P = i:in(c, u).P ′ .

-

{St(P, Q), att(u, v), Phase(i) -→ St(P ′ , Q ′ ); St(P, Q)} ∪ Rule(i:P ′ ; i:Q ′ ) when Q = i:in(c, v).Q ′ -{St(P, Q), att(u, x), Phase(i) -→ bad} otherwise (with x fresh).
Intuitively, abstract rules simply try to mimic each step of P by a similar step in Q. Clearly, if Q cannot follow P , the two processes are not in trace equivalence, which is modelled here by the bad state. Note that, in case P = i:out(c, u).P ′ whereas Q is not ready to perform an output, bad will be triggered only if the sent term is indeed a message. This transformation is then extended to protocols in a natural way considering in addition planning rule to model phase changes. We consider P = {P 1 , . . . , P n } and Q = {Q 1 , . . . , Q n }, and we assume w.l.o.g. that P i and Q i are basic processes on channel c i . We define:

-Rule(P, Q) = Rule(P 1 , Q 1 ) ∪ . . . ∪ Rule(P n , Q n ). -R phase = {Phase(i) -→ Phase(i + 1) ; Phase(i) | i ∈ N}.

Concrete protocol rules

Deriving concrete rules from the abstract ones can be obtained by instantiating them with arbitrary terms. However, this would not allow us to derive a decision procedure. Moreover, we would like our algorithm to have good performance. To achieve this, we first show that only three constants need to be considered (and no nonces), in addition to those explicitly mentioned in the protocol.

Given a protocol P that is type-compliant w.r.t. to a typing system (T P , δ P ) (and such that τ ⋆ does not occur in δ P (P)), an execution P tr -→ (P ′ ; φ ′ ; σ ′ ; i ′ ) is quasi-well-typed if δ P (xσ ′ ) δ P (x) for every variable x ∈ dom(σ ′ ) where is the smallest relation on types defined as follows:

τ ⋆ τ and τ τ for any type τ (initial or not);

-f(τ 1 , . . . , τ k ) f(τ ′ 1 , . . . , τ ′ k ) when τ 1 τ ′ 1 , . . . , τ k τ ′ k , and f ∈ Σ c .
The attacker needs at most the constants c ⋆ 0 , c ⋆ 1 , c ⋆ + to mount an attack.

Theorem 1. Let K P be an initial C 0 -configuration type-compliant w.r.t. (T P , δ P ) and K Q be another initial C 0 -configuration. Let C ⋆ = (C P ∪ C Q ) ⊎ {c ⋆ 0 , c ⋆ 1 , c ⋆ + }. We have that K P ⊑ t K Q w.r.t. C 0 if,
and only if, there exists a witness (tr, φ) ∈ trace(K P ) of this non-inclusion which only involves constants from C ⋆ , simple recipes, and with a quasi-well-typed underlying execution.

The existence of a quasi well-typed witness comes from [START_REF] Chrétien | Typing messages for free in security protocols[END_REF] with some extra work to guarantee that we can consider simple recipes. The reduction to three constants extends the previous reduction [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF] to asymmetric primitives.

Flattening. In terms of efficiency, one key step of our algorithm is to avoid composition rules from the attacker. For static inclusion, we only consider specific contexts, hence very specific synthesis rules, guided by the form of the underlying frames. For the active case, we transform protocol rules in order to pre-compute all necessary composition steps. This flattening step was already used in e.g. [START_REF] Armando | Sat-based model-checking for security protocols analysis[END_REF][START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], and is quite intuitive. We therefore only describe it informally on an example.

Consider our Denning Sacco protocol presented in Example 1. Agent B expects a message of the form u = {sign( a, b, x 3 , sk a )} pub(sk b ) . Either the attacker obtains a message m of the expected form, or the attacker obtains several components of it and forges the whole message. For example, it is sufficient for him to obtain m 1 of the form u 1 = sign( a, b, x 3 , sk a ) and m 2 of the form u 2 = pk(sk b ). Therefore, in addition to the (informal) protocol rule u → . . ., we also consider the rule u 1 , u 2 → . . .. Similarly, we also need to consider the rules a, b, x, sk a , pk(sk b ) → . . . and a, b, x, sk a , sk b → . . .. More generally, given an abstract protocol rule r, we can define Flat(r) the set of rules obtained by performing flattening on each fact. To decompose a term, we follow its structure, and the structure of a variable is given by its type. Moreover, when the other side of the process is not able to follow the decomposition, this leads us to a failure rule. A formal definition is provided in Appendix D.

Similarly to the static case, we define Concrete + (r) as the set of ground, quasi well-typed instantiations of a rule r where the instantiation of a state is obtained by simply composing the substitutions, i.e.

st c P,Q (σ P , σ Q )σ = st c P,Q (σ • σ P , σ • σ Q ).
We also define Concrete -(r) the concrete rule yielding to the bad state, when the right-hand side of the rule does not unify or is not a message. Given a pair of protocols, we initialise our planning system as follows.

Fact C (P, Q) = {Phase(0)} ∪ {att(c, c) | c ∈ C} ∪ {state c P,Q (∅, ∅) | P ∈ P, Q ∈ Q basic processes built on c}.
Our main technical result states that our encoding is sound and complete: two protocols are in trace inclusion if, and only if, the corresponding planning system has a solution. Moreover, when a witness of non-inclusion exists, we are able to bound the length of the resulting plan. Below, nb in (P) (resp. nb out (P)) denotes the number of inputs (resp. outputs) occurring in P whereas max phase (P) is the maximal integer occurring in a phase instruction in P.

Theorem 2. Let P a protocol type-compliant w.r.t. (T P , δ P ), and Q be another protocol. We consider the following set R of concrete rules:

Concrete(R Ana ∪ Flat(Rule(P, Q))) ∪ R phase ∪ R test1 fail ∪ R test2 fail ∪ R atom fail ∪ R check fail ∪ R pub fail Let Θ = F act 0 , Fact C ⋆ (P, Q), R
(P)) × [1 + nb in (P) + N ]
where N is the number of names occurring in P having a key type, i.e. such that δ P (n) (resp. pub(δ P (n))) occurs in key position of an encryption in δ P (P).

Proof. (Sketch) It is rather easy to establish that a solution to the planning problem defines a witness of non trace inclusion, Conversely, thanks to Theorem 1, if P ⊑ t Q, then there exists a quasi well-typed witness of non trace inclusion, that uses at most three constants (besides the constants of P and Q). This witness guides the definition of a plan of Π. Establishing a not too coarse bound on its length requires some care. It relies on the flattening of the protocol and the fact that the plan can mimic the computation of several messages in parallel.

Algorithm

Similarly to the algorithm presented in [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], we decide trace inclusion by applying graph planning and SAT-solving techniques to the planning problem that encodes trace inclusion (thanks to Theorem 2). Given a protocol P, type-compliant w.r.t. (T P , δ P ), and a protocol Q, our algorithm proceeds as follows.

1. It first computes the corresponding abstract rules, namely Flat(Rule(P; Q))∪ R Ana and the initial state Fact(P, Q). 2. It then applies a planning graph algorithm, a standard technique to solve planning problems (see e.g. [START_REF] Blum | Fast planning through planning graph analysis[END_REF]). The only difference is that, for efficiency reasons, we do not contruct the planning problem Π a priori but instead, we compute it "on the fly", while building the associated planning graph. This planning graph over-approximates the possible solutions by executing several actions in parallel, even if they may be incompatible. Some incompatibilities are recorded and propagated through so-called mutex. The planning graph is deemed to capture all possible plans. More precisely, the planning graph built until depth k captures all possible plans of length at most k. 3. In case no fact bad has been reached while building the planning graph, we can immediately conclude that P ⊑ t Q. Otherwise, since the planning graph over-approximates the possible executions, we need to check that bad is truly reachable. This is done by encoding each path leading to bad as a SAT formula. We then call the SAT solver mini-SAT to decide its satisfiability. In case bad is indeed reachable, mini-SAT provides a solution that is translated back to a witness of non-inclusion. To improve termination, we check accessibility of a state containing bad as soon as it appears in the graph, even if the construction of the graph is not completed yet.

Termination. The algorithm defined above may not terminate. The planning graph contains facts of the form att(u, v) where u must be (quasi) well-typed.

There is therefore only a finite number of such u. However, the planning graph construction may introduce several facts of the form att(u, v 1 ), . . . , att(u, v k ), where the v i get arbitrarily large. We exhibit some (contrived) examples in Appendix E where the algorithm does not terminate. [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF] suggests that termination could be enforce by checking at each step (thanks to the SAT-solver) that each node of the planning graph is indeed reachable. This would be however not practical. Instead, we can enforce termination thanks to the bound provided in Theorem 2 that also bounds the maximal depth of the planning graph that needs to be considered. Indeed, it is sufficient to simply stop the construction of the planning graph as soon as the bound is reached. The interest of this approach is that we guarantee termination at no cost (computing the bound is immediate).

In practice, the planning graph is typically much smaller than this bound.

SAT-Equiv. We have implemented our new algorithm in the tool SAT-Equiv, extending it to protocols with phases and all the standard cryptographic primitives and guaranteeing termination. Moreover, we significantly improve its efficiency by rewriting parts of the codes and modifying the data structure.

Experiments

In this section, we analyse several protocols of the literature and compare the results obtained using different tools. We ran our experiments a single Intel 3.1 GHz Xeon. We limit the memory to 128 Go (MO stands for memory out) and the execution time to 24h (TO stands for time out). For all the considered protocols, we analyse strong secrecy of the exchanged key or nonce, as for Example 5, except for the passport protocol (PA), for which we prove anonymity as in [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF]. We progressively increase the number of sessions in order to consider a semi complete scenario, where Alice's role is instantiated by honest a talking to honest b or dishonest c and Bob's role is instantiated by b talking to a or c. This typically corresponds to 7 sessions in the case of a symmetric key protocol (with 3 roles).

Comparison with the other tools

Our experiments show a significant speed-up w.r.t. the original version of SAT-Equiv [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF]. Our new is 100 faster in average, allowing to analyse about twice more sessions, as exemplified in Figure 2 (more experiments in [1]). We compare SAT-Equiv with other tools of the literature that decide equivalence for a bounded number of sessions, namely Spec [START_REF] Dawson | Automating open bisimulation checking for the spi-calculus[END_REF], Akiss [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF] and Deepsec [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF]. We did not include APTE in our study [START_REF] Cheval | Apte: an algorithm for proving trace equivalence[END_REF] as it is now subsumed by Deepsec. For each protocol, we progressively increased the number of sessions until we reached a time out. The overall results of our experiments are summarized in Figure 2. They show a significant speed-up even w.r.t. the very recent Deepsec tool. Note however that Deepsec covers more protocols (with else branches, or not type compliant), except if they include phases. Deepsec can also be parallelized thus the analysis time can be divided by the number of available cores. The detailed results for the Denning-Sacco protocol are below. The 2nd column for SAT-Equiv indicates the theoretical bound on the length of the planning graph, as given by Theorem 2. This illustrates that this bound remains reasonable although our tool actually terminates before reaching it.

Denning

Towards an unbounded number of sessions

Although equivalence is undecidable in general for an unbounded number of sessions, [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] exhibits a decidability result, for type-compliant protocols that have an acyclic dependency graph. Intuitively, the dependency graph captures how a message expected as input may be built (and therefore may depend) from messages sent as output of the protocol. Decidability is proven by showing that a (minimal) attack trace may be mapped to this dependency graph. Looking at the dependency graphs of the Denning-Sacco and the Needham-Schroeder symmetric key protocols, we deduce that it is sufficient to analyse respectively 42 and 94 sessions. Thanks to the efficiency of SAT-Equiv, we can easily analyse 42 sessions of Denning-Sacco (in 10s). We can therefore deduce from [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] that the protocol remains secure even if the considered sessions are arbitrarily replicated. The case of the Needham-Schroeder protocol requires a bit more work as 94 sessions is slightly out of reach of SAT-Equiv. However, we noticed that, according to [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF], we do not need to analyse 94 full sessions. Instead, some of some of them may be truncated (a minimal attack will use only the first step for example). Since SAT-Equiv can prove equivalence of these refined 94 sessions (in 20h30min), we can again deduce from [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] that the protocol remains secure even if the considered sessions are arbitrarily replicated.

As future work, we plan to optimize the bound on sessions induced by [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] and automatically generate the desired scenario, in order to extend SAT-Equiv to proofs of equivalence for an unbounded number of sessions.

A From static inclusion to planning

The main goal of this section is to prove Proposition 1. We introduce the notion of forced normal form, denoted u ։ . This is the normal form obtained when applying rewrite rules as soon as the destructor and the constructor match. More formally, we have that:

R f =    sdec(senc(x, y), z) ։ x adec(aenc(x, y), z) ։ x getmsg(sign(x, y)) ։ x check(x, y) ։ ok proj i j ( x 1 , . . . , x i i ) ։ x j with 2 ≤ i ≤ n and 1 ≤ j ≤ i
A term u can be rewritten in v using R f 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 . As usual, we denote ։ * , the reflexive-transitive closure of ։. We may note that such a rewriting system is confluent as it terminates and has no critical pair. From [START_REF] Chrétien | Typing messages for free in security protocols[END_REF], we get the following Lemma: Lemma 3. 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φ↓. Lemma 4. Let R be a recipe in normal form w.r.t. ։ such that Rφ↓ is a message for some frame φ. We have that R is a simple recipe.

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

Base case: R ∈ W ∪ C 0 . In both cases, the result holds since R is a simple recipe.

Induction case:

We have that R = f(R 1 , . . . , R k ) for some f ∈ Σ, and we know that R 1 , . . . , R k are in normal form w.r.t. ։.

-Case f ∈ Σ c . We have that Rφ↓ = f(R 1 φ↓, . . . , R k φ↓) is a message for some frame φ, and thus R i φ↓ is a message for i ∈ {1, . . . , k}. Applying our induction hypothesis on R i (1 ≤ i ≤ k), we easily conclude. -Case f = des ∈ Σ d ⊎ {check}. Let ℓ des -→ r des be the rewriting rule associated to des, and ℓ ′ des ։ r des be its associated forced rewriting rule. The case where des = check is impossible as R is in forced normal form. Therefore, we have that f ∈ {proj i j , sdec, adec, getmsg}. From now on, we assume that f = adec. The other cases can be done in a rather similar way. Since f = adec, we have that R = f(R 1 , R 2 ). As Rφ↓ is a message, R 1 φ↓ and R 2 φ↓ are messages. Applying our induction hypothesis, we deduce that both R 1 and R 2 are simple. As R 2 φ↓ is an atomic message, we know that R 2 is destructor-only. First, we assume that R 1 = g(R ′ 1 , . . . , R ′ n ) for some g ∈ Σ c . As Rφ↓ is a message, g = aenc. However, this contradicts the fact that R is in forced normal form. Thus, R 1 is destructor-only, and therefore R is simple.

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

φ ⊑ s ψ ⇔ φ ⊑ simple s ψ ⇔ φ ⊑ simple + s ψ. Proof. It is easy to see that φ ⊑ s ψ ⇒ φ ⊑ simple s ψ ⇒ φ ⊑ simple + s
ψ. Thus, we only consider the two other implications.

First implication: φ ⊑ simple s ψ ⇒ φ ⊑ s ψ. We consider an alternative definition of static inclusion, denoted ⊑ ′ s . This notion is similar to the one given in Definition 7 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 ψ. More precisely, given an arbitrary test T that holds in φ, we show that T also holds in ψ assuming that any test smaller than T have already been transfered 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.

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

µ(T ) = |R| + |R ′ |.
R is a recipe 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 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

R = C[adec(aenc(R 1 , R 2 ), R 3 )] and R ′ = C[R 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 (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 7.

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 ′ ψ↓. -Case 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.

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 forced normal form. R ։ (resp. R ′ ։ ) is a smaller recipe then 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 say 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 it concludes this case.

-Case R and R ′ are both simple recipes. In case they are both destructoronly recipes we conclude relying on our hypothesis. Otherwise, assume first

R = sign(R 1 , R 2 ).
In such a case, we have that vk(R 2 ) = R ′ and this test is smaller than R = R ′ , it holds in φ, and thus it can be transfered from φ to ψ by induction hypothesis. This allows us to conclude that R = R ′ holds in ψ. Now, assume that

R ′ = vk(R ′ 1 ). Since R ′ 1 φ↓ is an atomic message, R ′
1 is destructor only. We have that R ′ is destructor only, and thus sign(getmsg(R), R ′ ) is simple, R is destructor-only and the 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 ψ↓ = vk(s ′ ).
R is a recipe 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 ′ .

Second implication:

φ ⊑ simple + s ψ ⇒ φ ⊑ simple s ψ.
Let R be a simple recipe with constructor context C and R ′ be a destructor-only recipe such that Rφ↓ and R ′ φ↓ are both messages. Assume Rφ↓ = R ′ φ↓. We have to show that Rψ↓ = R ′ ψ↓. We show that such a test transfers from φ to ψ by induction on # senc (R) (number of occurrences of senc and . . . k at top level in C), and # adec (R ′ ) (number of occurrences of adec at top level in R ′ ) ordered lexicographically. Base case: (# senc (R), # adec (R ′ )) = (0, 0). In such a case, the test transfers by hypothesis.

Induction step: # senc (R) ≥ 1. In such a case, we consider R = senc(R 1 , R 2 ). We consider the test R 1 = sdec(R ′ , R 2 ). We have (R 1 = sdec(R ′ , R 2 ))φ so by induc- tion hypothesis, (R 1 = sdec(R ′ , R 2 ))ψ. We deduce that (R ′ = senc(R 1 , R 2 ))ψ that is (R = R ′ )ψ.
The case where R = R 1 , R 2 can be done in a similar way. Now, we consider the case where # senc (R) = 0 and # adec (R ′ ) ≥ 1. In such a case, we have that

R ′ = adec(R ′ 1 , R ′ 2 ). We consider the test aenc(R, pub(R ′ 2 )) = R ′ 1 . We still have that # senc (aenc(R, pub(R ′ 2 ))) = 0, and # adec (R ′ 1 ) < # adec (R ′ ). (aenc(R, pub(R ′ 2 )) = R ′ 1 )φ so by induction hypothesis (aenc(R, pub(R ′ 2 )) = R ′ 1 )ψ. We deduce that (R = adec(R ′ 1 , R ′ 2 ))ψ, that is (R = R ′ )ψ. ⊓ ⊔
Let t be a term, we define St ded (t) the set of subterms that occur at a deducible position as follows:

-St ded ( t 1 , . . . , t n n ) = { t 1 , . . . , t n n } ∪ St ded (t 1 ) ∪ . . . ∪ St ded (t n ); -St ded (f(t 1 , t 2 )) = {f(t 1 , t 2 )} ∪ St ded (t 1 ) with f ∈ {senc, aenc, sign}; -St ded (f(t)) = {f(t)} with f ∈ {hash, pub, vk}. Lemma 2. Let φ be a frame, R = C[R 1 , . . . , R k ] be a simple recipe such that root(R) ∈ {senc} ∪ { k | 2 ≤ k ≤ n},
and R ′ be a destructor-only recipe such that root(R ′ ) = adec. Assume that Rφ↓ and R ′ φ↓ are both messages such that Rφ↓ = R ′ φ↓. We have that either C is the empty context, or Rφ↓ ∈ St opti (φ)∪C 0 .

Proof. Let φ be a frame, R ′ be a destructor-only recipe such that R ′ φ↓ is a message. We first prove that R ′ φ↓ ∈ St ded (φ) ∪ C 0 by structural induction on R ′ .

Base case R ′ = w ∈ dom(φ) or R ′ = a ∈ C 0 . In both cases, we easily conclude that R ′ φ↓ ∈ St ded (φ) ∪ C 0 . Induction step: R ′ = g(R ′ 1 , . . . , R ′ k ).
We distinguish several cases depending on g.

In case g = sdec, we have that k = 2, R ′ 1 φ↓ = senc(t 1 , t 2 ), R ′ 2 φ↓ = t 2 , and R ′ φ↓ = t 1 for some t 1 , t 2 . Applying our induction hypothesis on R ′ 1 , we deduce that R ′ 1 φ↓ ∈ St ded (φ) ∪ C 0 , and thus R ′ φ↓ ∈ St ded (φ) ∪ C 0 . The case where R ′ = R ′ 1 , R ′ 2 , R ′ = getmsg(R ′ 1 ), and R ′ = adec(R ′ 1 , R ′
2 ) are similar. Now, we prove the proposition. Let R = C[R 1 , . . . , R k ] be a simple recipe such that root(R) ∈ {senc} ∪ { k | 2 ≤ k ≤ n}, and R ′ be a destructor-only recipe such that root(R ′ ) = adec. Thanks to the result we have just proved, we know that R ′ φ↓ ∈ St ded (φ) ∪ C 0 . Moreover, we know that either (i)

R ′ = w ∈ dom(φ) or (ii) R ′ = a ∈ C 0 or (iii) R ′ = g(R ′ 1 , . . . , R ′ k )
for some g ∈ Σ d {adec}. In cases (i) and (ii), we easily conclude that either C is empty or

Rφ↓ = C[R 1 φ↓, . . . , R k φ↓] ∈ St opti (φ) ∪ C 0 . In case (iii), assuming that g = sdec(R ′ 1 , R ′ 2 ), we deduce that R ′ 1 φ↓ ∈ St ded (φ) and since R ′ 1 φ↓ = senc(t 1 , t 2 ), we deduce that R ′ 1 φ↓ ∈ St opti (φ), and thus R ′ φ↓ ∈ St opti (φ) since R ′ φ↓ = Rφ↓ is headed neither with a symbol in { k | 2 ≤ k ≤ n},
nor with senc. The case where g ∈ { k | 2 ≤ k ≤ n} ∪ {getmsg} can be done in a similar way. Note that we know that g = adec.

⊓ ⊔ Before establishing Proposition 1, we start by establishing the following result regarding deduction using destructor-only recipes.

Lemma 5. Let φ and ψ be two frames having the same domain, and C ⊆ C 0 . Let Θ = F act 0 , Fact C (φ, ψ), Concrete + (R Ana ) and Π = Θ, {att(u, v)} for some messages u and v. If Π has a solution then there is a destructor-only C-recipe R such that Rφ↓ = u, and Rψ↓ = v.

Proof. Let π = r 1 , . . . , r n be a planning path from S 0 to S n , and att(u, v) ∈ S n . We show the result by induction on the length of π, and since applying planning rules in parallel does not change the set of reachable states, we assume w.l.o.g. that the planning path under study is such that each r i ∈ Concrete + (R Ana ). Base case. We have that π is empty. In such a case, by definition of S 0 , the result trivially holds. Inductive case. We know that r n is an instance of one of the abstract rules in R Ana , e.g. att(senc(u 1 , u 2 ), senc(v 1 , v 2 )), att(u 2 , v 2 ) -→ att(u 1 , v 1 ). Thanks to our induction hypothesis, we know that there exist:

-a destructor-only C-recipe R 1 such that R 1 φ↓ = senc(u 1 , u 2 ), and R 1 ψ↓ = senc(v 1 , v 2 ); -a destructor-only C-recipe R 2 such that R 2 φ↓ = u 2 , and R 2 ψ↓ = v 2 .
Therefore, the C-recipe R = sdec(R 1 , R 2 ) allows us to conclude. The reasoning is rather similar for the other rule.

⊓ ⊔

Let R be a destructor-only recipe. We denote by |R| main the length of its main path, i.e. the longest sequence of 1 which corresponds to a position in R. Lemma 6. Let φ be a frame, and R be a destructor-only recipe such that Rφ↓ is a message. We have that |R| main ≤ depth(φ).

Proof. We first establish that |R| main + depth(Rφ↓) ≤ depth(φ) for any R such that Rφ↓ is a message by structural induction on R. Base case: R = w or R ∈ C 0 . In such a case, we have

|R| main + depth(Rφ↓) = 0 + depth(Rφ↓) ≤ depth(φ).
Inductive case: R = g(R 1 , . . . , R k ) for some g ∈ Σ d . Since Rφ↓ is a message, we know that R 1 φ↓ is a message. Therefore, the induction hypothesis applies and we obtain that |R 1 | main + depth(R 1 φ↓) ≤ depth(φ). Moreover, we have that depth(R 1 φ↓) ≥ 1 + depth(Rφ↓), and |R| main = |R 1 | main + 1. Therefore, we have that:

|R| main + depth(Rφ↓) ≤ |R 1 | main + 1 + depth(R 1 φ↓) -1 ≤ depth(φ).
We have that |R| main + depth(Rφ↓) ≤ depth(φ). Since depth(Rφ↓) ≥ 0, we deduce that |R| main ≤ depth(φ).

⊓ ⊔ Given a destructor-only recipe R, the key-recipes of R, denoted Key(R), are all the recipes occurring as a subterm of R at a key position, i.e. as a second argument of sdec or adec, excepted those of the form c ∈ C 0 that do not count. This notation is extended as expected to sets of destructor-only recipes. Given a set of recipes R, we write |R| the number of elements occurring in it.

Lemma 7. Let φ and ψ be two frames having the same domain, and R be a set of destructor-only C-recipes such that Rφ↓ and Rψ↓ are messages for any R ∈ R.

Let Θ = F act 0 , Fact C (φ, ψ) ∪ {att(Rφ↓, Rψ↓) | R ∈ Key(R)}, Concrete + (R Ana )
, and Π = Θ, {att(Rφ↓, Rψ↓) | R ∈ R} . We have that Π has a solution of length at most depth(φ).

Proof. We show the existence of a solution of length at most ℓ = max{|R| main | R ∈ R}, and we conclude relying on Lemma 6 that ℓ ≤ depth(φ).

Base case: ℓ = 0. In such a case, we have that R ∈ dom(φ) ∪ C for any R ∈ R, and the empty planning path of length 0 is indeed a solution of Π.

Inductive case: ℓ > 0. Let R ′ = {R ∈ R | |R| main = ℓ} = {R 1 , . . . , R n }.
For each i ∈ {1, . . . , n}, we have that:

-either R i = des(R 1 i , R 2
i ) with des ∈ {adec, sdec}; and R 1 i φ↓ and R 1 i ψ↓, as well as R 2 i ψ↓ and R 2 i ψ↓ are messages. Moreover, we have that

R 2 i ∈ Key(R i ) or R 2
i ∈ C 0 , and thus by hypothesis, we have that att(R 2 i φ↓, R 2 i ψ↓) belongs to the initial state of our planning system Θ.

or R i = des(R 1 i ) with des ∈ {proj k ℓ , getmsg}; and R 1 i φ↓ and R 1 i ψ↓ are messages.

Moreover, we have that Key(R 1 i ) ⊆ Key(R ′ ) for any i ∈ {1, . . . , n}. Therefore, relying on our induction hypothesis, we deduce that there is a plan π 0 of length ℓ -1 of

Π 0 = Θ, {att(R 1 i φ↓, R 1 i ψ↓) | 1 ≤ i ≤ n} ∪ att(R ′ φ↓, R ′ ψ↓) | R ′ ∈ R R ′ } . Moreover, when R i = sdec(R 1 i , R 2 i ) (the case where R i = adec(R 1 i , R 2 i
) can be done in a similar way), as R i φ↓ and R i ψ↓ are messages, we know that

R 1 i φ↓ = senc(R i φ↓, R 2 i φ↓) and R 1 i ψ↓ = senc(R i ψ↓, R 2 i ψ↓)
. Let r i be the following planning rule:

att(senc(R i φ↓, R 2 i φ↓), senc(R i ψ↓, R 2 i ψ↓)), att(R 2 i φ↓, R 2 i ψ↓) -→ att(R i φ↓, R i ψ↓)
We have that:

-Add(r i ) = {att(R i φ↓, R i ψ↓)}; -att(senc(R i φ↓, R 2 i φ↓), senc(R i ψ↓, R 2 i ψ↓)) = att(R 1 i φ↓, R 1 i ψ↓)
, and att(R 2 i φ↓, R 2 i ψ↓) belongs to the initial state of our planning system Θ. So each r i (1 ≤ i ≤ n) is applicable after π 0 , and therefore π 0 .{r 1 , . . . , r n } is a planning path of length ℓ which is a solution of Π.

⊓ ⊔ Lemma 8. Let φ and ψ be two frames having the same domain, and R be a set of destructor-only C-recipes such that Key(R) ⊆ R; Rφ↓ and Rψ↓ are messages for any R ∈ R.

Let F = {att(Rφ↓, Rψ↓) | R ∈ R}, R 0 ⊆ R, and F0 = {att(Rφ↓, Rψ↓) | R ∈ R 0 }. Let Θ = F act 0 , Fact C (φ, ψ) ∪ F0 , Concrete + (Rule A )
, and Π = Θ, F . We have that Π has a solution of length at most |R R 0 | × depth(φ).

Proof. We consider the partial order R < R ′ over destructor-only recipes such that R < R ′ if, and only if, R ∈ Key(R ′ ). We show the result by induction on |R R 0 |, i.e. the number of elements in R R 0 .

Base case: |R R 0 | = 0. In such a case, the empty plan of length 0 is indeed a solution of Π = Θ, F .

Inductive case: |R R 0 | > 0. In such a case, we consider R a minimal element in R R 0 w.r.t. <. We have that Rφ↓ and Rψ↓ are messages. We know that Key(R) ⊆ R, and since R is minimal, we have that Key(R) ⊆ R 0 . Therefore, Lemma 7 applies to {R}, and we get a solution π of length at most depth(φ) of Θ, {att(Rφ↓, Rψ↓)} . Let Θ ′ = F 0 , Fact C (φ, ψ) ∪ F0 ∪ att(Rφ↓, Rψ↓), Concrete + (Rule A ) . By induction hypothesis, there is a solution

π ′ of Θ ′ , F of length at most |R (R 0 ∪ {R})| × depth(φ) = |R R 0 | × depth(φ) -depth(φ). We conclude that π.π ′ is a solution of Π of length at most |R R 0 | × depth(φ). ⊓ ⊔
A static inclusion test T w.r.t. ⊑ simple s is either a destructor-only recipe R, or a pair (R, R ′ ) of recipes such that R is simple whereas R ′ is destructor-only. We define Key(T ) as:

-Key(R) in the first case, -Key({R ′ , R 1 , . . . , R n }) in the second case assuming that R = C[R 1 , . . . , R n ].
Lemma 9. Let φ and ψ be two frames with dom(φ) = dom(ψ). Let R 0 be a set of destructor-only C 0 -recipes such that Key(R 0 ) ⊆ R 0 ; Rφ↓ and Rψ↓ are messages for any

R ∈ R 0 . Let F = {att(Rφ↓, Rψ↓) | R ∈ R 0 } and Θ = F act 0 , Fact C0 (φ, ψ) ∪ F , R where R = Concrete(R Ana ) ∪ R test1 fail ∪ R test2 fail ∪ R atom fail ∪ R check fail ∪ R pub fail . Let Π = Θ, {bad} . Assume φ ⊑ simple + s ψ. Let T be a static inclusion test w.r.t. ⊑ simple s that holds in φ but not in ψ. Then Π has a solution of length at most (k + 1) × depth(φ) + 1 where k = |Key(T ) R 0 |.
Proof. We have that φ ⊑ simple + s ψ. Following the definition of ⊑ simple + s , we consider the four cases separately.

1. There is a destructor-only recipe R such that Rφ↓ is a message but Rψ↓ is not. Let R ′ be the smallest subterm of R such that this property holds. Since both φ and ψ are frames, and thus contain messages, we have that

R ′ = g(R ′ 1 , R ′ 2 ) with g ∈ {sdec, adec}, or R ′ = g(R ′ 1 ) with g ∈ {getmsg} ∪ {proj k j | 2 ≤ k ≤ n, 1 ≤ j ≤ k}. We assume w.l.o.g. that R ′ = sdec(R ′ 1 , R ′ 2 )
, and by minimality of our test, R ′ 1 ψ↓ and R ′ 2 ψ↓ are messages. Applying Lemma 8 with

R ′ = Key({R ′ 1 , R ′ 2 }) ∪ {R ′ 2 }
and R 0 , we deduce the existence of a plan of length at most

|Key({R ′ 1 , R ′ 2 }) ∪ {R ′ 2 } R 0 | × depth(φ) leading to {att(Rφ↓, Rψ↓) | R ∈ Key({R ′ 1 , R ′ 2 }) ∪ {R ′ 2 }}. Thus, relying on Lemma 7, Θ, {att(R ′ 1 φ↓, R ′ 1 ψ↓), att(R ′ 2 φ↓, R ′ 2 ψ↓)} has a solution of length at most |(Key({R ′ 1 , R ′ 2 }) ∪ {R ′ 2 }) R 0 | × depth(φ) + depth(φ).
Then, we consider the rule r of the form:

att(R ′ 1 φ↓, R ′ 1 ψ↓), att(R ′ 2 φ↓, R ′ 2 ψ↓) → bad which is indeed an instance of a rule in Concrete -(R Ana ) since R ′ 1 φ↓ = senc(u 1 , u 2 ) for some u 1 , u 2 , and senc(u 1 , u 2 ), R ′ 1 ψ↓, R ′ 2 ψ↓ are messages whereas sdec(R ′ 1 ψ↓, R ′ 2
ψ↓)↓ is not a message. This rule r can be triggered and leads to bad. Since Key({R ′ 1 , R ′ 2 }∪{R ′ 2 }) ⊆ Key(R ′ ) ⊆ Key(R) = Key(T ), we have that Π has as solution of length at most

(|Key(T ) R 0 | + 1) × depth(φ) + 1.
Now, assuming that Rφ↓ is an atomic message, and Rψ↓ is a message but not an atomic one. In such a case, with a similar reasoning, we get that Θ, {att(Rφ↓, Rψ↓)} has a solution of length at most

|Key(T ) R 0 | × depth(φ) + depth(φ).
Then, we consider the rule r of the form: att(Rφ↓, Rψ↓) → bad which is indeed an instance of a rule R atom fail , and which leads to a solution for Π. Therefore, Π has as solution of length at most

(|Key(T ) R 0 | + 1) × depth(φ) + 1.
2. The minimal test is a destructor-only recipe R such that Rφ↓ = pub(s) for some atom s, whereas Rψ↓ = pub(s ′ ) for any atom s ′ . First, thanks to the first item, we may assume that Rψ↓ is a message. Applying Lemma 8 with R = Key(R) and R 0 , and then Lemma 7 on {R}, we get a solution of Θ, {att(Rφ↓, Rψ↓)} of length at most (|Key(R)| + 1) × depth(φ). Then, we consider the rule r of the form:

att(Rφ↓, Rψ↓) → bad which is indeed an instance of a rule R pub fail , and which leads to a solution for Π of length at most (|Key(T ) R 0 | + 1) × depth(φ) + 1. 3. There are destructor-only recipes R and R ′ such that Rφ↓ = sign(t, s), R ′ φ↓ = vk(s) for some message t, and some atom s, whereas Rψ↓ = sign(t ′ , s ′ ) or Rψ↓ = vk(s ′ ) for any message t ′ and any atom s ′ . First, thanks to the first item, we may assume that both Rψ↓, and R ′ ψ↓ are messages. Applying Lemma 8 with R = Key({R, R ′ }) and R 0 , and then Lemma 7 on {R, R ′ }, we get a solution of Θ, {att(Rφ↓, Rψ↓), att(R ′ φ↓, R ′ ψ↓)} of length at most

(|Key({R, R ′ }) R 0 | + 1) × depth(φ)
. Then, we consider the rule r of the form:

att(Rφ↓, Rψ↓), att(R ′ φ↓, R ′ ψ↓) → bad
which is indeed an instance of a rule R check fail , and which leads to a solution for Π of length at most (|Key(T ) R 0 | + 1) × depth(φ) + 1. 4. There is a simple recipe R = C[R 1 , . . . , R i ] and a destructor-only recipe R ′ such that Rφ↓ = R ′ φ↓ are messages whereas Rψ↓ = R ′ ψ↓. Moreover, we know that root(R) ∈ {senc} ∪ { k | 2 ≤ k ≤ n}, and also that root(R ′ ) = adec. First, thanks to the first item, we may assume that R 1 ψ↓, . . . , R k ψ↓, as well as Rψ↓, are messages. Applying Lemma 8 on Key({R 1 , . . . , R i , R ′ }), and then Lemma 7 on {R 1 , . . . , R i , R ′ }, we get a solution of

Θ, {att(R 1 φ↓, R 1 ψ↓), . . . , att(R i φ↓, R i ψ↓), att(R ′ φ↓, R ′ ψ↓)} of length at most (|Key({R 1 , . . . , R i , R ′ }) R 0 | + 1) × depth(φ)
. Then, we consider the rule r of the form:

att(R 1 φ↓, R 1 ψ↓), . . . , att(R i φ↓, R i ψ↓), att(R ′ φ↓, R ′ ψ↓) → bad
which is an instance of a rule in R test1 fail or R test2 fail . Indeed, thanks to Lemma 2, we know that:

either C is the empty context, and thus r is an instance of R test1 fail since R ′ φ↓ = Rφ↓, and R ′ ψ↓ = Rψ↓; -or Rφ↓ ∈ St opti (φ) ∪ C 0 , and thus r is an instance of

R test2 fail since R ′ φ↓ = Rφ↓ = C[R 1 φ↓, . . . , R i φ↓], and R ′ ψ↓ = Rψ↓ = C[R 1 ψ↓, . . . , R i ψ↓].
Therefore, this allows us to conclude that Π has a solution of length at most

(|Key(T ) R 0 | + 1) × depth(φ) + 1. ⊓ ⊔
Proposition 1. Let φ and ψ be two frames with dom(φ) = dom(ψ), and Θ = F act 0 , Fact C0 (φ, ψ), R where

R = Concrete(R Ana ) ∪ R test1 fail ∪ R test2 fail ∪ R atom fail ∪ R check fail ∪ R pub fail . Let Π = Θ, {bad} .
We have that φ ⊑ s ψ if, and only if, Π has a solution of length at most (N + 1) × depth(φ) + 1 where N is the number of names n occurring in φ at a key position, i.e. such that n (resp. pub(n)) occurs in key position of an encryption in φ.

Proof. First, thanks to Lemma 1, it is sufficient to show that φ ⊑ simple + s ψ if, and only if, Π has a solution. We show the two directions separately. (⇒) We have that φ ⊑ simple + s ψ. We consider a static inclusion test T w.r.t. ⊑ simple + s . We consider one such that Key(T ) is minimal, and then among those that have a minimal Key(T ), we consider one whose size (number of function symbols) is minimal. Lemma 9 applies with R 0 = ∅. Therefore, we have that Π has a solution of length at most (|Key(T )|+1)×depth(φ)+1. To conclude, we need to show that |Key(T )| ≤ N . Actually, we have that {Rφ↓ | R ∈ Key(T )} C 0 ≤ N since all these recipes occur in key position (i.e. second argument of sdec/adec) of a recipe that leads to a message in φ. Now, in case there are two recipes in K, K ′ ∈ Key(T )∪C 0 such that Kφ↓ = K ′ φ↓, then by minimality of our test (note that at least the size of the test has descreased), we know that Kψ↓ = K ′ ψ↓, and therefore replacing K by K ′ will give us a smaller test according to our measure. This allows us to conclude that Π has a solution of length at most (N + 1) × depth(φ) + 1.

(⇐) We have a plan of bad. We consider such a plan r 1 , . . . , r n of minimal length without performing rules in parallel. Since this plan is mimimal, we know that r 1 , . . . , r n-1 are rules in Concrete + (R Ana ), and therefore, we can rely on Lemma 5 to conclude that there exists a destructor-only recipe R such that Rφ↓ = u and Rψ↓ = v for any att(u, v) ∈ S n-1 (the state resulting from the application of r 1 , . . . , r n-1 ). Then, in order to derive bad, we have applied a rule in Concrete -(R Ana ) ∪ Rule test1 fail ∪ Rule test2 fail ∪ Rule atom fail ∪ Rule check fail ∪ Rule pub fail . It is actually easy to derive a witness of φ ⊑ s ψ. For instance, regarding the first case, according to the definition of Concrete -(R Ana ), we have for instance r n = att(senc(u 1 , u 2 ), v), att(u 2 , v ′ ) -→ bad with v not of the form senc(v 0 , v ′ ) for some v 0 . Moreover, we have destructor-only recipes R 1 (and R 2 ) allowing us to derive these facts. In such a case, we conclude using the recipe sdec(R 1 , R 2 ). The other cases are rather similar.

⊓ ⊔

B Reduction to well-typed witness

In this section, we exploit a result established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. The main idea is to show that we can restrict ourselves to consider well-typed execution when looking for a witness of non0-inclusion. However, to achieve this, we need to assume the existence of an infinite set C bitstring 0 of constants of sort bitstring. In the following, we will consider

C + 0 = C 0 ⊎ C bitstring 0
, and we further assume the existence of an infinite number of constants of any type in both sets.

All our definitions (messages, recipes, frames, configurations, processes, etc), as well as our semantics can be easily extended to take into account this new set of constants, and we sometimes parametrized these definition explicitly with the underlying set of constants (typically C 0 or C bitstring 0 ) to avoid confusion. Note that any constant in C bitstring 0 is of sort bitstring, and therefore not an atomic constant. Such a constant c can not occur at a key position, e.g. in senc(m, c). Theorem 3. Let K P be a C 0 -configuration type-compliant w.r.t. (T P , δ P ) and K Q be a C 0 -configuration. We have that K P ⊑ t K Q w.r.t. C 0 if, and only if, there exists a witness (tr, φ) ∈ trace C0 (K P ) of this non-inclusion which only involves simple recipes, and with a well-typed underlying execution.

Theorem 3 is a direct consequence of the result established in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. It only remains to establish that the witness tr can be choosen such that it only involves simple recipes. Actually, this can be obtained by taking recipes in forced normal form, and it is a direct consequence of Lemma 3 and Lemma 4 (see Appendix A).

C Bounding constants

Our goal is to bound the number of constants used in an attack. We show here that actually, two constants are sufficient. The proof technique is inspired from [START_REF] Chrétien | Checking trace equivalence: How to get rid of nonces[END_REF] and [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] which respectively reduce the number of nonces and agents in the context of equivalence properties. A direct application of the proof technique would however yield two constants of each type, which represents still a high number of constants. Instead, we show here how to further reduce the number of additional constants to only 3, considering a weaker version of well-typed execution, namely quasi-well-typed execution.

Given a protocol P, we denote C P the constants from C 0 that occur in P. Sometimes, to make clear the set of constants C that may be used, we write → w.r.t. C, trace C (K), C-recipe, C-message, . . . Theorem 1. Let K P be an initial C 0 -configuration type-compliant w.r.t. (T P , δ P ) and

K Q be another initial C 0 -configuration. Let C ⋆ = (C P ∪ C Q ) ⊎ {c ⋆ 0 , c ⋆ 1 , c ⋆ + }. We have that K P ⊑ t K Q w.r.t. C 0 if,
and only if, there exists a witness (tr, φ) ∈ trace(K P ) of this non-inclusion which only involves constants from C ⋆ , simple recipes, and with a quasi-well-typed underlying execution.

Given A ⊆ C + 0 , an A-renaming is a function ρ such that dom(ρ)∪img(ρ) ⊆ A; and ρ(a) is of sort atom when a is of sort atom. Given a typing system (T , δ), we say that ρ is type-preserving when δ(a) = δ(ρ(a)) for any a ∈ dom(ρ).

Lemma 10. Let t and t ′ be two terms in T (Σ, C + 0 ⊎ N ).

1. If t↓ is a C + 0 -message then (t↓)ρ = (tρ)↓ for any C + 0 -renaming ρ. 2. If t↓ is not a C + 0 -message, then there exists c 0 ∈ C + 0 such that for any

C + 0 - renaming ρ such that c 0 ∈ dom(ρ) ∪ img(ρ), tρ↓ is not a C + 0 -message. 3. If t↓ and t ′ ↓ are C + 0 -messages and t↓ = t ′ ↓, then there exists c 0 ∈ C + 0 such that for any C + 0 -renaming ρ such that c 0 ∈ dom(ρ) ∪ img(ρ), tρ↓ = t ′ ρ↓.
Proof. We prove the three items separately.

Item 1. Let t ∈ T (Σ, C + 0 ⊎ N ) such that t↓ is a C + 0 -message.
We show the result by structural induction on t. Base case. In such a case, we have that t ∈ C + 0 ⊎ N , and thus (t↓)ρ = tρ = (tρ)↓. Inductive case. First, we consider the case where t = f(t 1 , . . . , t k ) with f ∈ Σ c . In such a case, relying on our induction hypothesis, we have that:

(t↓)ρ = f(t 1 ↓ρ, . . . , t k ↓ρ) = f(t 1 ρ↓, . . . , t k ρ↓) = f(t 1 , . . . , t k )ρ↓ = (tρ)↓.
Second, we consider the case where t = g(t 1 , . . . , t k ) with g ∈ Σ d ∪ {check}. For sake of clarity, we consider the case where g = adec. In such a case, we have that t = adec(t 1 , t 2 ), t 1 ↓, t 2 ↓ are C + 0 -messages, t 1 ↓ = aenc(u, pub(v)), t 2 ↓ = v and sdec(t 1 , t 2 )↓ = u for some C + 0 -message u, and some atom v. Thanks to our induction hypothesis, we have that:

-(t 1 ↓)ρ = aenc(u, pub(v))ρ = aenc(uρ, pub(vρ)) = (t 1 ρ)↓; and -(t 2 ↓)ρ = vρ = (t 2 ρ)↓.
Therefore, we have that:

-(t↓)ρ = (adec(t 1 , t 2 )↓)ρ = (adec(t 1 ↓, t 2 ↓)↓ρ = u↓ρ = uρ; and -(tρ)↓ = (adec(t 1 , t 2 )ρ)↓ = adec(t 1 ρ↓, t 2 ρ↓)↓ = uρ.
This allows us to conclude when g = adec, and the other cases can be done in a similar way. Item 2. Let t ∈ T (Σ, C + 0 ⊎ N ) be a term in normal form and such that t is not a C + 0 -message. In case t ∈ T (Σ c , C + 0 ⊎ N ), the only case where tρ is a message (whereas t is not) is if there is a constant c of sort bitstring such that pub(c) occurs in t, and ρ(c) is of sort atom. Let c 0 be such a constant, and ρ be a C + 0renaming such that c 0 / ∈ dom(ρ) ∪ img (ρ), we have that tρ↓ is not a C + 0 -message since pub(c 0 ) occurs in tρ as a subterm and c 0 is not of sort atom. Now, t must contain at least one symbol in Σ d ∪ {check}. Let p be one of the lowest positions such that t = C[g(t 1 , . . . , t k )] p for some g ∈ Σ d ∪ {check} and t 1 , . . . , t k ∈ T (Σ c , C + 0 ⊎ N ). Let u = g(t 1 , . . . , t k ), and ρ 0 be a special renaming that maps any constant in C + 0 to c 0 ∈ C + 0 (i.e. an arbitrary constant of sort atom). Let ℓ → r be the rewriting rule associated to g. Either the rule does not apply on uρ 0 , and thus the rule will not apply on uρ for any C + 0 -renaming ρ. Otherwise, we have that the rule can be applied on uρ 0 whereas it can not be applied on u. In such a case, we have that there are two positions p 1 = p 2 such that ℓ| p1 = ℓ| p2 ∈ X , and thus u| p1 = u| p2 whereas (uρ 0 )| p1 = (uρ 0 )| p2 . Moreover, we know that u| p1 and u| p2 are both constants in C + 0 (they are of sort atom since otherwise reduction is not possible). Let c 1 = u| p1 . Any C + 0renaming ρ with c 1 / ∈ (dom(ρ) ∪ img (ρ)) will prevent the rewriting rule ℓ → r to be applicable on uρ and thus on tρ. This allows us to conclude that tρ↓ is not a C + 0 -message.

Item 3. Let t 1 , t 2 ∈ T (Σ, C + 0 ⊎ N ) such that t 1 ↓, t 2 ↓ are C + 0 -messages and t 1 ↓ = t 2 ↓. Thanks to Item 1, we have that (t 1 ↓)ρ = (t 1 ρ)↓ and (t 2 ↓)ρ = (t 2 ρ)↓.
Therefore, we can simply show that if t 1 , t 2 are C + 0 -messages and t 1 = t 2 then there exists c 0 ∈ C + 0 such that t 1 ρ = t 2 ρ for any C + 0 -renaming ρ such that c 0 ∈ dom(ρ) ∪ img(ρ). Base case: The only non trivial base case is when both t 1 and t 2 are in C + 0 . Assume w.l.o.g. that t 2 = c 0 . Since t 1 = t 2 , we have that t 1 ρ = t 2 ρ for any C + 0renaming ρ such that c 0 ∈ dom(ρ) ∪ img(ρ). The other base cases where either t 1 or t 2 is in C + 0 ⊎ N are trivial and we may actually choose any C + 0 -renaming ρ. Inductive case: Now, in case t 1 and t 2 are not atomic, we distinguish two cases. In case they do not have the same function symbol at their root, we can choose any C + 0 -renaming ρ, and the disequality between t 1 ρ and t 2 ρ will be preserved. Now, assume that t 1 = f(u 1 , . . . , u k ) and t 2 = f(v 1 , . . . , v k ) with f ∈ Σ c . We know that u i = v i for some i ∈ {1, . . . , k}. We can apply our induction hypothesis to conclude that there exists c 0 such u i ρ = v i ρ for any C + 0 -renaming ρ such that c 0 ∈ dom(ρ) ∪ img(ρ). Therefore, considering any C + 0 -renaming that satisfies such a condition will allow us to conclude.

⊓ ⊔ Lemma 11. Let K P be an initial C + 0 -configuration type-compliant w.r.t. (T P , δ P ), ρ be a type-preserving A-renaming such that A ⊆ C + 0 C P , and K P tr -→ (P ′ ; φ ′ ; σ ′ ; i ′ ) be a quasi-well-typed execution. We have that K P trρ --→ (P ′ ; φ ′ ρ; σ ′ ρ; i ′ ) is a quasiwell-typed execution.

Proof. Let K P = (P; ∅; ∅; 0), and K ′ P = (P ′ ; φ ′ ; σ ′ ; i ′ ). We show this result by induction on the length n of the execution trace K P tr -→ K ′ P . Base case. We have that K ′ P = K P , and the result trivially holds. Induction case. In such a case, we have that tr = tr -• α, and we have that:

K P tr - --→ (P -; φ -; σ -; i -) α -→ (P ′ ; φ ′ ; σ ′ ; i ′ ).
Relying on our induction hypothesis, we know that K P tr - --→ (P -ρ; φ -ρ; σ -ρ; i -). We distinguish three cases depending on α.

-Case α = phase i ′ . In such a case, we have that P ′ = P -, σ ′ = σ -, φ ′ = φ -, and i -< i ′ . We have that (P -; φ -ρ; σ -ρ; i -) phase i ′ ----→ (P -; φ -ρ; σ -ρ; i ′ ), and this allows us to conclude since (P -; φ -ρ; σ -ρ; i ′ ) = (P ′ ; φ ′ ρ; σ ′ ρ; i ′ ).

-Case α = out(c, w). In such a case, we have that P -= {i -:out(c, u).P 0 } ∪ P 0 for some u, P 0 , and P 0 . We have also that

σ ′ = σ -, φ ′ = φ -∪ {w ⊲ uσ -} and i ′ = i -. To conclude that (P -; φ -ρ; σ -ρ; i -) out(c,w) -----→ (P ′ ; φ ′ ρ; σ ′ ρ; i ′ ), it is sufficient to show that (uσ -)ρ = u(σ -ρ). Actually, (uσ -)ρ = (uρ)(σ -ρ),
and since dom(ρ) ⊆ C + 0 C P , we deduce that uρ = u, and since ρ(a) is an atom when a is an atom, this allows us to conclude.

-Case α = in(c, R). In such a case, we have that P -= {i -:in(c, u).P 0 } ∪ P 0 for some u, P 0 , and P 0 . We have also that φ ′ = φ -, σ ′ = σ -⊎ σ 0 for some σ 0 such that Rφ -↓ = (uσ -)σ 0 and Rφ -↓ is a message. Moreover, i -= i ′ .

To conclude that (P

-; φ -ρ; σ -ρ; i -) in(c,Rρ) -----→ (P ′ ; φ ′ ρ; σ ′ ρ; i ′ ), it remains to show that (Rρ)(φ -ρ)↓ = u(σ -ρ)σ ′ 0 and σ ′ ρ = σ -ρ ⊎ σ ′ 0 for some σ ′ 0 .
Since Rφ -↓ = (uσ -)σ 0 , we deduce that (Rφ -↓)ρ = ((uσ -)σ 0 )ρ, and thanks to Lemma 10 (item 1), we have that (Rφ -)ρ↓ = ((uρ)(σ -ρ))(σ 0 ρ). Lastly, since ρ is an A-renaming and A ⊆ C 0 C P , we know that uρ = u, and therefore we have that (Rρ)(φ -ρ)↓ = (u(σ -ρ))(σ 0 ρ). Moreover, since σ ′ = σ -⊎ σ 0 , we have that σ ′ ρ = σ -ρ ⊎ σ 0 ρ. Therefore, choosing σ ′ 0 = σ 0 ρ allows us to conclude.

Since ρ is type-preserving, the resulting execution is quasi-well-typed when the original one is quasi-well-typed.

⊓ ⊔ Theorem 1. Let K P be an initial C 0 -configuration type-compliant w.r.t. (T P , δ P ) and

K Q be another initial C 0 -configuration. Let C ⋆ = (C P ∪ C Q ) ⊎ {c ⋆ 0 , c ⋆ 1 , c ⋆ + }.
We have that K P ⊑ t K Q w.r.t. C 0 if, and only if, there exists a witness (tr, φ) ∈ trace(K P ) of this non-inclusion which only involves constants from C ⋆ , simple recipes, and with a quasi-well-typed underlying execution.

Proof. The ⇐ direction is actually easy to establish. It is a direct consequence of Lemma 3.11 established and proved in [START_REF] Chrétien | Typing messages for free in security protocols[END_REF]. Therefore, we consider the other direction (⇒).

First, we apply Theorem 3 to obtain a witness (tr, φ) ∈ trace C + 0 (K P ) of this non-inclusion which only involves simple recipes, and with a well-typed underlying execution. Then, considering

C ⋆⋆ = (C P ∪ C Q ) ⊎ {c ∈ C + 0 | δ P (c) = τ ⋆ },
and applying an alpha-renaming along the derivation to rename constants from C + 0 C ⋆⋆ to constants from C ⋆⋆ , we easily derive a witness which only involves simple recipes built using constants from C ⋆⋆ , and with a quasi-well-typed underlying execution.

We consider a minimal (in length) witness of non-inclusion, i.e. a trace (tr, φ) ∈ trace C ⋆⋆ (K P ) such that:

1. either (tr, ψ) ∈ trace C ⋆⋆ (K Q ) for any ψ; or 2. (tr, ψ) ∈ trace C ⋆⋆ (K Q ) but φ ⊑ s ψ.

We will apply a renaming on such a witness to get rid of constants from C ⋆⋆ (C P ∪ C Q ). Such a renaming ρ will be such that dom(ρ) ⊆ C ⋆⋆ (C P ∪ C Q ), and img(ρ) ⊆ {c ⋆ 0 , c ⋆ 1 , c ⋆ + }. Moreover, in case c is of sort atom, then ρ(c) will be of sort atom.

In the following, we will consider different renamings. In particular, we consider ρ 0 which maps any constant from C ⋆⋆ to c ⋆ 0 , as well as the renaming ρ 1 which maps any constant from C ⋆⋆ of sort atom to c ⋆ 0 , and any constant from C ⋆⋆ of sort bitstring to c ⋆ + . Case 1: tr = tr -• α does not pass in K Q . In such a case, we have that:

-K P tr - --→ (P -; φ -; σ - P ; i -) α -→ (P; φ; σ P ; i); -K Q tr - --→ (Q -; ψ -; σ - Q ; i -); and -φ -⊑ s ψ -.
Relying on Lemma 11, we have that:

-K P tr -ρ ---→ (P -; φ -ρ; σ - P ρ; i -) αρ --→ (P; φρ; σ P ρ; i); and

-K Q tr -ρ ---→ (Q -; ψ -ρ; σ - Q ρ; i -)
for any A-renaming ρ such that A ⊆ C + 0 (C P ∪ C Q ). Thus, to conclude, it remains to justify that αρ can not be triggered from (Q -; ψ -ρ; σ - Q ; i -) for a C + 0renaming ρ such that img(ρ) ⊆ {c ⋆ 0 , c ⋆ 1 , c ⋆ + }. We consider three cases depending on the action α.

1. Case α = phase i. In such a case, we have that (Q -; ψ -; σ - Q ; i -) phase i ----→ and this is impossible since α can be triggered from (P -; φ -; σ - P ; i -), and thus i -< i. 2. Case α = out(c, w). In such a case, we have that P -= out(c, u).P 0 ⊎ P 0 .

Either Q -is not ready to perform an output on channel c, and thus this is the case for (Q -; ψ -ρ 0 ; σ - Q ρ 0 ; i -), and we are done. Otherwise, we have that

Q -= out(c, v).Q 0 ⊎ Q 0 but vσ - Q is not a C ⋆⋆ -message. We have that (vσ - Q )ρ 1 = v(σ - Q ρ 1
) is still not a message, and we are done. 3. Case α = in(c, R). In such a case, we have that P -= in(c, u).P 0 ⊎ P 0 . Either Q -is not ready to perform an imput on channel c, and thus (Q -; ψ -; σ - Q ; i -) is not ready to perform an input on channel c, and we are done. Otherwise, since φ -⊑ s ψ -, and Rφ -↓ is a message, we deduce that Rψ -↓ is a message, and we have that Rψ -↓ρ 0 = (Rψ -)ρ 0 ↓ = (Rρ 0 )(ψ -ρ 0 )↓ is a message (Lemma 10 -item 1). Hence, since the input can not be triggered, this is due to a problem of filtering, there does not exist τ such that (vσ - Q )τ = Rψ -↓. If Rψ -↓ and vσ - Q do not match because their structure differ, then no renaming will change that. Therefore, we consider the renaming ρ 0 , and it is easy to see that (Rρ 0 )(ψ -ρ 0 )↓ and v(σ -Qρ 0 ) do not match. Otherwise, the only possibility is that there are two position p 1 and p 2 in (vσ

- Q ) such that (vσ - Q )| p1 = (vσ - Q )| p2 ∈ X , but (Rψ -↓)| p1 = (Rψ -↓)| p2 .
Thanks to Lemma 10 (item 3), there is a constant c 0 such that for any C + 0 -renaming ρ with c 0 ∈ dom(ρ) ∪ img(ρ), t 1 ρ = t 2 ρ. In case c 0 ∈ C P ∪ C Q , then we can simply consider ρ 0 that will kept c 0 unchanged. Otherwise, we assume w.l.o.g. that c 0 is c ⋆ 0 (or c ⋆ + ) (performing an alpha-renaming), and we consider the renaming ρ which maps any constants from C ⋆⋆ (except c ⋆ 0 or c ⋆ + ) to c + 1 .

Case 2: We have that K P tr -→ (P; φ; σ P ; i); K Q tr -→ (Q; ψ; σ Q ; i); and φ ⊑ s ψ. Relying on Lemma 11, we have that:

-K P trρ --→ (P; φρ; σ P ρ; i); and

-K Q trρ --→ (Q; ψρ; σ Q ρ; i)
for any A-renaming ρ such that A ⊆ C + 0 (C P ∪C Q ). Thus, to conclude, it remains to justify that φρ ⊑ ψρ for a C + 0 -renaming ρ such that img(ρ) ⊆ {c ⋆ 0 , c ⋆ 1 , c ⋆ + }. We distinguish two cases depending on the form of the test.

Case message.

There is a recipe R w.r.t. C ⋆⋆ such that Rφ↓ is a C + 0 -message whereas Rψ↓ is not. Therefore, by Lemma 10 (item 2), there is a constant c 0 ∈ C + 0 such that for any C + 0 -renaming ρ such that c 0 ∈ dom(ρ)∪img (ρ), we have that (Rψ)ρ↓ is not a message. In case c 0 ∈ C P ∪ C Q , then we consider the renaming ρ 0 . We have that (Rρ 0 )(φρ 0 )↓ = (Rφ)ρ 0 ↓ = Rφ↓ρ 0 (Lemma 10 -item 1) is a message. Moreover, we have seen that (Rρ 0 )(ψρ 0 )↓ = (Rψ)ρ 0 ↓ is not a message. This allows us to conclude. Now, in case c 0 ∈ C P ∪ C Q , we assume w.l.o.g. that c 0 is c ⋆ 0 (or c ⋆ + ) (performing an alpha-renaming, and we consider the renaming ρ which maps any constants from C ⋆⋆ (except c ⋆ 0 or c ⋆ + ) to c + 1 . We have that (Rρ)(φρ)↓ = (Rφ)ρ↓ = Rφ↓ρ (Lemma 10item 1) is a message. Moreover, we have seen that (Rρ)(ψρ)↓ = (Rψ)ρ↓ is not a message. Therefore, we have our witness of non-inclusion. 2. Case test. There are two recipes R 1 and R 2 w.r.t. C ⋆⋆ such that R 1 φ↓, R 2 φ↓ are messages, and R 1 φ↓ = R 2 φ↓. Moreover, we have that R 1 ψ↓ and R 2 ψ↓ are mesages, but R 1 ψ↓ = R 2 ψ↓. Thanks to Lemma 10 (item 3), there is a constant c 0 ∈ C + 0 such that for any C + 0 -renaming ρ such that c 0 ∈ dom(ρ) ∪ img(ρ), we have that (R 1 ψ)ρ↓ = (R 2 ψ)ρ↓. In case c 0 ∈ C P ∪ C Q , then we consider the renaming ρ 0 . We have that (R i ρ 0 )(φρ 0 )↓ = (R i φ)ρ 0 ↓ = R i φ↓ρ 0 (Lemma 10 -item 1) is a message (i ∈ {1, 2}). Similarly, we have that (R i ρ 0 )(ψρ 0 )↓ = (R i ψ)ρ 0 ↓ = R i ψ↓ρ 0 with i ∈ {1, 2}. This allows us to conclude that R 1 ρ 0 ? = R 2 ρ 0 is a test that holds in φρ 0 but not in ψρ 0 . Now, in case c 0 ∈ C P ∪ C Q , we assume w.l.o.g. that c 0 is c ⋆ 0 (or c ⋆ + ) (performing an alpha-renaming, and we consider the renaming ρ which maps any constants from C ⋆⋆ (except c ⋆ 0 or c ⋆ + ) to c + 1 . We have that (R i ρ)(φρ)↓ = (R i φ)ρ↓ = R i φ↓ρ (Lemma 10 -item 1) is a message (i ∈ {1, 2}). Similarly, we have that (R i ρ)(ψρ)↓ = (R i ψ)ρ↓ = R i ψ↓ρ with i ∈ {1, 2}. This allows us to conclude that R 1 ρ ? = R 2 ρ is a test that holds in φρ but not in ψρ. Therefore, we have our witness of non-inclusion.

⊓ ⊔

D From trace inclusion to planning

The goal of this section is to establish Theorem 2. Before starting to prove this theorem, we formally define the notion of flattening (see Section D.1) and the notion of concretization (see Section D.2) briefly described in Section 4.2.

D.1 Flattening

We explain how to formally compute the set of flattened rules from a given abstract rule r. For this, we start by explaining how to decompose a fact att(u, v).

Definition 8. Given a term u ∈ T 0 (Σ c , C ⊎ N ⊎ X ), we say that u is decomposable when:

either u ∈ X and δ P (u) is not an initial type;

-or u ∈ C ⊎ N ⊎ X .
Intuitively, a variable of non initial type is decomposable since it may be instantiated by a non atomic term which, in turns, may have been obtained by composition. Given att(u, v) with u decomposable, and let f ∈ Σ c be such that δ P (u) = f(τ 1 , . . . , τ k ), we define split(att(u, v)) as follows:

split(att(u, v)) = (f; {att(x 1 , y 1 ), . . . , att(x k , y k )}; σ P ; σ Q ) where x 1 , . . . , x k are fresh variables of type τ 1 , . . . , τ k and σ P = mgu(u, f(x 1 , . . . , x k )); -y 1 , . . . , y k are fresh variables, σ Q = mgu(v, f(y 1 , . . . , y k )).

Note that σ P exists and is necessarily a quasi-well-typed substitution. By convention, we assume that mgu(u, u ′ ) = ⊥ when u and u ′ are not unifiable.

Let r be an abstract rule of the form Pre -→ Add; Del with f = att(u, v) ∈ Pre such that u is decomposable and split(f ) = (f, S, σ P , σ Q ). The decomposition of r w.r.t. f , denoted decom(r, f ), is defined as follows:

1. (Pre f ) ∪ S -→ bad σ P in case σ Q = ⊥; 2. (Pre f ) ∪ S -→ Add; Del (σ P ⊎ σ Q ) otherwise.

D.2 Concretization

Given an abstract rule r, we denote vars left (r) the variables occurring on the left (first parameter) of a predicate occurring in r, i.e.

vars left (att(u, v)) = vars(u); and vars left (state c P,Q (σ P , σ Q )) = vars(img(σ P )). Given a substitution σ grounding for r, the application of σ on an abstract state is the concrete state obtained by simply composing the substitutions, i.e.

st c P,Q (σ P , σ Q )σ = st c P,Q (σ • σ P , σ • σ Q ).
Given an abstract protocol rule r, its positive concretization simply consists in all its instantiations that are quasi-well-typed w.r.t. the left side of the rule.

Concrete + (r) = {rσ | σ substitution such that rσ only involves messages with constants in C ⋆ and δ P (xσ) δ P (x) for any x ∈ vars left (r)}

Similarly to the static case, we need to make sure that we can detect when P and Q are not in trace inclusion. For this, we consider additional rules that express when a step that can be performed on the left hand side cannot be mimicked on the right hand side.

Given an abstract protocol rule r = Pre -→ Add; Del, Concrete -(r) is the set of planning rules that contains: f 1 , . . . , f k -→ bad for any sequence of facts f 1 , . . . , f k such that f 1 , . . . , f k left-unify with Pre with substitution σ L and u ∈ T 0 (Σ c , N ∪ C ⋆ ) for any att(u, v) ∈ Addσ L , and such that one of the following conditions holds:

f 1 , . . . , f k does not right-unify with Pre; -f 1 , . . . , f k right-unify with Pre with substitution σ R but v ∈ T 0 (Σ c , N ∪ C ⋆ ) for some att(u, v) ∈ Addσ R .

D.3 Bounded planning

In this section, we state one of our main lemma that allows on to relate execution traces and planning paths, and we rely on the following definitions: Let K P = (P; σ P ; φ; i P ) and K Q = (Q; σ Q ; ψ; i Q ) be two configurations with dom(φ) = dom(ψ) and such that i P = i Q . The set of facts associated to K P and K Q w.r.t. a given set of constants C is defined as follows:

Fact C (K P , K Q ) = {Phase(i)} ∪ Fact C (φ, ψ) ∪ {state c P,Q (σ P , σ Q ) | P ∈ P, Q ∈ Q are basic processes on channel c, σ P = σ P | fv (P ) and σ Q = σ Q | fv (Q) }
Note that this definition is in line with the one provided in the core of the paper for protocols assuming that P represents the configuration (P; ∅; ∅; 0). Definition 9. Given two sets of facts S and S ′ such that S = Fact C (K P , K Q ) with K P = (P; φ; σ P ; i) and K Q = (Q; ψ; σ Q ; i) with dom(φ) = dom(ψ), we write Fact C (K P , K Q ) ↑ S ′ when: from Fact C ⋆ (K P , K Q ) to some S ′′ . Moreover, we have that Fact C ⋆ (K ′′ P , K ′′ Q ) ↑ S ′′ , and att(Rφ↓, Rψ↓) ∈ S ′′ for any R ∈ Key(tr ′ ). We perform a case analysis on the action α.

Case α = phase i ′ . We have that i ′ > i ′′ , P ′ = P ′′ , φ ′ = φ ′′ and σ ′ P = σ ′′ P . Similarly, we have

Q ′ = Q ′′ , ψ ′ = ψ ′′ and σ ′ Q = σ ′′ Q . As Fact C ⋆ (K ′′ P , K ′′ Q ) ↑ S ′′ , we have that Phase(i ′′ ) ∈ S ′′ . Let r i = Phase(i) → Phase(i + 1); Phase(i) with i ∈ N.
We have that π = π 0 .r i ′′ . . . . .r i ′ -1 is a planning path from Fact C ⋆ (K P , K Q ) to some S ′ , with Fact C ⋆ (K ′ P , K ′ Q ) ↑ S ′ and att(Rφ↓, Rψ↓) ∈ S ′ for any R ∈ Key(tr). Since φ ′ = φ ′′ , and tr = tr ′ .phase i ′ , the length of π is at most nb in (tr) + nb out (tr) + max phase (tr) + (nb in (tr) + |Key(tr)|) × depth(φ).

Case α = out(c, w). We have that there exist P ′ c , and Q ′ c , as well as u and v such that -P ′′ = {i ′′ :out(c, u).P ′ c } ⊎ P 0 , and

P ′ = {i ′′ :P ′ c } ⊎ P 0 ; -Q ′′ = {i ′′ :out(c, v).Q ′ c } ⊎ Q 0 , and Q ′ = {i ′′ :Q ′ c } ⊎ Q 0 . Moreover, we have that φ ′ = φ ′′ ⊎ {w ⊲ uσ ′′ P }, and ψ ′ = ψ ′′ ⊎ {w ⊲ vσ ′′ Q }; and σ ′ Q = σ ′′
P , as well as σ ′ Q = σ ′′ Q , and i ′ = i ′′ . Moreover, we know that uσ ′′ P and vσ ′′ Q are messages. Let r be the abstract protocol rule corresponding to this step. We have that r ∈ Rule(P, Q) and this rule is of the form:

Phase(i ′′ ), St(P, Q) -→ att(u, v), St(P ′ , Q ′ ); St(P, Q)
Now, we consider the concrete instance that corresponds to the execution mentioned above, i.e. the one obtained by applying σ ′ P ⊎ σ ′ Q . This allows us to conclude in one step, and since nb out (tr) = nb out (tr ′ ) + 1, nb in (tr) = nb in (tr ′ ), Key(tr) = Key(tr ′ ), and depth(φ ′ ) ≥ depth(φ ′′ ), we get a plan of length at most nb in (tr) + nb out (tr) + max phase (tr) + (nb in (tr) + |Key(tr)|) × depth(φ).

Case α = in(c, R). We know that R is a simple recipe, i.e. R = C[R 1 , . . . , R k ], and we have that there exist P ′ c , and Q ′ c , as well as u and v such that:

-P ′′ = {i ′′ :in(c, u).P ′ c } ⊎ P 0 , and Let r be the abstract protocol rule corresponding to this step. We have that r ∈ Rule(P, Q) and this rule is of the form:

P ′ = {i ′′ :P ′ c } ⊎ P 0 ; -Q ′′ = {i ′′ :in(c, v).Q ′ c } ⊎ Q 0 , and Q ′ = {i ′′ :Q ′ c } ⊎ Q 0 . Moreover, we have that φ ′ = φ ′′ , ψ ′ = ψ ′′ ; σ ′ P = σ ′′ P ⊎ mgu(Rφ ′′ ↓, uσ ′′ P ), and σ ′ Q = σ ′′ Q ⊎ mgu(Rψ ′′ ↓, vσ ′′ Q ),
Phase(i ′′ ), St(P, Q), att(u, v) -→ St(P ′ , Q ′ ); St(P, Q).
and r n is an instance of r f (σ ′′ P ∪ σ ′′ Q ) where σ ′′ P (resp. σ ′′ Q ) is the substitution obtained after executing tr ′ . Let τ P , and τ Q be grounding substitution such that r n = (r f (σ ′′ P ∪ σ ′′ Q ))(τ P ∪ τ Q ). We know that there exist destructor only recipes R 1 , . . . , R k such that R i φ ′′ ↓ = u i σ ′′ P τ P and R i ψ ′′ ↓ = v i σ ′′ Q τ Q by Lemma 5. We can apply Lemma 13 on rule r n written as:

r n = Pre, att(u 1 , v 1 ), . . . , att(u n , v n ) -→ Add; Del
We are in the case where bad-flat / ∈ Add, so there exists a constructor context C and a substitution τ such that r f (σ

′′ P ∪ σ ′′ Q )τ = Pre, att(u, v) -→ Add; Del where u = C[u 1 , . . . , u n ] and v = C[v 1 , . . . , v n ]. Therefore, consider the trace tr ′ • in(c, C[R 1 , . . . , R k ]
). This step can be done on the P side, as well as on the Q side. Hence, the result.

⊓ ⊔ Theorem 2. Let P a protocol type-compliant w.r.t. (T P , δ P ), and Q be another protocol. We consider the following set R of concrete rules:

Concrete(R Ana ∪ Flat(Rule(P, Q))) ∪ R phase ∪ R test1 fail ∪ R test2 fail ∪ R atom fail ∪ R check fail ∪ R pub fail Let Θ = F act 0 , Fact C ⋆ (P, Q), R
(P)) × [1 + nb in (P) + N ]
where N is the number of names occurring in P having a key type, i.e. such that δ P (n) (resp. pub(δ P (n))) occurs in key position of an encryption in δ P (P).

Proof. We show the two directions separately. (⇒) In case P ⊑ t Q, we know thanks to Theorem 1 that there exists a witness of this fact such that (tr, φ) ∈ trace(P) is quasi-well-typed, only involve the constants we consider here, and tr is made of simple recipes. We consider such a witness of minimal length, and then we consider one such that Key(tr) is minimal. By minimality of tr, we can assume that there is no phase i action in tr for i > max phase (P). We distinguish two cases depending on the fact that (tr, ψ) ∈ trace(Q) for some ψ or not.

Case (tr, ψ) ∈ trace(Q) for some ψ. Lemma 16 allows us to conclude that there exists a planning path π 0 from Fact C ⋆ (P, Q) to S of length at most nb in (tr) + nb out (tr) + max phase (tr) + (nb in (tr) + |Key(tr)|) × depth(φ) such that:

-Fact C ⋆ (K ′ P , K ′ Q ) ↑ S where K ′ P (resp. K ′ Q )
is the resulting configuration starting from P (resp. Q) and executing tr; and -{att(Rφ↓, Rψ↓) | R ∈ Key(tr)} ⊆ S.

In case (tr, ψ) ∈ trace(Q), we know that φ ⊑ simple + s ψ. We consider a static inclusion test T w.r.t. ⊑ simple + s which is minimal for the following measure (ordered lexicographically):

-Key(T ) Key(tr); -its size, i.e. number of function symbols occurring in T . Lemma 9 applies with R 0 = Key(tr). We deduce that there is a plan π 1 of bad of length at most Since nb in (tr) ≤ nb in (P), n out (tr) ≤ nb out (P), max phase (tr) ≤ max phase (P) (by minimality of tr), depth(φ) ≤ depth(δ P (P)), to conclude it remains to prove that |Key(tr) ∪ Key(T )| ≤ N . First, we have that {Rφ↓ | R ∈ Key(tr) ∪ Key(T )} C 0 ≤ N since all these recipes occur in key position (i.e. 2nd argument of sdec/adec) of a recipe that leads to a message in φ. Now, in case there are two recipes in K, K ′ ∈ Key(tr) ∪ Key(T ) ∪ C 0 such that Kφ↓ = K ′ φ↓, then by minimality of our witness of non-inclusion, we know that Kψ↓ = K ′ ψ↓, and therefore replacing K or K ′ with the one which is deducible earlier or the smallest one in case they are both deducible at the same stage will give us a smaller test according to our measure. So we get that the length is smaller than nb in (P) + nb out (P) + max phase (P) + [nb in (P) + N + 1] × depth(δ P (P)) + 1 Case tr does not pass in Q. Let tr = tr -1.α. We have that (tr -1 , ψ -1 ) ∈ trace(Q) but the last action α can not be performed. Lemma 16 allows us to conclude that there exists a planning path π 0 from Fact C ⋆ (P, Q) to S of length at most nb in (tr -1 ) + nb out (tr -1 ) + max phase (tr -1 ) + (nb in (tr -1 ) + |Key(tr -1 )|) × depth(φ) such that:

-Fact C ⋆ (K ′ P , K ′ Q ) ↑ S where K ′ P = (P ′ ; φ ′ ; σ ′ P ; i ′ ) (resp. K ′ Q = (Q ′ ; ψ ′ ; σ ′ Q ; i ′ )) is the resulting configuration starting from P (resp. Q) and executing tr -1 ; and -{att(Rφ↓, Rψ↓) | R ∈ Key(tr -1 )} ⊆ S.

We consider three cases depending on the action α. Case: α = phase i. This case is impossible since this action can be performed by Q as soon as its current phase is smaller than i, and this is the case since both P and Q are synchronised and the action α is feasible by P. Case: α = out(c, w). If such an action can not be performed, it means that this action is not available in the process or would lead to output a term that is not a message. In the first case, we have an abstract protocol rule r that can be instantiated to mimick this step. In the second case, we have to consider the instance in Concrete -(r). Note that for such a rule Flat(r) = r. In each case, we only use one rule, so the plan is of length at most nb in (tr -1 )+ nb out (tr -1 )+ max phase (tr -1 )+ (nb in (tr -1 )+ |Key(tr -1 )|)× depth(φ)+ 1

As before, it is smaller than nb in (P) + nb out (P) + max phase (P) + depth(δ P (P)) × [1 + nb in (P) + N ] + 1 Case: α = in(c, R) with R = C[R 1 , . . . , R k ] a simple recipe. We consider in(c, u) the corresponding action in K ′ p and we have that Rφ ′ ↓ = (uσ ′ P )τ P for some substitution τ P . If such an action can not be performed, it means that either this action is not syntactically available in the process or the term in the Q side does not match. Let r be the abstract protocol rule corresponding to this step.

Thanks to Lemma 8 applied with R = Key({R 1 , . . . , R k }) and R 0 = Key(tr -1 ), there is a plan π 1 of length at most |Key({R 1 , . . . , R k }) Key(tr -1 )| × depth(φ) of {att(R ′′ φ↓, R ′′ ψ↓) | R ′′ ∈ Key({R 1 , . . . , R k })}. It allows us to apply Lemma 7 on R = {R 1 , . . . , R k }: there is a plan π 2 of length at most depth(φ) of {att(R 1 φ↓, R 1 ψ↓), . . . , att(R k φ↓, R k ψ↓)}.

Thus, with a similar reasoning as before, π 0 .π 1 .π 2 is a plan of length at most nb in (P) + nb out (P) + max phase (P) + depth(δ P (P)) × [1 + nb in (P) + N ] If the input is not syntactically available in the process, then r is of the form Phase(i), St (P, Q), att(u, y) -→ bad-proto where y is a fresh variable and i an integer. St(P, Q) unifies with the corresponding fact of S with substitution σ ′ P ⊎ σ ′ Q ⊎ τ P such that -St(P, Q)(σ ′ P ⊎ σ ′ Q ⊎ τ P ) ∈ S. -Rφ ′ ↓ = u(σ ′ P ⊎ τ P ) -δ P (x(σ ′ P ⊎ τ P )) δ P (x) for any x ∈ vars left (r). We can apply Lemma 12 on r and σ ′ P ⊎ σ ′ Q ⊎ τ P ⊎ {y → Rψ ′ ↓} (Note that Rψ ′ ↓ is a message by minimality of our witness tr). We get a rule r f ∈ Flat(r):

r f = Pre ′ , att(u ′ 1 , v ′ 1 ), . . . , att(u ′ k , v ′ k ) -→ Add ′ ; Del ′
and a grounding substitution σ ′ such that:

δ P (xσ ′ ) δ P (x) for any x ∈ vars left (r ′ ) -(Pre ′ , Add ′ , Del ′ )σ ′ = (St(P, Q), bad-proto, ∅)(σ ′ P ⊎ σ ′ Q ⊎ τ P ⊎ {y → Rψ ′ ↓}) -u(σ ′ P ⊎ τ P ) = C[u ′ 1 , . . . , u ′ k ] and Rψ ′ ↓ = C[v ′ 1 , . . . , v ′ k ]. As the att(R i φ ′ ↓, R i ψ ′ ↓) unify with Pre(r f ), there is a rule r ′ in Concrete + (r f ) such that its preconditions are exactly the att(R i φ ′ ↓, R i ψ ′ ↓). This concludes the case where the input is not syntactically available in the process.

The cases where there is an input in(c, v) in the Q side can be done in a rather similar way. We rely on Lemma 12 when v unifies with C[z 1 , . . . , z k ], and we have a plan reaching bad applying a concrete rule in Concrete -(Flat(r)). We rely on Lemma 14 otherwise, and the concrete planning rule leading to bad is either in Concrete + (Flat(r)) or in Concrete -(Flat(r)).

F Benchmark

In this Appendix, we present the results of our experiments on bounded equivalence checkers. Figure 3 compares the results of SAT-Equiv as in [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF] with the current version on three symmetric protocols. Figures 4, 6, 7, as 5, are results on examples of symmetric protocols on which we compared the tools. We extended our benchmark to some assymmetric protocols. The corresponding results can be found on Figures 8 and9.

Yahalom-Lowe CSF '

k

  : bitstring × • • • × bitstring → bitstring senc : bitstring × atom → bitstring aenc : bitstring × bitstring → bitstring sign : bitstring × atom → bitstring ok :

  and i ′ = i ′′ . Moreover, we know that uσ ′ P and vσ ′ Q are messages. Applying Lemma 8 with R = Key(tr) and R 0 = Key(tr ′ ), we get a plan π 1 to S ′′ such that {att(R ′ φ↓, R ′ ψ↓) | R ′ ∈ Key(tr ′ )} ⊆ S ′′ , and the length of π 1 is at most |Key({R 1 , . . . , R k }) Key(tr ′ )| × depth(φ ′′ ).

(

  |Key(T ) Key(tr)| + 1) × depth(φ) + 1 It gives us a plan π 0 .π 1 of bad of length at most nb in (tr)+nb out (tr)+max phase (tr)+(nb in (tr)+|Key(tr)∪Key(T )|+1)×depth(φ)+1

Fig. 9 .

 9 Fig. 9. Analysis of Needham-Schroeder-Low protocol (left) and Denning-Sacco protocol with signature from [6] (right). The second column of Sat-Eq indicates the theoretical bound of the planning graph.

  Definition 6. A planning system is tuple F act, Init, Rule where F act is a set of ground formulas called facts, Init 0 ⊆ F act is a set of facts representing the initial state, and Rule is a set of rules of the form Pre -→ Add; Del where Pre, Add, Del are finite sets of facts such that Add ∩ Del = ∅, Del ⊆ Pre. We write Pre -→ Add when Del = ∅.

  Comparison of SAT-Equiv with the other tools. We indicate the number of sessions for which the tool fails (time out, memory out, or other issues). When we did not reach the limit of the tool, we write ≥ k to indicate that the tool can analyse more than k sessions, and we indicate the analysis time for k.

		Spec Akiss Deepsec CSF'17	Sat-Eq
	Denning-Sacco	7	10	35	98 > 210 (4h)
	Needham-Schroeder sym	6	6	21	21	94 * (20h30)
	Wide Mouth Frog	7	12	28	84 > 210 (6min)
	Yahalom-Paulson	6	6	12	7	> 28 (7h)
	Passive Authentication	6	8	46	-	> 400 (98s)
	Active Authentication	6	8	50	-	> 400 (78s)
	Needham-Schroeder-Lowe 4	6	16	-	> 64 (11min)
	Denning-Sacco signature	8	8	18	-	> 64 (100s)
	Fig. 2.

* see Section 6.2

  Comparison of new and old version of Sat-Equiv for Yahalom-Lowe protocol, Otway-Rees protocol and the simple stateful example as in[START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF]. Analysis of the Yahalom-Paulson protocol. The second column of Sat-Eq indicates the theoretical bound of the planning graph. Analysis of the Denning-Sacco protocol. The second column of Sat-Eq indicates the theoretical bound of the planning graph. Analysis of the Wide-Mouth-Frog protocol. The second column of Sat-Eq indicates the theoretical bound of the planning graph. Analysis of the Needham-Schroeder protocol. The second column of Sat-Eq indicates the theoretical bound of the planning graph. For the examples with 47 and 94 roles, we also consider refined scenarios where some roles are cut before the end, as explained in Subsection 6.2. Analysis of the Passive-Authentication protocol (left) and Active Authentication (right). The second column of Sat-Eq indicates the theoretical bound of the planning graph. For Passive Authentication, the verified property is anonymity.

	17 Current 300ms 3m 5s 800ms 19m 1.9s 206m 5s 19h 13s TO 23s Simple stateful CSF'17 Current Otway-Rees CSF'17 Current 3 104s 900ms 6 46m 3s 7 50m 5s 10 276m 11s 12 9h40m 16s 14 TO 27s 1 200ms 20ms 2 1s 80ms 3 2s 150ms 4 6s 200ms 12 155s 800ms 36 85m 3s 60 6h40m 9s Fig. 3. YP Spec Akiss Deepsec CSF'17 Sat-Eq 3 6 7 10 12 14 3 23m 7s <10ms 50s 400ms 73 6 MO TO 900ms 165m 5s 122 7 6s TO 17s 136 10 85m 63s 185 12 TO 143s 214 14 6m 248 21 155m 360 28 7h 472 Fig. 4. Denning-Sacco Spec Akiss Deepsec CSF'17 Sat-Eq 3 12s 80ms <0.01s 300ms 70ms 42 6 5h 9s <0.01s 1s 100ms 64 7 MO 75s <0.01s 2s 200ms 74 10 SO 0.01s 4s 300ms 114 12 0.04s 7s 400ms 134 14 0.2s 11s 500ms 152 21 18s 60s 1.3s 216 28 25m 3m30s 3s 280 35 TO 9m 6s 344 42 23m 10s 408 63 164m 51s 600 84 13h 164s 792 91 23h 4m15s 856 98 TO 6m 920 105 8m 984 126 20m 1176 140 35m 1304 154 56m 1432 168 75m 1560 182 128m 1688 196 3h10m 1816 210 4h20m 1944 Fig. 5. WMF Spec Akiss Deepsec CSF'17 Sat-Eq 3 6s 40ms <10ms 100ms 10ms 29 6 58m 1.6s <10ms 1s 20ms 42 7 TO 5s <10ms 2s 70ms 47 10 8m30s 60ms 7s 100ms 60 12 SO 440ms 40s 200ms 69 14 5s 118s 350ms 78 21 21m 77s 200ms 106 28 TO 4m45s 400ms 137 35 24m 600ms 168 42 36m 1s 199 56 163m 2.4s 261 63 5h 4s 292 70 9h 5s 323 77 18h 7s 354 84 TO 9s 385 112 24s 509 140 55s 633 154 93s 695 168 140s 757 182 3m30s 819 196 4m30s 881 210 6m 943 Fig. 6. NSS Spec Akiss Deepsec CSF'17 Sat-Eq 3 1m 4s <10ms 2s 80ms 50 6 MO TO 10ms 54s 400ms 88 7 50ms 153s 1.2s 98 10 600ms 8m 3s 132 12 7s 22m 4s 155 14 120s 77m 11s 176 21 TO TO 51s 346 28 178s 452 47 ref. 48m 527 47 129m 759 94 ref. 20h30m 1024 94 MO 1489 2 3s 100ms <10ms 10ms 27 4 14m 4s 10ms 30ms 43 6 MO 10m 20ms 60ms 59 8 TO 20ms 90ms 75 10 80ms 100ms 91 20 3s 300ms 171 40 3h20m 800ms 332 46 TO 1s 380 50 1.1s 412 54 1.2s 444 60 1.7s 492 80 3s 652 120 6s 972 160 12s 1292 200 20s 1612 400 98s 3212 AA Spec Akiss Deepsec Sat-Eq 2 3s 100ms <10ms 10ms 37 4 15m 3s <10ms 40ms 61 6 MO 5m 20ms 70ms 85 8 SO 20ms 70ms 109 10 60ms 100ms 133 20 2s 300ms 253 40 2h30m 800ms 493 46 23h50m 900ms 565 50 TO 1.1s 613 54 1.2s 661 60 1.7s 733 80 3s 973 120 6s 1453 160 11s 1933 200 18s 2413 400 78s 4813 Fig. 8. NSL Spec Akiss Deepsec Sat-Eq DS sig. Spec Akiss Deepsec Sat-Eq Fig. 7. PA Spec Akiss Deepsec Sat-Eq 2 11s 40ms 10ms 20ms 27 4 MO 2s 10ms 40ms 43 6 SO 120ms 200ms 59 8 7s 500ms 75 12 58m 0.9s 107 16 TO 3s 139 32 35s 267 48 162s 395 64 11m 523 2 1.5s 60ms <10ms 0.01s 39 4 4m 1.5s <10ms 0.02s 55 8 MO SO 240ms 0.2s 87 16 4h50m 0.9s 151 18 TO 1.1s 167 24 3s 215 32 8s 279 48 66s 407 64 100s 535

Then, decomposition is applied recursively on each rule. Flat(r) = Flat({decom(r, f ) | f = att(u, v) ∈ Pre(r) with u decomposable}) ∪ {r} Lemma 12. Let r = Pre, att(u, v) -→ Add; Del be an abstract rule. Let σ be a grounding substitution for r such that δ P (xσ) δ P (x) for any x ∈ vars left (r). Let C be a constructor context such that uσ = C[u 1 , . . . , u n ] and vσ = C[v 1 , . . . , v n ]. There exists r ′ = Pre ′ , att(u ′ 1 , v ′ 1 ), . . . , att(u ′ n , v ′ n ) -→ Add ′ ; Del ′ in Flat(r), and σ ′ a grounding substitution for r ′ such that:

1. δ P (xσ ′ ) δ P (x) for any x ∈ vars left (r ′ ); 2. (Pre ′ , Add ′ , Del ′ )σ ′ = (Pre, Add, Del)σ; and 3. att(u, v)σ = att(C[u ′ 1 , . . . , u ′ n ], C[v ′ 1 , . . . , v ′ n ])σ ′ . For the next lemmas, we need to be more specific on how the fact bad has appeared. Therefore, from now on, we consider three facts instead: bad-proto, bad-flat, and bad-concrete. Moreover, we assume that in protocol rules, bad is replaced by bad-proto, in flattening rules, bad is replaced by bad-flat, and in concretization rules bad is replaced by bad-concrete. When the precise origin of the failure does not matter, we simply write bad (meaning one of the three cases above).

Lemma 13. Let r be an abstract protocol rule, and r ′ ∈ Flat(r) be such that For the next lemma, we need to define the relation = left on facts as

with c = c ′ , P = P ′ and σ P = σ ′ P . We extend this definition to Pre. Lemma 14. Let r = Pre, att(u, v) -→ Add; Del be an abstract protocol rule. Let σ be a grounding substitution for vars left (r) such that δ P (xσ) δ P (x) for any x ∈ vars left (r). Let C be a constructor context such that uσ = C[u 1 , . . . , u n ], whereas v and C[z 1 , . . . , z n ] are not unifiable.

There exists r ′ = Pre ′ , att(u ′ 1 , v 1 ), . . . , att(u ′ n , v n ) -→ bad in Flat(r), and σ ′ a grounding substitution for vars left (r) such that u ′ i σ ′ = u i for any i ∈ {1, . . . , n}, and Pre ′ σ ′ = left Preσ. Lemma 15. Let r be an abstract protocol rule, and r ′ ∈ Flat(r) be such that

There exists a constructor context C, a substitution τ , a term v, and two sets Add 0 and Del 0 such that rτ = Pre, att(C[u 1 , . . . , u n ], v) -→ Add 0 ; Del 0 but v does not unify with C[z 1 , . . . , z n ].

-Fact C (K P , K Q ) and S ′ coincide on states fact, and also the phase fact; -for any att(u, v) ∈ Fact C (K P , K Q ), att(u, v) ∈ S ′ ; and for any att(u, v) ∈ S ′ , there exists a destructor-only C-recipe R such that Rφ↓ = u, and Rψ↓ = v.

Below, nb in (tr) (resp. nb out (tr)) is the number of input actions (resp. output actions) occurring in tr whereas max phase (tr) is the maximal integer occurring in a phase instruction in tr.

Lemma 16. Let P be a protocol type-compliant w.r.t. (T P , δ P ), and Q be another protocol. Let Θ = F act 0 , Fact C ⋆ (P, Q), R where

Let (tr, φ) ∈ trace(P) w.r.t. C ⋆ for some φ such that:

tr only contains simple recipes;

Then, there exists a planning path from Fact C ⋆ (P, Q) to some S such that

where

is the resulting configuration starting from P (resp. Q) and executing tr, and {att(Rφ↓,

Conversely, let π be a planning path from Fact C ⋆ (P, Q) to S such that bad ∈ S. Then, there exist a trace tr, and frames φ and ψ such that:

tr only contains simple recipes; -(tr, φ) ∈ trace(P) w.r.t. C ⋆ and is quasi-well-typed w.r.t. (T P , δ P );

is the resulting configuration starting from P (resp. Q) and executing tr.

Proof. We show the two directions separately. (⇒) We do the proof by induction on the execution K P tr -→ K ′ P . Base case. The empty planning path can be used to establish the result.

Inductive case. We have that tr = tr ′ .α. Therefore, we consider K ′′ P and

We apply our induction hypothesis on tr ′ and we obtain a planning path π 0 of length at most Lemma 12, there exists a rule r ′ ∈ Flat(r):

and σ ′ a grounding substitution for r ′ such that:

We have that att

Thanks to Lemma 7 there is a plan π 2 (that we can apply after π 1 ) of length at most depth(φ ′ ) containing only attacker rules such that att(R i φ ′ ↓, R i ψ ′ ↓) is in the final state after π 2 . We consider r ′ σ ′ ∈ Concrete + (r ′ ), and we obtain the expected result considering the plan π 0 .π 1 .π 2 .r ′′ of length at most

We show this result by induction on the length of the planning path. Base case. Obvious.

Inductive case. We have a planning path r 1 , . . . , r n . Thanks to our induction hypothesis, we know that the result holds for r 1 , . . . , r n-1 leading to the state S n-1 , and therefore the existence of a trace tr ′ such that:

tr ′ only contains simple recipes; -(tr ′ , φ ′′ ) ∈ trace(P) w.r.t. C ⋆ and is quasi-well-typed w.r.t. (T P , δ P ); -(tr ′ , ψ ′′ ) ∈ trace C (Q) w.r.t. C ⋆ for some ψ ′′ ; and -Fact C ⋆ (K ′′′ P , K ′′ Q ) ↑ S where K ′′ P (resp. K ′′ Q ) is the resulting configuration starting from P (resp. Q) and executing tr ′ .

We distinguish several cases depending on the rule r n . In case r n is an instance of Concrete + (R Ana ), we consider tr = tr ′ again. The case where r n is a rule that adds bad is impossible since bad ∈ S n . The case where r n is Phase(i) → Phase(i + 1); Phase(i) can be mimicked in the execution by the phase instruction. Now, if r n is an instance of an abstract rule in Flat(Rule(P, Q)). Let r f be the flattened abstract rule, and r the abstract protocol rule.

In case r is a rule corresponding to the case of an output on channel c, then r n is an instance of r since the flattening does not produce any other rule. In such a case, we can mimick this step by considering tr ′ .out(c, w).

In case r is a rule corresponding to an input, then r n is an instance of a rule r f ∈ Flat(r). We have that r f is of the form:

In each case, we conclude with a plan of bad of length at most nb in (P) + nb out (P) + max phase (P) + depth(δ P (P)) × [1 + nb in (P) + N ] + 1 (⇐) We show this result by induction on the length of planning path leading to bad. We consider one without rules in parallel of minimal length. We have that π = r 1 , . . . , r n , and we denote S i the state obtained after executing r 1 , . . . , r i . We apply Lemma 16 on r 1 , . . . , r n-1 . We obtain the trace tr ′ , and frames φ ′ nad ψ ′ such that:

tr ′ only contains simple recipes; -(tr ′ , φ ′ ) ∈ trace(P) w.r.t. C ⋆ and is quasi-well-typed w.r.t. (T P , δ P );

is the resulting configuration starting from P (resp. Q) and executing tr.

Note that it implies that Phase(i) ∈ S n-1 . Now, we distinguish several cases depending on whether r n is

Note that r n cannot be a phase rule as it would not allows us to reach bad. In the first case, we conclude relying on Proposition 1, and therefore we obtain that the frames φ ′ and ψ ′ resulting from the execution of tr ′ are not in static inclusion. The second case occurs when r n ∈ Concrete(Flat(Rule(P, Q))). So there is an abstract protocol rule r f such that r n ∈ Concrete(Flat(r f )). Similarly to the proof done in [START_REF] Cortier | SAT-Equiv: an efficient tool for equivalence properties[END_REF], we show that this "planning" step can be mimicked on the protocol side form the P side, and has no counterpart on the Q side. To prove this, we rely on Lemma 13 and Lemma 15 to establish that any planning rule obtained by flattening is linked to an abstract protocol rule, which in turn can be mimicked on the protocol side.

⊓ ⊔

E Examples of non termination

We exhibit here two examples on which the original SAT-Equiv algorithm does not terminate. Given a channel c, consider the processes P (c) and Q(c) defined as follows.

where a is a public constant and x a variable. We consider K P = {P (c 1 ); P (c 2 )} and K Q = {Q(c 1 ); Q(c 2 )} for some public channel names c 1 , c 2 . On this example, starting with att(b, b) (b being simply a public constant in the initial knowledge of the attacker), the following facts will be successively added when computing the planning graph: Here, it is easy to see that K P is not trace included in K Q , as an attacker can distinguish between b and b, b . So, as soon as a message is outputted, the resulting frames are not in static inclusion. Therefore, termination can easily be retrieved by enforcing SAT-Equiv to stop the exploration of the planning graph as soon as an attack is found. We can turn this example into a more complex one on which the original SAT-Equiv will not terminate even if we decide to stop the exploration of the planning graph as soon as an attack is found. Consider the processes P 0 (c), P 1 (c) and Q 1 (c) given below. We assume that k is name representing a symmetric secret key, whereas a, b, c are public constants. P 0 (c) = in(c, x).out(c, senc(x, k)) P 1 (c) = in(c, senc(a, k), senc(b, k), senc(c, k) 3 ).P (c) Q 1 (c) = in(c, senc(a, k), senc(b, k), senc(c, k) 3 ).Q(c)

We consider the configurations K ′ P = {P 0 (c 0 ); P 0 (c 1 ); P 1 (c 2 ); P 1 (c 3 )} and K ′ Q = {P 0 (c 0 ); P 0 (c 1 ); Q 1 (c 2 ); Q 1 (c 3 )} where c 0 , c 1 , c 2 , c 3 are public channel names. Processes P 0 on channels c 0 and c 1 are used as oracles. Roughly, we can get two ciphertexts among the three ciphertexts: senc(a, k), senc(b, k), and senc(c, k). It is however not possible to get the three of them. Noticing this, it is then easy to see that K P and K Q are trace included. However, as in the previous example, the planning graph is not precise enough to detect that it is not possible to obtain these three ciphertexts. Once the inputs on channel c 2 and c 3 are executed, we reach a situation similar to the one discussed in the previous example. Each time bad will be added into the planning graph, our SAT encoding will tell us that this state is not truly reachable (but only exists in the over-approximation). Thus, we will continue to explore the planning graph for ever since no attack will be found (the protocols are traceequivalent).