Steve Kremer

Robert Künnemann

Keywords: Automated verification, Stateful security protocols, Security APIs

Automated analysis of security protocols with global state

Introduction

Automated analysis of security protocols has been extremely successful. Using automated tools, flaws have been for instance discovered in the Google Single Sign On Protocol [START_REF] Armando | Formal analysis of saml 2.0 web browser single sign-on: Breaking the saml-based single sign-on for google apps[END_REF], in commercial security tokens implementing the PKCS#11 standard [START_REF] Bortolozzo | Attacking and fixing PKCS#11 security tokens[END_REF], and one may also recall Lowe's attack [START_REF] Lowe | Breaking and fixing the Needham-Schroeder public-key protocol using FDR[END_REF] on the Needham-Schroeder public key protocol 17 years after its publication. While efficient tools such as ProVerif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF], AVISPA [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF] or Maude-NPA [START_REF] Escobar | Maude-npa: Cryptographic protocol analysis modulo equational properties[END_REF] exist, these tools are generally not suitable to analyze protocols that require non-monotonic global state, i.e., some database, register or memory location that can be read and altered by different parallel threads. The input language of the AVISPA tool offers support for this kind of state but only supports a bounded number of sessions. This is particularly restrictive when analysing security APIs where attacks typically require several keys and API calls, which are difficult to bound a priori. ProVerif, one of the most efficient and widely used protocol analysis tools for an unbounded number of sessions, relies on an abstraction that encodes protocols in first-order Horn clauses. This abstraction is well suited for the monotonic knowledge of an attacker (who never forgets), makes the tool extremely efficient for verifying an unbounded number of protocol sessions and allows to build on existing techniques for Horn clause resolution. However, Horn clauses are inherently monotonic: once a fact is true it cannot be set to false anymore. As a result, even though ProVerif's input language, a variant of the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], allows a priori encodings of a global memory, the abstractions performed by ProVerif introduce false attacks. In the ProVerif user manual [START_REF] Blanchet | ProVerif 1.88: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]Section 6.3.3] such an encoding of memory cells and its limitations are indeed explicitly discussed: "Due to the abstractions performed by ProVerif, such a cell is treated in an approximate way: all values written in the cell are considered as a set, and when one reads the cell, ProVerif just guarantees that the obtained value is one of the written values (not necessarily the last one, and not necessarily one written before the read)." Some work [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF][START_REF] Mödersheim | Abstraction by set-membership: verifying security protocols and web services with databases[END_REF][START_REF] Delaune | Formal analysis of protocols based on TPM state registers[END_REF] has nevertheless used ingenious encodings of mutable state in Horn clauses, but these encodings have limitations that we discuss below.

A prominent example where non-monotonic global state appears are security APIs, such as the RSA PKCS#11 standard [START_REF]PKCS #11: Cryptographic Token Interface Standard[END_REF], IBM's CCA [START_REF]CCA Basic Services Reference and Guide[END_REF] or the trusted platform module (TPM) [START_REF]TPM Specification version 1.2. Parts[END_REF]. They have been known to be vulnerable to logical attacks for some time [START_REF] Longley | An automatic search for security flaws in key management schemes[END_REF][START_REF] Bond | API level attacks on embedded systems[END_REF] and formal analysis has shown to be a valuable tool to identify attacks and find secure configurations. One promising paradigm for analyzing security APIs is to regard them as a participant in a protocol and use existing analysis tools. However, Herzog [START_REF] Herzog | Applying protocol analysis to security device interfaces[END_REF] already identified not accounting for mutable global state as a major barrier to the application of security protocol analysis tools to verify security APIs. Apart from security APIs many other protocols need to maintain databases: key servers need to store the status of keys, in optimistic contract signing protocols a trusted party maintains the status of a contract, RFID protocols maintain the status of tags and more generally websites may need to store the current status of transactions.

Our contributions We propose a tool for analyzing protocols that may involve non-monotonic global state, relying on Schmidt et al.'s tamarin tool [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF][START_REF] Schmidt | The tamarin prover for the symbolic analysis of security protocols[END_REF] as a backend. We designed a new process calculus that extends the applied pi calculus by defining, in addition to the usual constructs for specifying concurrent processes, constructs for explicitly manipulating global state. This calculus serves as the tool's input language. The heart of our tool is a translation from this extended applied pi calculus to a set of multiset rewrite rules that can then be analyzed by tamarin which we use as a backend. We prove the correctness of this translation and show that it preserves all properties expressible in a dedicated first order logic for expressing security properties. As a result, relying on the tamarin prover, we can analyze protocols without bounding the number of sessions, nor making any abstractions. Moreover it allows to model a wide range of cryptographic primitives by the means of equational theories. As the underlying verification problem is undecidable, tamarin may not terminate. However, it offers an interactive mode with a GUI which allows to manually guide the tool in its proof. Our specification language includes support for private channels, global state and locking mechanisms (which are crucial to write meaningful programs in which concurrent threads manipulate a common memory). The translation has been carefully engineered in order to favor termination by tamarin, including a goal ranking method tailored to the output of the translation. Several case studies illustrate the tool's capability: a simple security API in the style of PKCS#11, a complex case study of the Yubikey security token, as well as several examples analyzed by other tools that aim at analyzing stateful protocols. In all of these case studies we were able to avoid restrictions that were necessary in previous works.

Related work

The most closely related work is the StatVerif tool by Arapinis et al. [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF]. They propose an extension of the applied pi calculus, similar to ours, which is translated to Horn clauses and analyzed by the ProVerif tool. Their translation is sound but allows for false attacks, limiting the scope of protocols that can be analyzed. Moreover, StatVerif can only handle a finite number of memory cells: when analyzing an optimistic contract signing protocol this appeared to be a limitation and only the status of a single contract was modeled, providing a manual proof to justify the correctness of this abstraction. In important case studies, e. g. key-management APIs like PKCS#11 or the Yubikey, an unbounded amount of memory is required to avoid artificially bounding the number of keys or Yubikey devices. Finally, StatVerif is limited to the verification of secrecy properties. As illustrated by the Yubikey case study, our work is more general and we are able to analyze complex injective correspondence properties.

Mödersheim [START_REF] Mödersheim | Abstraction by set-membership: verifying security protocols and web services with databases[END_REF] proposed a language with support for sets together with an abstraction where all objects that belong to the same sets are identified. His language, which is an extension of the low level AVISPA intermediate format, is compiled into Horn clauses that are then analyzed, e. g., using ProVerif. His approach is tightly linked to this particular abstraction, limiting the scope of applicability, e. g., when keys may be compromised (all keys with the same attributes are abstracted to one and the same, thus either all are revealed, or none) or when the set of states a key or value is not bounded a priori (as in the Yubikey case study). Mödersheim also discusses the need for a more high-level specification level which we provide in this work.

There has also been work tailored to particular applications. In [START_REF] Delaune | Formal analysis of PKCS#11 and proprietary extensions[END_REF], Delaune et al. show by a dedicated hand proof that for analyzing PKCS#11 one may bound the message size. Their analysis still requires to artificially bound the number of keys. Similarly in spirit, Delaune et al. [START_REF] Delaune | Formal analysis of protocols based on TPM state registers[END_REF] give a dedicated result for analyzing protocols based on the TPM and its registers. However, the number of reboots (which reinitialize registers) needs to be limited.

Guttman [START_REF] Guttman | State and progress in strand spaces: Proving fair exchange[END_REF] also extended the strand space model by adding support for state. While the protocol execution is modeled using the classical strand spaces model, state is modeled by a multiset of facts, and manipulated by multiset rewrite rules. The extended model has been used for analyzing by hand an optimistic contract signing protocol. In a more recent paper Ramsdell et al. [START_REF] Ramsdell | A hybrid analysis for security protocols with state[END_REF] propose another approach also based on the strand space model. Using the CPSA tool they obtain a symbolic representation (called skeletons) of all possible attacks. However, as their model analyzed by CPSA encodes the state in a message passing style, the tool may consider false attacks. They therefore import the CPSA result, as an axiom, in the theorem prover PVS and, based on a more precise model of the possible state transitions, refine their analysis to exclude the false attacks. The approach has been applied to the so-called envelope protocol, which was also analysed (in a slightly more restrictive model) in [START_REF] Delaune | Formal analysis of protocols based on TPM state registers[END_REF].

In the goal of relating different approaches for protocol analysis Bistarelli et al. [START_REF] Bistarelli | Relating multiset rewriting and process algebras for security protocol analysis[END_REF] also proposed a translation from a process algebra to multiset rewriting: they do however not consider private channels, have no support for global state and assume that processes have a particular structure. These limitations significantly simplify the translation and its correctness proof. Moreover their work does not include any tool support for automated verification.

Obviously any protocol that we are able to analyze can be directly analyzed by the tamarin prover [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF][START_REF] Schmidt | The tamarin prover for the symbolic analysis of security protocols[END_REF] as the rules produced by our translation could have been given directly as an input to tamarin. Indeed, tamarin has already been used for analyzing a model of the Yubikey device [START_REF] Künnemann | YubiSecure? Formal security analysis results for the Yubikey and YubiHSM[END_REF], the case studies presented with Mödersheim's abstraction, as well as those presented with StatVerif. It is furthermore able to reproduce the aforementioned results on PKCS#11 [START_REF] Delaune | Formal analysis of PKCS#11 and proprietary extensions[END_REF] and the TPM [START_REF] Delaune | Formal analysis of protocols based on TPM state registers[END_REF] -moreover, it does so without bounding the number of keys, security devices, reboots, etc. Contrary to ProVerif, tamarin sometimes requires additional typing lemmas which are used to guide the proof. These lemmas need to be written by hand (but are proved automatically). In our case studies we also needed to provide a few such lemmas manually. In our opinion, an important disadvantage of tamarin is that protocols are modeled as a set of multiset rewrite rules. This representations is very low level and far away from actual protocol implementations, making it very difficult to model a protocol adequately. Encoding private channels, nested replications and locking mechanisms directly as multiset rewrite rules is a tricky and error prone task. As a result we observed that, in practice, the protocol models tend to be simplified. For instance, locking mechanisms are often omitted, modeling protocol steps as a single rule and making them effectively atomic. Such more abstract models may obscure issues in concurrent protocol steps and increase the risk of implicitly excluding attacks in the model that are well possible in a real implementation, e. g., race conditions. Using a more high-level specification language, such as our process calculus, arguably eases protocol specification and overcomes some of these risks. Examples in which the explicit modelling of locking mechanisms in SAPIC improved the protocol and/or the analysis include the Yubikey case study presented in Section 7. In our modelling of the Yubikey the server can handle several requests from different devices in parallel, which was not possible in the direct modelling in [START_REF] Künnemann | YubiSecure? Formal security analysis results for the Yubikey and YubiHSM[END_REF]. Another example is the model of the enhanced authorization mechanism introduced in the TPM 2.0 specification by Shao et al. [START_REF] Shao | Formal analysis of enhanced authorization in the TPM 2.0[END_REF]. In this work, a model of the TPM that executes API commands sequentially is compared to one that executes them in parallel, finding flaws in the parallel version. The TPM model in the tamarin example files models TPM commands as atomic steps. While an explicit modelling of locking steps is possible in tamarin, judging from existing models, it is not widely used, although protocols and analysis could benefit from it.

Since the first prototype of this translation was presented [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], subsequent work has demonstrated and extended its scope. The present calculus and verification method have been used to verify a configuration of the key-management API PKCS#11 [START_REF] Künnemann | Automated backward analysis of PKCS#[END_REF] and was extended with loops to allow for the analysis of the streaming protocol TESLA [START_REF] Rakotonirina | Vérification automatique de protocoles de sécurité avec mémoire globale et boucles[END_REF]. In [START_REF] Shao | Formal analysis of enhanced authorization in the TPM 2.0[END_REF], Shao et al. used our tool to analyse the enhanced authorization mechanism introduced in the TPM 2.0 specification.

Preliminaries

Terms and equational theories. As usual in symbolic protocol analysis we model messages by abstract terms. Therefore we define an order-sorted term algebra with the sort msg and two incomparable subsorts pub and fresh. For each of these subsorts we assume a countably infinite set of names, FN for fresh names and PN for public names. Fresh names will be used to model cryptographic keys and nonces while public names model publicly known values. We furthermore assume a countably infinite set of variables for each sort s, V s and let V be the union of the set of variables for all sorts. We write u : s when the name or variable u is of sort s. Let Σ be a signature, i.e., a set of function symbols, each with an arity. We write f /n when function symbol f is of arity n. We denote by T Σ the set of well-sorted terms built over Σ, PN , FN and V. For a term t we denote by names(t), respectively vars(t) the set of names, respectively variables, appearing in t. The set of ground terms, i.e., terms without variables, is denoted by M Σ . When Σ is fixed or clear from the context we often omit it and simply write T for T Σ and M for M Σ .

We equip the term algebra with an equational theory E, that is a finite set of equations of the form M = N where M, N ∈ T . From the equational theory we define the binary relation = E on terms, which is the smallest equivalence relation containing equations in E that is closed under application of function symbols, bijective renaming of names and substitution of variables by terms of the same sort. Furthermore, we require E to distinguish different fresh names, i. e., ∀a, b

∈ FN : a = b ⇒ a = E b.
Example. Symmetric encryption can be modelled using a signature Σ = { senc/2, sdec/2 } and an equational theory defined by sdec(senc(m, k), k) = m.

For the remainder of the article we assume that E refers to some fixed equational theory and that the signature and equational theory always contain symbols and equations for pairing and projection, i.e., { ., . , fst, snd} ⊆ Σ and equations fst( x, y ) = x and snd( x, y ) = y are in E. We will sometimes use x 1 , x 2 , . . . , x n as a shortcut for x 1 , x 2 , . . . , x n-1 , x n . . . . We suppose the usual notion of positions for terms. A position p is a sequence of positive integers and t| p denotes the subterm of t at position p.

Facts. We also assume an unsorted signature Σ fact , disjoint from Σ. The set of facts is defined as

F := {F (t 1 , . . . , t k ) | t i ∈ T Σ , F ∈ Σ fact of arity k}.
Facts will be used both to annotate protocols, by the means of events, and for defining multiset rewrite rules. We partition the signature Σ fact into linear and persistent fact symbols. We suppose that Σ fact always contains a persistent, unary symbol !K and a linear, unary symbol Fr. Given a sequence or set of facts S we denote by lfacts(S) the multiset of all linear facts in S and pfacts(S) the set of all persistent facts in S. By notational convention facts whose identifier starts with '!' will be persistent. G denotes the set of ground facts, i.e., the set of facts that does not contain variables. For a fact f we denote by ginsts(f ) the set of ground instances of f . This notation is also lifted to sequences and sets of facts as expected.

Predicates. We assume an unsorted signature Σ pred of predicate symbols that is disjoint from Σ and Σ fact . The set of predicate formulas is defined as

P := {pr (t 1 , . . . , t k ) | t i ∈ T Σ , pr ∈ Σ pred of arity k}.
Predicate formulas will be used to describe branching conditions in protocols. The semantics of a predicate is defined via a first-order formula over atoms of the form t 1 ≈ t 2 , i.e. the grammar for such formulae is

φ ::= t 1 ≈ t 2 | ¬φ | φ 1 ∧ φ 2 | ∃x.φ
where t 1 , t 2 are terms and x ∈ V. For an n-ary predicate symbol pr , pr (x 1 , ..., x n ) is defined by a formula φ pr such that fv (φ pr ) ⊆ x 1 , ..., x n , where fv denotes the free variables in a formula, i. e., variables v ∈ V not bound by ∃v. The semantics of the first-order formulae is as usual where we interpret ≈ as = E .

Example. Suppose encSucc ∈ Σ pred is a binary predicate symbol. We can define it as follows, so that it allows to check whether a term x 1 was encrypted using a key x 2 :

φ encSucc = ∃m.enc(m, x 2 ) ≈ x 1
Substitutions. A substitution σ is a partial function from variables to terms. We suppose that substitutions are well-typed, i.e., they only map variables of sort s to terms of sort s, or of a subsort of s. We denote by σ = { t 1 / x 1 , . . . , tn / xn } the substitution whose domain is D(σ) = {x 1 , . . . , x n } and which maps x i to t i . As usual we homomorphically extend σ to apply to terms and facts and use a postfix notation to denote its application, e.g., we write tσ for the application of σ to the term t. A substitution σ is grounding for a term t if tσ is ground. Given function g we let g(x) = ⊥ when x ∈ D(x). When g(x) = ⊥ we say that g is undefined for x. We define the function Sets, sequences and multisets. We write N n for the set {1, . . . , n}. Given a set S we denote by S * the set of finite sequences of elements from S and by S # the set of finite multisets of elements from S. We use the superscript # to annotate usual multiset operation, e.g. S 1 ∪ # S 2 denotes the multiset union of multisets S 1 , S 2 . Given a multiset S we denote by set(S) the set of elements in S. The sequence consisting of elements e 1 , . . . , e n will be denoted by [e 1 , . . . , e n ] and the empty sequence is denoted by []. We denote by |S| the length, i.e., the number of elements of the sequence. We use • for the operation of adding an element either to the start or to the end, e.g., e 1 • [e 2 , e 3 ] = [e 1 , e 2 , e 3 ] = [e 1 , e 2 ] • e 3 . Given a sequence S, we denote by idx (S) the set of positions in S, i.e., N n when S has n elements, and for i ∈ idx (S) S i denotes the ith element of the sequence. Set membership modulo E is denoted by ∈ E and defined as e ∈ E S iff ∃e ∈ S. e = E e. ⊂ E and = E are defined for sets in a similar way. Application of substitutions are lifted to sets, sequences and multisets as expected. By abuse of notation we sometimes interpret sequences as sets or multisets; the applied operators should make the implicit cast clear.

f := g[a → b] with D(f ) = D(g) ∪ { a } as f (a) := b and f (x) := g(x) for x = a.

A cryptographic pi calculus with explicit state

Syntax and informal semantics

Our calculus, dubbed SAPiC (Stateful Applied Pi calculus) is a variant of the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. In addition to the usual operators for concurrency, replication, communication and name creation, it offers several constructs for reading and updating an explicit global state. The grammar for processes is described in Figure 1.

0 denotes the terminal process. P | Q is the parallel execution of processes P and Q and !P the replication of P , allowing an unbounded number of sessions in protocol executions. The construct νn; P binds the name n ∈ FN in P and models the generation of a fresh, random value. The processes out(M, N ); P and in(M, N ); P represent the output, respectively input, of message N on channel M . Readers familiar with the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] may note that we opted for the possibility of pattern matching in the input construct, rather than merely binding the input to a variable x. The process if Pred then P else Q will execute P or Q, depending on whether Pred holds. For example, if Pred = equal (M, N ), and φ equal = x 1 ≈ x 2 , then if equal (M, N ) then P else Q will execute P if M = E N and Q otherwise. (In the following, we will use M = N as short-hand for equal (M, N ).) The event construct is merely used for annotating processes and will be useful for stating security properties. For readability we sometimes omit to write else Q when Q is 0, as well as trailing 0 processes.

The remaining constructs are used for manipulating state and are new compared to the applied pi calculus. The construct insert M ,N binds the value N to a key M . Successive inserts allow changing this binding. We emphasise that we have only one value bound to a key, and that successive inserts update the binding. The delete M operation simply "undefines" the mapping for the key M . The lookup M as x in P else Q allows for retrieving the value associated to M , binding it to the variable x in P . If the mapping is undefined for M the process behaves as Q. The lock and unlock constructs are used to gain or waive exclusive access to a resource M , in the style of Djkstra's binary semaphores: if a term M has been locked, any subsequent attempt to lock M will be blocked until M has been unlocked. This is essential for writing protocols where parallel processes may read and update a common memory.

In the following example, which will serve as our running example, we model a security API that, even though much simplified, illustrates the most salient issues that occur in the analysis of security APIs such as PKCS#11 [START_REF] Delaune | Formal analysis of PKCS#11 and proprietary extensions[END_REF][START_REF] Bortolozzo | Attacking and fixing PKCS#11 security tokens[END_REF][START_REF] Fröschle | Reasoning with past to prove PKCS#11 keys secure[END_REF].

Example. We consider a security device that allows the creation of keys in its secure memory. The user can access the device via an API. If he creates a key, he obtains a handle, which he can use to let the device perform operations on his behalf. For each handle the device also stores an attribute which defines what operations are permitted for this handle. The goal is that the user can never gain knowledge of the key, as the user's machine might be compromised. We model the device by the following process (we use out(m) as a shortcut for out(c, m) for a public channel c):

!P new | !P set | !P dec | !P wrap , where P new := νh; νk; event NewKey(h,k); insert 'key',h ,k; insert ' att ' , h , 'dec'; out(h)
In the first line, the device creates a new handle h and a key k and, by the means of the event NewKey(h, k), logs the creation of this key. It then stores the key that belongs to the handle by associating the pair 'key', h to the value of the key k. In the next line, 'att', h is associated to a public constant 'dec'. Intuitively, we use the public constants 'key' and 'att' to distinguish two databases. The process P set := in(h); insert 'att',h , 'wrap' allows the attacker to change the attribute of a key from the initial value 'dec' to another value 'wrap'. If a handle has the 'dec' attribute set, it can be used for decryption:

P dec := in( h,c ); lookup 'att',h as a in if a='dec' then lookup 'key' ,h as k in if encSucc(c,k) then event DecUsing(k,sdec(c,k)); out(sdec(c,k))
The first lookup stores the value associated to 'att', h in a. The value is compared against 'dec'. If the comparison and another lookup for the associated key value k succeeds, we check whether decryption succeeds and, if so, output the plaintext.

If a key has the 'wrap' attribute set, it might be used to encrypt the value of a second key, e. g., to export the key for external storage:

P wrap := in( h 1 ,h 2 ); lookup 'att',h 1 as a 1 in if a 1 ='wrap' then lookup 'key' ,h 1 as k 1 in lookup 'key', h 2 as k 2 in event Wrap(k 1 ,k 2 ); out(senc(k 2 ,k 1 )) a ∈ FN ∪ PN a / ∈ ñ ν ñ.σ a DNAME ν ñ.σ t t = E t ν ñ.σ t DEQ x ∈ D(σ) ν ñ.σ xσ DFRAME ν ñ.σ t 1 • • • ν ñ.σ t n f ∈ Σ k ν ñ.σ f (t 1 , . . . , t n ) DAPPL Fig. 2. Deduction rules.
The bound names of a process are those that are bound by νn. We suppose that all names of sort fresh appearing in the process are under the scope of such a binder. Free names must be of sort pub. A variable x can be bound in two ways: (i) by the construct lookup M as x, or (ii) x ∈ vars(N ) in the construct in(M, N ) and x is not under the scope of a previous binder, While the construct lookup M as x always acts as a binder, the input construct does not rebind an already bound variable but performs pattern matching. For instance in the process

P = in(c,f (x)); in(c,g(x))
x is bound by the first input and pattern matched in the second. It might seem odd that lookup acts as a binder, while input does not. We justify this decision as follows: as P dec and P wrap in the previous example show, lookups appear often after input was received. If lookup were to use pattern matching, the following process P = in(c, x); lookup 'store' as x in P might unexpectedly perform a check if 'store' contains the message given by the adversary, instead of binding the content of 'store' to x, due to an undetected clash in the naming of variables.

A process is ground if it does not contain any free variables. We denote by P σ the application of the homomorphic extension of the substitution σ to P . As usual we suppose that the substitution only applies to free variables. We sometimes interpret the syntax tree of a process as a term and write P | p to refer to the subprocess of P at position p (where |, if and lookup are interpreted as binary symbols, all other constructs as unary). Our tool supports additional syntactic sugar: else-branches consisting of the 0-Process can be omitted, as well as let-construct for terms ( let m = dec(c, k) in out(m) ) and processes ( let P = . . . in !P ) perform simple substitution.

Semantics

Frames and deduction. Before giving the formal semantics of SAPiC we introduce the notions of frame and deduction. A frame consists of a set of fresh names ñ and a substitution σ and is written ν ñ.σ. Intuitively a frame represents the sequence of messages that have been observed by an adversary during a protocol execution and secrets ñ generated by the protocol, a priori unknown to the adversary. Deduction models the capacity of the adversary to compute new messages from the observed ones.

Definition 1 (Deduction). We define the deduction relation ν ñ.σ t as the smallest relation between frames and terms defined by the deduction rules in Figure 2. Example. If one key is used to wrap a second key, then, if the intruder learns the first key, he can deduce the second. For

x 1 ∈ D(σ) ν ñ.σ c x 2 ∈ D(σ) ν ñ.σ k 1 ν ñ.σ sdec(c, k 1 ) sdec(c, k 1 ) = E k 2 ν ñ.σ k 2
ñ = k 1 , k 2 and σ = { senc(k 2 ,k 1 ) / x 1 , k 1 / x 2 }, ν ñ.σ k 2 ,
as witnessed by the proof tree given in Figure 3.

Operational semantics. We can now define the operational semantics of our calculus. The semantics is defined by a labelled transition relation between process configurations. A process configuration is a 5-tuple (E, S, P, σ, L) where -E ⊆ FN is the set of fresh names generated by the processes; -S : M Σ → M Σ is a partial function modeling the store; -P is a multiset of ground processes representing the processes executed in parallel; σ is a ground substitution modeling the messages output to the environment; -L ⊆ M Σ is the set of currently acquired locks.

The transition relation is defined by the rules described in Figure 4. Transitions are labelled by sets of ground facts. For readability we omit empty sets and brackets around singletons, i.e., we write → for

∅ -→ and f -→ for { f } -→.
We write → * for the reflexive, transitive closure of → (the transitions that are labelled by the empty sets) and write f ⇒ for → * f →→ * . We can now define the set of traces, i.e., possible executions that a process admits. Definition 2 (Traces of P ). Given a ground process P we define the set of traces of P as

traces pi (P ) = [F 1 , . . . , F n ] | (∅, ∅, {P }, ∅, ∅) F 1 =⇒ (E 1 , S 1 , P 1 , σ 1 , L 1 ) F 2 =⇒ . . . Fn =⇒ (E n , S n , P n , σ n , L n )
Example. In Figure 5 we display the transitions corresponding to the creation of a key on the security device in our running example and witness that [NewKey(h , k )] ∈ traces pi (P ).

Labelled multiset rewriting

We now recall the syntax and semantics of labelled multiset rewriting rules, which constitute the input language of the tamarin tool [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF].

Definition 3 (Multiset rewrite rule). A labelled multiset rewrite rule ri is a triple (l, a, r), l, a, r ∈ F * , written l -[ a ]→ r. We call l = prems(ri ) the premises, a = actions(ri ) the actions, and r = conclusions(ri ) the conclusions of the rule. Definition 4 (Labelled multiset rewriting system). A labelled multiset rewriting system is a set of labelled multiset rewrite rules R, such that each rule l -[ a ]→ r ∈ R satisfies the following conditions:

Standard operations: l, a, r do not contain fresh names and r does not contain Fr-facts.

(E, S, P ∪ # {0}, σ, L) -→ (E, S, P, σ, L) (E, S, P ∪ # {P |Q}, σ, L) -→ (E, S, P ∪ # {P, Q}, σ, L) (E, S, P ∪ # {!P }, σ, L) -→ (E, S, P ∪ # {!P, P }, σ, L) (E, S, P ∪ # {νa; P }, σ, L) -→ (E ∪ {a }, S, P ∪ # {P {a /a}}, σ, L) if a is fresh (E, S, P, σ, L) K(M ) ----→ (E, S, P, σ, L) if νE.σ M (E, S, P ∪ # {out(M, N ); P }, σ, L) K(M ) ----→ (E, S, P ∪ # {P }, σ ∪ { N / x }, L) if x is fresh and νE.σ M (E, S, P ∪ # {in(M, N ); P }, σ, L) K( M,N τ ) -------→ (E, S, P ∪ # {P τ }, σ, L) if νE.σ M,
(E, S, P ∪ # {insert M, N ; P }, σ, L) -→ (E, S[M → N ], P ∪ # {P }, σ, L) (E, S, P ∪ # {delete M ; P }, σ, L) -→ (E, S[M → ⊥], P ∪ # {P }, σ, L) (E, S, P ∪ # {lookup M as x in P else Q }, σ, L) -→ (E, S, P ∪ # {P {V /x}}, σ, L) if S(N ) = E V is defined and N = E M (E, S, P ∪ # {lookup M as x in P else Q }, σ, L) -→ (E, S, P ∪ # {Q}, σ, L) if S(N ) is undefined for all N = E M (E, S, P ∪ # {lock M ; P }, σ, L) -→ (E, S, P ∪ # {P }, σ, L ∪ { M }) if M ∈ E L (E, S, P ∪ # {unlock M ; P }, σ, L) -→ (E, S, P ∪ # {P }, σ, L \ { M | M = E M })
A labelled multiset rewriting system is called well-formed, if additionally

-for each l -[ a ]→ r ∈ E ginsts(l -[ a ]→ r) we have that ∩ r = E r names(r ) ∩ FN ⊆ ∩ l = E l names(l ) ∩ FN .
We define one distinguished rule FRESH which is the only rule allowed to have Fr-facts on the righthand side

FRESH : [] -[]→ [Fr(x : fresh)]
The semantics of the rules is defined by a labelled transition relation.

(∅, ∅, { !P new | !P set |!P dec |!P wrap =:P } # , ∅, ∅) → (∅, ∅, { P new } # ∪ # P , ∅, ∅) → (∅, ∅, { ν h; ν k; event NewKey(h, k); . . . } # ∪ # P , ∅, ∅) → * ({ h , k }, ∅, { event NewKey(h , k ); . . . } # ∪ # P , ∅, ∅) NewKey(h ,k ) ---------→ ({ h , k }, ∅, { insert 'key , h , k ; . . . } # ∪ # P , ∅, ∅) → * ({ h , k }, S, { out(h ); 0 } # ∪ # P , ∅, ∅) → * ({ h , k }, S, P , { h / x 1 }, ∅)
where S( 'key , h ) = k and S( 'att , h ) = 'dec'.

→ R ⊆ G # × P(G) × G # as S a -→ R ((S \ # lfacts(l)) ∪ # r) if and only if l -[ a ]→ r ∈ E ginsts(R ∪ FRESH), lfacts(l) ⊆ # S and pfacts(l) ⊆ S.
Definition 6 (Executions). Given a multiset rewriting system R we define its set of executions as

exec msr (R) = ∅ A 1 -→ R . . . An -→ R S n | ∀a, i, j : 0 ≤ i = j < n. (S i+1 \ # S i ) = {Fr(a)} ⇒ (S j+1 \ # S j ) = {Fr(a)}
The set of executions consists of transition sequences that respect freshness, i. e., for a given name a the fact Fr(a) is only added once, or in other words the rule FRESH is at most fired once for each name. We define the set of traces in a similar way as for processes.

Definition 7 (Traces). The set of traces is defined as

traces msr (R) = [A 1 , . . . , A n ] | ∀ 0 ≤ i ≤ n. A i = ∅ and ∅ A 1 =⇒ R . . . An =⇒ R S n ∈ exec msr (R)
where

A =⇒ R is defined as ∅ -→ * R A -→ R ∅ -→ * R .
Note that both for processes and multiset rewrite rules the set of traces is a sequence of sets of facts.

Security Properties

In the tamarin tool [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF] security properties are described in an expressive two-sorted first-order logic. The sort temp is used for time points, V temp are the temporal variables.

Definition 8 (Trace formulas). A trace atom is either false ⊥, a term equality t 1 ≈ t 2 , a timepoint ordering i j, a timepoint equality i . = j, or an action F @i for a fact F ∈ F and a timepoint i. A trace formula is a first-order formula over trace atoms.

As we will see in our case studies this logic is expressive enough to analyze a variety of security properties, including complex injective correspondence properties.

To define the semantics, let each sort s have a domain D(s). D(temp) = Q, D(msg) = M, D(fresh) = FN , and D(pub) = PN . A function θ : V → M ∪ Q is a valuation if it respects sorts, i. e., θ(V s ) ⊂ D(s) for all sorts s. If t is a term, tθ is the application of the homomorphic extension of θ to t. Definition 9 (Satisfaction relation). The satisfaction relation (tr , θ) ϕ between a trace tr , a valuation θ and a trace formula ϕ is defined as follows:

(tr , θ) ⊥ never (tr , θ) F @i iff θ(i) ∈ idx (tr) and F θ ∈ E tr θ(i) (tr , θ) i j iff θ(i) < θ(j) (tr , θ) i . = j iff θ(i) = θ(j) (tr , θ) t 1 ≈ t 2 iff t 1 θ = E t 2 θ (tr , θ) ¬ϕ iff not (tr , θ) ϕ (tr , θ) ϕ 1 ∧ ϕ 2 iff (tr , θ) ϕ 1 and (tr , θ) ϕ 2 (tr , θ) ∃x : s.ϕ iff there is u ∈ D(s) such that (tr , θ[x → u]) ϕ
For readability, we define t 1 t 2 as ¬(t 1 t 2 ∨ t 1 . = t 2 ) and ( • ≤, . =, • ≥) as expected. We also use classical notational shortcuts such as t 1 t 2 t 3 for t 1 t 2 ∧ t 2 t 3 and ∀i ≤ j. ϕ for ∀i. i ≤ j → ϕ. When ϕ is a ground formula we sometimes simply write tr ϕ as the satisfaction of ϕ is independent of the valuation.

Definition 10 (Validity, satisfiability). Let Tr ⊆ (P(G)) * be a set of traces. A trace formula ϕ is said to be valid for Tr , written Tr ∀ ϕ, if for any trace tr ∈ Tr and any valuation θ we have that (tr , θ) ϕ.

A trace formula ϕ is said to be satisfiable for Tr , written Tr ∃ ϕ, if there exist a trace tr ∈ Tr and a valuation θ such that (tr , θ) ϕ.

Note that Tr ∀ ϕ iff Tr ∃ ¬ϕ. Given a multiset rewriting system R we say that ϕ is valid, written R ∀ ϕ, if traces msr (R) ∀ ϕ. We say that ϕ is satisfied in R, written R ∃ ϕ, if traces msr (R) ∃ ϕ. Similarly, given a ground process P we say that ϕ is valid, written P ∀ ϕ, if traces pi (P ) ∀ ϕ, and that ϕ is satisfied in P , written P ∃ ϕ, if traces pi (P ) ∃ ϕ.

Example. The following trace formula expresses secrecy of keys generated on the security API, which we introduced in Section 3.

¬(∃h, k : msg, i, j : temp. NewKey(h, k)@i ∧ K(k)@j)

A translation from processes into multiset rewrite rules

In this section we define a translation from a process P into a set of multiset rewrite rules P and a translation on trace formulas such that P |= ∀ ϕ if and only if P |= ∀ ϕ . Note that the result also holds for satisfiability, as an immediate consequence. For a rather expressive subset of trace formulas (see [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF] for the exact definition of the fragment), checking whether P |= ∀ ϕ can then be discharged to the tamarin prover that we use as a backend.

Out(x) -[ ]→ !K(x) (MDOUT) !K(x) -[ K(x) ]→ In(x) (MDIN) -[ ]→ !K(x : pub) (MDPUB) Fr(x : fresh) -[ ]→ !K(x : fresh) (MDFRESH) !K(x 1 ), . . . , !K(x k ) -[ ]→ !K(f (x 1 , . . . , x k )) for f ∈ Σ k (MDAPPL)
Fig. 6. The set of rules MD.

Definition of the translation of processes

To model the adversary's message deduction capabilities, we introduce the set of rules MD defined in Figure 6. In order for our translation to be correct, we need to make some assumptions on the set of processes we allow. These assumptions are however, as we will see, rather mild and most of them without loss of generality. First we define a set of reserved variables that will be used in our translation and whose use we therefore forbid in the processes.

Definition 11 (Reserved variables and facts). The set of reserved variables is defined as the set containing the elements n a for any a ∈ FN and lock l for any l ∈ N. The set of reserved facts F res is defined as the set containing facts f (t 1 , . . . , t n ) where t 1 , . . . , t n ∈ T and f ∈ { Init, Insert, Delete, IsIn, IsNotSet, state, Lock, Unlock, Out, Fr, In, Msg, ProtoNonce, Event, InEvent, Pred pr , Pred_not pr | pr ∈ Σ pred }.

For our translation to be sound, we require that for each process, there exists an injective mapping assigning to every unlock t in a process a lock t that precedes it in the process' syntax tree. Moreover, given a process lock t; P the corresponding unlock in P shall not be under a parallel or replication. These conditions allow us to annotate each corresponding pair lock t, unlock t with a unique label l. The annotated version of a process P is denoted P . In case the annotation fails, i.e., P violates one of the above conditions, the process P contains ⊥. This is similar to the hypotheses on locks made in StatVerif [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF]. They precisely require that:

"In every branch of the syntax tree, every lock must be followed by precisely one corresponding unlock. In lock; P , the part of the process P that occurs before the next unlock, if any, may not include parallel, replication, or lock." Unlike StatVerif we do not need to forbid nested locks for our results to hold, even though nested locks are not very useful as they directly lead to deadlocks.

Definition 12 (Process annotation). Given a ground process P we define the annotated ground process P as ap(P, []) where: ap(0, A) := 0

ap(P |Q, A) :=    ap(P, A)|ap(Q, A) if A = [] ⊥ otherwise ap(!P, A) :=    !ap(P, A) if A = [] ⊥ otherwise ap(if
               unlock l t; ap(P, A \ {(t, l)}) if ∃i. A i = (t, l)
and ∀l , j < i.A j = (t, l )

for A = (A 0 , . . . , A m ) ⊥ otherwise
Intuitively, the function ap(P, A) makes a traversal of the process P and maintains the list A of pending unlocks. A pair (l, t) is in A whenever the instruction lock t was encountered, annotated by the label l and no corresponding instruction unlock t was found yet. When encountering an unlock t instruction we annotate it with the first corresponding label that was added to the list. We choose the first occurrence in the list in order to guarantee that the resulting process is uniquely defined. Remark that the Appendix of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] contains a different but equivalent formulation of this definition.

Definition 13 (well-formed). A ground process P is well-formed if no reserved variable nor reserved fact appears in P , any bound name and variable in P cannot be rebound, i.e., if u is bound in P then u is not under the scope of a previous binder, and -P does not contain ⊥.

A trace formula ϕ is well-formed if no reserved variable nor reserved fact appear in ϕ.

The two first restrictions of well-formed processes can be assumed without loss of generality as processes and formulas can be consistently renamed to avoid reserved variables and α-converted to avoid binding names or variables several times. Also note that the second condition is not necessarily preserved during an execution, e.g. when unfolding a replication, !P and P may bind the same names. We only require this condition to hold on the initial process for our translation to be correct.

The annotation of locks restricts the set of protocols we can translate, but allows us to obtain better verification results, since we can predict which unlock is "supposed" to close a given lock. This additional information is helpful for tamarin's backward reasoning. We think that our locking mechanism captures all practical use cases. Obviously, locks can be modelled both in tamarin's multiset rewriting calculus (this is actually what the translation does) and Mödersheim's set rewriting calculus [START_REF] Mödersheim | Abstraction by set-membership: verifying security protocols and web services with databases[END_REF]. However, protocol steps typically consist of a single input, followed by several database lookups, and finally an output. In practice, they tend to be modelled as a single rule, and are therefore atomic. Real implementations are however different, as several entities might be involved, database lookups could be slow, etc. In this case, such simplified models could, e. g., miss race conditions. To the best of our knowledge, StatVerif is the only comparable tool that models locks explicitly and it has stronger restrictions. Definition 14. Given a well-formed ground process P we define the labelled multiset rewriting system P as

MD ∪ {INIT} ∪ P , [], [] ,
where the rule INIT is defined as

INIT : [] -[ Init() ]→ [state [] (
)] and P, p, x is defined inductively for process P , position p ∈ N * and sequence of variables x in Figure 7. For a position p in P we define state p to be persistent if P | p = !Q for some process Q; otherwise state p is linear.

In the definition of P, p, x we intuitively use the family of facts state p to indicate that the process is currently at position p in its syntax tree. A fact state p will indeed be true in an execution of these rules whenever some instance of P p (i.e. the process defined by the subtree at position p of the syntax tree of P ) is in the multiset P of the process configuration. The translation of the zero-process, parallel and replication operators merely use state p -facts. For instance P | Q, p, x defines the rule

[state p (x)] → [state p•1 (x), state p•2 (x)]
which intuitively states that when a process is at position p (modelled by the fact state p (x) being true) then the process is allowed to move both to P (putting state p•1 (x) to true) and Q (putting state p•2 (x) to true). The translation of P | Q, p, x also contains the set of rules P, p • 1, x ∪ Q, p • 2, x expressing that after this transition the process may behave as P and Q, i.e., the processes at positions p • 1, respectively p • 2, in the process tree. Also note that the translation of !P results in a persistent fact as !P always remains in P. The translation of the construct ν a translates the name a into a variable n a , as msr rules must not contain fresh names. Any instantiation of this rule will substitute n a by a fresh name, which the Fr-fact in the premise guarantees to be new. This step is annotated with a (reserved) action ProtoNonce. This annotation is merely used in the proof of correctness to distinguish adversary and protocol nonces which is useful as it allows us to identify the restricted names of the process. Note that the fact state p•1 in the conclusion carries n a , so that the following protocol steps are bound to the fresh name used to instantiate n a . The first rules of the translation of out and in model the communication between the protocol and the adversary, and vice versa. In the case of out, the adversary must know the channel M , modelled by the fact In(M ) in the rule's premisse, and learns the output message, modelled by the fact Out(N ) in the conclusion. In the case of in, the knowledge of the message N is additionally required and the variables of the input message are added to the parameters of the state fact to reflect that these variables are bound. The second and third rules of the translations of out and in model an

0, p, x = {[state p (x)] → []} P | Q, p, x = {[state p (x)] → [state p•1 (x), state p•2 (x)]} ∪ P, p • 1, x ∪ Q, p • 2, x !P, p, x = {[!state p (x)] → [state p•1 (x)]} ∪ P, p • 1, x νa; P, p, x = {[state p (x), Fr(n a : fresh)] -[ ProtoNonce(n a : fresh) ]→ [state p•1 (x, n a : fresh)]} ∪ P, p • 1, (x, n a : fresh) Out(M, N ); P, p, x = {[state p (x), In(M )] -[ InEvent(M ) ]→ [Out(N ), state p•1 (x)], [state p (x)] → [Msg(M, N ), state semi p (x)], [state semi p (x), Ack(M, N )] → [state p•1 (x)]} ∪ P, p • 1, x In(M, N ); P, p, x = {[state p (x), In( M, N )] -[ InEvent( M, N ) ]→ [state p•1 (x ∪ vars(N ))], [state p (x), Msg(M, N )] → [state p•1 (x ∪ vars(N )), Ack(M, N )]} ∪ P, p • 1, x ∪ vars(N ) if pr (M 1 , . . . , M k ) then P else Q, p, x = {[state p (x)] -[ Pred pr (M 1 , . . . , M k ) ]→ [state p•1 (x)], [state p (x)] -[ Pred_not pr (M 1 , . . . , M k ) ]→ [state p•2 (x)]} ∪ P, p • 1, x ∪ Q, p • 2, x event F ; P, p, x = {[state p (x)] -[ Event(), F ]→ [state p•1 (x)]} ∪ P, p • 1, x insert s, t; P, p, x = {[state p (x)] -[ Insert(s, t) ]→ [state p•1 (x)]} ∪ P, p • 1, x delete s; P, p, x = {[state p (x)] -[ Delete(s) ]→ [state p•1 (x)]} ∪ P, p • 1, x lookup M as v in P else Q, p, x = {[state p (x)] -[ IsIn(M, v) ]→ [state p•1 ( M , v)], [state p (x)] -[ IsNotSet(M ) ]→ [state p•2 (x)]} ∪ P, p • 1, (x, v) ∪ Q, p • 2, x lock l s; P, p, x = {[Fr(lock l ), state p (x)] -[ Lock(lock l , s) ]→ [state p•1 (x, lock l )]} ∪ P, p • 1, x unlock l s; P, p, x = {[state p (x)] -[ Unlock(lock l , s) ]→ [state p•1 (x)]} ∪ P, p • 1, x Fig. 7.
Translation of processes: definition of P, p, x internal communication, which is synchronous. For this reason, when the second rule of the translation of out is fired, the state-fact is substituted by an intermediate, semi-state fact, state semi , reflecting that the sending process can only execute the next step if the message was successfully received. The fact Msg(M, N ) models that a message is present on the synchronous channel. Only with the acknowledgement fact Ack(M, N ), resulting from the second rule of the translation of in, is it possible to advance the execution of the sending process, using the third rule in the translation of out, which transforms the semi-state and the acknowledgement of receipt into state p•1 (. . .). Only now the next step in the execution of the sending process can be executed. The remaining rules essentially update the position in the state facts and add labels. Some of these labels are used to restrict the set of executions. For instance the label Pred_pr (M 1 , . . . , M k ) will be used to indicate that we only consider executions in which φ pr holds for M 1 , . . . , M k . As we will see in the next section these restrictions will be encoded in the trace formula.

[] -[ Init() ]→ [!state [] ()] [!state [] ()] -[ ]→ [state [1] ()] [state [1] (), Fr(h)] -[ ]→ [state [11] (h)] [state [11] (h), Fr(k)] -[ ]→ [state [111] (k, h)] [state [111] (k, h)] -[ Event(), NewKey(h, k) ]→ [state [1111] (k, h)] [state [1111] (k, h)] -[ Insert( 'key', h , k) ]→ [state [11111] (k, h)] [state [11111] (k, h)] -[ Insert( 'att', h , 'dec') ]→ [state [111111] (k, h)] [state [111111] (k, h)] -[ ]→ [Out(h), state [1111111] (k, h)]
Example. Figure 8 illustrates the above translation by presenting the set of msr rules !P new (omitting the rules in MD already shown in Figure 6). A graph representation of an example trace, similar to the one generated by the tamarin tool, is depicted in Figure 9. Every node stands for the application of a multiset rewrite rule, where the premises are at the top, the conclusions at the bottom, and the actions (if any) annotate the node. Every premise needs to have a matching conclusion, visualized by the arrows, to ensure the graph depicts a valid msr execution. (This is a simplification of the dependency graph representation tamarin uses to perform backwardinduction [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF][START_REF] Schmidt | The tamarin prover for the symbolic analysis of security protocols[END_REF].) We also note that in the current example !state [] () is persistent and can therefore be used multiple times as a premise. As Fr( ) facts are generated by the FRESH rule which has an empty premise and action, we omit instances of FRESH and leave those premises, but only those, disconnected.

Remark 1. One may note that, while for all other operators, the translation produces well-formed multiset rewriting rules (as long as the process is well-formed itself), this is not the case for the translation of the lookup operator, i. e., it violates the well-formedness condition from Definition 4. Tamarin's constraint solving algorithm requires all rules, with the exception of FRESH, to be well-formed. We show however that, under these specific conditions, the solution procedure is still correct. See Appendix A for the proof.

Definition of the translation of trace formulas

We can now define the translation for formulas.

Definition 15. Given a well-formed trace formula ϕ we define

ϕ ∀ := α ⇒ ϕ and ϕ ∃ := α ∧ ϕ
where α is defined in Figure 10.

The formula α uses the actions of the generated rules to filter out executions that we wish to discard:

α init ensures that the init rule is only fired once.

! α pred ensures that we only consider traces where for all positive and negative branches in conditionals the corresponding predicate formula, respectively its negation, hold. α in and α notin ensure that a successful lookup was preceded by an insert that was neither revoked nor overwritten while an unsuccessful lookup was either never inserted, or deleted and never reinserted.

state 11111 (h,k) Out(h) state 11111 (h,k) state 11111 (h ,k ) state 11111 (h ,k ) Out(h )
α lock checks that between each two matching locks there must be an unlock. Furthermore, between the first of these locks and the corresponding unlock, there is neither a lock nor an unlock. α inev ensures that whenever an instance of MDIN is required to generate an In-fact, it is generated as late as possible, i. e., there is no visible event between the action K(t) produced by MDIN, and a rule that requires In(t).

We also note that Tr ∀ ϕ ∀ iff Tr ∃ ¬ϕ ∃ .

Discussion of design choices

There exist certainly other ways of correctly translating our calculus into msr rules. Most of our choices were guided by the way tamarin internally works. To better appreciate our choices we will give a highlevel overview of the procedure implemented in tamarin. A detailed review of the procedure is however out of scope of this paper and we refer the reader to [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF] for a detailed description.

A short overview of tamarin. Tamarin basically applies a backward reasoning approach to try to find a trace which satisfies a given formula. (Validity claims are first translated to satisfiability claims.) This is reminiscent to the reasoning when proving protocol correctness in the strand space model [START_REF] Thayer Fabrega | Strand spaces: Proving security protocols correct[END_REF]. More precisely, rather than reasoning about traces, tamarin reasons about dependency graphs, an enriched representation of traces. Dependency graphs are DAGs, where each node corresponds to a ground instance of an msr rule and the edges represent the causal dependencies among these rules. For every premise of a rule there is an incoming edge from another rule with a conclusion that matches the premise. Moreover, linear facts may have at most one outgoing edge and fresh rules are unique. Every topological ordering then corresponds to a trace. Tamarin's backward search is formalised by a constrained solving algorithm. The solutions of a constraint system are the dependency graphs whose traces satisfy the constraints. The initial constraint system is simply the formula to be satisfied. The procedure then applies simplification rules which preserve all solutions. If the constraint system reaches ⊥ the formula is unsatisfiable. In case no more rules can be applied the system is solved, and the dependency graphs that are the solutions of the constraint system can be directly constructed.

α := α init ∧ α pred ∧ α noteq ∧ α in ∧ α notin ∧ α lock ∧ α inev and α init := ∀i, j. Init()@i ∧ Init()@j =⇒ i . = j α pred := pr ∈Σ pred {∀x 1 , . . . , x k , i. Pred pr (x 1 , . . . , x k )@i =⇒ φ pr | pr is of arity k}∧ pr ∈Σ pred {∀x 1 , . . . , x k , i. Pred_not pr (x 1 , . . . , x k )@i =⇒ ¬(φ pr ) | pr is of arity k} α in := ∀x, y, t 3 . IsIn(x, y)@t 3 =⇒ ∃t 2 . Insert(x, y)@t 2 ∧ t 2 t 3 ∧ ∀t 1 . Delete(x)@t 1 =⇒ (t 1 t 2 ∨ t 3 t 1 ) ∧ ∀t 1 , y. Insert(x, y)@t 1 =⇒ (t 1 • ≤ t 2 ∨ t 3 t 1 ) α notin := ∀x, t 3 . IsNotSet(x)@t 3 =⇒ (∀t 1 , y. Insert(x, y)@t 1 =⇒ t 3 t 1 )∨ (∃t 1 . Delete(x)@t 1 ∧ t 1 t 3 ∧ ∀t 2 , y. (Insert(x, y)@t 2 ∧ t 2 t 3 ) =⇒ t 2 t 1 )
α lock := ∀x, l, l , t 1 , t 3 . Lock(l, x)@t 1 ∧ Lock(l , x)@t 3 ∧ t 1 t 3 =⇒ ∃t 2 . Unlock(l, x)@t 2 ∧ t 1 t 2 t 3 ∧ (∀t 0 . Unlock(l, x)@t 0 =⇒ t 0 . = t 2 ) ∧ (∀l , t 0 . Lock(l , x)@t 0 =⇒ t 0 • ≤ t 1 ∨ t 2 t 0 ) ∧ (∀l , t 0 . Unlock(l , x)@t 0 =⇒ t 0 t 1 ∨ t 2 • ≤ t 0 ) α inev := ∀x, t 3 . InEvent(x)@t 3 =⇒ ∃t 2 . K(x)@t 2 ∧ t 2 t 3 ∧ (∀t 0 . Event()@t 0 =⇒ (t 0 t 2 ∨ t 3 t 0 )) ∧ (∀t 0 , x . K(x )@t 0 =⇒ (t 0 • ≤ t 2 ∨ t 3 t 0 ))
Slightly simplifying, a typical rule in the constraint solving algorithm would state that if the formula is of the form a@i then the dependency graph must contain a node corresponding to a rule b -→ r with an action b that matches a. Next, it will try to solve each premise in by adding a constraint that this rule must be preceded by a node corresponding to rules with a fact in its conclusion matching this premise.

Another example of a simplification rule is the following, which reasons about the uniqueness of fresh names: when the constraint system contains both Fr(n)@i and Fr(n)@j it concludes that i . = j. The constraint simplification procedure may of course enter a loop and not terminate. This is natural given that the underlying problem is undecidable. The algorithm can nevertheless be guided by heuristics to avoid some of these loops and use previously proven lemmas and axioms to prune otherwise infinite branches.

Design choices. The axioms in the translation of the formula are designed to work hand in hand with the translation of the process into rules. They express the correctness of traces with respect to our calculus' semantics, but are also meant to guide tamarin's constraint solving algorithm. The use of axioms, rather than other possible encodings, often helps the algorithm to enforce termination as they can be used to cut branches that are not consistent with the axioms. We will discuss the axioms related to state manipulation.

Let us first consider the axioms related to lock actions. A naïve axiomatization would postulate that "every lock is preceded by an unlock and no lock or unlock in between, unless it is the first lock." This would however cause tamarin to loop, as we will see below. We will first illustrate how the axiom α lock avoids this caveat because it only applies to pairs of locks carrying the same annotations.

Consider the constraint solving procedure for the following process

P := !(lock 's'; lookup 'visited' as v in unlock 's' else event Visit (); insert ' visited ' , 's' ; unlock 's')
and the trace formula ∀i, j.Visit()@i∧Visit()@j =⇒ i . = j. The msr rules generated by our translation are depicted in Figure 11. i : Visit() j : Visit() i j Fig. 12. Constraint system resulting from the negation of ∀i, j.Visit()@i ∧ Visit()@j =⇒ i . = j.

[] -[ Init() ]→ [!state()] [!state()] -[ ]→ [state 1 ()] [state 1 (), Fr(l)] -[ Lock(l, 's') ]→ [state 11 (l)] [state 11 (l)] -[ IsIn('visited', v) ]→ [state 111 (l, v)] [state 111 (l, v)] -[ (l, 's') ]→ [state 1111 (l, v)] [state 11 (l)] -[ IsNotSet('visited') ]→ [state 112 (l)] [state 112 (l)] -[ Event(), Visit() ]→ [state 1121 (l)] [state 1121 (l)] -[ Unlock('visited', 's') ]→ [state 11211 (l)] [state 11211 (l)] -[ Unlock(l, 's') ]→ [state 112111 (l)]
1. Tamarin shows validity of the trace formula by showing that its negation ∃i, j.Visit()@i ∧ Visit()@j ∧(i j ∨j i) is not satisfiable. Two symmetrical constraint systems need to be refuted, we focus on the one pictured in Figure 12, i. e., the case where i j.

! Fig. 14. By α lock , there exists node Unlock(l1,'s') at position t2 such that t1 t2 t3 without any matching lock or unlock for 's' between t1 and t2.

i j t1 t2 t3 ∀l , t0. Lock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 ∀l , t0. Unlock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 !state [] () state 1 () !state [] () state 1 () t 1 : Fr(l
2. As all state-premises have exactly one rule with a matching conclusion, there are two chains of rule instances from i and j up to the INIT rule, which is unique by α init . Both are recovered in this step, see Figure 13. As tamarin pre-computes chains of rule instantiations whose open premises can be uniquely resolved, this is done in two steps, one for each chain. 3. Now α lock is applied, which adds the constraint that the first lock needs to have a matching unlock, i. e., a node Unlock(l 1 ,'s') has to appear at some position t 2 between positions t 1 and t 3 as sketched in Figure 14. More precisely, we require the existence of an unlock for 's' annotated with l 1 , and no lock or unlock for 's' in between. The axiom itself contains only one case, so the only case distinction that takes place is over which rule produces the matching Unlock-action. Due to the

!state [] () Init() i j t1 t2 t3 ∀l , t0. Lock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 ∀l , t0. Unlock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 !state [] () state 1 () !state [] () state 1 () !state [] () state 1 () t 1 : Fr(l 1 ) state 1 () state 11 (l 1 )
Fr(l annotation, however, all but one are refuted immediately in the next step, as two nodes containing the same fact Fr(l 1 ) in the premise are unified immediately. 4. Due to the annotation, the fact state 11211 (l 1 ) contains the same fresh name l 1 that instantiates the annotation variable in Unlock(l 1 ,'s') at t 1 . Every fact state p (. . .) for some position p that is a prefix of p and a suffix of the position of the corresponding lock contains this fresh name. Furthermore, every rule instantiation that is an ancestor of a node in the dependency graph corresponds to the execution of a command that is an ancestor in the process tree. Therefore, the backward search eventually reaches the matching lock, including the annotation, which is determined to be l 1 , and hence appears in the Fr-premise (Figure 15). 5. Because of the common premise Fr(l 1 ), both subgraphs are merged. The result is a sequence of nodes from the first lock to the corresponding unlock, and graph constraints restricting the second lock to not take place between the first lock and the unlock. We note that the axiom α lock is only instantiated once per pair of locks, since it requires that i j, thereby fixing their order. If we would not annotate locks with fresh names, these two subgraphs would not be merged, as they could be different. In fact, the axion α lock would apply again, e. g., for Lock(l 1 ,'s') (or rather Lock('s')) at t 1 and the newly created rule instantiation with the same action. We would thus run in a loop. 6. We have achieved a total ordering on all rule instantiations that appear in the constrain system. Now α notin can be applied for the rule instantiation at k as pictured in Figure 16. Since t 2 t 3 , it holds that i k and thus the first case can be refuted. The second case is also refuted right away, as there is no rule with action Delete in the translation of P .

!state [] () Init() i j t1 t2 t3 ∀l , t0. Lock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 ∀l , t0. Unlock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 Fig. [START_REF] Garay | Abuse-free optimistic contract signing[END_REF]. Because of the identical premise Fr(l1) in both chains leading to ti and t2, and as all state-facts below position [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] are linear, both subgraphs are merged.

!state [] () state 1 () !state [] () state 1 () t 1 : Fr(l
In contrast, consider now the naïve formulation of α lock ( "every lock is preceded by an unlock and no lock or unlock in between, unless it is the first lock"):

α lock = ∀t 1 , l, s.Lock (l, s)@t 1 =⇒ (∃t 0 , l . Unlock (l , s)@t 0 ∧ t 0 t 1 ∧(∀t i , l i .Lock (l i , s)@t i ⇒ (t i t 0 ) ∨ (t 1 t i )) ∧(∀t i , l i .Unlock (l i , s)@t i ⇒ (t i t 0 ) ∨ (t 1 t i ))) ∨(∀t i , l i .Lock (l i , s)@t i ⇒ t 0 t i )
Even if annotations are employed, this would easily provoke a loop: applied after the second step, to the Lock-node at t 3 (see Figure 13), the first case would require a node Unlock(l ,'s') at position t 0 with t 0 t 3 . Similar to the second step, a chain of rule instances from this node to the unique instantiation of the INIT rule would be created in one step, pictured in Figure 17. Observe that the rule instantiation at position t 0 has an action Lock(l ,'s'). As l is not necessarily equal to l 1 or l 2 , this chain of rule instantiations cannot be merged with any other subgraphs. Hence the Lock-action at position t 0 needs is considered to be new, and thus α lock can be applied again, resulting in a loop. This loop is triggered whenever an action Lock(l,'s') appears.

In summary, a careful formulation of this axiom was necessary to avoid loops. The annotation helps distinguishing which unlock is expected between two locks, vastly improving the speed of the backward search. This optimisation, however, required us to put restrictions on the locks. The axiom is formulated in a way that links the lock with the corresponding unlock by means of this annotation. The equivalence between α lock and the naïve formulation is non-trivial, but shown in the proof of Lemma 10 in Appendix B.

state [] () Init() i j t1 t2 t3 ∀l , t0. Lock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 ∀l , t0. Unlock(l ,'s') @t0 =⇒ t0 t1 ∨ t2 t0 Similarly, the axioms α in and α notin are designed to work well with tamarin's constraint solving algorithm: when a constraint with the action IsIn is created, by definition of the translation, this corresponds to a lookup command. The existential in α in translates into a graph constraint that postulates the existence of an insert node for the value fetched by the lookup, and three formulas assuring that (i) this insert node appears before the lookup, (ii) is uniquely defined, i. e., it is the last insert to the corresponding key, and (iii) there is no delete in between. Due to these conditions, α notin only adds one Insert node per IsIn node -the case where an axiom postulates a node, which itself allows for postulating yet another node needs to be avoided, as tamarin runs into loops otherwise. The technique of enforcing correctness of the translation through rewriting the formula via these axioms additionally allows us to convey information on the nature of our rules resulting from the translation to the constraint solving algorithm.

!state [] () state 1 () !state [] () state 1 () !state [] () state 1 () t 1 : Fr(l

Correctness of the translation

The correctness of our translation is stated by the following theorem.

Theorem 1. Given a well-formed ground process P and a well-formed trace formula ϕ we have that

traces pi (P ) ϕ iff traces msr ( P ) ϕ
where is either ∀ or ∃.

We here give an overview of the main propositions and lemmas needed to prove Theorem 1. To show the result we need two additional definitions. We first define an operation that allows to restrict a set of traces to those that satisfy the trace formula α as defined in Definition 15. The following proposition states that if a set of traces satisfies the translated formula then the filtered traces satisfy the original formula. where is either ∀ or ∃.

Proof. We first show the two directions for the case = ∀. We start by showing that Tr ∀ ϕ implies filter (Tr ) ϕ.

Tr ∀ ϕ ∀ ⇒ filter (Tr ) ∀ ϕ ∀ (since filter (Tr ) ⊆ Tr ) ⇔ filter (Tr ) ∀ α ⇒ ϕ (by definition of ϕ ∀ ) ⇔ filter (Tr ) ∀ ϕ (since filter (Tr ) ∀ α)
We next show that filter (Tr ) ∀ ϕ implies Tr ∀ ϕ ∀ .

filter (Tr ) ∀ ϕ ⇒ filter (Tr ) ∀ α ∧ ϕ (since filter (Tr ) ∀ α) ⇔ Tr ∀ ¬α ∨ (α ∧ ϕ) (since filter (Tr ) ⊆ Tr and (Tr \ filter (Tr )) ∀ α) ⇔ Tr ∀ α ⇒ ϕ ⇔ Tr ∀ ϕ ∀ (by definition of ϕ ∀ )
The case of = ∃ now easily follows:

Tr ∃ ϕ ∃ iff Tr ∀ ¬ϕ ∀ iff filter (Tr ) ∀ ¬ϕ iff filter (Tr ) ∃ ϕ.
Next we define the hiding operation which removes all reserved facts from a trace. As expected well-formed formulas that do not contain reserved facts evaluate the same whether reserved facts are hidden or not. We proceed by structural induction on ϕ.

ϕ = ⊥, ϕ = i j, ϕ = i . = j or t 1 . = t 2 . In these cases we trivially conclude as the truth value of these formulas does not depend on the trace and for both statements we simply let θ := θ. ϕ = f @i. We start with the first statement. Suppose that (tr , θ) f @i. If θ(i) < n then we have also that tr , θ f @i. By induction hypothesis, there exists θ such that (tr , θ ) f @i. Hence we also have that (tr , θ ) f @i and letting θ := θ allows us to conclude. If θ(i) = n we know that f ∈ tr n . As ϕ is well-formed f ∈ F res and hence f ∈ hide(tr ) n where n = |hide(tr )|. The proof of the other statement is similar. ϕ = ¬ϕ , ϕ = ϕ 1 ∧ ϕ 2 , or ϕ = ∃x : s.ϕ . We directly conclude by induction hypotheses (on the structure of ϕ).

From the above statements we easily have that Tr ∃ ϕ iff hide(Tr ) ∃ ϕ. The case of = ∀ now easily follows:

Tr ∀ ϕ iff Tr ∃ ¬ϕ iff hide(Tr ) ∃ ¬ϕ iff hide(Tr ) ∀ ϕ
We can now state our main lemma which is relating the set of traces of a process P and the set of traces of its translation into multiset rewrite rules.

Lemma 1. Let P be a well-formed ground process. We have that traces pi (P ) = hide(filter (traces msr ( P ))).

The proof is given in Appendix B. Our main theorem can now be proven by applying Lemma 1, Proposition 2 and Proposition 1.

Proof of Theorem 1.

traces pi (P ) ϕ ⇔ hide(filter (traces msr ( P ))) ϕ (by Lemma 1)

⇔ filter (traces msr ( P )) ϕ (by Proposition 2)

⇔ traces msr ( P ) ϕ (by Proposition 1)

Case studies and dedicated heuristics

In the following we will briefly overview some case studies we performed. These case studies include a simple security API similar to PKCS#11 [START_REF]PKCS #11: Cryptographic Token Interface Standard[END_REF], the Yubikey security token, the optimistic contract signing protocol by Garay, Jakobsson and MacKenzie (GJM) [START_REF] Garay | Abuse-free optimistic contract signing[END_REF] and a few other examples discussed in Arapinis et al. [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF] and Mödersheim [START_REF] Mödersheim | Abstraction by set-membership: verifying security protocols and web services with databases[END_REF]. We do not detail all the formal models of the protocols and properties that we studied, and sometimes present slightly simplified versions. All files of our prototype implementation and our case studies are available at http://sapic.gforge.inria.fr/ In addition to the syntax of the calculus described in Section 3 our tool also allows the user to fall back to labelled msr rules inside of processes. The treatment of this extension is described in the conference version [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]. Having an access to the underlying formalism may sometimes be convenient, but as we do not use it in the examples described in this paper we chose to omit this feature to clarify the presentation. Related work complements these case studies with an analysis of a more complete model of PKCS#11 [START_REF] Künnemann | Automated backward analysis of PKCS#[END_REF], and the enhanced authorisation mechanism in the TPM 2.0 [START_REF] Shao | Formal analysis of enhanced authorization in the TPM 2.0[END_REF], as well as an extension of SAPIC that allows for the analysis of stream protocols such as TESLA [START_REF] Rakotonirina | Vérification automatique de protocoles de sécurité avec mémoire globale et boucles[END_REF].

We will also discuss a dedicated heuristics we developed that favours termination of tamarin on msr systems produced by our tool. The results are summarized in Table 1. For each case study we provide the number of typing lemmas that were needed by the tamarin prover and whether manual guidance of the tool was required. In case no manual guidance is required we also give execution times. [START_REF] Künnemann | YubiSecure? Formal security analysis results for the Yubikey and YubiHSM[END_REF][START_REF]The YubiKey Manual -Usage, configuration and introduction of basic concepts (Version 2.2)[END_REF] 5 no no GJM protocol [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF][START_REF] Garay | Abuse-free optimistic contract signing[END_REF] 0 yes (11, 5s) yes (9, 9s) Mödersheim's example [START_REF] Mödersheim | Abstraction by set-membership: verifying security protocols and web services with databases[END_REF] 0 no yes(0, 8s) Security Device [

Security API à la PKCS#11

This example illustrates how our modelling might be useful for the analysis of Security APIs in the style of the PKCS#11 standard [START_REF]PKCS #11: Cryptographic Token Interface Standard[END_REF]. Indeed, Künnemann [START_REF] Künnemann | Automated backward analysis of PKCS#[END_REF] used our tool to perform an automated analysis of PKCS#11 v2.20. In addition to the processes presented in the running example in Section 3 the actual case study models the following two operations: (i) encryption: given a handle and a plaintext, the user can request an encryption under the key the handle points to. (ii) unwrap given a ciphertext senc(k 2 , k 1 ), and a handle h 1 , the user can request the ciphertext to be unwrapped, i.e. decrypted, under the key pointed to by h 1 . If decryption is successful, the result is stored on the device, and a handle pointing to k 2 is returned. Moreover, contrary to the running example, at creation time keys are assigned the attribute 'init', from which they can move to either 'wrap', or 'unwrap'. Furthermore, the database maps handles to pairs of keys and attributes. See the following snippet: in( ' set_dec ' , h ); lock h;

lookup h as v in if att (v)=' init ' then event DecKey(h,key(v)); insert h, key(v) , 'dec' ; unlock h
Note that, in contrast to the running example, it is necessary to encapsulate the state changes between lock and unlock. Otherwise an adversary can stop the execution after line 3, set the attribute to 'wrap' in a concurrent process and produce a wrapping. After resuming operation at line 4, he can set the key's attribute to 'dec', even though the attribute is set to 'wrap'. Hence, the attacker is allowed to decrypt the wrapping he has produced and can obtain the key. Such subtleties can produce attacks that our modeling allows to detect. If locking is handled correctly, we show secrecy of keys produced on the device, proving the property introduced in Example 6. If locks are removed the attack described before is found. The conference version [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] mistakenly reported that the verification of this example was fully automated, but the verified model contained a typo, where P set_wrap wrote to attr , h rather than att, h , effectively disabling unwrapping altogether. Using the new heuristics, it is again possible to verify this example automatically.

Yubikey

The Yubikey [START_REF]The YubiKey Manual -Usage, configuration and introduction of basic concepts (Version 2.2)[END_REF] is a small hardware device designed to authenticate a user against network-based services. Manufactured by Yubico, a Swedish company, the Yubikey itself is a low cost ($25), thumbsized USB device. In its typical configuration, it generates one-time passwords based on encryptions of a secret value, a running counter and some random values using a unique AES-128 key contained in the device. The Yubikey authentication server accepts a one-time password only if it decrypts under the correct AES key to a valid secret value containing a counter larger than the last counter accepted. The counter is thus a means to prevent replay attacks. To date, over a million Yubikeys have been shipped to more than 50,000 customers including governments, universities and enterprises, e.g. Google, Microsoft and Facebook [START_REF] Yubico | Yubico customer list[END_REF].

The following process P Yubikey models a single Yubikey, as well as its initial configuration, where an entry in the server's database for the public id pid is created. This entry contains a tuple consisting of the Yubikey's secret id, AES key, and an initial counter value. P Yubikey = ν k; ν pid; ν secretid ; insert ' Server ' , pid , secretid , k , 'zero' ; insert 'Yubikey', pid , ('zero'+'one'); event Init (pid , secretid , k); out(pid); !P Plugin | !P ButtonPress Here, the processes !P Plugin and !P ButtonPress model the Yubikey being unplugged and plugged in again (possibly on a different computer), and the emission of the one-time password. We will only discuss P ButtonPress here. When the user presses the button on the Yubikey, the device outputs a one-time password consisting of a counter tc, the secret id secretid and additional randomness npr encrypted using the AES key k. For readability, we leave out events that are only used in helping lemmas as well as message input from the adversary that is included in the model to force him to provide the next counter (which he always can, as it is public). The one-time password senc( secretid, tc, npr , k) can be used to authenticate against a server that shares the same secret key, which we model in the process P Server . The process receives the encrypted one-time password along with the public id pid of a Yubikey and a nonce that is part of the protocol, but is irrelevant for the authentication of the Yubikey on the server. The server then looks up the secret id and the AES key associated to the public id, as well as the last recorded counter value otc. If the key and secret id used in the request match the values retrieved from the database, then the event Login(pid , k, tc) is logged, marking a successful login of the Yubikey pid with key k for the counter value tc. Afterwards, the old tuple secretid , k, otc is replaced by secretid , k, tc , to update the latest counter value received. Note that, in our modelling, the server keeps one lock per public id, which means that it is possible to have several active instances of the server thread in parallel as long as all requests concern different Yubikeys.

P
P Server = ! in( pid ,
We model the counter as a multiset only consisting of the symbols "one" and "zero". The multiplicity of 'one' in the multiset is the value of the counter. A counter value is considered smaller than another one, if the first multiset is included in the second, therefore

φ smaller (x 1 , x 2 ) := ∃z.x 1 + z = x 2
The process we analyse models a single authentication server (that may run arbitrarily many threads) and an arbitrary number of Yubikeys, i. e., P Server | !P Yubikey . Among other properties, we show by the means of an injective correspondence property that an attacker that controls the network cannot perform replay attacks, and that each successful login was preceded by a user "pressing the button", formally:

∀ pid , k, x, t 2 .Login(pid , k , x )@t 2 ⇒ ∃sid , t 1 .YubiPress(pid , sid , k , x )@t 1 ∧ t 1 t 2 ∧ ∀t 3 .Login(pid , k , x )@t 3 ⇒ t 3 . = t 2
Besides injective correspondence, we show the absence of replay attacks and the property that a successful login invalidates previously emitted one-time passwords. All three properties follow more or less directly from a stronger invariant, which itself can be proven in 516 steps. To find theses steps, tamarin needs some additional human guidance (17 steps), which can be provided using the interactive mode. This mode still allows the user to complement his manual efforts with automated backward search. The example files contain the modelling in our calculus, the complete proof, and the manual part of the proof which can be verified by tamarin without interaction. Our analysis makes three simplifications: First, in P Server , we use pattern matching instead of decryption as demonstrated in the process P dec we introduced in Section 3. Second, we omit the CRC checksum and the time-stamp that are part of the one-time password in the actual protocol, since they do not add to the security of the protocol in the symbolic setting. Third, the Yubikey has actually two counters instead of one, a session counter, and a token counter. We treat the session and token counter on the Yubikey as a single value, which we justify by the fact that the Yubikey either increases the session counter and resets the token counter, or increases only the token counter, thereby implementing a complete lexicographical order on the pair (session counter , token counter ).

A similar analysis has already been performed by Künnemann and Steel, using tamarin's multiset rewriting calculus [START_REF] Künnemann | YubiSecure? Formal security analysis results for the Yubikey and YubiHSM[END_REF]. However, the model in our new calculus is more fine-grained and we believe more readable. Security-relevant operations like locking and tests on state are written out in detail, resulting in a model that is closer to the real-life operation of such a device. The modeling of the Yubikey takes approximately 38 lines in our calculus, which translates to 49 multiset rewrite rules. The model of [START_REF] Künnemann | YubiSecure? Formal security analysis results for the Yubikey and YubiHSM[END_REF] contains only four rules, but they are quite complicated, resulting in 23 lines of code. More importantly, the gap between their model and the actual Yubikey protocol is larger -in our calculus, it becomes clear that the server can treat multiple authentication requests in parallel, as long as they do not claim to stem from the same Yubikey. An implementation on the basis of the model from Künnemann and Steel would need to implement a global lock accessible to the authentication server and all Yubikeys. This is however unrealistic, since the Yubikeys may be used at different places around the world, making it unlikely that there exist means of direct communication between them. While a server-side global lock might be conceivable (albeit impractical for performance reasons), a real global lock could not be implemented for the Yubikey as deployed.

The GJM contract signing protocol [16]

A contract signing protocol allows two parties to sign a contract in a fair way: none of the participants should be bound to the contract without the other participant being bound as well. A straightforward solution is to use a trusted party that collects both signatures on the contract and then sends the signed contracts to each of the participants. Optimistic protocols have been designed to avoid the use of a trusted party whenever possible (optimizing efficiency, and avoiding the potential cost of a trusted party). In these protocols the parties first try to simply exchange the signed contracts; in case of failure, or cheating behavior of one of the parties, the trusted party can be contacted. Depending on the situation, the trusted party may either abort the contract, or resolve it. In case of an abort decision the protocol ensures that none of the parties obtains a signed contract, while in case of a resolve the protocol ensures that both participants obtain the signed contract. For this the trusted party needs to maintain a database with the current status of all contracts (aborted, resolved, or no decision has been taken). In our calculus the status information is naturally modelled using our insert and lookup constructs. The use of locks is also crucial here to avoid the status to be changed between a lookup and an insert.

This protocol was also studied by Arapinis et al. [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF]. They showed the crucial property that a same contract can never be both aborted and resolved. However, due to the fact that StatVerif only supports a finite number of memory cells, they have shown this property for a single contract and provide a manual proof to lift the result to an unbounded number of contracts. We directly prove this property for an unbounded number of contracts.

Further Case Studies

We investigated the case study presented by Mödersheim [START_REF] Mödersheim | Abstraction by set-membership: verifying security protocols and web services with databases[END_REF], a key-server example, as well as a simple security device which served as an example for StatVerif [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF]:the device is initialized once, either to left or right. Later on, it accepts pairs of encryptions and decrypts either the left component of the pair or the right component, but not both. As the input language of StatVerif is very similar to ours their model could be easily adapted to our tool. In fact, we were able to remove the restriction to a single security device. Finally, we also illustrate the tool's ability to analyze classical security protocols by analyzing the Needham Schroeder Lowe protocol [START_REF] Lowe | Breaking and fixing the Needham-Schroeder public-key protocol using FDR[END_REF].

Heuristics

In order to improve our results on the case studies presented in the conference version [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], we have altered the heuristics of the tamarin-prover. We make use of the a priori knowledge that the msr system is an output of our translation. These heuristics can be switched on using the command line switch --heuristic=p and alter the ranking of goals which is used to determine the next step in an automatic proof. The heuristics have no bearing on the correctness of tamarin, but often improve automation of the verification procedure, as our case studies show (see Table 1). These heuristics also allowed an automated proof of the PKCS#11 case study [START_REF] Künnemann | Automated backward analysis of PKCS#[END_REF].

The main goal is to avoid a loop in the resolution procedure, so our approach is conservative in that we only prioritize goals that do not cause other prioritized goals to appear, unless the protocol has been annotated to do that. The heuristic alters tamarin's standard "smart" heuristic in the following way: statefacts are resolved right away. As state-goals can only be solved by exactly one rule (except for message transmission), and state predicates in the premise of a rule are indexed with a position that is a prefix of the position of the state predicate in the conclusion, loops are impossible and case distinctions rare. Moreover, tamarin precomputes chains and is hence often able to resolve the chain until state 0 in one step. Goals for Unlock-actions are solved right away. As these goals are produced by α lock , they identify the correct unlock using the annotations introduced in Definition 12. By reformulating α lock (compared to the conference article), we were able to avoid the repeated application of this rule. We removed the prioritisation of goals for adversarial deduction of fresh values, as it is counter-productive in the case of handles. They are fresh values that can usually be derived from protocol output, so a case distinction on all possible ways of deriving them is sometimes misleading. Another addition prioritizes goals for Insert-actions when the first element of the key is prefixed "F_", so the user can prioritize the reasoning on lookups to keys like F_database , p . Adversarial deduction for fresh values can be prioritized in the same way, using "L_" instead of "F_" achieves deprioritisation.

Proof effort

A comparison between the effort needed to derive a proof for a protocol in our calculus and a protocol modelled via multiset rewrite rules is only sound when both model the same thing. Whenever the direct encoding is simplified, e. g., in the Yubikey model, the proof is obviously simpler, but on the other hand, as we have already discussed in Section 7.2, it may be oversimplified. Whenever models were relatively close, our experiments suggested that the same kind of lemmas are needed. In particular for the GJM contract signing protocol, the simple security device and the Needham-Schroeder-Lowe protocol, the lemmas were literally the same. This suggests that these helping lemmas prove properties beyond the level of representation, i.e., properties of the protocol itself.

Our dedicated heuristics discussed in the previous section also improve termination. One may note that tamarin also includes several heuristics that can be chosen from and combined in several ways to help termination. Some of the case studies, e.g., the group protocols analysed in [START_REF] Schmidt | Automated verification of group key agreement protocols[END_REF], also required the development of dedicated heuristics. Our heuristics benefit from the fact that the msr rules are generated and, therefore, are more restricted than the arbitrary msr rules that may be given to tamarin using a direct msr rule modelling.

When these heuristics fail, or the user wishes to inspect the proof, tamarin's interactive mode allow manual inspection and selection of the proof goals that are chosen at each step. To make use of this, in addition to the working of the tamarin interactive mode, a basic understanding of our translation (but not of the correctness proof) is necessary. A tight integration of SAPIC into tamarin would surely aid in this regard, but requires significant engineering effort. Such an integration could additionally provide information given by the process description. Relations between locks, lookup and inserts could be highlighted and protocol roles (often defined as abbreviations by protocol designers) distinguished.

For protocols which have complicated control flow or structure (e. g. group protocols [START_REF] Schmidt | Automated verification of group key agreement protocols[END_REF]), a direct encoding may actually be better suited. We provide a mechanism for embedding labelled msr rules directly inside processes (described in the conference version [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]), which may useful is some circumstances, and such a mixed model might sometimes give the user "the best of the two approaches".

Conclusion

We present a process calculus which extends the applied pi calculus with constructs for accessing a global, shared memory together with an encoding of this calculus in labelled msr rules which enables automated verification using the tamarin prover as a backend. Our prototype verification tool, automating this translation, has been successfully used to analyze several case studies. As future work we plan to increase the degree of automation of the tool by automatically generating helping lemmas. To achieve this goal we can exploit the fact that we generate the msr rules, and hence control their form. We also plan to use the tool for more complex case studies, specifically contract signing protocols.

Appendix

A. Correctness of tamarin's solution procedure for translated rules The multiset rewrite system produced by our translation for a well-formed process P could actually contain rewrite rules that are not valid with respect to Definition 4, because they violate the third condition, which is:

for each l -[ a ]→ r ∈ R ∈ E ginsts(l -[ a ]→ r) we have that ∩ r = E r names(r ) ∩ FN ⊆ ∩ l = E l names(l ) ∩ FN .
This does not hold for rules in P =p where p is the position of the lookup-operator. The right handside of this rule can be instantiated such that, assuming the variable bound by the lookup is named v, this variable v is substituted by a names that does not appear on the left-hand side. In the following, we will show that the results from [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF] still hold. In practice, this means that the tamarin-prover can be used for verification, despite the fact that it outputs well-formedness errors for each rule that is a translation of a lock.

First we give some intuition. The third condition assures that rules do not introduce new names on the right-hand side of rules, i. e., all new names originate from the FRESH rule. While the condition is indeed violated by the appearance of v, v cannot be instantiated to a new name, since α in guarantees that each value v retrieved in a lookup has appeared in an insert before. We show that one could as well introduce a dummy fact !Dum(v) at the left-hand side of the rewrite rule corresponding to the lookup, and consequently at the right-hand side of the rewrite rule corresponding to the previous insert, which must exist in each trace satisfying α in . This modified translation would not violate the third condition anymore, but as these dummy facts constitute overhead and rather a proof argument than a real necessity, we will use the modified translation to show that the actual translation is correct despite the warning.

We will introduce some notation first. the exception of two cases, P = lookup M as v in P else Q and P = insert s, t; P , where it is defined as follows:

lookup M as v in P else Q, p, x D = {[state p (x), !Dum(v)] -[ IsIn(M, v) ]→ [state p•1 ( M , v)], [state p (x)] -[ IsNotSet(M ) ]→ [state p•2 (x)]} ∪ P, p • 1, (x, v) D ∪ Q, p • 2, x D insert s, t; P, p, x D = { [state p (x)] -[ Insert(s, t) ]→ [state p•1 (x), !Dum(t)] } ∪ P, p • 1, x D
The only difference between P and P D is therefore, that P D produces a permanent fact !Dum for every value v that appears in an action insert(k, v), which is a premise to every rule instance with an action IsIn(k , v). We see that P D contains now only valid multiset rewrite rules.

In the following, we would like to show that the tamarin-prover's solution algorithm is correct for P . To this end, we make use of the proof of correctness of tamarin as presented in Benedikt Schmidt's Ph.D. thesis [START_REF] Schmidt | Formal Analysis of Key-Exchange Protocols and Physical Protocols[END_REF]. We will refer to Lemmas, Theorems and Corollaries in this work by their numbers. We will use the notation of this work, to make it easier to the reader to compare our statements against the statements there. In particular, trace(execs(R)) is traces msr (R) in our notation. Again, we give some intuition first. The crucial step in the correctness proof is Lemma A.12, as the third condition is used only once in the overall correctness proof, namely in Lemma A.14 (which is used by Lemma A.12). In this step the switch is made from dependency graphs to normalized dependency graphs, which enforce normalized message deduction, e. g., that messages are not deduced twice, that a message deduced is not unnecessarily deconstructed, and that rule instances are normal with respect a rewriting system that simplifies message deduction for Diffie-Hellman groups (RDH e ). Normalized dependency graphs are much more constrained than dependency graphs and thus necessary for efficient backward analysis. Lemma A.12 shows that normal dependency graphs have the same observable traces as traces generated using multiset rewriting. For this step it is necessary to show that all accessible factors (or their inverses) that appear in the normalized dependency graph are known to the adversary (Lemma A.14). In general, if the third condition is not met, a new factor could appear 'out of nowhere', when the right-hand side of the rule is instantiated. However, as Lemma A.14 holds for the dummy translation, it holds for the actual translation, too, given a trace that satisfies α in . This will be detailed below, but first we recall the overall proof structure.

Formally, we have to show that:

Lemma 2. For all well-formed process P and guarded trace properties φ, trace(execs( P ∪ MD) DHe ¬α in ∨ φ if and only if trace(ndgraphs( P )) ACC ¬α in ∨ φ.

Proof. The proof proceeds similar to the proof to Theorem 3.27. We refer to results in [START_REF] Schmidt | Formal Analysis of Key-Exchange Protocols and Physical Protocols[END_REF], whenever their proofs apply despite the fact that the rules in P do not satisfy the third condition of multiset rewrite rules. It is only in Lemma A.12 where the third condition is used: The proof to this lemma applies Lemma A.14, which says that all factors (or their inverses) are known to the adversary. We will quote Lemma A.14 here: Lemma 3 (Lemma A.14 in [START_REF] Schmidt | Formal Analysis of Key-Exchange Protocols and Physical Protocols[END_REF]). For all ndg ∈ ndgraphs(P ), conclusions (i, u) in ndg with conclusion fact f and terms t ∈ afactors(f ), there is a conclusion (j, v) in ndg with j < i and conclusion fact

K d (m) such that m ∈ ACC { t, (t -1 ) ↓ RBPe }.
If there is ndg ∈ ndgraphs( P ), such that trace(ndg) ACC α in , then

trace(ndgraphs( P )) ACC ¬α in ∨ φ ⇔∀ndg ∈ ndgraphs( P ) s. t. trace(ndg) ACC α in trace(ndg) ACC φ
Since for the empty trace, [] ACC α in , we only have to show that Lemma A.14 holds for ndg ∈ ndgraphs( P ), such that trace(ndg) ACC α in .

For every ndg ∈ ndgraphs( P ), such that trace(ndg) ACC α in , there is a trace equivalent ndg ∈ ndgraphs( P D ), since the only difference between P and P D lies in the dummy conclusion and premises, and α in requires that any v in an action IsIn(u, v) appeared previously in an action Insert(u, v) (equivalence modulo ACC ). Therefore, ndg has the same K d -conclusions ndg has, and every conclusion in ndg is a conclusion in ndg .

We have that Lemma A.14 holds for P D , since all rules generated in this translation are valid multiset rewrite rules. Therefore, Lemma A.14 holds for all ndg ∈ ndgraphs( P ), such that trace(ndg) ACC α in , too, concluding the proof by showing the marked (*) step.

B. Proof of Lemma 1

We will first show a few useful preliminary lemmas. Then we will show each of the two directions of Lemma 1.

B.1. Preliminary definitions and lemmas

In order to prove Lemma 1, we need a few additional lemmas. We say that a set of traces Tr is prefix closed if for all tr ∈ Tr and for all tr which is a prefix of tr we have that tr ∈ Tr .

Lemma 4 (filter is prefix-closed). Let Tr be a set of traces. If Tr is prefix closed then filter (Tr ) is prefix closed as well.

Proof. It is sufficient to show that for any trace tr = tr •a we have that if ∀θ.(tr , θ) α then ∀θ.(tr , θ) α. This can be shown by inspecting each of the conjuncts of α.

We next show that the translation with dummy facts defined in Definition 18 produces the same executions as P , excluding executions not consistent with the axioms. For this we define the function d which removes any dummy fact from an execution, i.e.,

d(∅

F 1 -→ S 1 F 2 -→ . . . Fn -→ S n ) = ∅ F 1 -→ S 1 F 2 -→ . . . Fn -→ S n
where S i = S i \ # ∪ t∈T !Dum(t). To state this property we lift the function filter (Definition 16) from traces to executions, i.e. for a set of msr executions Ex we define

filter (Ex) = {∅ F 1 -→ S 1 F 2 -→ . . . Fn -→ S n ∈ Ex | [F 1 , . . . , F n ] α}
where α is defined in Definition 15.

Lemma 5. Given a ground process P , we have that filter (exec msr ( P )) = filter (d(exec msr ( P D ∪ MD)))

Proof. The only rules in P D that differ from P are translations of insert and lookup. The first one only adds a permanent fact, which by the definition of d, is removed when applying d. The second one requires a fact !Dum(t), whenever the rule is instantiated such the actions equals IsIn(s, t) for some s. Since the translation is otherwise the same, we have that filter (d(exec msr ( P D ∪ MD))) ⊆ filter (exec msr ( P ))

For any execution in filter (d(exec msr ( p ∪ MD))) and any action IsIn(s, t) in this execution, there is an earlier action Insert(s , t ) such that s = s and t = t , as otherwise α in would not hold. Therefore the same execution is part of filter (d(exec msr ( p D ∪ MD))), as this means that whenever !Dum(t) is in the premise, !Dum(t ) for t = t has previously appeared in the conclusion. Since it is a permanent fact, it has not disappeared and therefore filter (d(exec msr ( P D ∪ MD))) ⊇ filter (exec msr ( P )) Lemma 6. Let P be a ground process and ∅

F 1 -→ S 1 F 2 -→ . . . Fn -→ S n ∈ filter (exec msr ( P )). For all 1 ≤ i ≤ n, if Fr(a) ∈ S i and F (t 1 , . . . , t k ) ∈ S i for any F ∈ Σ fact \ { Fr }, then a ∈ ∩ t= E t names(t ), for any t ∈ {t 1 , . . . , t k }.
Proof. The translation with the dummy fact introduced in Appendix A will make this proof easier as for P D ∪ MD, we have that the third condition of Definition 4 holds, namely,

∀l -[ a ]→ r ∈ E ginsts(l -[ a ]→ r) : ∩ r = E r names(r ) ∩ FN ⊆ ∩ l = E l names(l ) ∩ FN (1)
We will show that the statement holds for all ∅

F 1 -→ S 1 F 2 -→ . . .

Fn

-→ S n ∈ filter (exec msr ( P D ∪ MD)), which implies the claim by Lemma 5. We proceed by induction on n, the length of the execution.

-Base case, n = 0. We have that S 0 = ∅ and therefore the statement holds trivially.

-Inductive case, n ≥ 1. We distinguish two cases.

1. A rule that is not FRESH was applied and there is a fact F (t 1 , . . . , t k ) ∈ S n , such that F (t 1 , . . . , t k ) / ∈ S n-1 , and Fr(a) ∈ S n such that a ∈ ∩ t i = E t names(t ) for some t i . (If there are no such F (t 1 , . . . , t k ) and Fr(a) we immediately conclude by induction hypothesis.) By Equation 1, a ∈ t j for some F (t 1 , . . . , t l ) ∈ S n-1 . Since FRESH is the only rule that adds a Fr-fact and Fr(a) ∈ S n , it must be that Fr(a) ∈ S n-1 , contradicting the induction hypothesis. Therefore this case is not possible. 2. The rule FRESH was applied, i. e., Fr(a) ∈ S n and Fr(a) / ∈ S n-1 . If there is no a ∈ ∩ t i = E t names(t ) for some t i , and F (t 1 , . . . , t k ) ∈ S n , then we conclude by induction hypothesis. Otherwise, if there is such a F (t 1 , . . . , t k ) ∈ S n , then, by Equation 1, a ∈ t j for some F (t 1 , . . . , t l ) ∈ S i for i < n. We construct a contradiction to the induction hypothesis by taking the prefix of the execution up to i and appending the instantiation of the FRESH rule to its end. Since d(exec msr ( P D ∪ MD)) is prefix closed by Lemma 4 we have that ∅

F 1 -→ S 1 F 2 -→ . . . F i -→ S i ∈ filter (d(exec msr ( P D ∪ MD))
). Moreover as rule FRESH was applied adding Fr(a) ∈ S n it is also possible to apply the same instance of FRESH to the prefix (by Definition 6) and therefore

∅ F 1 -→ S 1 F 2 -→ . . . F i -→ S i -→ S i ∪ { Fr(a) } ∈ filter (d(exec msr ( P D ∪ MD)))
contradicting the induction hypothesis. Lemma 7. For any frame ν ñ.σ, t ∈ M and a ∈ FN , if a ∈ st(t), a ∈ st(σ) and ν ñ.σ t, then ν ñ, a.σ t.

Proof. In [1, Proposition 1] it is shown that ν ñ.σ t if and only if ∃M.fn(M ) ∩ ñ = ∅ and M σ = E t. Define M as M renaming a to some fresh name, i.e., not appearing in ñ, σ, t. As a ∈ st(σ, t) and the fact that equational theories are closed under bijective renaming of names we have that M σ = E t and fn(M ) ∩ (ñ, a) = ∅. Hence ν ñ, a.σ t.

Lemma 8. Let P be a ground process and ∅

F 1 -→ S 1 F 2 -→ . . . Fn -→ S n ∈ filter (exec msr ( P )). Let ñ = {a : fresh | ProtoNonce(a) ∈ 1≤j≤n F j }, {t 1 , . . . , t m } = {t | Out(t) ∈ 1≤j≤n S j }. Let σ = { t 1 / x 1 , . . . , tm / xm }. We have that 1. if !K(t) ∈ S n then ν ñ.σ t; 2. if ν ñ.σ t then there exists S such that -∅ F 1 -→ S 1 F 2 -→ . . . Fn -→ S n -→ * S ∈ filter (exec msr E ( P )), -!K(t) ∈ E S and -S n → * R S for R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }.
Proof. We prove both items separately.

1. The proof proceeds by induction on n, the number of steps of the execution.

Base case: n=0. This case trivially holds as S n = ∅.

Inductive case: n>0. By induction we suppose that if !K(t) ∈ S n-1 then ν ñ .σ t where ñ , σ are defined in a similar way as ñ, σ but for the execution of size n -1. We proceed by case analysis on the rule used to extend the execution.

-MDOUT. Suppose that Out(u) -[ ]→!K(u) ∈ ginsts(MDOUT) is the rule used to extend the execution. Hence Out(u) ∈ S n-1 and by definition of σ there exists x such that xσ = u.

We can apply deduction rule DFRAME and conclude that ν ñ.σ u. If !K(t) ∈ S n and t = u we conclude by induction hypothesis as ñ = ñ , σ = σ . -MDPUB. Suppose that -[ ]→ K(a : pub) ∈ ginsts(MDPUB) is the rule used to extend the execution. As names of sort pub are never added to ñ we can apply deduction rule DNAME and conclude that ν ñ.σ a. If K(t) ∈ S n and t = a we conclude by induction hypothesis as ñ = ñ , σ = σ . -MDFRESH. Suppose that Fr(a : fresh) -[ ]→ K(a : fresh) ∈ ginsts(MDFRESH) is the rule used to extend the execution. By definition of an execution we have that Fr(a : fresh) = (S j+1 \ S j ) for any j = n -1. Hence n ∈ ñ. We can apply deduction rule DNAME and conclude that ν ñ.σ a. If !K(t) ∈ S n and t = a we conclude by induction hypothesis as

ñ = ñ , σ = σ . -MDAPPL. Suppose that !K(t 1 ), . . . , !K(t k ) -[ ]→!K(u) ∈ ginsts(MDAPPL)
is the rule used to extend the execution. We have that K(t 1 ), . . . , K(t k ) ∈ S n-1 and u = E f (t 1 , . . . , t k ). By induction hypothesis, ν ñ .σ t i for 1 ≤ i ≤ k. As ñ = ñ , σ = σ we have that ν ñ.σ t i for 1 ≤ i ≤ k. We can apply deduction rule DAPPL and conclude that ν ñ.σ f (t 1 , . . . , t k ). Hence, ν ñ.σ u by rule DEQ. If K(t) ∈ S n and t = f (t 1 , . . . , t k ) we conclude by induction hypothesis as ñ = ñ , σ = σ .

-If S n-1

ProtoNonce(a)

---------→S n we have that Fr(a) ∈ S n-1 . By Lemma 6, we obtain that if !K(t) ∈ S n-1 then there exist t and σ such that t = E t, σ = E σ and a ∈ st(t ) and a ∈ st(σ ). For each !K(u) ∈ S n there is !K(u) ∈ S n-1 , and by induction hypothesis, ν ñ .σ u. By Lemma 7 and the fact that σ = E σ we have that ν ñ , a.σ u. As ñ , a = ñ and σ = σ we conclude.

-All other rules do neither add !K( )-facts nor do they change ñ and may only extend σ.

Therefore we conclude by the induction hypothesis.

2. Suppose that ν ñ.σ t. We proceed by induction on the proof tree witnessing ν ñ.σ t.

Base case. The proof tree consists of a single node. In this case one of the deduction rules DNAME or DFRAME has been applied.

-DNAME. We have that t ∈ ñ. Inductive case. We proceed by case distinction on the last deduction rule which was applied.

-DAPPL. In this case t = f (t 1 , . . . , t k ), such that f ∈ Σ k and ν ñr.σ t i for every i ∈ {1, . . . , k}. Applying the induction hypothesis we obtain that there are k transition sequences S n → * R S i for 1 ≤ i ≤ k which extend the execution such that t i ∈ S i . All of them only add !K facts which are persistent facts. If any two of these extensions remove the same Out(t)fact or the same Fr(a)-fact it also adds the persistent fact !K(t), respectively !K(a), and we simply remove the second occurrence of the transition. Therefore, applying the same rules as for the transitions S n → * S i (and removing duplicate rules) we have that S n → * S and !K(t 1 ), . . . , !K(t k ) ∈ S . Applying rule MDAPPL we conclude.

-DEQ. By induction hypothesis there exists S as required with !K(t ) ∈ E S and t = E t which allows us to immediately conclude that !K(t) ∈ E S.

Lemma 9. If ν ñ.σ t, ñ = E ñ , σ = E σ and t = E t , then ν ñ .σ t .
Proof. Assume ν ñ.σ t. Since an application of DEQ can be appended to the leafs of its proof tree, we have ν ñ.σ t. Since DEQ can be applied to its root, we have ν ñ.σ t . Since ñ, ñ consist only of names, ñ = ñ and thus ν ñ .σ t . B.2. Proof that traces pi (P ) ⊆ hide(filter (traces msr ( P )))

To state our next lemma we need two additional definitions.

Definition 19. Let P be a well-formed ground process and p t a position in P . We define the set of multiset rewrite rules generated for position p t of P , denoted P =pt as follows: 18.

P =pt := P, [], [] =pt where •, •, • =pt is defined in Figure
The next definition will be useful to state that for a process P every fact of the form state p ( t) in a multiset rewrite execution of P corresponds to an active process in the execution of P which is an instance of the subprocess P | p . Definition 20. Let P be a ground process, P be a multiset of processes and S a multiset of ground facts. We write P ↔ P S if there exists a bijection between P and the multiset {state p ( t) | ∃p, t. state p ( t) ∈ # S} # such that whenever Q ∈ # P is mapped to state p ( t) ∈ # S we have that 1. P | p τ = Qρ, for some substitution τ and some bijective renaming ρ of fresh, but not bound names in Q, and 2. ∃ri ∈ E ginsts( P =p ). state p ( t) ∈ prems(ri).

0, p, x =pt = { [state p (x)] → [] } p ? =pt P | Q, p, x =pt = { [state p (x)] → [state p•1 (x), state p•2 (x)] } p ? =pt ∪ P, p • 1, x =pt ∪ Q, p • 2, x =pt !P, p, x =pt = { [!state p (x)] → [state p•1 (x)] } p ? =pt ∪ P, p • 1, x =pt νa; P, p, x =pt = { [state p (x), Fr(n a : fresh)] -[ ProtoNonce(n a : fresh) ]→ [state p•1 (x, n a : fresh)] } p ? =pt ∪ P, p • 1, (x, n a : fresh) =pt Out(M, N ); P, p, x =pt = { [state p (x), In(M )] -[ InEvent(M ) ]→ [Out(N ), state p•1 (x)], [state p (x)] → [Msg(M, N ), state semi p (x)], [state semi p (x), Ack(M, N )] → [state p•1 (x)] } p ? =pt ∪ P, p • 1, x =pt In(M, N ); P, p, x =pt = { [state p (x), In( M, N )] -[ InEvent( M, N ) ]→ [state p•1 (x ∪ vars(N ))], [state p (x), Msg(M, N )] → [state p•1 (x ∪ vars(N )), Ack(M, N )] } p ? =pt ∪ P, p • 1, x ∪ vars(N ) =pt if pr (M 1 , . . . , M k ) then P else Q, p, x =pt = { [state p (x)] -[ Pred pr (M 1 , . . . , M k ) ]→ [state p•1 (x)], [state p (x)] -[ Pred_not pr (M 1 , . . . , M k ) ]→ [state p•2 (x)] } p ? =pt ∪ P, p • 1, x =pt ∪ Q, p • 2, x =pt event F ; P, p, x =pt = { [state p (x)] -[ Event(), F ]→ [state p•1 (x)] } p ? =pt ∪ P, p • 1, x =pt insert s, t; P, p, x =pt = { [state p (x)] -[ Insert(s, t) ]→ [state p•1 (x)] } p ? =pt ∪ P, p • 1, x =pt delete s; P, p, x =pt = { [state p (x)] -[ Delete(s) ]→ [state p•1 (x)] } p ? =pt ∪ P, p • 1, x =pt lookup M as v in P else Q, p, x =pt = { [state p (x)] -[ IsIn(M, v) ]→ [state p•1 ( M , v)], [state p (x)] -[ IsNotSet(M ) ]→ [state p•2 (x)] } p ? =pt ∪ P, p • 1, (x, v) =pt ∪ Q, p • 2, x =pt lock l s; P, p, x =pt = { [Fr(lock l ), state p (x)] -[ Lock(lock l , s) ]→ [state p•1 (x, lock l )] } p ? =pt ∪ P, p • 1, x =pt unlock l s; P, p, x =pt = { [state p (x)] -[ Unlock(lock l , s) ]→ [state p•1 (x)] } p ? =pt ∪ P, p • 1, x =pt
When P ↔ P S, Q ∈ # P and state p ( t) ∈ # S we also write Q ↔ P state p ( t) if this bijection maps Q to state p ( t). Remark 2. Note that ↔ P has the following properties (by the fact that it defines a bijection between multisets).

-If P 1 ↔ P S 1 and P 2 ↔ P S 2 then P 1 ∪ # P 2 ↔ P S 1 ∪ # S 2 .

-If P 1 ↔ P S 1 and Q ↔ P state p ( t) for Q ∈ P 1 and state p ( t) ∈ S 1 (i.e. Q and state p ( t) are related by the bijection defined by P 1 ↔ P S 1 ) then

P 1 \ # {Q} ↔ P S 1 \ # {state p ( t)}.
We are now ready to prove the first part of Lemma 1, i. e., traces pi (P ) ⊆ hide(filter (traces msr ( P )))

However, as we proceed by induction, we need to strengthen the induction hypothesis and prove the following, stronger lemma. Lemma 10. Let P be a well-formed ground process. If

(E 0 , S 0 , P 0 , σ 0 , L 0 ) E 1 -→ (E 1 , S 1 , P 1 , σ 1 , L 1 ) E 2 -→ . . . En -→ (E n , S n , P n , σ n , L n )
where (E 0 , S 0 , P 0 , σ 0 , L 0 ) = (∅, ∅, ∅, { P }, ∅, ∅) then there are (F 1 , S 1 ), . . . , (F n , S n ) such that

S 0 F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n ∈ exec msr ( P )
and there exists a monotonic, strictly increasing function f :

N n → N n such that f (n) = n , S 0 = ∅,
and for all i ∈ N n

1.

E i = { a | ProtoNonce(a) ∈ 1≤j≤f (i) F j } 2. ∀t ∈ M. S i (t) =      u if ∃j ≤ f (i).Insert(t, u) ∈ F j ∧∀j , u .j < j ≤ f (i) → Insert(t, u ) ∈ E F j ∧ Delete(t) ∈ E F j ⊥ otherwise 3. P i ↔ P S f (i) 4. { xσ i | x ∈ D(σ i ) } # = { t | ∃k ∈ N f (i)-1 .Out(t) ∈ S k+1 \ S k } # 5. L i = E { t | ∃j ≤ f (i), u. Lock(u, t) ∈ E F j ∧ ∀j < k ≤ f (i).Unlock(u, t) ∈ E F k } 6. [F 1 , . . . , F n ] α where α is defined as in Definition 15. 7. ∃k. f (i -1) < k ≤ f (i) and E i = F k and ∪ f (i-1)<j =k≤f (i) F j ⊆ F res
To see that this lemma indeed implies traces pi (P ) ⊆ hide(filter (traces msr ( P ))) note that for every trace [E 1 , . . . , E n ] ∈ traces pi (P ) there exists [F 1 , . . . F n ] ∈ traces msr ( P ) such that, by Condition 6, [F 1 , . . . F n ] ∈ filter (traces msr ( P )) and, by Condition 7, hide([F 1 , . . .

F n ]) = [E 1 , . . . , E n ].
Proof. We proceed by induction over the number of transitions n.

Base Case. For n = 0, we let f (n) = 1 and S 1 be the multiset obtained by using the Rule INIT: Inductive step. Assume the invariant holds for n -1 ≥ 0. We have to show that the lemma holds for n transitions

∅ Init -→ { state [] () } #
(E 0 , S 0 , P 0 , σ 0 , L 0 ) E 1 -→ (E 1 , S 1 , P 1 , σ 1 , L 1 ) E 2 -→ . . . En -→ (E n , S n , P n , σ n , L n )
By induction hypothesis, we have that there exists a monotonically increasing function from N n-1 → N n and an execution

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n ∈ exec msr ( P )
such that Conditions 1 to 7 hold. Let f p be this function and note that n = f p (n -1). Fix a bijection such that P n-1 ↔ P S fp(n-1) . We will abuse notation by writing P ↔ P state p ( t), if this bijection goes from P to state p ( t).

We now proceed by case distinction over the type of transition from (E n-1 , S n-1 , P n-1 , σ n-1 , L n-1 ) to (E n , S n , P n , σ n , L n ). We will (unless stated otherwise) extend the previous execution by a number of steps, say s, from S n to some S n +s , and prove that Conditions 1 to 7 hold for n (since by induction hypothesis, they hold for all i < n) and a function f : N n → N n +s that is defined as follows:

f (i) := f p (i) if i ∈ N n-1 n + s if i = n Case: (E n-1 , S n-1 , P n-1 = P ∪ {0}, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P , σ n-1 , L n-1 )
. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that 0 ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose

ri = [state p ( t)] -[ ]→ [].
We can extend the previous execution by one step using ri , therefore:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n - → P S n +1 ∈ exec msr ( P ) with S n +1 = { S f (n-1) \ {state p ( t) }.
= P n-1 \ # {0}, S f (n) = S f (n-1) \ # { state p ( t) } # , and 0 ↔ P state p ( t) (see Remark 2). Case: (E n-1 , S n-1 , P n-1 = P ∪ {Q|R}, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ {Q, R}, σ n-1 , L n-1 )
. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that Q|R ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ ]→ [state p•1 ( t), state p•2 ( t)]. We can extend the previous execution by one step using ri , therefore: Case:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n - → P S n +1 ∈ exec msr ( P ) with S n +1 = S f (n-1) \ { state p ( t) } # ∪ { state p•1 ( t), state p•2 ( t) } # .
(E n-1 , S n-1 , P n-1 = P ∪ {!Q}, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ {!Q, Q}, σ n-1 , L n-1 )
. Let p and t such that ! i Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state

p ( t)] -[ ]→ [state p ( t), state p•1 ( t)].
We can extend the previous execution by 1 step using ri , therefore: Case:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n (ri) → P S n +1 ∈ exec msr ( P ) with S n +1 = S f (n) ∪ # { state p•1 ( t) } # .
(E n-1 , S in-1 , P n-1 = P ∪ { νa; Q }, σ n-1 , L n-1 ) → (E n-1 ∪ {a }, S in-1 , P ∪ {Q{ a / a }}, σ n-1 , L n-1
) for a fresh a . Let p and t be such that {νa; Q} ↔ P state p ( t). There is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , there is a ri ∈ ginsts( P =p ), ri = [state p ( t), Fr(a : fresh)] -[ ProtoNonce(a : fresh) ]→ [state p•1 ( t, a : fresh)]. Assume there is an i < n such that Fr(a ) ∈ S i . If Fr(a ) ∈ S n , then we can remove the application of the instance of FRESH that added Fr(a ) while still preserving Conditions 1 to 7. If Fr(a ) is consumned at some point, by the definition of P , the transition where it is consumned is annotated either ProtoNonce(a ) or Lock (a , t) for some t. In the last case, we can apply a substitution to the execution that substitutes a by a different fresh name that never appears in ∪ i ≤ n S i . The conditions we have by induction hypothesis hold on this execution, too, since Lock ∈ F res , and therefore Condition 7 is not affected. The first case implies that a ∈ E n-1 , contradicting the assumption that a is fresh with respect to the process execution. Therefore, without loss of generality, the previous execution does not contain an i < n such that Fr(a ) ∈ S i , and we can extend the previous execution by two steps using the FRESH rule and ri , therefore:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n (FRESH) → P S n +1 (ri) → P S n +2 ∈ exec msr ( P ) with S n +1 = S n ∪ # { Fr(a : fresh) } # and S n +2 = S f (n) = S n ∪ # { state p•1 ( t, a : fresh) } # . We define f (i) := f p (i) for i < n and f (n) := f (n -1) + 2.
We now show that Condition 3 holds. As by induction hypothesis νa; Q ↔ P state p•1 ( t) we also have that P | p σ = νa; Qρ for some σ and ρ. Extending ρ with {a → a} it is easy to see from definition of P =p that {Q{ a / a }} ↔ P {state p•1 ( t, a )}. As P n = P n-1 \ # {νa; Q} ∪ # { Q{ a / a } } # , we also immediately obtain that P n ↔ P S f (n) . Since a is fresh, and therefore { a } = E n \ E n-1 , and F n = ProtoNonce(a ), Condition 1 holds. Condition 2, Condition 4, Condition 5, Condition 6 and Condition 7 hold trivially.

Case:

(E n-1 , S n-1 , P n-1 , σ n-1 , L n-1 ) K(t) -→ (E n-1 , S n-1 , P n-1 , σ n-1 , L n-1
). This step requires that νE n-1 .σ n-1 t. From Lemma 8 follows that there is an execution

∅ F 1 -→S 1 F 2 -→ . . . F n --→S n → * S ∈ exec msr E ( P ) such that !K(t) ∈ E S and S n → * R S for R = { MDOUT, MDPUB, MDFRESH, MDAPPL }.
From S, we can go one further step using MDIN, since !K(t) ∈ S:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n --→ P S n - → * R⊂ P S = S n +s-1 K(t)
---→ P S n +s ∈ exec msr ( P )

where S n +s = S ∪ {In(t)}.

From the fact that S f (n-1) Case:

→ * R S f (n) = S,
(E n-1 , S n-1 , P n-1 = P ∪ { out(t, t ); Q }, σ n-1 , L n-1 ) K(t) ---→(E n-1 , S n-1 , P ∪ # { Q }, σ n-1 ∪ { t / x }, L n-1
). This step requires that x is fresh and νE n-1 .σ t. Using Lemma 8, we have that there is an execution

∅ F 1 -→S 1 F 2 -→ . . . F f (n)
---→S f (n-1) → * S ∈ exec msr E ( P ) such that !K(t) ∈ E S and S f (n-1) → * R S for R = { MDOUT, MDPUB, MDFRESH, MDAPPL }. Let p and t such that {out(t, t ); Q} ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. From the definition of P =p , we see that we can choose ri = [state p ( t),

In(t)] -[ InEvent(t) ]→ [Out(t ), state p•1 ( t)].
To apply this rule, we need the fact In(t). Since νE n-1 .σ t, as mentioned before, we can apply Lemma 8. It follows that there is an execution

∅ F 1 -→S 1 F 2 -→ . . . F n --→S n → * S ∈ exec msr E ( P ) such that !K(t) ∈ E S and S n → * R S for R = { MDOUT, MDPUB, MDFRESH, MDAPPL }.
From S, we can now go two steps further, using MDIN and ri :

∅ F 1 -→ P S 1 . . . F n -→ P S n → * R⊂ P S = S n +s-2 K(t) ---→ P S n +s-1 InEvent(t)
------→ P S n +s ∈ exec msr ( P )

where

S n +s-1 = S ∪ # { In(t) } # and S f (n) = S \ # { state p ( t) } ∪ # { Out(t ), state p•1 ( t) }.
Taking k = n + s -1 we immediately obtain that Condition 7 holds. Note first that, since S n → R S, set(S n ) \ { Fr(t), Out(t)|t ∈ M } ⊂ set(S) and set(S) \ { !K(t)|t ∈ M } ⊂ set(S n ). Since P n = P n-1 \ {out(t, t ); Q} ∪ {Q} and {Q} ↔ P {state p•1 ( t)} (by definition of P =p ), we have that P n ↔ P S f (n) , i. e., Condition 3 holds. Condition 4 holds since t was added to σ n-1 and Out(t) added to S f (n-1) . Condition 6 holds since K(t) appears right before InEvent(t). Condition 1, Condition 2, and Condition 5 hold trivially.

Case: (E n-1 , S n-1 , P n-1 = P ∪ {in(t, N ); Q}, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ # { Qθ }, σ n-1 , L n-1 ). This step requires that θ is grounding for N and that νE n-1 .σ n-1 t, N θ . Using Lemma 8, we have that there is an execution

∅ F 1 -→S 1 F 2 -→ . . . F f (n-1)
-----→S f (n-1) → * S ∈ exec msr E ( P ) such that !K(t) ∈ E S and S f (n-1) → * R S for R = { MDOUT, MDPUB, MDFRESH, MDAPPL }. The same holds for N θ. We can combine those executions, by removing duplicate instantiations of FRESH, MDFRESH and MDOUT. (This is possible since !K is persistent.) Let

∅ F 1 -→S 1 F 2 -→ . . . F f (n-1) -----→S f (n-1) → *
R S ∈ exec msr E ( P ) this combined execution, and !K(t), !K(N θ) ∈ E S.

Let p and t be such that, in(t, N ); Q ↔ P state p ( t). By Definition 20 there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. From the definition of P =p and the fact that θ is grounding for N θ, we have state p ( t) in their premise, namely,

ri = [state p ( t), In( t, N θ )] -[ InEvent( t, N θ ) ]→ [state p•1 ( t ∪ (vars(N )θ)].
From S n , we can first apply the above transition S n → * R S, and then, (since !K(t), !K(N θ), state p (x) ∈ S), MDAPPL for the pair constructer, MDIN and ri : ------→ P S n +s-2

∅ F 1 -→ P S 1 . . .
K( t,N θ ) ------→ P S n +s-1 InEvent( t,N θ )
----------→ P S n +s ∈ exec msr ( P )

where

-since S n → R S, S is such that set(S n ) \ { Fr(t), Out(t)|t ∈ M } ⊆ set(S), set(S) \ { !K(t)|t ∈ M } ⊆ set(S n ), and !K(t), !K(N θ) ∈ S -S n +s-2 = S ∪ # { !K( t, N θ ) } # , -S n +s-1 = S ∪ # { In( t, N θ ) } # , -S n +s = S \ # { state p ( t) } ∪ # { state p•1 ( t ∪ (vars(N )θ)) }.
Letting k = n + s -1 we immediately have that Condition 7 holds.

We now show that Condition 3 holds. Since by induction hypothesis, in(t, N ); Q ↔ P state p ( t), we have that P | p τ = in(t, N ); Qρ for some τ and ρ. Therefore we also have that P | p•1 τ = Qρ. Thus (P | p•1 τ )(θρ) = (Qρ)(θρ) = Qθρ. Now it is easy to see from the definition of P =p that {Qθ} ↔ P {state p•1 ( t, (vars(N )θ))}.

Since P n = P n-1 \ # {in(t, N ); Q} ∪ # {Q}, we have that P n ↔ P S f (n) , i. e., Condition 3 holds. Condition 6 holds since K t, N θ ) appears right before InEvent t, N θ ). Condition 1, Condition 2, Condition 4, Condition 5 and Condition 6 hold trivially.

Case: (E, S, P ∪ {out(c, m); Q} ∪ {in(c , N ); R}, σ, L) → (E, S, P ∪ { Q, Rθ }, σ, L). This step requires that θ grounding for N , t = E N θ and c = E c . Let p, p and t, Ñ such that {out(c, m); P } ↔ P state p ( t), {in(c , N ); Q} ↔ P state p ( t ), and there are ri ∈ ginsts( P =p ) and ri ∈ ginsts( P =p ) such that state p ( t) and state p ( t ) are part of their respective premise. From the definition of P =p and the fact that θ is grounding for N , we have:

ri 1 = [state p ( t)] → [Msg(t, N θ), state semi p•1 ( t)] ri 2 = [state p ( t ), Msg(t, N θ)] → [state p •1 ( t ∪ (vars(N )θ)), Ack(t, N θ)] ri 3 = [state semi p ( t), Ack(t, N θ)] → [state p•1 ( t)].
This allows to extend the previous execution by 3 steps: → P S n +s ∈ exec msr ( P )

∅ F 1 -→ P S 1 . . .
where:

-

S n +s-2 = S n \ # { state p ( t) } ∪ # { Msg(t, N θ), state semi p•1 ( t) } # , -S n +s-1 = S n \ # { state p ( t), state p ( t ) }∪ # { state semi p•1 ( t), state p •1 ( t ∪(vars(N )θ)), Ack(t, N θ) } # , -S n +s = S n \ # { state p ( t), state p ( t ) } ∪ # { state p•1 ( t), state p •1 ( t ∪ (vars(N )θ)) }.
We have that Case: ----------→ P S n +1 ∈ exec msr ( P )

P n = P n-1 \ # { out(c, m); Q, in(c , t ); R }∪ # { Q, Rθ } # .
(E n-1 , S n-1 , P n-1 = P ∪ { if pr (t 1 , . . . , t l ) then Q else Q }, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ { Q }, σ n-1 , L n-1
with S n +1 = { S n \ # { state p ( t) } # ∪ # { state p•1 ( t) } # }.
It is left to show that Conditions 1 to 7 hold for n. The last step is labelled F f (n) = Pred pr (t 1 , . . . , t l ). As σ pr t 1 / x 1 , . . . , t l / x l is satisfied, Condition 6 holds, in particular, α pred is not violated. Since Pred pr is reserved, Condition 7 holds as well.

As before, since we have that Case:

P n = P n-1 \ # { if pr (t 1 , . . . , t l ) then Q else Q } ∪ # {Q} and {Q} ↔ {state p•1 ( t,
(E n-1 , S n-1 , P n-1 = P ∪ { if pr (t 1 , . . . , t l ) then Q else Q }, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ { Q }, σ n-1 , L n-1
). This step requires that the predicate σ pr t 1 / x 1 , . . . , t l / x l is not satisfied. This proof step is similar to the previous case, except ri is chosen to be

[state p ( t)] -[ Pred_not pr (t 1 , . . . , t l ) ]→ [state p•2 ( t)].
The condition in α noteq holds since σ pr t 1 / x 1 , . . . , t l / x l is not satisfied, and thus, by definition of the satisfaction relation, ¬σ pr t 1 / x 1 , . . . , t l / x l is satisfied.

Case:

(E n-1 , S n-1 , P n-1 = P ∪ { event(F );Q }, σ n-1 , L n-1 ) F -→(E n-1 , S n-1 , P ∪ { Q }, σ n-1 , L n-1 )
. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that event(F );Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ F, Event() ]→ [state p•1 ( t)]. We can extend the previous execution by one step using ri , therefore: Case: We can extend the previous execution by one step using ri , therefore: α notin : as the Insertaction was added at the last position of the trace, it appears after any InIn or IsNotSet-action and by the semantics of the logic the formula holds.

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n F,Event() ------→ P S n +1 ∈ exec msr ( P ) with S n +1 = S n ) \ # {state p ( t)} ∪ # {state p•1 ( t)}.
(E n-1 , S n-1 , P n-1 = P ∪ { insert t, t ; Q }, σ n-1 , L n-1 ) → (E n-1 , S n = S n-1 [t → t ], P ∪ { Q }, σ n-1 , L n-1
∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n Insert(t,t ) ------→ P S n +1 ∈ exec msr ( P ) with S n +1 = S f (n-1) \ # { state p ( t) } # ∪ # { state p•1 ( t) } # .
Since Case:

P n = P n-1 \ # { insert t, t ; Q } ∪ # { Q } and
(E n-1 , S n-1 , P n-1 = P ∪ { delete t; Q }, σ n-1 , L n-1 ) → (E n-1 , S n = S n-1 [t → ⊥], P ∪ { Q }, σ n-1 , L n-1 )
. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that delete t; Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ Delete(t) ]→ [state p•1 ( t)]. We can extend the previous execution by one step using ri , therefore:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n Delete(t) -----→ P S n +1 ∈ exec msr ( P ) with S n +1 = S f (n-1) \ # {state p ( t)} ∪ # {state p•1 ( t)}.
It is left to show that Conditions 1 to 7 hold for n.

This step is labelled F f (n) = Delete(t), hence Condition 7 holds. Since, by induction hypothesis, Condition 6 holds, i.e., [F 1 , . . . F n ] α, it holds for this step too. In particular, if [F 1 , . . . F n ] α in and [F 1 , . . . F n ] α notin , we also have that [F 1 , . . . F n , F f (n) ] α in and [F 1 , . . . F n , F f (n) ] α notin : as the Insert-action was added at the last position of the trace, it appears after any InIn or IsNotSet-actions and by the semantics of the logic the formula holds.

We now show that Condition 2 holds. We have that S n = S n-1 [t → ⊥] and therefore, for all t = E T t, S n (x) = S n-1 (x). Hence for all such t we have by induction hypothesis that for some u,

∃j ≤ n .Insert(t , u) ∈ F j ∧ ∀j , u .j < j ≤ n → Insert(t , u ) ∈ E F j ∧ Delete(t ) ∈ E F j
As, F n +1 = E Delete(x, u) and, for all u ∈ M, F n +1 = E Insert(x, u ) we also have that

∃j ≤ n + 1.Insert(t , u) ∈ F j ∧ ∀j , u .j < j ≤ n + 1 → Insert(t , u ) ∈ E F j ∧ Delete(t ) ∈ E F j .
For t = E t, the above condition can never be true, because F n +1 = Delete(t) which allows us to conclude that Condition 2 holds.

Since Case:

P n = P n-1 \ # { delete t; Q } ∪ # { Q } and {P } ↔ {state p•1 ( t)} (
(E n-1 , S n-1 , P n-1 = P ∪ { lookup t as x in Q else Q }, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ { Q{ v / x } }, σ n-1 , L n-1
). This step requires that S n-1 (t ) = E v for some t = E t. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that lookup t as v in Q else Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state

p ( t)] -[ IsIn(t, v) ]→ [state p•1 ( t, v)]
. This is possible, since by well-formedness of P , no variable is bound twice. Thus, by definition of the translation, x is not bound by the left-hand side in P =p (i. e., x / ∈ x), and thus x and can be instantiated to v (or anything else). We can extend the previous execution by one step using ri , therefore: This step is labelled F f (n) = IsIn(t, v), hence Condition 7 holds.

∅ F 1 -→ P S 1
From the induction hypothesis, Condition 2, we have that there is a j such that Insert(t, t ) ∈ E F j , j ≤ n and

∀j , u . j < j ≤ n → Insert(t, u ) ∈ E F j ∧ Delete(t) ∈ E F j This can be strengthened, since F f (n) = { IsIn(t, v) }: ∀j , u . j < j ≤ f (n) → Insert(t, u ) ∈ E F j ∧ Delete(t) ∈ E F j
This allows to conclude that Condition 2 holds. From Condition 2 it also follows that Condition 6, in particular α in , holds.

We now show that Condition 3 holds. By induction hypothesis we have that lookup t as x in Q else Q ↔ P state p ( t), and hence P | p τ = (lookup t as x in Q else Q )ρ for some τ and ρ. Therefore, we also have that

P | p•1 τ = Qρ. Thus (P | p•1 τ ){ vρ / x }) = (Qρ){ vρ / x } = Q{ v / x }ρ.
Now it is easy to see from the definition of P =p that {Q{ v / x }} ↔ P {state p•1 ( t, v)}. Since Case:

P n = P n-1 \ # { lookup t as x in Q else Q } ∪ # { Q{ v / x } } we have that P n ↔ P S f (n) , i.
(E n-1 , S n-1 , P n-1 = P ∪ { lookup t as x in Q else Q }, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ { Q }, σ n-1 , L n-1
≤ f (n), u. Insert(t, u) ∈ E F j → ∃j , u .j < j ≤ f (n) ∧ (Insert(t, u ) ∈ E F j ∨ Delete(t) ∈ E F j ) Now suppose that ∃i ≤ f (n), y.Insert(t, y) ∈ E F i )
As there exists an insert, there is a last insert and hence we also have

∃i ≤ f (n), y.Insert(t, y) ∈ E F i ∧ ∀i , y .i < i ≤ f (n) → Insert(t, y ) / ∈ E F i Applying Condition 2 (cf above) we obtain that ∃i ≤ f (n), y.Insert(t, y) ∈ E F i ∧ ∀i , y . i < i ≤ f (n) → Insert(t, y ) / ∈ E F i ∧ ∃j , u . i < j ≤ f (n) ∧ (Insert(t, u ) ∈ E F j ∨ Delete(t) ∈ E F j ) which simplifies to ∃i ≤ f (n), y.Insert(t, y) ∈ E F i ∧ ∀i , y . i < i ≤ f (n) → Insert(t , y ) / ∈ F i ∧ ∃j . i < j ≤ f (n) ∧ Delete(t) ∈ E F j
Now we weaken the statement by dropping the first conjunct and restricting the quantification ∀i .

i < i ≤ f (n) to ∀i .j < i ≤ f (n), since i < j . ∃i ≤ f (n). ∃j . i < j ≤ f (n) ∧ ∀i . j < i ≤ f (n) → Insert(t , y ) / ∈ F i ∧ Delete(t) ∈ E F j
We further weaken the statement by weakening the scope of the existential quantification ∃j . i < j ≤ f (n) to ∃j . j ≤ f (n). Afterwards, i is not needed anymore.

∃j . j ≤ f (n) ∧ ∀i . j < i ≤ f (n) → Insert(t , y ) / ∈ F i ∧ Delete(t) ∈ E F j
This statement was obtained under the hypothesis that ∃i ≤ f (n), y.Insert(t, y) ∈ E F i ). Hence we have that

∀i ≤ f (n), y.Insert(t, y) ∈ E F i ∨∃j ≤ f (n). Delete(t) ∈ E F j ∧ ∀i . j < i ≤ f (n) → Insert(t , y ) / ∈ F i
This shows that Condition 6, in particular α notin , holds.

Since Case:

P n = P n-1 \ # { lookup t as x in Q else Q } ∪ # { Q } and {Q } ↔ {state p•1 ( t)} (
(E n-1 , S n-1 , P n-1 = P ∪ { lock t; Q }, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ # { Q }, σ n-1 , L n-1 ∪{ t }).
( t)] -[ Lock(l, t) ]→ [state p•1 ( t, l)]
for a fresh name l, that never appeared in a Fr-fact in ∪ j≤f (n-1) S j . We can extend the previous execution by s = 2 steps using an instance of FRESH for l and ri :

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n - → { FRESH } S n +s-1 Lock(l,t) -----→ P S n +s ∈ exec msr ( P ) with S n +s-1 = S f (n-1) \ # { state p ( t) } # ∪ # { Fr(l) } and S n +s = S f (n-1) \ # { state p ( t) } # ∪ # { state p•1 ( t) } # .
f (n) = L f (n-1) ∪ { t }.
In the following we show by contradiction that α lock , and therefore Condition 6 holds. α lock held in the previous step, and F f (n-1)+1 is empty, so we assume (by contradiction), that F f (n) = Lock(l, t) violates α lock . If this was the case, then:

∃i < f (n), l 1 . Lock(l 1 , t) ∈ E F i ∧∀i < j < f (n). Unlock(l 1 , t) ∈ E F j ∨∃k. k = j ∧ Unlock(l 1 , t) ∈ E F k ∨∃l 2 , k. Lock(l 2 , t) ∈ E F k ∧ i < k ≤ j ∨∃l 2 , k. Unlock(l 2 , t) ∈ E F k ∧ i ≤ k < j
We first note that the condition

∃k. k = j ∧ Unlock(l 1 , t) ∈ E F k
is never satisfied if the first condition in the disjuction is unsatisfied and that hence this condition can be removed: if there is j such that i < j < f (n) and Unlock(l 1 , t) ∈ E F j , then any k such that j = k and Unlock(l 1 , t) has Fr(l 1 ) in the premise (by definition of the translation). Since Fr is linear, and since, by Definition 6, Fr(l 1 ) is only added once, this is impossible. Thus said condition can be removed.

Next we observe that, by definition of the translation, Unlock(a, b) ∈ E F i if and only if Lock(a , b) / ∈ E F i . This allows us to tighten the bounds on the timepoint k in the two last disjuncts:

we can remove the corner case Lock(l 2 , t) ∈ E F j , as it implies Unlock(l 1 , t) ∈ E F j , and therefore satisfies the first disjunct; we can remove the corner case Unlock(l 2 , t) ∈ E F i , as it contradicts the first conjunct (Lock(l 1 , t) ∈ E F i ).

These simplifications result in the following formula.

∃i < f (n), l 1 .Lock(l 1 , t) ∈ E F i ∧ ∀i < j < f (n). Unlock(l 1 , t) ∈ E F j ∨ ∃l 2 , i < k < j. (Lock(l 2 , t) ∈ E F k ∨ Unlock(l 2 , t) ∈ E F k ) (2)
Since the semantics of the calculus requires that for all t = E t, t / ∈ L n-1 , by induction hypothesis, Condition 5, we have that

∀i ≤ f (n -1), l 1 . Lock(l 1 , t) ∈ E F i → ∃i < j ≤ f (n -1). Unlock(l 1 , t) ∈ E F j Since F f (n-1)+1 = ∅ and f (n) = f (n -1) + 2, we have: ∀i < f (n), l 1 .Lock(l 1 , t) ∈ E F i → ∃i < j < f (n). Unlock(l 1 , t) ∈ E F j We also have that ∃i < j < f (n). Unlock(l 1 , t) ∈ E F j ⇔ ∃j. i < j < f (n) ∧ Unlock(l 1 , t) ∈ E F j ∧ ∀i < k < j. Unlock(l 1 , t) ∈ E F k
To see that this statement holds consider two cases. Either the above statement is not satisfiable, i.e. there is no j such that Unlock(l 1 , t) ∈ E F j . Then the second formula is not satisfiable either. Or the above formula is satisfied, i.e., there exists j, such that Unlock(l 1 , t) ∈ E F j . Choosing j to be minimal, we immediately have that ∀i < k < j. Unlock(l 1 , t) ∈ E F k .

Hence, we obtain Case:

∀i < f (n), l 1 . Lock(l 1 , t) ∈ E F i → ∃i < j < f (n). Unlock(l 1 , t) ∈ E F j ∧ ∀i < k < j. Unlock(l 1 , t) ∈ E F k n Lock(l ,
(E n-1 , S n-1 , P n-1 = P ∪ { unlock t; Q }, σ n-1 , L n-1 ) → (E n-1 , S n-1 , P ∪ # { Q }, σ n-1 , L n-1 \ { t : t = E t }).
By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that unlock t; Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ Unlock(l, t) ]→ [state p•1 ( t)]. We can extend the previous execution by one step using ri , therefore:

∅ F 1 -→ P S 1 F 2 -→ P . . . F n -→ P S n Unlock(l,t) ------→ P S n +1 ∈ exec msr ( P ) with S n +1 = S f (n-1) \ # {state p ( t)} ∪ # {state p•1 ( t)}.
It is left to show that Conditions 1 to 7 hold for n.

The step from S f (n-1) to S f (n) is labelled F f (n) = Unlock(l, t), hence Condition 7 and Condition 2 hold.

In order to show that Condition 5 holds, we perform a case distinction. Assume t ∈ E ∈ L n-1 . Then, L f (n-1) = L f (n) . In this case, Condition 5 holds by induction hypothesis. In the following, we assume t ∈ E L n-1 . Thus, there is j ∈ n , l such that Lock(l , t) ∈ E F j and for all k such that j < k ≤ n , Unlock(l , t) ∈ E F k .

Since P | p is an unlock node and P is well-formed, there is a prefix q of p, such that P | q is a lock with the same parameter and annotation. By definition of P , there is no parallel and no replication between q and p. Note that any rule in P that produces a state named state p for a non-empty p is such that it requires a fact with name state p for p = p • 1 or p = p • 2 (in case of the translation of out, it might require state semi p , which in turn requires state p ). This means that, since state p ( t) ∈ S n , there is an i such that state q ( t ) ∈ S i and state q ( t ) ∈ S i-1 for t a prefix to t. This rule is an instance of P =q and thus labelled F i = Lock(l, t). We proceed by case distinction. Case 1: j < i (see Figure 22). By induction hypothesis, Condition 6 holds for the trace up to n . But, [F 1 , . . . , F i ] α lock , since we assumed that for all k such that j < k ≤ n , Unlock(l , t) ∈ E F k . Case 2: i < j (see Figure 23). As shown in the lock case, any k such that Unlock(l, t) ∈ E F k is k = n + 1. This contradicts Condition 6 for the trace up to j, since [F 1 , . . . , F j ] α lock , because there is not k such that i < k < j such that Unlock(l, t) ∈ E F k . This concludes the proof that Condition 5 holds for n + 1.

Condition 6 holds, since none of the axioms, in particular not α lock , become unsatisfied if they were satisfied for the trace up to f (n -1) and an Unlock is added.

Since To prove this direction we actually need to make a detour. We first define the notion of a normal msr execution and we next show that any msr execution resulting from a translation of a process has an equivalent normal execution. Finally we show that { tr ∈ hide(filter (traces msr ( P ))) | tr is normal } ⊆ traces pi (P ) Definition 21 (normal msr execution). An msr execution ∅ E 1 -→ P • • • En --→ P S n ∈ exec msr ( P ) for the multiset rewrite system P defined by a ground process P is normal if:

P n = P n-1 \ # { unlock t; Q } ∪ # { Q } and {Q} ↔ {state p•1 ( t)} (
1. The first transition is an instance of the INIT rule, i. e., S 1 = state [] () and there is at least this transition. 2. S n neither contains any fact with the symbol state semi p for any p, nor any fact with symbol Ack. 3. if for some i and t 1 , t 2 ∈ M, Ack(t 1 , t 2 ) ∈ (S i-1 \ # S i ), then there are p and q such that:

S i-3 - → R 1 S i-2 - → R 2 S i-1 - → R 3 S i , where: -R 1 = [state p (x)] → [Msg(t 1 , t 2 ), state semi p (x)] -R 2 = [state q (ỹ), Msg(t 1 , t 2 )] → [state q•1 (ỹ ∪ ỹ ), Ack(t 1 , t 2 )] -R 3 = [state semi p (x), Ack(t 1 , t 2 )] → [state p•1 (x)]. 4. S n-1 En --→ P,[],[] ,MDIN,INIT S n 5. if In(t) ∈ (S i-1 \ # S i ) for some i and t ∈ M, then S i-2 K(t) ---→ MDIN S i-1
Intuitively, a normal execution always starts with an INIT rule (item 1), internal communications are always finished (item 2), and not interleaved with any other actions (item 3). Furthermore, the last action is neither the generation of a fresh name, nor a message deduction rule. Indeed such a transition is not useful if it is the last one, as the freshly generated name, or the deduced message would not be used. Finally, if the attacker inputs a term to a process, this term is deduced just before (item 5).

We will now show that any execution has an equivalent normal execution, i. e., an execution that has the same labels, up to reserved facts, and preserves α.

Lemma 11 (Normalisation). Le P be a well-formed ground process. If

S 0 = ∅ E 1 -→ P S 1 E 2 -→ P . . . En -→ P S n ∈ exec msr ( P )
and [E 1 , . . . , E n ] α, then there exists a normal msr execution

T 0 = ∅ F 1 -→ P T 1 F 2 -→ P . . . F n -→ P T n ∈ exec msr ( P ) such that hide([E 1 , . . . , E n ]) = hide(F 1 , . . . , F n ) and [F 1 , . . . , F n ] α.
Proof. We will modify S 0 Inductive step. Assume the invariant holds for n -1 ≥ 1. We have to show that the lemma holds for n transitions, i. e., we assume that

∅ E 1 -→ P S 1 E 2 -→ P . . . En -→ P S n ∈ exec msr ( P )
is normal and [E 1 , . . . , E n ] α. Then it is to show that there is

(E 0 , S 0 , P 0 , σ 0 , L 0 ) F 1 -→ (E 1 , S 1 , P 1 , σ 1 , L 1 ) F 2 -→ . . . F n +1 -→ (E n +1 , S n +1 , P n +1 , σ n +1 , L n +1 )
fulfilling Conditions 1 to 7.

Assume now for the following argument, that there is no fact with the symbol Ack in S n-1 \ # S n . This is the case for all cases except for the case where rule instance applied from S n-1 to S n has the

form ri = [state semi p (s), Ack(t 1 , t 2 )] -[]→ [state p•1 (s)]
. This case will require a similar, but different argument, which we will present when we come to this case.

Since ∅ In the following case distinction, we will (unless stated otherwise) extend the previous execution by one step from (E n , S n , P n , σ n , L n ) to (E n +1 , S n +1 , P n +1 , σ n +1 , L n +1 ), and prove that Conditions 1 to 6 hold for n + 1. By induction hypothesis, they hold for all i ≤ n . We define a function f : N n → N n +1 as follows:

f (i) :=      f p (i) if i ∈ N m n if m < i < n n + 1 if i = n
Since, S m → * R S n for R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }, only S n \ # S m contains only Fr-facts and !K-facts, and S m \ # S n contains only Fr-facts and Out-facts. Therefore, 3 and 4 hold for all i ≤ n -1. Since E m+1 , . . . , E n-1 = ∅, Condition 1, 2,5 and 6 hold for all i ≤ n -1.

Fix a bijection such that P n P S m . We will abuse notation by writing P P state p ( t), if this bijection maps P to state p ( t).

We now proceed by case distinction over the last type of transition from S n-1 to S n . Let l linear = E S n-1 \ S n and r = E S n \ S n-1 . l linear can only contain linear facts, while r can contain linear as well as persistent facts. The rule instance ri used to go from S n-1 to S n has the following form:

[l linear , l persistent ] -[ E n ]→ r for some l persistent ⊂ # E S n-1 . Note that l linear , E n and r uniquely identify which rule in R ∈ P, [], [] ri is an instance of. If R is uniquely determined, we fix some ri ∈ ginsts(R).

with E n +1 = E n ∪ a , S n +1 = S n , P n +1 = P n \ # { ν a; Q } # ∪ # { Q { a / a } } # , σ n +1 = σ n and L n +1 = L n .

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P , state p•1 (x, a) ∈ prems(R ) for an R ∈ P =p•1 . We can choose θ := θ[n a → a ] and have Condition 3 holds, since furthermore ν a ; Q' ↔ state p ( t), Let θ be a grounding substitution for state(x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

P n +1 = P n \ # { ν a ; Q' } # ∪ # { Q { a / a } } # ,
From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = out (t 1 , t 2 ); Q for a process Q = P | p•1 τ ρ.

From the induction hypothesis, and since E m+1 , . . . , E n-2 = ∅, we have that

E n = { a ∈ FN | ProtoNonce(a) ∈ E 1≤j≤n-2 E j }.
From the induction hypothesis, and since no rule producing Out-facts is applied between step m and step n -2, we have that

{ xσ n | x ∈ D(σ n ) } # = E { Out(t) ∈ ∪ k≤n-2 S k } # . (3)
Let r = { a : fresh | RepNonce(a) ∈ 1≤j≤n-2 F j }. Since !K(t 1 ) ∈ prems(MDINσ) for σ(x) = t 1 , we have !K(t 1 ) ∈ E S n-2 . By Lemma 8 and Lemma 9, we have νE n , r.σ n t. Therefore, νE n .σ n t. We chose the following transition:

• • • F n --→(E n , S n , P n , σ n , L n ) K(t 1 )
---→(E n +1 , S n +1 , P n +1 , σ n +1 , L n +1 ) with E n +1 = E n , S n +1 = S n , P n +1 = P n \ # { out (t 1 , t 2 ); Q } # ∪ # { Q } # , σ n +1 = σ n ∪ { t 2 / x } and L n +1 = L n for a fresh x.

We define f as follows: Condition 4 holds since σ n +1 = σ n ∪ { t 2 / x }, and therefore: Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = E xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22). From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = in (t 1 , N ); Q , for N a term that is not necessarily ground, and a process Q = P | p•1 τ ρ. Since ri ∈ E ginsts(R), we have that there is a substitution τ such that N τ = E t 2 .

f (i) :=      f p (i) if i ∈ N m n if m < i < n -1 n + 1 if i = n
{ xσ n +1 | x ∈ D(σ n +1 ) } # ={ xσ n | x ∈ D(σ n ) } # ∪ # { t 2 } # = E { Out(t) ∈ ∪ k≤n-2 S k } # ∪ # {
From the induction hypothesis, and since E m+1 , . . . , E n-2 = ∅, we have that

E n = { a | ProtoNonce(a) ∈ 1≤j≤n-2 E j }.
From the induction hypothesis, and since no rule producing Out-facts is applied between step m and step n -2, we have that

{ xσ n | x ∈ D(σ n ) } # = { Out(t) ∈ ∪ k≤n-2 S k } # . (4)
Let r = { a : fresh | RepNonce(a) ∈ 1≤j≤n-2 F j }. Since !K( t 1 , t 2 ) ∈ prems(MDINσ) for σ(x) = t 1 , t 2 , we have !K( t 1 , t 2 ) E ∈ S n-2 . By Lemma 8 and Lemma 9, we have νE n , r.σ n t 1 , t 2 . Therefore, νE n .σ n t 1 , t 2 . Using DEQ and DAPPL with the function symbols fst and snd , we have νE n .σ n t 1 and νE n .σ n t 2 . Therefore, we chose the following transition:

• • • F n --→(E n , S n , P n , σ n , L n ) K(t 1 )
---→(E n +1 , S n +1 , P n +1 , σ n +1 , L n +1 )

with E n +1 = E n , S n +1 = S n , P n +1 = P n \ # { in (t 1 , N ); Q } # ∪ # { Q τ } # , σ n +1 = σ n and L n +1 = L n .
We define f as follows: Let θ such that ri = θ R. As established before, we have τ such that N τ = E t 2 . By definition of P =p , we have that state p•1 ( t, t ) ∈ E ginsts(P =p•1 ), and that θ = θ • τ . Since τ and ρ are induced by θ, θ induces τ • τ and the same ρ. We have that Q τ = (P | p•1 τ ρ)τ = P | p τ τ ρ and therefore Q τ P state p•1 ( t, t ). Thus, and since in (t 1 , N ); Q P state p ( t), P n +1 = P n \ # { in (t 1 , N ); Q } # ∪ # { Q τ } # and S n = S n-1 \ # { In( t 1 , t 2 ), state p ( t) } # ∪ # { state p•1 ( t, t ) } # , Condition 3 holds.

f (i) :=      f p (i) if i ∈ N m n if m < i < n -1 n + 1 if i = n
Conditions Condition 1, 2 and 4 hold trivially.

Case: ri = [state semi p (s), Ack(t 1 , t 2 )] -[]→ [state p•1 (s)] (for some p, t and t 1 , t 2 ∈ M). Since the msr execution is normal, we have that there p,q,x, ỹ, ỹ such that: .

S n-3 - → R 1 S n-2 - → R 2 S n-1 - → R 3 S
Since in this case, there is a fact with symbol Ack removed from S n-1 to S n , we have to apply a different argument to apply the induction hypothesis.

Since ∅ In the following case distinction, we extend the previous execution by one step from (E n , S n , P n , σ n , L n ) to (E n +1 , S n +1 , P n +1 , σ n +1 , L n +1 ), and prove that Conditions 1 to 6 hold for n + 1. By induction hypothesis, they hold for all i ≤ n . We define a function f : N n → N n +1 as follows:

f (i) :=      f p (i) if i ∈ N m n if m < i ≤ n -3 n + 1 if i = n
Since, S m → * R S n for R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }, only S n \ # S m contains only Fr-facts and !K-facts, and S m \ # S n contains only Fr-facts and Out-facts. Therefore, 3 and 4 hold for all i ≤ n -3. Since E m+1 , . . . , E n-1 = ∅, Condition 1, 2, 5 and 6 hold for all i ≤ n -3.

Fix a bijection such that P n P S m . We will abuse notation by writing P P state p ( t), if this bijection maps P to state p ( t). Since { MDOUT, MDPUB, MDFRESH, MDAPPL } and FRESH do not add or remove state-facts, P n P S n-3 . Let P ∈ # P n such that P P state p (s). Let Q ∈ # P n such that Q P state q ( t). Let θ be a grounding substitution for state q (ỹ) ∈ prems( P =q ) such that t = E ỹθ . Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | q τ ρ = Q (see Definition 22).

From the form of the rules R 1 and R 3 , and since P = E P | p τ ρ, for τ and ρ induced by the grounding substitution for state p (x), we can deduce that P = E out t 1 , t 2 ; P for a process P = P | p•1 τ ρ. Similarly, from the form of R 2 , we can deduce Q = E in (t 1 , N ); Q , for N a term that is not necessarily ground, and a process Q = P | q•1 τ ρ . Since S n-2 -→ R 2 S n-1 , we have that there is a substitution τ * such that N τ ρ τ * = E t 2 and ((ỹ ∪ vars(N )) \ ỹ)τ * = E t , where t such that state q•1 ( t, t ) ∈ S n-1 \ # S n-2 .

Given that Q = E in (t 1 , N ); Q and P = E out t 1 , t 2 ; P , have that P n = P ∪ # { out t 1 , t 2 ; P , in (t 1 , N ); Q } # with t 1 = E t 1 and t 2 = E N τ * . Therefore, we chose the following transition:

• • • F n --→(E n , S n , P n , σ n , L n ) K(t 1 )
---→(E n +1 , S n +1 , P n +1 , σ n +1 , L n +1 ) with E n +1 = E n , S n +1 = S n , P n +1 = P ∪ # { P , Q } # , σ n +1 = σ n and L n +1 = L n .

Conditions 1 to 7 hold for i ≤ n -3. It is left to show that Conditions 1 to 7 hold for n.

As established before, we have τ * such that N τ ρ τ * = E t 2 . Let state q ( t, t ) be the state variable added to S n-1 . Then, ((ỹ ∪ vars(N )) \ ỹ)τ * = t . By definition of P =q , we have that state q•1 ( t, t ) ∈ prems(ginsts(P =p•1 )) for a grounding substitution θ q•1 = θ • τ * . Since τ and ρ are induced by θ , θ q•1 induces τ • τ and the same ρ. We have that Q τ = (P | q•1 τ ρ )τ * = P | q•1 τ τ ρ and therefore Q τ * P state q•1 ( t, t ). Similarly, we have P P state q•1 (s). We conclude that Condition 3 holds. Conditions Condition 1, 2, 4, 5 and 6 hold trivially.

Case: ri = [state p ( t)] -[ Pred pr (t 1 , . . . , t l ) ]→ [state p•1 ( t)] (for some p, t 1 , . . . , t l ∈ M and t ). By induction hypothesis, we have P n P S m , and thus, as previously established, P n P S n-1 . Let Q ∈ # P n such that Q P state p ( t). Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = if pr (t 1 , . . . , t l ) then Q 1 else Q 2 for a process Q = P | p•1 τ ρ.

Fig. 1 .

 1 Fig. 1. Syntax, where M, N ∈ T and Pred ∈ P

Fig. 3 .

 3 Fig. 3. Proof tree witnessing that ν ñ.σ k2, where c = senc(k2, k1)

Fig. 4 .

 4 Fig. 4. Operational semantics

Fig. 5 .

 5 Fig. 5. Example of transitions modelling the creation of a key on a PKCS#11-like device

Fig. 8 .

 8 Fig. 8. The set of multiset rewrite rules !Pnew (omitting the rules in MD)

Fig. 9 .

 9 Fig. 9. Example trace for the translation of !Pnew .

Fig. 10 .

 10 Fig. 10. Definition of α.

Fig. 11 .

 11 Fig. 11. Translation of process P

Fig. 15 .

 15 Fig. 15. state-premise at position t2 can be resolved up to INIT. Same fresh value l1 is generated at positions t1 and t2.

Definition 16 .

 16 Let α be the trace formula as defined in Definition 15 and Tr a set of traces. We define filter (Tr ) := {tr ∈ Tr | ∀θ.(tr , θ) α}.

Proposition 1 .

 1 Let Tr be a set of traces and ϕ a trace formula. We have thatTrϕ iff filter (Tr ) ϕ

Definition 17 (

 17 hide). Given a trace tr and a set of facts F we inductively define hide([]) = [] and hide(F • tr ) := hide(tr ) if F ⊆ F res (F \ F res ) • hide(tr ) otherwise Given a set of traces Tr we define hide(Tr ) = {hide(t) | t ∈ Tr }.

Proposition 2 .

 2 Let Tr be a set of traces and ϕ a well-formed trace formula. We have thatTrϕ iff hide(Tr ) ϕwhere is either ∀ or ∃.Proof. We start with the case = ∃ and show the stronger statement that for a trace tr ∀θ.∃θ . if (tr , θ) ϕ then (hide(tr ), θ ) ϕ and ∀θ.∃θ . if (hide(tr ), θ) ϕ then (tr , θ ) ϕ.We will show both statements by a nested induction on |tr | and the structure of the formula. (The underlying well-founded order is the lexicographic ordering of the pairs consisting of the length of the trace and the size of the formula.) If |tr | = 0 then tr = [] and tr = hide(tr ) which allows us to directly conclude letting θ := θ. If |tr | = n, we define tr and F such that tr = tr • F . By induction hypothesis we have that ∀θ.∃θ . if (tr , θ) ϕ then (hide(tr ), θ ) ϕ and ∀θ.∃θ . if (hide(tr ), θ) ϕ then (tr , θ ) ϕ.

Definition 18 .

 18 We re-define P to contain the INIT rule and P , [], [] , but not MD (which is different to Definition 14). We furthermore define a translation with dummy-facts, denoted P D , that contains INIT and P , [], [] D , which is defined as follows: We define P D := INIT ∪ P , [], [] D , where P , [], [] D is defined just as P , [], [] , with

  trace(execs( P ∪ MD) DHe ¬α in ∨ φ ⇔ trace(execs( P ∪ MD) DHe ¬α in ∨ φ (Lemma 3.7 (unaltered)) ⇔ trace(execs( P ∪ MD)) ↓ RDHe DHe ¬α in ∨ φ (Definition of DHe ) ⇔ trace(dgraphs DHe ( P ∪ MD)) ↓ RDHe DHe ¬α in ∨ φ (Lemma 3.10 (unaltered)) ⇔ trace({dg | dg ∈ dgraphs ACC ( P ∪ MD RDHe insts ) ∧dg ↓ RDHe -normal}) DHe ¬α in ∨ φ (Lemma 3.11 (unaltered)) ⇔ trace(ndgraphs( P )) DHe ¬α in ∨ φ (Lemma A.12 (*)) ⇔ trace(ndgraphs( P )) ACC ¬α in ∨ φ (Lemma 3.7 and A.20(both unaltered))

Fig. 18 .

 18 Fig. 18. Definition of P, p, x =p t where {•} a ? =b = { • } if a = b and ∅ otherwise.

Condition 1 ,

 1 Condition 2, Condition 4, Condition 5, Condition 6 and Condition 7 hold trivially. To show that Condition 3 holds, we have to show that P 0 ↔ P { state [] () } # . Note that P 0 = { P } # . We choose the bijection such that P ↔ P state [] (). For τ = ∅ and ρ = ∅ we have that P | [] τ = P τ = P ρ. By Definition 19, P =[] = P, [], [] =[] . We see from Figure 18 that for every P we have that state [] () ∈ prems( P, [], [] =[] ). Hence, we conclude that there is a ground instance ri ∈ E ginsts( P =[] ) with state [] () ∈ prems(ri ).

  It is left to show that Conditions 1 to 7 hold for n. Condition 1, Condition 2, Condition 4, Condition 5, Condition 6, and Condition 7 hold trivially. Condition 3 holds because P

  Condition 3 holds because P n = P n-1 ∪ # {Q} and {Q} ↔ P {state p•1 ( t)} (by definition of P =p ). Condition 1, Condition 2, Condition 4, Condition 5, Condition 6 and Condition 7 hold trivially.

  and the induction hypothesis, we can conclude that Condition 7 holds. Condition 3 holds since P n = P n-1 and no state-facts where neither removed nor added. Condition 1, Condition 2, Condition 4, Condition 5 and Condition 6 hold trivially.

F n -

 n → P S n → * R⊂ P S = S n +s-3 (MDAPPL)

(ri 1 )→ P S n +s- 2 (ri 2 )→ P S n +s- 1 (ri 2 )

 12212

  a)} (by definition of the translation), we have that P n ↔ P S f (n) , and therefore Condition 3 holds. Condition 1, Condition 2, Condition 4 and Condition 5 hold trivially.

  It is left to show that Conditions 1 to 7 hold for n. Condition 3 holds becauseP n = P n-1 \ # { event(F );Q } ∪ # { Q } and {Q} ↔ {state p•1 ( t)} (by definition of P =p ). Taking k = f (n) Condition 7 holds. Condition 1, Condition 2, Condition 4, Condition 5 and Condition 6 hold trivially.

  {Q} ↔ {state p•1 ( t)} (by definition of P =p ), we have that Condition 3 holds. Condition 1, Condition 4 and Condition 5 hold trivially.

  by definition of P =p ), we have that Condition 3 holds. Condition 1, Condition 4 and Condition 5 hold trivially.

F 2 -

 2 → P . . .

  --→ P S n +1 ∈ exec msr ( P )with S n +1 = S f (n-1) \ # {state p ( t)} ∪ # {state p•1 ( t)}.It is left to show that Conditions 1 to 7 hold for n.

  e., Condition 3 holds. Condition 1, Condition 4 and Condition 5 hold trivially.

  by definition of P =p ), we have that Condition 3 holds. Condition 1, Condition 4 and Condition 5 hold trivially.

Fig. 22 .

 22 Fig. 22. Visualisation of Case 1.

Fig. 23 .

 23 Fig. 23. Visualisation of Case 2.

  by definition of the translation), we have that Condition 3 holds. Condition 1, and Condition 4 hold trivially. B.3. Proof that traces pi (P ) ⊇ hide(filter (traces msr ( P )))

E 1 - 1 -

 11 → P . . .En-→ P S n by applying one transformation after the other, each resulting in an msr execution that preserves satisfaction of α.1. If an application of the INIT rule appears in S 0E → P . . .En-→ P S n , we move it to the front. Therefore, S 1 = state [] (). This is possible since the left-hand side of the INIT rule is empty. If the rule is never instantiated, we prepend it to the trace. Since Init() ∈ F res , the resulting msr execution S

E 1 - 1 - 1 -

 111 → P • • • En --→ P S n ∈ exec msr ( P ) is normal and n ≥ 2, by Proposition 3, there exists m < n such that S m → * R S n for R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH } and ∅ E → P • • • Em --→ P S m ∈ exec msr ( P ) is normal, too. This allows us to apply the induction hypothesis on ∅ E→ P • • • Em --→ P S m ∈ exec msr ( P ).Hence there is a monotonically increasing function from N m → N n and an execution such that Conditions 1 to 7 hold. Let f p be this function and note that n = f p (m).

  state p•1 ( t, a ) = state p•1 (x, a)θ . Since Q = P | p τ ρ for τ and ρ induced by θ, Q { a / a } = P | p τ ρ for τ and ρ induced by θ , i. e., τ = τ and ρ = ρ[a → a ]. Therefore, Q { a / a } P state p•1 ( t, a ).

Therefore, Conditions 1

 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n. Condition 6 holds since hide([E 1 , . . . , E m ]) = E [F 1 , . . . , n ], and [E m+1 , . . . , E n-1 ] = E [F n +1 ], since E n-1 = K(t 1 ).

  Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.Condition 6 holds since hide([E 1 , . . . , E m ]) = [F 1 , . . . , n ], and [E m+1 , . . . , E n-1 ] = [F n +1 ], since E n-1 = K(t 1 ).

E 1 - 1 - 1 -

 111 → P • • • En --→ P S n ∈ exec msr ( P ) is normal, n ≥ 2, and t 1 , t 2 ∈ M, Ack(t 1 , t 2 ) ∈ (S n-1 \ # S n ), there exists m ≤ n-3 such that S m → * R S n-3 for R = { MDOUT, MDPUB, MDFRESH, MDAPPL } ∪ FRESH and ∅ E → P • • • Em --→ P S m ∈ exec msr ( P ) is normal.This allows us to apply the induction hypothesis on ∅E → P • • • Em --→ P S m ∈ exec msr ( P ).Hence there is a monotonically increasing function from N m → N n and an execution such that Conditions 1 to 7 hold. Let f p be this function and note that n = f p (m).

  Pred then P else Q, A) := if Pred then ap(P, A) else ap(Q, A) ap(lookup M as x in P else Q, A) := lookup M as x in ap(P, A) else ap(Q, A)

	ap(α; P, A) := α; ap(P, A)	where α / ∈ { lock t, unlock t : t ∈ T }
	ap(lock t; P, A) := lock l t; ap(P, A • (t, l))	where l ∈ N is a fresh label
	ap(unlock t; P, A) :=

  state [] ()

	Init()
	!state [] ()	!state [] ()
	state 1 ()	state 1 ()
	Fr(h) state 1 ()	state 1 () Fr(h )
	state 11 (h)	state 11 (h )
	Fr(k) state 11 (h)
	state 111 (h,k)

state 11 (h ) Fr(k ) state 111 (h ,k ) state 111 (h,k) state 1111 (h,k) state 111 (h ,k ) state 1111 (h ,k ) Event() NewKey(h, k) Event() NewKey(h , k ) state 1111 (h,k) state 11111 (h,k) state 1111 (h ,k ) state 11111 (h ,k ) Insert( 'att',h ,'dec') Insert( 'att',h ,'dec')

  1 ) state 1 () state 11 (l 1 )t 3 : state 1 () Fr(l 2 )

		Lock(l 1 , 's')	. =	Lock(l 1 , 's')	state 11 (l 2 )	Lock(l 2 , 's')
	state 11 (l 1 ) state 112 (l 1 )	IsNotSet('visited')	state 11 (l 1 ) state 112 (l 1 )	IsNotSet('visited')	state 11 (l 2 ) state 112 (l 2 )	IsNotSet('visited')
		Event() Visit()					Event() Visit()
			state 1121 (l 1 ) state 11211 (l 1 )	Insert('visited','s')

i : state 112 (l 1 ) state 1121 (l 1 ) state 112 (l 1 ) state 1121 (l 1 ) j : state 112 (l 2 ) state 1121 (l 2 ) t 2 : state 11211 (l 1 ) state 112112 (l 1 ) Unlock(l 1 ,'s')

  1 ) state 1 () state 11 (l 1 )t 3 : state 1 () Fr(l 2 )

		Lock(l 1 , 's')	state 11 (l 2 )	Lock(l 2 , 's')
	state 11 (l 1 ) state 112 (l 1 )	IsNotSet('visited')	k : state 11 (l 2 ) state 112 (l 2 )	IsNotSet('visited')
		Event() Visit()		Event() Visit()

i : state 112 (l 1 ) state 1121 (l 1 ) j : state 112 (l 2 ) state 1121 (l 2 ) i : state 1121 (l 1 ) state 11211 (l 1 ) Insert('visited','s') t 2 : state 11211 (l 1 ) state 112112 (l 1 ) Unlock(l 1 ,'s')

  1 ) state 1 ()state 11 (l 1 )t 0 : Fr(l ) state 1 ()

		Lock(l 1 , 's')	state 11 (l )	Lock(l , 's')	t 3 : state 1 () Fr(l 2 ) state 11 (l 2 )	Lock(l 2 , 's')
	state 11 (l 1 ) state 112 (l 1 )	IsNotSet('visited')	state 11 (l ) state 112 (l )	IsNotSet('visited')	state 11 (l 2 ) state 112 (l 2 )	IsNotSet('visited')
		Event() Visit()					Event() Visit()
			state 1121 (l ) state 11211 (l )	Insert('visited','s')

i : state 112 (l 1 ) state 1121 (l 1 ) state 112 (l ) state 1121 (l ) j : state 112 (l 2 ) state 1121 (l 2 ) t 0 : state 11211 (l ) state 112112 (l ) Unlock(l ,'s') Fig. 17. The naïve formulation α lock provokes a loop: t1 and t 0 are possibly distinct, thus α lock applies to Lock(l ,'s') at t 0 .

  nonce,senc( secretid , tc , npr , k) ); lock ' Server ' , pid ; lookup ' Server ' , pid as tuple in if fst ( tuple )= secretid then if fst (snd( tuple ))=k then in (otc); if snd(snd( tuple ))=otc then if smaller (otc , tc ) then event Login(pid, k , tc ); insert ' Server ' , pid , secretid , k , tc ; unlock ' Server ' , pid

  If t ∈ PN we use rule MDPUB and we have that S n → S = S n ∪ {!K(t)}. In case t ∈ FN we need to consider 3 different cases: (i) !K(t) ∈ S n and we immediately conclude (by letting S = S n ), (ii) Fr(t) ∈ S n and applying rule MDFRESH we have that S n → S = S n ∪ {!K(t)}, (iii) Fr(t) ∈ S n . By inspection of the rules we see that Fr(t) ∈ S i for any 1 ≤ i ≤ n: the only rules that could remove Fr(t) are MDFRESH which would have created the persistent fact !K(t), or the ProtoNonce rules which would however have added t to ñ. Hence, applying successively rules FRESH and MDFRESH yields a valid extension of the execution S n → S n ∪ {Fr(t)} → S = S n ∪ {!K(t)}.-DFRAME. We have that xσ = t for some x ∈ D(σ), that is, t ∈ {t 1 , . . . , t m }. By definition of {t 1 , . . . , t m }, Out(t) ∈ S i for some i ≤ n. If Out(t) ∈ S n we have that S n → S = (S n \ {Out(t)}) ∪ {!K(t)} applying rule MDOUT. If Out(u) ∈ S n , the fact that the only rule in P that allows to remove an Out-fact is MDOUT, suggests that it was applied before, and thus !K(u) ∈ S.

  It is left to show that Conditions 1 to 7 hold for n. Condition 1, Condition 2, Condition 4, Condition 5, Condition 6 and Condition 7 hold trivially. We now show that Condition 3 holds. Condition 3 holds because P n = P n-1 \ # {Q|R} ∪ # {Q, R}, {Q} ↔ P {state p•1 (x)} and {R} ↔ P {state p•2 (x)} (by definition of the translation) (see Remark 2).

  Exactly as in the two previous cases we have that Q ↔ state p•1 ( t), as well as Rθ ↔ state p •1 ( t ). Hence we have that, Condition 3 holds. Condition 1, Condition 2, Condition 4, Condition 5, Condition 7 and Condition 6 hold trivially.

  ). This step requires that σ pr t 1 / x 1 , . . . , t l / x l is satisfied. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that if pr (t 1 , . . . , t l ) then Q else Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ Pred pr (t 1 , . . . , t l ) ]→ [state p•1 ( t)]. We can extend the previous execution by one step using ri , therefore:

	∅	F 1 -→ P S 1	F 2 -→ P . . .	F n -→ P S n	Predpr (t 1 ,...,t l )

  ). By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that insert t, t ; Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ Insert(t, t ) ]→ [state p•1 ( t)].

  It is left to show that Conditions 1 to 7 hold for n. This step is labelled F f (n) = Insert(t, t ), hence Condition 7 holds. To see that Condition 2 holds we let j = f (n) for which both conjuncts trivially hold. Since, by induction hypothesis, Condition 6 holds, i.e., [F 1 , . . . F n ] α, it holds for this step too. In particular, if [F 1 , . . . F n ] α in and [F 1 , . . . F n ] α notin , we also have that [F 1 , . . . F n , F f (n) ] α in and [F 1 , . . . F n , F f (n) ]

  ). This step requires that S(t ) is undefined for all t = E t. By induction hypothesis we have that P n-1 ↔ P S n . Let p and t be such that lookup t as x in Q else Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [state p ( t)] -[ IsNotSet(t) ]→ [state p•1 ( t)]. We can extend the previous execution by one step using ri , therefore: It is left to show that Conditions 1 to 7 hold for n. This step is labelled F f (n) = IsNotSet(t), hence Condition 7 holds. Condition 2 also holds trivially and will be used to show Condition 6. Since this step requires that S(t ) is undefined for all t = E t, we have by Condition 2 that ∀j

	∅	F 1 -→ P S 1	F 2 -→ P . . .	F n -→ P S n	IsNotSet(t)

-------→ P S n +1 ∈ exec msr ( P )

with S n +1 = S f (n-1) \ # state p ( t) ∪ # state p•1 ( t).

  This step requires that for all t = E t, t / ∈ L n-1 . Let p and t such that lock t; Q ↔ P state p ( t). By Definition 20, there is a ri ∈ ginsts( P =p ) such that state p ( t) is part of its premise. By definition of P =p , we can choose ri = [Fr(l), state p

  (see Figure21). Again, α lock is not satisfied, i.e., [F 1 , . . . , F n ] α lock , since there is no o such that i < o < n and Unlock(l 1 , t) ∈ E F o . Fig. 21. Visualisation of Case 2b.Since we could, under the assumption that Condition 1 to Condition 7 hold for i ≤ n , reduce every case in which [F 1 , . . . , F n +1 ] α lock to a contradiction, we can conclude that Condition 6 holds for n + 1.SinceP n = P n-1 \ # { lock t; Q }∪ # { Q } and{Q} ↔ {state p•1 ( t)} (by definition of the translation), we have that Condition 3 holds. Condition 1, and Condition 4 hold trivially.

	t)	Lock(l 1 , t)	Unlock(l , t)	Unlock(l 1 , t)
		i	m	j
		Fig. 20. Visualisation of Case 2a.
	Case 2b: i < n i Lock(l 1 , t)	n Lock(l , t)	m Unlock(l , t)	j Unlock(l 1 , t)

  and S n = S n-1 \ # { Fr(a), state p ( t) } # ∪ # state p•1 ( t, a : fresh). Condition 1, holds since E n +1 = E n ∪ a , and E n = ProtoNonce(a ). Condition 6 holds since ProtoNonce(a) ∈ F res . Conditions 2 and 4 hold trivially. Case: ri = [state p ( t), In(t 1 )] -[ InEvent(t 1 ) ]→ [state p•1 ( t), Out(t 2 )] (for some p, t and t 1 , t 2 ∈ M). Since the msr execution is normal, we have that S n-2 K(t 1 ) ---→ MDIN S n-1 . Since S 0 P S m is a normal trace and S m → * R S n-1 for R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }. By induction hypothesis, we have P n P S m , and thus, since { MDOUT, MDPUB, MDFRESH, MDAPPL }and FRESH do not add or remove state-facts, P n P S n-2 . Let Q ∈ # P n such that Q

	E 1

-→ P . . . En --→ P S n is normal, so is S 0 E 1 -→ P . . . E n-1

---→ P S n-1 , and therefore S 0

E 1 -→ P . . . E n-2 ---→ P S n-2 . Hence there is an m < n -2 such S 0 E 1 -→ P . . . Em --→ P state p ( t).

  t 2 } # (by (4)) ={ Out(t) ∈ ∪ k≤n S k } # By definition of P and P =p , we have that Q P state p•1 ( t). Therefore, and since we have that out (t 1 , t 2 ); Q P state p ( t), P n +1= P n \ # { out (t 1 , t 2 ); Q } # ∪ # { Q } # , and S n = E S n-1 \ # { In(a), state p ( t) } # ∪ # { state p•1 ( t), Out(t 2 ) },Condition 3 holds. Conditions Condition 1, 2 hold trivially. P S m is a normal trace and S m → * R S n-1 for R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }. By induction hypothesis, we have P n P S m . Since { MDOUT, MDPUB, MDFRESH, MDAPPL }, FRESH and MDIN do not add or remove state-facts, P n P S n-2 . Let Q ∈ # P n such that Q

Case: ri = [state p ( t), In( t 1 , t 2 )] -[ InEvent( t 1 , t 2 ) ]→ [state p•1 ( t, t )

] (for some p, t, t and t 1 , t 2 ∈ M). Since the msr execution is normal, we have that S n-2

K(t 1 ) ---→ MDIN S n-1 . Since S 0 E 1 -→ P . . . En --→ P S n is normal, so is S 0 E 1 -→ P . . . E n-1

---→ P S n-1 , and therefore we have that

S 0 E 1 -→ P . . .

E n-2 ---→ P S n-2 . Hence there is an m < n -2 such S 0 E 1 -→ P . . . Em --→ P state p ( t).

  -R 2 = [state q (ỹ), Msg(t 1 , t 2 )] → [state q•1 (ỹ ∪ ỹ ), Ack(t 1 , t 2 )] -R 3 = [state semi p (x), Ack(t 1 , t 2 )] → [state p•1 (x)]

n , where:

-R 1 = [state p (x)] → [Msg(t 1 , t 2 ), state semi p (x)]

Acknowledgments. This work has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No 645865-SPOOC), and from the German Federal Ministry of Education and Research (BMBF) within EC SPRIDE.

Combining this with [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] we obtain that

Fix i < f (n), j such that i < j < f (n), and l 1 such that Lock(l 1 , t) ∈ E F i and Unlock(l 1 , t) ∈ E F j . Then, there are l 2 and k such that i < k < j and either Lock(l 2 , t) ∈ E F k or Unlock(l 2 , t) ∈ E F k , but l 2 = E l 1 . We proceed by case distinction. Case 1: there is no unlock in between i and j, i. e., for all m, i < m < j, Unlock(l , t) ∈ F m . Then there is a k and l 2 such that Lock(l 2 , t) ∈ E F k . In this case, α lock is already invalid at the trace produced by the k-prefix of the execution, contradicting the induction hypothesis. Case 2: there are l and m, i < m < j such that Unlock(l , t) ∈ F m (see Figure 19). We first observe that for any l, u, i 1 , i 2 , if Unlock(l, u) ∈ E F i 1 and Unlock(l, u) ∈ E F i 2 , then i 1 = i 2 . We proceed by contradiction. By definition of P and well-formedness of P , the steps from i 1 -1 to i 1 and from i 2 -1 to i 2 must be ground instances of rules P =q and P =q such that P | q and P | q start with unlock commands that are labelled the same and have the same parameter, since every variable lock l in P appears in a Fr-fact in the translation for the corresponding lock command. By definition of P , this means q and q have a common prefix q l that starts with a lock with this label.

Let q l ≤ q denote that q l is a prefix of q. Since P gives ⊥ if there is a replication or a parallel between q l and q or q , and since P is well-formed (does not contain ⊥), we have that every state fact state r for q l ≤ r ≤ q or q l ≤ r ≤ q appearing in P is a linear fact, since no replication is allowed between q l and q or q . This implies that q = q. Furthermore, every rule in ∪ q l ≤r≤q∨q l ≤r≤q P =r adds at most one fact state r and if it adds one fact, it either removes a fact state r where r = r • 1 or r • 2, or removes a fact state semi r where r = r • 1, which in turn requires removing state r (see translation of out). Therefore, either q ≤ q or q ≤ q. But this implies that both have different labels, and since P =q l requires Fr(l), and E distinguishes fresh names, we have a contradiction. (A similiar observation is possible for locks: For any l, u, i 1 , i 2 , if Lock(l, u) ∈ E F i 1 and Lock(l, u) ∈ E F i 2 , then i 1 = i 2 , since by definition of the translation, the transition from i 1 -1 to i 1 or i -2 -1 to i 2 removes fact Fr(l).)

From the first observation we learn that , l = E l 1 for any l and m, i < m < j such that Unlock(l , t) ∈ F m . We now choose the smallest such m. By definition of P , the step from S m-1 to S m must be ground instance of a rule from P =q for P | q starting with unlock. Since P is well-formed, there is a q l such that P | q l starts with lock, with the same label and parameter as the unlock. As before, since P is well-formed, and therefore there are no replications and parallels between q l and q, there must be n such that Lock(l , t) ∈ F n and n < m. We proceed again by case distinction. Case 2a: n < i (see Figure 20). By the fact that m > i we have that there is no o such that n < o < i and Unlock(l , t) ∈ E F o (see first observation). Therefore, the trace produced by the i-prefix of this execution does already not satisfy α lock , i. e., [F 1 , . . . , F i ] α lock .

-→ P . . .

n (1) is such that hide

n [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] , it also contains a fact state semi p ( t) for some p and t such that there exists a rule of type R 3 that consumes both of them, since Ack(t 1 , t 2 ) can only be produced by a rule of type R 2 which consumes Msg(t 1 , t 2 ) which in turn can only be produced along with a fact state semi p ( t), and by definition of P , there exists a rule in P =p of form R 3 that consumes Ack(t 1 , t 2 ) and state semi p ( t). We append as many applications of rules of type R 3 as there are facts Ack(t 1 , t 2 ) ∈ S

(1) n (1) , and repeat this for all t 1 , t 2 such that Ack(t 1 , t 2 ) ∈ S

(1)

n and S

n does not contain Ack-facts anymore. If S [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] n contains a fact state semi p ( t), we remove the last transition that produced this fact, i. e., for i such that

The resulting execution is valid, since state semi

n . The latter is the case because if Msg(t 1 , t 2 ) would be consumed at a later point, say j, j + 1 would contain Ack(t 1 , t 2 ), but since S (1) n -1 does not contain Ack-facts, they can only be consumed by a rule of type R 3 , which would have consumed state semi p ( t). We repeat this procedure for every remaining

n , and call the resulting trace

Since no rule added or removed has an action,

We transform S

(1) 0

n [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] as follows (all equalities are modulo E): Let us call instances of R 1 , R 2 or R 3 that appear outside a chain

for some i and t 1 , t 2 ∈ M "unmarked". Do the following for the smallest i that is an unmarked instance of R 3 ( we will call the instance of R 3 ri 3 and suppose it is applied from S i-1 to S i ): Apply ri 3 after j < i such that S j-1 to S j is the first unmarked instance of R 2 , for some q and ỹ, i. e., this instance produces a fact state q•1 (ỹ, ỹ ) and a fact Ack(t 1 , t 2 ). Since there is no rule between j and i that might consume Ack(t 1 , t 2 ) (only rules of form R 3 do, and ri 3 is the first unmarked instance of such a rule) and since ri 3 does not consume state q•1 (ỹ, ỹ ), we can move ri 3 between j and j + 1, adding the conclusions of ri 3 and removing the premises of ri 3 from every S j+1 , . . . , S i . Note that unmarked instances of R 2 and R 3 are guaranteed to be preceeded by a marked R 1 , and therefore only remove facts of form Ack(. . .) or Msg(. . .) that have been added in that preceeding step. Since the transition at step j requires a fact Msg(t 1 , t 2 ), there is an instance of R 1 prior to j, say at k < j, since only rules of form R 1 produces facts labelled Msg(t 1 , t 2 ). Since ri 3 is now applied from S j to S j+1 , we have that an instance ri 1 of a rule of form R 1 that produces state semi p ( t) must appear before j, i. e., ri 1 ∈ ginsts( P =p ). Therefore, it produces a fact Msg(t 1 , t 2 ) indeed. We choose the largest k that has an unmarked R 1 that produces Msg(t 1 , t 2 ) and state semi p ( t) and move it right before j, resulting in the following msr execution:

We apply this procedure until it reaches a fixpoint and call the resulting trace

(3) n (3) Since no rule moved during the procedure has an action,

4. If the last transition is in { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }, we remove it. Repeat until fixpoint is reached and call the resulting trace

n (4) Since no rule removed during the procedure has an action,

1 , . . . , E

n (4) ] α.

If there is

n (4) -1 , then there is a transition where In(t) is produced and never consumned until n (4) -1. The only rule producing In(t) is MDIN. We can move this transition to just before n (4) -1 and call the resulting trace

(5) n (5) Since [E

α, especially α inev , there is no action that is not in F res between the abovementioned instance of MDIN, therefore, hide

n (5) ]) holds. Since α inev is the only part of α that mentions K, and since the tranformation preserved α inev , we have that [E

The next proposition states that normal executions have a kind of prefix closure. Normality is preserved when removing a prefix, except if the prefix ends in the middle of an internal communication or with an action in { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH }. In that case removing some additional actions will provide a normal execution. Proposition 3. If P is a ground process and ∅

INIT,MDIN S m , or, if there is an Ack-fact in S n-1 \S n , we will chose the largest m < n-2

since otherwise there would be a larger m.

We will now show that the prefixes of the execution until m are normal.

-Item 1 of Definition 21 is preserved as in both cases m ≥ 1.

-

, implies item 2 of Definition 21, as none of the rules in R = { MDOUT, MDPUB, MDFRESH, MDAPPL, FRESH } remove Ackor state semi -facts, and the chain of rules R 1 , R 2 , R 3 consumes as many as it produces. Thus, if they where in S m , they would be in S n , too.

-Items 3 and 5 of Definition 21 hold for all parts of the trace, and therefore also for the prefix of size m. -Item 4 of Definition 21 holds trivially since

Definition 22. Let P be a ground process, P be a multiset of processes and S a multiset of multiset rewrite rules. We write P P S if there exists a bijection between P and the multiset {state p ( t) | ∃p, t. state p ( t) ∈ # S} # such that whenever Q ∈ # P is mapped to state p ( t) ∈ # S, then:

1. state p ( t) ∈ E prems(R) for R ∈ ginsts( P =p ). 2. Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then

for a substitution τ , and a bijective renaming ρ of fresh, but not bound names in Q, defined as follows:

is normal (see Definition 21) and [E 1 , . . . , E n ] α (see Definition 15), then there are (E 0 , S 0 , P 0 , σ 0 , L 0 ), . . . , (E n , S n , P n , σ n , L n ) and F 1 , . . . , F n such that:

where (E 0 , S 0 , P 0 , σ 0 , L 0 ) = (∅, ∅, ∅, { P }, ∅, ∅) and there exists a monotonically increasing, surjective function f :

The Lemma indeed implies that { tr ∈ hide(filter (traces msr ( P ))) | tr is normal } ⊆ traces pi (P ): for any normal trace [E 1 , . . . , E n ] that satisfies α, i.e. in filter (traces msr ( P )) we show there exists a trace [F 1 , . . . , F n ] ∈ traces pi (P ) such that hide([E 1 , . . . ,

Proof. We proceed by induction over the number of transitions n.

Base Case. A normal msr execution contains at least an application of the init rule, thereby the shortest normal msr execution is

We chose n = 0 and thus

To show that Condition 3 holds, we have to show that P 0 P { state [] () } # . Note that P 0 = { P } # . We choose the bijection such that P

From the induction hypothesis, and since E m+1 , . . . , E n = ∅, we have that

From the induction hypothesis, and since no rule producing Out-facts is applied between step m and step n, we have that

Then, by Lemma 8 and Lemma 9, we have that νE n , r.σ n t. Therefore, νE n .σ n t. This allows us to chose the following transition:

Conditions 1 to 7 hold trivially.

Case: ri = [state p ( t)] -[]→ [] (for some p and t). By induction hypothesis, we have P n P S m , and thus, as previously established,

Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = 0. We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

Condition 3 holds since Q ↔ state p ( t), P n +1 = P n \ # { 0 } # and S n = S n-1 \ # { state p ( t) } # . Conditions 1, 2, 4 and 6 hold trivially.

] (for some p and t). By induction hypothesis, we have P n P S m , and thus, as previously established,

Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since

We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q 1 ↔ state p•1 ( t) and Q 2 ↔ state p•2 ( t). Therefore, and since Q ↔ state p ( t), Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = !Q for a process

We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q P state p•1 ( t). Therefore, and since

Conditions 1, 2, 4 and 6 hold trivially.

Case: ri = [state p ( t), Fr(a : fresh)] -[ ProtoNonce(a : fresh) ]→ [state p•1 ( t, a : fresh)] (for some p, t and a ∈ F N ). By induction hypothesis, we have P n P S m , and thus, as previously established,

Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = ν a; Q for a name a ∈ F N and a process

By definition of exec msr , the fact Fr(a ) can only be produced once. Since this fact is linear it can only be consumed once. Every rule in P that produces a label ProtoNonce(x) for some x consumes a fact Fr(x). Therefore,

The induction hypothesis allows us to conclude that a / ∈ E n ,i. e., a is fresh. We therefore chose the following transition:

Since [E 1 , . . . , E n ] α, and thus [E 1 , . . . , E m ] α pred , σ pr t 1 / x 1 , . . . , t l / x l is satisfied. We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q 1 ↔ state p•1 ( t). Therefore, and since

we have that Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since

We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q ↔ state p•1 ( t). Therefore, and since insert t 1 , t 2 ; Q ↔ state p ( t),

Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since

We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q ↔ state p•1 ( t). Therefore, and since delete

is the last element of the trace. Conditions 1, 4, 5 and 6 hold trivially.

)] (for some p, t and t 1 , t 2 ∈ M). By induction hypothesis, we have P n P S m , and thus, as previously established, P n P S n-1 . Let Q ∈ # P n such that Q P state p ( t). Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = lookup t 1 as v in Q 1 else Q 2 for some variable V , and two processes

Since [E 1 , . . . , E n ] α in , there is an i < n such that Insert(t 1 , t 2 ) ∈ E E i and there is no j such that i < j < n and Delete(t 1 ) ∈ E E j or and Insert(t 1 , t 2 ) ∈ E T E j . Since E m , . . . , E n = ∅, we know that i < m. Hence, by induction hypothesis, S n (t 1 ) = t 2 . We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that

] and ρ = ρ). Therefore, and since lookup t Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = lookup t 1 as v in Q 1 else Q 2 for a variable v and two processes

Since [E 1 , . . . , E n ] α notin , there is no i < n such that Insert(t 1 , t 2 ) ∈ E E i and there is no j such that i < j < n and Delete(t 1 ) ∈ E E j or and Insert(t 1 , t 2 ) ∈ E T E j . Since E m , . . . , E n = ∅, we know that holds j < m. Hence, by induction hypothesis, S n (t 1 ) is undefined. We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q 2 ↔ state p•2 ( t). Therefore, and since lookup t Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since Q = P | p τ ρ, we can deduce that Q = lock l t; Q for

Since [E 1 , . . . , E n ] α lock , for every i < n such that Lock (l p , t) ∈ E E i , there a j such that i < j < n and Unlock (l p , t) ∈ E E j , and in between i and j, there is no lock or unlock, i. e., for all k such that i < k < j, and all l i , Lock (l i , t) / ∈ E E k and Unlock (l i , t) / ∈ E E k . Since E m , . . . , E n = ∅, we know that this holds for i < m and j < m as well. By induction hypothesis, Condition 5, this implies that t ∈ E L n . We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q ↔ state p•1 ( t). Therefore, and since lock l t; Q ↔ state p ( t), Let θ be a grounding substitution for state p (x) ∈ prems( P =p ) such that t = xθ. Then θ induces a substitution τ and a bijective renaming ρ for fresh, but not bound names (in Q) such that P | p τ ρ = Q (see Definition 22).

From the form of the rule R, and since

We therefore chose the following transition:

We define f as on page 62. Therefore, Conditions 1 to 7 hold for i < n -1. It is left to show that Conditions 1 to 7 hold for n.

By definition of P and P =p , we have that Q ↔ state p•1 ( t). Therefore, and since unlock l t; Q ↔ state p ( t),

We show that Condition 5 holds for L n +1 = L n \ { t }: For all t = E t, t ∈ E L n ⇔ t ∈ E L n +1 by induction hypothesis. If t ∈ E L n , then ∀j ≤ m, u.Lock(u, t) ∈ E E j → ∃j < k ≤ n.Unlock(u, t) ∈ E E k . Since we have E m , . . . , E n-1 = ∅ and E n = { Unlock(n l , t) } # , we can strengthen this to ∀j ≤ n, u.Lock(u, t) ∈ E E j → ∃j < k ≤ n.Unlock(u, t) ∈ E E k , which means that the condition holds in this case. If t ∈ E L n , then ∃j ≤ n, u.Lock(u, t) ∈ E E j ∧ ∀j < k ≤ n.Unlock(u, t) ∈ E E k and since E m , . . . , E n-1 = ∅ and E n = { Unlock(n l , t) } # , a contradiction to Condition 5 would constitute of j and u = E n l such that Lock(u, t) ∈ E E j and ∀j < k ≤ n.Unlock(u, t) ∈ E E k .

We will show that this leads to a contradiction with [E 1 , . . . , E n ] α. Fix j and u. By definition of P and well-formedness of P , there is a p l that is a prefix of p such that P | q l = lock l t; Q for the same annotation l and parameter t. The form of the translation guarantees that if state p ( t) ∈ S n , then for some t there is i ≤ n such that state p ( t ) ∈ S i , if p is a prefix of p. We therefore have that there is i < n such that E i = E { Lock(n l , t) } # . We proceed by case distinction: Case 1: j < i (see Figure 24). Case 2: i < j (see Figure 25). By definition of P , there is no parallel and no replication between p l and p. Note that any rule in P that produces a state named state q for a non-empty q is such that it requires a fact with name state q for q = q • 1 or q = q • 2 (in case of the translation of out, it might require state semi q , which in turn requires state q ). Therefore, there cannot be a second k = n such that Unlock(n l , t) ∈ E E k (since n l was added in a Fr-fact in to S i ). This means in particular that there is not k such that i < k < n and Unlock(n l , t) ∈ E E k . Therefore, [E 1 , . . . , E n ] α lock . Conditions 1, 2, 4 and 6 hold trivially.

B.4. Proof of Lemma 1: putting the pieces together Lemma 1. Let P be a well-formed ground process. We have that traces pi (P ) = hide(filter (traces msr ( P ))).

Proof. From Lemma 10, we can conclude that traces pi (P ) ⊆ { hide(t)|tr ∈ traces msr ( P ) and tr α } = hide(filter (traces msr ( P ))).

From Lemma 11, we have that hide(filter (traces msr ( P ))) = { tr ∈ hide(filter (traces msr ( P ))) | tr is normal }.

From Lemma 12, we can conclude that { tr ∈ hide(filter (traces msr ( P ))) | tr is normal } ⊆ traces pi (P ), and hence hide(filter (traces msr ( P ))) ⊆ traces pi (P ).