Vincent Cheval

Charlie Jacomme

Steve Kremer

Robert Künnemann

Sapic + : protocol verifiers of the world, unite!

Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With Sapic + , we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from Sapic to Tamarin, and extend it with automated translations from Sapic + to ProVerif and DeepSec, as well as powerful, protocol-independent optimizations of the existing translation. We prove each part of these translations sound. A user can thus, with a single Sapic + file, verify reachability and equivalence properties on the specified protocol, either using ProVerif, Tamarin or DeepSec. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models. This includes a large case study of the 5G authentication protocols, previously analyzed in Tamarin. Encoding this model in Sapic + we demonstrate the effectiveness of our approach. Moreover, we study four new case studies: the LAKE [46] and the Privacy-Pass [20] protocols, both under standardization, the SSH [47] protocol with the agent-forwarding feature, and the recent KEMTLS [45] protocol, a post-quantum version of the main TLS key exchange.

Foreword. This paper is the long version of the version presented at USENIX'22. It is globally more formal and more detailed, especially in Sections 3 to 5. For a first read, we recommend the conference version. * If #P 2 ≤ 1, then P 2 = {s 2 }, and m can be executed at the position of l.

* If #P 2 > 1 ∧ Out ∈ R 1 , the difficulty would be if In 2 ∈ P 2 , but by E 1 ̸ = ∅ and (iv) this is impossible, and m can be executed at the position of l.

Introduction

By leveraging automated reasoning techniques and a symbolic abstraction of cryptographic primitives, protocol verification tools, such as ProVerif and Tamarin, have reached a high degree of maturity in the last decades. Precise models of real-world protocols like TLS 1.3 [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1[END_REF][START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF], 5G authentication protocols [START_REF] Basin | A formal analysis of 5g authentication[END_REF], WPA 2 [START_REF] Cremers | A formal analysis of IEEE 802.11's WPA2: Countering the kracks caused by cracking the counters[END_REF], Noise [START_REF] Kobeissi | Noise explorer: Fully automated modeling and verification for arbitrary noise protocols[END_REF][START_REF] Girol | A spectral analysis of noise: A comprehensive, automated, formal analysis of diffiehellman protocols[END_REF] and Signal [START_REF] Cohn-Gordon | A formal security analysis of the signal messaging protocol[END_REF][START_REF] Kobeissi | Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach[END_REF], show these tools can be used to great effect. However, such case studies tend to only be carried out by experts of the corresponding tool and often at the cost of significant efforts. Further, although multiple tools have very different strength and weaknesses, they have yet to be used in collaboration.

A closer look at the development workflow reveals why. First, even specification languages that are very similar on the surface, e.g., the Sapic front end [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] to Tamarin [START_REF] Schmidt | Automated analysis of diffie-hellman protocols and advanced security properties[END_REF] and ProVerif's applied π calculus [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF] require different modeling regimes, e.g., when storing or receiving values, setting locks or parsing network messages. In practice, this makes it very hard to switch between tools, even if they share many syntactic elements.

Second, deciding which tool to target in the first place is even harder. Powerful abstractions deployed by ProVerif generally offer better automation and speed than Tamarin, but may lead in some cases to false attacks or hinder attack reconstruction. In cases where neither a proof nor an attack is found expert knowledge, with a good understanding of ProVerif's internals, is required to guide the proof. Tamarin on the other hand guarantees correctness, hence, no false attacks, in case of termination. Tamarin also provides a GUI to interactively guide the proof search when automated search does not terminate. Experts may also write so-called oracles to automate such guidance. Another aspect that may guide the choice of the tool is the support for cryptographic primitives. Both tools provide the possibility for user-defined primitives, with slightly different, incomparable scopes. In particular, Tamarin has builtin support for several theories that feature an associative, commutative operator and therefore offers a more precise for modeling Diffie-Hellman exponentiation and exclusive or (xor). Given all of these parameters, the choice of the right tool requires not only insight into the protocol, but insight into the modeling strategy.

Third, these requirements change during development. As protocol modeling is an incremental process, it may for instance be desirable to use a simplified Diffie-Hellman theory in the early stages. Throughout the development, it is vital to perform sanity checks, i.e., to find honest traces that show the protocol can execute and thus spot bugs in the model before starting time-consuming proofs. While ProVerif is often faster in finding proofs, it can sometimes struggle to show the existence of 'good' traces. Given the radically different reasoning techniques underlying these two tools it is hard to predict which one will perform better on a given protocol. On a same protocol, one tool may even be capable of proving one property, but not another, while the other tool has the reverse capabilities.

In this work, we aim at exploiting the strengths of each of the tools. Therefore, we design a common input language, called Sapic + , which may be used as an input for several tools: Tamarin, ProVerif, GSVerif [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF], and DeepSec [START_REF] Cheval | DEEPSEC: deciding equivalence properties in security protocols theory and practice[END_REF]. Sapic + is an extension of Sapic (which only translated to Tamarin and did not support equivalence-based properties) that can be automatically translated to each of these tools, thus removing the need to choose and making these tools more accessible. While current protocol models only target one of these tools, a common platform encourages the implementation of tool-specific encodings in a model-agnostic manner, which promises consistent verification results even for users who are oblivious to the underlying reasoning technique which is necessary for wide adoption. We believe that this approach has a number of advantages. [START_REF]Sapic+ tool chain[END_REF] The distinctive features of each tool are available for the same model while sidestepping many encoding pitfalls (such as subtle differences in the semantics for similar syntactic constructs) that one would encounter when porting manually an existing model to another tool. Moreover, even though we generate the specification for each particular tool, we maintain the possibility for experts to guide the tools. We illustrate this fact on the 5G case study [START_REF] Basin | A formal analysis of 5g authentication[END_REF]: we are able to use oracles to provide termination for Tamarin. Moreover, unlike Sapic, we support the verification of equivalence properties through ProVerif, and above all DeepSec, a tool that specializes in these properties. [START_REF] Tamarin | [END_REF] An essential part of our work is that we formally prove the correctness of the translations, which enables a workflow that can take advantage of each of these tool's strengths throughout model development on the same input file. Lemmas proven in one verifier can be used as assumptions in the other, potentially increasing the scope of verification. Again, on the 5G case study, we show that several attacks can be recovered much faster using ProVerif. On the other hand, we are able to use Tamarin to prove axioms assumed by ProVerif, removing the need to prove correctness of these lemmas by hand on some examples.

(3) Similar to Isabelle's Sledgehammer, multiple verifiers can be run in parallel, terminating when any of them does. This is especially useful when it is not clear if security is provable or an attack can be found, or when the user is unsure which verifier is most suited for the lemma at hand. (4) Finally, for researchers, Sapic + provides a convenient target for meta-theories and encodings. Existing results (e.g., distance-bounding [START_REF] Mauw | Distance-Bounding Protocols: Verification without Time and Location[END_REF] or human errors [START_REF] Basin | Modeling Human Errors in Security Protocols[END_REF]) could cover a wide set of tools rather than being developed for a single tool. Source-to-source encodings in applied-π-like calculi (e.g., [START_REF] Jacomme | Symbolic models for isolated execution environments[END_REF][START_REF] Künnemann | Automated verification of accountability in security protocols[END_REF][START_REF] Kobeissi | Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach[END_REF]) translate with relatively little work.

Contributions We can summarize our contributions as follows.

1. Translations: we provide provably correct translations from Sapic + to both ProVerif (supporting stateful reasoning by using ProVerif's GSVerif frontend) and DeepSec and extend the existing translation to Tamarin. Our translations cover both protocol and property specification. In addition, unlike Sapic, we support privacy-type properties expressed as process equivalences in DeepSec (verifying trace equivalence) and ProVerif (verifying diff equivalence, which implies trace equivalence). The translations' correctness proof guarantees that results from one tool carry over to any of the other tools as explained above. Our proofs also relate ProVerif's and Tamarin's security property languages in terms of expressivity, showing subtle differences that even experts of one of the tools may not be aware of.

2. Protocol-platform: we automate these translations by integrating Sapic + (including [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]) directly into Tamarin to improve visual feedback in manual, interactive proofs, and include a(n optional) type system, similar to that of ProVerif, to catch modeling errors in development. This allows to easily use the different tools from a single input file and exploit the strengths of each of the tools, avoiding the time-consuming and potentially error-prone process of carrying over models.

3. Extensions and optimizations of Sapic: we extend the scope and efficiency compared to Sapic [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]. We encode support for destructor symbols, let-bindings and macro declarations in Sapic's translation procedure to Tamarin. We also introduce a compression technique to reduce the size of the models produced by the translation, prove its correctness and demonstrate its efficiency. Our case studies show that this significantly increases the scope of Sapic + , enabling the verification of larger and more realistic protocol models.

4.

Case studies: we evaluate the new development workflow on four entirely new protocol models: KEMTLS, Privacy-Pass, LAKE and SSH with agent forwarding. We also demonstrate that existing case studies would have benefited from being directly analyzed in Sapic + without loss of efficiency. In particular, we ported an existing Tamarin model of the complex 5G authentication protocols case study [START_REF] Basin | A formal analysis of 5g authentication[END_REF] to Sapic + : we observe that the dedicated, handwritten oracles used to automate the proofs in Tamarin carried over straightforwardly, and verification time was preserved, showing the efficiency of the generated model. Moreover, using ProVerif, with a less precise, but attack preserving modeling of xor, we detected the existing attacks in a completely automated way, and much faster.

Related Work

The AVISPA [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF] and, its successor, AVANTSSAR projects [START_REF] Armando | The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures[END_REF] pioneered the protocol platform approach. They provide a front end for modeling protocols that allows to use different tools to verify security properties. However, the expressiveness and efficiency of these back-ends lack in comparison to the more recent Tamarin and ProVerif. Also, contrary to our work, the translations were not formally proven correct, limiting the interaction between the backends.

Other works have taken a different approach by developing front ends for a single tool to make it more expressive (e.g., [START_REF] Pedroza | AVATAR: A sysml environment for the formal verification of safety and security properties[END_REF][START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF][START_REF] Basin | Alice and bob meet equational theories[END_REF]). Similarly, many other independent tools enable automatic protocol verification (see [START_REF] Barbosa | Sok: Computer-aided cryptography[END_REF] for an almost extensive presentation), but we believe that they have not yet reached Tamarin's and ProVerif's level of maturity and adoption by the community.

Outline We provide some general background about the symbolic model and the multiple tools we rely on in Section 2. We then define the Sapic + language in Section 3, before describing the translations and their optimizations for Tamarin in Section 4 and ProVerif in Section 5. We finally showcase the tool and our case studies in Section 6. An understanding of the more formal definitions of Section 3 is neither needed to understand at a high-level the remainder of the paper nor to use the tool.

Background

In this section, we provide background on symbolic methods for the verification of cryptographic protocols. We first explain how messages and cryptographic primitives are represented using a term algebra. We then review the different verification tools that are relevant for this work.

Modeling messages as terms

Terms and substitutions Messages sent in a protocol execution are modeled as terms. Fresh values are modeled by constants from an infinite set of names N , divided into public (attacker) names N pub and secret (protocol) names N priv . We also assume a set of variables X . Terms are then built over names in N , variables in X and applications of a function symbols in F on terms. We consider two kinds of function symbols, i.e., F = F c ⊎ F d , for constructor and destructor function symbols. Consider for example the term enc(m, k) modeling the encryption of another term m with the secret key k: encryption is modeled by the constructor function enc ∈ F c , k ∈ N priv is a secret name and m is another term.

A substitution σ is a function from variables to terms. We lift the application of substitutions from variables to terms and use postfix notation, i.e., we write tσ for the term in which we replace each variable x occurring in the domain of σ and in t by σ(x).

Equational theories and rewrite systems Properties of constructor terms, i.e., terms containing no destructor symbol, are expressed by an equational theory E, which is defined by a set of equations (t 1 = t 2 ) on name-free constructor terms. This induces a relation = E on constructor terms, defined as the smallest equivalence relation = E that contains all t 1 = t 2 ∈ E, is closed under substitution of variables for constructor terms, and application of function symbols. For example, dec(enc(x, y), y) = x models functional correctness of an encryption scheme. An equational theory for DH exponentiation could include (among others) the equations exp(exp(g, a), b) = exp(g, a • b)

and a • b = b • a.
The semantics of destructor symbols is defined through a set of rewrite rules of the form d(t 1 , . . . , t n ) → r where d ∈ F d of arity n and the t i s are name-free constructor terms. Terms are rewritten bottom-up modulo the equational theory E to ensure that destructors are only applied to constructor terms. We require that the resulting rewrite system is convergent modulo E, meaning that (roughly speaking) any term t has a normal form modulo E, which we denote by t↓ . For example, assuming that dec ∈ F d is a destructor, we can define the rule dec(enc(x, y), y) → x. Then, assuming the equational theory for DH from above, dec(enc(m, g a•b ), g b•a ) rewrites into m, as g a•b = E g b•a . When a term t contains a destructor symbol that does not rewrite, we say that the destructor fails, and we write t → E fail. Note that the decryption of an invalid ciphertext (here modeled as a random value n) dec(n, k) would fail. Finally, we lift = E to arbitrary terms and define

t 1 = E t 2 to hold if t 1 ̸ → E fail ∧ t 2 ̸ → E fail ∧ t 1 ↓ = E t 2 ↓ .
Patterns We define the set of patterns Pat ⊆ T (F c , N , X ) to be a subset of terms. Patterns define the terms against which we can perform pattern matching in let constructs and protocol inputs. Typically, Tamarin allows matching against arbitrary terms. ProVerif, on the other hand, only allows executable patterns, that is patterns where the variables to be bound can only directly occur under data constructors. A data constructor is a function for which there exist destructors that allow to access each of its arguments. Tuples are a typical example. We denote the set of executable patterns Pat ex (). In the DeepSec tool, the only data functions are built-in tuples.

The Tamarin prover

Protocol specification In Tamarin protocols are described using multiset rewrite (MSR) rules of the form

[lhs] -[ actions ]→ [rhs].
They describe the manipulation of the protocol state represented as a multiset of facts. Intuitively, for such a rule to fire, we require the (multiset of) facts on the left-hand side lhs. Then these facts are deleted, and the facts on the right-hand side rhs are added. The actions are facts that annotate this rule, and will be used to specify properties. As an example, consider the following 3 rules.

R 0 : [Fr(lk)] -[]→ [!SP(lk), !SQ(lk)] R P : [SP(lk), Fr(k)] -[ Honest(k) ]→ [Out(enc(⟨key, ′ hs ′ ⟩, lk))] R Q : [SQ(lk), In(enc(⟨k, ′ hs ′ ⟩, lk))] -[ Accept(k) ]→ []
In rule R 0 we require a fresh long-term key lk, shared between P and Q, and move these two parties into the states SP(lk) and SQ(lk), respectively. Whenever P is in state SP and we have a fresh session key k, then P may output the term enc(⟨k, ′ hs ′ ⟩, lk) where ′ hs ′ is a constant. During this transition, the key k is tagged as an honest key. Q on the other hand, when in state SQ(lk) and with an available input matching enc(⟨k, ′ hs ′ ⟩, lk), can accept key k. The facts Fr(•), In(•) and Out(•) are built-in facts. The fresh fact Fr(•) is always available, but guarantees that its argument is instantiated with a fresh name, i.e., a name that did not appear elsewhere, modeling the generation of a random key. In(•) and Out(•) facts provide the network interface.

As we assume that the network is controlled by the attacker, creating a fact Out(t) adds t to the attacker knowledge; conversely, In(t) requires the attacker to construct a term that matches t. When we generated the facts SP(lk) and SQ(lk) we preceded them by '!', marking them as permanent. They are available an unbounded number of times, modeling that P and Q can execute an arbitrary number of sessions with the long-term key lt, generating a fresh session key k each time.

Equational theories In Tamarin, cryptographic primitives can be specified by an arbitrary equational theory that is convergent and has the finite variant property. Introducing these notions goes beyond the 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][START_REF] Dreier | Beyond subterm-convergent equational theories in automated verification of stateful protocols[END_REF]. In addition, Tamarin offers built-in support for several other operations, including DH exponentiation and exclusive or.

Tamarin allows to pattern match any term in its inputs, but does not support destructors.

Property specification Tamarin uses a temporal logic to express security properties about the possible protocol executions, which are modeled as traces. Traces are simply the sequence of actions triggered by MSR rules. We can write lemmas that must be valid on all traces. For instance, to express in our previous example that, whenever Q accepts a key k, k must have been honestly generated by P . This can be written as:

All k #i.Accept(k)@i =⇒ Ex #j.Honest(k)@j & j < i
More precisely, we require that if an Accept event was raised for k at any time point i of the trace, then the Honest event must have been raised for the same value k at a previous time point j. We can also write restrictions, which constrain the set of traces considered when proving security properties. In our example, it could be used to only focus on traces with at most one successful session of Q by writing:

All k l #i #j.Accept(k)@i & Accept(l)@j =⇒ #i=#j
Automation To automatically find proofs, Tamarin tries to refute the existence of a counterexample by negating the property and exploring in a backward search all paths that would lead to this negated formula. The reasoning is done symbolically, based on a dedicated constraint solving algorithm. If the tool can prove that no such path exists, the property is valid. The proof search may, however, not terminate. In such cases, the user can guide the backward search in interactive mode, or (requiring more advanced knowledge) specify tailored heuristics through so-called oracles.

ProVerif

Protocol specification In ProVerif protocols are expressed in a dialect of the applied π calculus. As an example consider the protocol described in Figure 1, similar to the example given for Tamarin. We define two agents P and Q, parameterized by a long-term secret key 'lk and for P a fresh session key k as well. The main process is described on line 13: the ! operator allows to spawn an unbound number of sessions, and in each session we sample a fresh value k thanks to the new instruction. On line 3, P outputs (on channel c) an encryption with 'lk of the key on the network. ! may input a ciphertext, and check if decryption succeeds and whether the plaintext is of the expected form <k ,'hs'>. If so, it raises a success event and sends a success message. Else, it outputs an error message.

Equational theories As for Tamarin, cryptographic primitives can be specified using arbitrary convergent equational theories that have the finite variant, but in ProVerif, no associativecommutative symbols are allowed, such as required for DH exponentiation or exclusive. However, ProVerif additionally allows for so-called linear equations (where each variable appears at most once on the left-hand and on the right-hand side). This allows to approximate DH exponentiation by the equation (g x ) y = (g y ) x for a constant g. Moreover, ProVerif supports the definition of destructor symbols, hence allowing a convenient way to model that some function applications may fail.

Property specification Properties on traces can be expressed by means of (injective) correspondence queries. E.g., query event(Accept(x) =⇒ event(Honest(x))

expresses that whenever (an instance of) the event Accept(x) executes, the event Honest(x) must have been executed before (with the same value for x). If the query is specified to be injective we require that each Accept(x) can be matched by a distinct Honest(x).

Moreover, ProVerif offers support for properties expressed in terms of indistinguishability, i.e., by specifying that two protocols cannot be distinguished by an attacker. Continuing our example, we could specify strong secrecy of k as a non-interference property, encoded as an equivalence. ProVerif can then be used to prove this equivalence: Intuitively, even if the attacker chooses two session keys k 1 and k 2, it is unable to distinguish which one was used. Similarly, we could model unlinkability: can the attacker distinguish the case where all sessions of P and Q have the same shared secret key from the scenario where each pair of sessions has a distinct key? This property does, in fact, not hold. Moreover, ProVerif is unable to conclude, returning cannot be proved. This comes in particular from the fact that ProVerif tries to prove a very strong form of equivalence, dubbed diff-equivalence which is not satisfied on this example.

Automation Internally, ProVerif translates the protocol specification into a particular form of first-order logic formulas, called Horn clauses. It then uses a resolution algorithm that simplifies these clauses in such a way that the security property can be verified on this simplified form. The verification in ProVerif is generally much faster than in Tamarin. This is in particular due to the fact that the translation from the applied π calculus into Horn clauses introduces (sound) abstractions: in addition to nontermination the tool may sometimes fail and find neither a proof nor an attack. This problem occurs in particular when protocols maintain a global, mutable state, i.e., different protocol sessions update this state. Recently, the GSVerif front end significantly improved on this limitation building on the following simple, but effective idea: rather than verifying the formula ϕ, GSVerif verifies whether 'ϕ or some action that should occur only once occurred twice' by automatically adding protocol annotations and transforming queries accordingly.

DeepSec

DeepSec specializes in indistinguishability properties, notably trace equivalence. Protocols are described in basically the same language as ProVerif, but without replication, hence limiting verification to a bounded number of sessions. On the flip side, DeepSec provides a decision procedure, ensuring termination (in theory-in practice the tool may run out of resources on large instances). Therefore, when ProVerif does not terminate or is inconclusive, we can use DeepSec, but we must bound the number of replications. Continuing our example, this would correspond to: let scen1 = new sk ; !^3(new key ; P(sk ,key ) | Q(sk )). let scen2 = !^3(new sk ;(new key ; P(sk ,key ) | Q(sk ))). query trace_equiv(scen1,scen2).

where we check the equivalence for three sessions. DeepSec is indeed able to reconstruct an attack trace. Note that ProVerif may sometimes be unable to prove the equivalence even when the processes are equivalent, as it verifies a stricter form of equivalence than DeepSec. This happens for instance on the Basic Access Control (BAC) protocol implemented in the electronic passport [START_REF]PKI for machine readable travel documents offering ICC read-only access[END_REF].

Regarding equational theories, DeepSec provides support for a class of subterm convergent destructor theories, a class strictly included in those of ProVerif.

Sapic

In Sapic, protocols are described in a stateful dialect of the applied π calculus, including constructs for manipulating global, mutable state and for acquiring locks to manipulate this state concurrently. These processes are translated into Tamarin. The property specification language is exactly that of Tamarin. As a result, Sapic inherits the strengths of Tamarin, but also its limitations. In particular, Sapic does neither support destructors nor equivalence properties. Moreover, the generated MSR rules sometimes add a performance overhead.

The Sapic + language

We describe here in more detail the Sapic + language (which builds on Sapic [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF][START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]). The added features include the possibility to define destructors, i.e., function symbols whose application may fail (see below), let bindings with pattern matching and else branches and a slightly modified semantics suitable for expressing equivalence properties.

Before defining Sapic + 's language more formally, we give a short overview of its main features.

Overview

Protocol specification Sapic + 's syntax for specifying protocols is an applied π calculus similar to ProVerif and Sapic; Fig. 1 is actually a valid Sapic + example. Compared to Sapic, the added features include the definition of destructors, i.e., function symbols whose application may fail (see below), let bindings with pattern matching and else branches.

Equational theories Through its exports, Sapic + supports the union of the theories supported by Tamarin and ProVerif. When exporting a theory like DH exponentation to ProVerif (which only has partial support for this theory), we export an abstraction of the theory, that can still be useful.

Property specification Sapic + supports reachability properties expressed in the same logic as Sapic and Tamarin, but additionally translates and exports them to ProVerif's query language. Further, Sapic + supports equivalence properties that can be expressed similarly to ProVerif and DeepSec.

Automation Sapic + automatically translates to ProVerif, Tamarin and DeepSec, and thus benefits from the automation of each of those backends. In contrast to Sapic, which was a stand-alone preprocessor, Sapic + is integrated into Tamarin. This improves user interaction, as now Sapic + -generated rules display as process actions in interactive proofs and error reporting is more precise. Moreover, it aids future development, as the Sapic + module interfaces directly with Tamarin's term theory and parser, benefiting from new developments. Most importantly, we significantly improved on Sapic's level of automation, first through several (provably correct) optimizations for the translation to Tamarin and second with the addition of translations to ProVerif and DeepSec. Both improvements are illustrated by our case-studies, notably 5G-AKA.

Extra features Sapic + naturally inherits previous extensions to Sapic (e.g., a local-progress semantics, needed to show liveness-like properties [START_REF] Backes | A novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange[END_REF]). Direct encodings in Sapic (e.g., SGX reports [START_REF] Jacomme | Symbolic models for isolated execution environments[END_REF] or accountability [START_REF] Künnemann | Automated verification of accountability in security protocols[END_REF]) translate for free, and become available in ProVerif for the first time.

Modeling messages as terms

Terms and substitutions. We model the messages sent in a protocol execution as terms.

Terms are built using a set of function symbols F, each with an arity n. Moreover, we suppose that F = F c ⊎ F d for constructor and destructor functions. Fresh values are modeled by constants from an infinite set of names N , divided into public (attacker) names N pub and secrets (protocol) names N priv . We also assume a set of variables X . Given F ⊆ F, N ⊆ N and X ⊆ X we denote by T (F, N, X) the set of terms built over functions in F, names in N and variables in X.

A substitution σ : X → T (F, N , X ) is a function from variables to terms. We homomorphically lift the application of substitutions from variables to terms and use postfix notation, i.e., we write tσ for the term in which we replace each variable x occurring in the domain of σ and in t by σ(x).

Equational theories and rewrite systems Properties of constructor terms, i.e., terms containing no destructor symbol, are expressed by an equational theory E, defined by a set of equations (t 1 = t 2 ) such that t 1 , t 2 ∈ T (F c , ∅, X ). This induces a relation = E on constructor terms, defined as the smallest equivalence relation = E that contains all t 1 = t 2 ∈ E, is closed under substitution of variables for constructor terms, and application of function symbols. An equational theory for DH exponentiation could include (among others) the equations exp(exp(g, a)

, b) = exp(g, a • b) and a • b = b • a.
The semantics of destructor symbols is defined through a set of rewrite rules E D of the form d(t 1 , . . . , t n ) → r where d ∈ F d of arity n and t i ∈ T (F c , ∅, X ). As usual, we denote that t 1 rewrites to t 2 by t 1 → t 2 and write t → E u when t contains a single destructor d and t

= d(t 1 , . . . , t n ) rewrites to u modulo E, i.e., t → E u iff d(v 1 , . . . , v n ) → v for some constructor terms v 1 = E t 1 , . . . , v n = E t n and v = E u.
Terms with several destructors are rewritten bottom-up to ensure that we only rewrite destructors applied to constructor terms. We require that the resulting rewrite system is convergent modulo the equational theory E and denote by t↓ the normal form of t (up to E). When a term contains a destructor symbol that does not rewrite, we say that the destructor fails. We suppose that protocols only send valid messages which we capture using the Msg predicate: we define Msg(t) to hold if for any subterm u of t we have that u↓ ∈ T (F c , N , X ). For example, a symmetric encryption scheme that provides ciphertext integrity could be modeled by the rule dec(enc(m, k), k) → m. Note that the decryption of an invalid ciphertext (here modeled as a random value n) dec(n, k) would fail.

Finally, we lift = E to arbitrary terms and define

t 1 = E t 2 to hold if Msg(t 1 ) ∧ Msg(t 2 ) ∧ t 1 ↓ = E t 2 ↓ .
Patterns Finally we define the set of patterns Pat ⊆ T (F c , N , X ) to be a subset of terms. Patterns define the terms against which we can perform pattern matching in let constructs. Typically, Tamarin allows matching against arbitrary terms. ProVerif, on the other hand, only allows executable patterns, that is patterns where the variables to be bound can only directly occur under data constructors. A data constructor is a function f of arity n for which there exist n destructors d i defined by d i (f (x 1 , . . . , x n )) → x i for 1 ≤ i ≤ n, i.e., data constructors allow to access each of its arguments. A typical example are tuples. Denoting the set of data constructors by F data , we denote the set of executable patterns Pat ex (F data ). In the DeepSec tool the only data functions are built-in tuples.

Conditional formulae Following [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], conditional branchings in protocols are described by first-order formulae over equalities on terms of the form t 1 = t 2 , possibly containing variable quantifiers. The semantics of formulae is as usual where we interpret = as = E .

Facts We define a set of fact symbols F f each with an arity over which we construct the set of facts Facts by applying fact symbols on constructor terms. These facts will be used to annotate processes and log events. In particular, F f will contain the facts K, In, Out to log attacker knowledge, input and output facts.

Protocols

Syntax

We present the syntax of Sapic + in Fig. 2 where t, t i range over arbitrary terms in T (F, N , X ), n ranges over private names in N priv , x ranges over variables in X and p ranges over patterns in Pat. Elementary processes model finite protocols that simply sample fresh values with the new construct, perform input and output, based on some control flow. Extended processes can model unbounded protocols, that can also raise events that provide a convenient way to model reachability properties. Finally, we also define stateful processes that can manipulate global shared states.

Semantics

We equip Sapic + with operational semantics that will be suitable for expressing both equivalence and reachability properties. A configuration (E, S, P, σ, L) defines the set of currently bound names E, the current values of the states S, the set of executable processes P, the current attacker knowledge inside the substitution σ, and the active locks L. We assume an infinite set of variables AX = {att i } i∈N , that will be mapped to the attacker knowledge, and σ is thus mapping variables in AX to the sequence of outputs of the protocol. The semantics is a labeled transition system between configurations, partially defined through its transition relation l -→ (where l may be empty, or otherwise is a set of facts) in Fig. 3 (see Fig. 9 in App. G for the full version).

K(t) ---→ (E, S, P, σ, L) if t =E Rσ for some R ∈ T (F, Npub, AX ) (E, S, P ∪ # {out(t1, t2); P }, σ, L) Out(R),K(t 1 ) --------→ (E, S, P ∪ # {P }, σ ∪ {attn → t2}, L) if t1 =E Rσ for some R ∈ T (F, Npub, AX ), Msg(t2) and n = |σ| + 1 (E, S, P ∪ # {in(t, x); P }, σ, L) In(R,R ′ ),K(⟨t,R ′ σ⟩) -------------→ (E, S, P ∪ # {P {x → R ′ σ}}, σ, L) if t =E Rσ, Msg(R ′ σ) for some R, R ′ ∈ T (F, Npub, AX ) (E, S, P ∪ # {let p = t in P else Q}, σ, L) -→ (E, S, P ∪ # {P τ }, σ, L) if pτ =E t and τ is grounding for p (E, S, P ∪ # {let p = t in P else Q}, σ, L) -→ (E, S, P ∪ # {Q}, σ, L) if for all τ, pτ ̸ =E t
The labels contain both the terms corresponding to the values sent over the network (K(⟨t 1 , t 2 ⟩)), but also the recipes used by the attacker to compute the protocol inputs (In(R, R ′ )), as well as the recipes used by the attacker to show that it can compute the channel of an output (Out(R)). This allows us to define both reachability and equivalence based properties.

We define

C i l1•••••ln = ==== ⇒C f to hold when C i - → * l1 -→-→ * . . . - → * ln -→-→ * C f
and, for ease of reading, we write When the attacker knowledge is not important, by abuse of notation, we sometimes refer to a trace simply as tr instead of (tr , σ).

P l1•••••ln = ==== ⇒C instead of (∅, ∅, {P }, ∅, ∅) l1•••••ln = ==== ⇒C.

Security properties

Reachability properties

To express reachability properties, we use the same temporal logic as the one of Tamarin [START_REF] Schmidt | Automated analysis of diffie-hellman protocols and advanced security properties[END_REF]. In the Tamarin tool, security properties are described in an expressive two-sorted first-order logic: we distinguish the sort msg that ranges over terms and the sort temp used for time points.

Definition 1 (Trace formulas). An atomic trace formula is either false ⊥, a term equality t 1 ≈ t 2 , a time point ordering i ⋖ j, a time point equality i . = j, or an action F @i for a fact F ∈ Facts and a time point i. A trace formula is a first-order formula over atomic trace formulas.

To define the semantics, let each sort s have a domain dom(s): dom(temp) = Q and dom(msg) = T (F, N ). Moreover, we denote by X temp the set of temporal variables and X msg the set of message variables. A function θ : X → T (F, N ) ∪ Q is a valuation if it respects sorts, i.e., θ(X s ) ⊂ dom(s) for all sorts s. If t is a term, tθ is the application of the homomorphic extension of θ to t. Moreover, given a trace tr , we denote by idx (tr) the set of positions in the trace and by tr i the multiset of facts of tr at position i.

Definition 2 (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 (tr , θ[x → u]) ⊨ φ for some u ∈ dom(s)
When φ is a closed formula, we sometimes simply write tr ⊨ φ as the satisfaction of φ is independent of the valuation.

For a set of traces Tr we also write Tr ⊨ φ if φ holds on any trace in Tr and any valuation, and even P ⊨ φ when traces pi ⊢ (P ) ⊨ φ. Actually Sapic + (and Tamarin) also allows checking satisfiability, i.e., the existence of a satisfying trace and valuation, denoted ⊨ ∃ : this is the dual notion and Tr ⊨ φ iff Tr ̸ ⊨ ∃ ¬φ and sometimes ⊨ ∀ is used for ⊨ to emphasize that we refer to validity.

Equivalence properties

Some properties are defined as the indistinguishability by an attacker of two processes. Indistinguishability can be modeled by trace equivalence. To define trace equivalence we first defined the notion of static equivalence which models the indistinguishability of two sequences of terms (represented as substitutions).

Definition 3. Two substitutions σ 1 , σ 2 : AX → T (F c , N , ∅) are statically equivalent, written σ 1 ∼ E σ 2 , iff ∀M, N ∈ T (F, N pub , AX ). M σ 1 = E N σ 1 ⇔ M σ 2 = E N σ 2
We can now define equivalence of processes P and Q by requiring that for any trace of P there exists a trace in Q obtained by the same sequence of labels, i.e., attacker actions, and resulting in statically equivalent attacker knowledge (and vice versa). Definition 4 (Trace equivalence). Let P and Q be two processes. P is a trace included in Q,

written P ⊑ E Q, iff ∀tr , σ P . ∃σ Q . (tr , σ P ) ∈ traces pi ≈ (P ) =⇒ (tr , σ Q ) ∈ traces pi ≈ (Q) ∧ σ P ∼ E σ Q P and Q are trace equivalent, written P ≈ E Q, iff P ⊑ E Q and Q ⊑ E P .

Overview of translations and results

We give here a summary of the translations and associated correctness results. Recall that Tamarin's input language is a set of multiset rewrite rules and security properties are expressed in the first-order logic of Section 3.4.1. ProVerif's specification language, on the other hand, is a dialect of the applied π-calculus, as Sapic + , but with subtle differences between both languages. Properties in ProVerif are expressed either using dedicated queries for reachability properties or observational equivalence. We will denote the satisfaction relation of ProVerif's reachability queries by ⊨ PV .

Reachability properties We will show that, for reachability it is possible to directly translate Sapic + specifications into both Tamarin's and ProVerif's input formats. In the following sections, we define in more detail these translations which we denote by • Tam for the translation to Tamarin and • PV for the one to ProVerif (by abuse of notation we use the same translation function for both the processes and the security formulas). We suppose that reachability formulas only contain K(•) facts, as well as facts defined through events (to avoid clashes with reserved facts added by the translation). The correctness and the conditions under which the translation can be applied are stated in the following theorems.

Theorem 1. Let P be a process and φ a formula such that P does not contain conditional branchings with destructors.

P ⊨ φ ⇔ P Tam ⊨ φ

Tam

One may note that although the property language for Sapic + and Tamarin is the same, we need to translate the formula φ as it encodes additional information. We can now define a similar correctness theorem for the translation to ProVerif.

Theorem 2. Let P be a process and φ a formula such that • Pat = Pat ex (F data ) and P does not contain conditional branchings with variable quantifiers;

• φ is a formula with a single quantifier alternation.

Then P ⊨ φ ⇔ P PV ⊨ PV φ PV .
Equivalence For equivalence, we can export Sapic + to either the ProVerif or DeepSec tool.

ProVerif indeed allows to verify a strong process equivalence, that we denote by P ∼ =E Q. It was shown in [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF] that ∼ =E implies observational equivalence, which in turn implies trace equivalence. Therefore, for extended processes, i.e., non-stateful processes, and the same hypotheses on processes as in in Theorem 2 we have that

if P PV ∼ =E Q PV then P ≈ E Q.
Moreover, on elementary processes the syntax of Sapic + and DeepSec coincide for predicates restricted to equality. Therefore, we can directly, for free, employ DeepSec to verify trace equivalence on this subclass of processes. Hence, we will not detail the (straightforward) translation to DeepSec in the following. Note, however, that DeepSec only supports a constructor-destructor term algebra defined by a subterm convergent rewrite system and no equational theory. As of now, there is no clear link between process equivalence and Tamarin's notion of equivalence between rewrite systems [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF]. We thus do not translate equivalence properties to Tamarin.

From Sapic + to Tamarin

We extend the 2014 translation from Sapic to Tamarin [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] with new syntactic features that improve usability (cf. Appendix D) or interoperability with ProVerif (let binders with pattern matching and destructors). Moreover, we heavily optimize the number of rules produced and the encoding of common edge cases for communication and database access.

Multiset rewriting Tamarin describes processes as sets of multiset rewrite rules (MSRs), each of form l -[ a ]→ r with l, a and r being multisets of facts. Facts consist of a fact symbol (e.g. F ) and a (possibly empty) sequence of terms t 1 , . . . , t n ), written F (t 1 , . . . , t n ). Substitution application can be lifted to facts and then MSRs, where the result is called a rule instance. The system state is a multiset of facts S. It can be rewritten by any rule instance l -[ a ]→ r that applies, meaning that l is contained in S (modulo the equational theory E). The application of this rule substitutes all facts in l by those in r. The set of traces is the sequence of actions a 0 , . . . , a n in a series of steps starting from the empty multiset, ∅ a0

-→S 0 • • • an --→S n . The fact Fr(n)
is special: it can only be introduced once per name n.

Sapic translation

We only give the idea of the translation here and refer to [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] for details. A SAPIC reduction C → C ′ is represented by one or more MSRs of form

state p (x), . . . a -→ state p ′ (x ′ ), . . .
where state p (x) is a 'ticket' to apply this rule. That 'ticket' is available (i.e., present in S) iff the set of currently running processes contains the subprocess of the overall process at position p1 with all unbound variables and names set to the values x. Protocol inputs and outputs or name restrictions can be expressed by adding Tamarin's special facts In, Out and Fr to the left or right, respectively. Parallel execution is captured by having two state-facts on the right, conditionals by having two rules with the same state-fact on the left, etc.

For efficiency reasons, state manipulation is not encoded in the system state S, but instead in the actions: inserts, lookups, locks and unlocks follow the above schema, but the action a logs these events, e.g., state p (x)

Insert(s,t) -------→state p ′ (x) represents an insertion, state p (x)
Lookup(s,y) -------→state p ′ (x • y) represents a lookup. In the latter, y is a priori unbound; however, a trace is only considered valid if it adheres to the following restriction: each lookup action follows a corresponding insert action that was not overwritten and any lock is either the first for its term, or a previous unlock released it.

The Sapic + extensions

First, we show how let bindings with else-branches can be translated to Tamarin, then, how we can add destructors on their right-hand side.

Let bindings with pattern matching

Sapic only supports let bindings for a single variable of the form let x = t in P . We generalize to pattern matchings with a failure branch of the form let s = t in P else Q where s, t ∈ T (F c , E, X ).

Assuming the current position in the process is represented by state p (x), we add the following rules, where v 1 , . . . , v n = vars(s) \ x are the unbound variables in the pattern.

state p (x), Fr(n) → Let(t, n), state semi p (x) (1)
state semi p (x), Let(s, n) → state p•1 (x • v 1 • . . . • v n ) ( 2
)
state semi p (x), Let(y, n) -[ NoMatch s (x, t) ]→ state p•2 (x) (3)
The fresh name n identifies the Let-fact with this rule instance. The state semi p (x) represents a 'semi'state in the process where the reduction of the let-process at position p is not yet completed. It permits the application of one of the two following rules.

Rule (2) represents the case where the term t in Let(t, n) can be matched with the pattern s in Let(s, n) and the process moves into the positive branch P at position p•1, while rule (3) is the else branch where its left-hand side (lhs) fact Let(y, n) with the fresh variable y can merge with any Let(t ′ , n) produced by rule [START_REF]Sapic+ tool chain[END_REF]. To enforce that we only take the else branch when the matching fail, we use a restriction: the third rule can only appear in a trace if s cannot be instantiated to match t. ∀x, t, i. NoMatch s (x, t)@i =⇒ ∀v 1 , .., v n . t ̸ = s

In Appendix E.1.1, we show the correctness of this translation. Notably, we managed to extend the 40-page proof from [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] in a black box fashion with the following technique. Their SAPIC semantics includes a feature for embedding MSRs within the process, which we omitted here for the ease of presentation. We expressed the above three rules using this feature, and show that the translation of the let construct into a process with the embedded MSRs is correct. The correctness of the translation to MSRs then follows by transitivity.

Let bindings with destructors

We now generalize this development to allow destructor function symbols to appear on the righthand side (rhs) of a let expression. Recall that Tamarin does not support destructor functions and hence all terms in the resulting MSRs need to be in T (F c , N , X ). On the other hand, the rhs term t in the process let s = t in P else Q may contain destructor symbols. For simplicity, we focus on the case where the destructor symbol dest must be at the top level2 and where only one rewrite rule applies to dest and this rewrite rule reduces to a single variable3 . We translate let x = dest( ⃗ t) in P else Q where dest(⃗ u) → x ∈ E D to let ⃗ u = ⃗ t in P dest else Q dest with all variables in ⃗ u fresh except for x and • dest the recursive call to this translation. Note first that neither ⃗ u nor ⃗ t contain a destructor symbol, so the translated let-expression is covered by the translation for pattern matches we just discussed. The translated process checks that the parameters to the destructor ⃗ t match the pattern ⃗ u defined by the reduction. If they match, this will assign a value to the variable x that occurs in ⃗ u. We once again extend the proof of correctness in a black box fashion (Appendix E.1.2).

Optimizations

The number of rules produced by the translation and the encodings chosen have decisive impact on the verification speed, as we will show. This is the reason why handwritten Tamarin models are typically faster to verify than translated models. For non-experts, what constitutes the best encoding is opaque and performing these optimizations is often out of reach. Here, we show the potential for improvement by discussing two optimizations, one that applies in general, one that applies to a frequent edge case. This compression step is not always permissible; hence we need to define carefully under which circumstances correctness is maintained. For instance, two rules cannot be compressed if the second rule may require the attacker to know the output of the first. e.g., new a; out(c, a); . . . cannot be compressed with its continuation . . . ; in(c, x); . . .. We define this compression as an optimization of the MSRs that is, in principle, applicable to handwritten Tamarin models. We provide in Appendix E.2.1 the complete set of conditions under which rules can be compressed and the corresponding proof (once again made in a black box fashion).

We find that this optimization is very effective (see Fig. 4). On all examples, the reduction in the number of rules is significant, and the running time of the verification can be reduced by a factor of up to 52. We observe that the ratio is more pronounced on examples where verification is slow to begin with, possibly indicating that path compression is most effective during the constraint solving procedure (as opposed to precomputation).

Alternate secret channel encoding

For private communications, it depends on the knowledge of the adversary whether or not the sender can proceed after emitting a message. Naturally, the encoding of channels in Sapic + reflects that, but typically, private channels remain trivially secret throughout the protocol run. We optimize the translation for this frequently occurring special case.

We syntactically check a sufficient condition of secrecy: a name n is a secret channel if there is a single process of form new n; P and all other occurrences of n have either the form in(n, m) or out(n, m) with n not occurring in m. If the condition is fulfilled, we can remove one out of two rules produced for each out-processes and one out of three rules in the translation of in-processes. The rules removed capture the case where an attacker can deduce the channel name and thus trigger the asynchronous communication behavior. It both reduces the number of rules and removes the need for a case distinction about whether n is deducible.

We find significant performance improvements with three case studies (see Fig. 6). SSH-NEST and OTP will be detailed in Section 6.2 and have a speed up of two and three, while U2F-TOY was already in the Sapic's repository. Note that on the latter, Tamarin times out without this optimization.

From Sapic + to ProVerif

The syntax and semantics of ProVerif are very similar to Sapic + as both tools use dialects of the applied π-calculus for their input languages.

Translating conditionals Extended processes only differ in the semantics of conditional branching containing destructors. In Sapic + if u = v then P else Q reduces to P when u = E v, which implies that both u and v reduce to constructor terms. Q is executed when u ̸ = E v, thus when u and v are not equal or u or v is not a message. In ProVerif, the semantics for the then branch is the same, however, Q is only executed when both u and v are messages and u and v are not equal. The process blocks when either u or v is not a message. Such if u = v then P else Q conditional branching is translated in ProVerif using let bindings.

This may seem anecdotal, but verification results can change if a part of the process becomes non-executable. ProVerif or DeepSec users may not even be aware of this discrepancy, illustrating the risks of working with different tools. There are multiple such pitfalls when trying to move from models in ProVerif, Tamarin or DeepSec, either due to some subtle differences between the semantics or different implementation choices. Notably, bindings inside pattern matchings, destructor inside conditional and pairs are not handled the same way in ProVerif and Tamarin. We detail those differences in Appendix C.

Translating states

ProVerif has no direct syntax for stateful processes and requires an encoding using internal communication on private channels. Although semantically correct, ProVerif struggles to prove security properties relying on this encoding which leads to false attack. The recent GSVerif front end [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] addresses many false attacks related to stateful protocols. However, GSVerif's transformations easily lead to non-termination issues and are sometimes too restrictive to handle general stateful processes. We therefore updated the GSVerif tool (available in [START_REF]Sapic+ tool chain[END_REF][START_REF] Tamarin | [END_REF]) to lift these restrictions and better exploit the most recent features of ProVerif (e.g., lemmas, axioms) leading to more efficient verification and favoring termination.

From states to channels

Although the applied π-calculus does not provide explicit constructs for stateful processes, private memory cells are classically encoded by reading and writing on private channels. For a private channel cell, reading the cell is achieved by in(cell,x); P, and writing by out(cell,t)|P. Note that for writing, the output is put in parallel as communication over private channels is synchronous. With this encoding, as long as an output on cell is not available, the cell is in fact locked.

States in Sapic + behave similarly to this encoding when a lookup is directly preceded by a lock, or an insert directly followed by an unlock. We call such a state pure. They can be translated through replacement of lock t; lookup t as x in else 0 by in(t, x); and insert t, t ′ ; unlock t; by out(t, t ′ );

where n ∈ N priv is a fresh private name. We give a precise definition of pure states and show the correctness of this encoding in Appendix E.2.3. This transformation also provides an alternate encoding when translating to Tamarin. Interestingly, it does not always improve performance, although it describes a natural way to write cells in Tamarin. E.g., on the AC protocol [START_REF] Barbosa | Foundations of hardware-based attested computation and application to SGX[END_REF][START_REF] Jacomme | Symbolic models for isolated execution environments[END_REF], the verification time shrinks from 127 seconds to 1 but on the SD protocol [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF][START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], the encoding seems to lead to non-termination. Using Sapic + , we can easily switch between both encodings.

Handling non-static states

The above translation of states is efficient and sufficient for most of our cases studies. However, it does not cover all the Sapic + processes. Notably, two syntactically different states need to be un-unifiable, since our transformation replaces the state t with a fresh private name. Thus, if two states were to become unified in the Sapic + process, then their respective translated fresh channel names would still be considered as different, hence yielding an unsound translation. We show how we could build a more general translation that removes these restrictions.

Though ProVerif does not have a native syntax for states, it allows declaring tables that are a form of global memory. Processes can insert and look up elements inside a table. However, unlike states in Sapic + , tables are append-only: once inserted, an element cannot be removed nor replaced. The syntax for table is illustrated as follows: We rely on these tables to encode states that may be unified with other states as follows: we declare two new tables lock_tbl and state_tbl, both containing pairs of bitstring and channel (t,n) where t corresponds to Sapic + 's state and n is the fresh private channel used in our state translation. Intuitively, to lock a state t, we first lookup in the table whether a private channel has already been generated for a state equal to t (modulo E). If so, we translate the lock as an input on this private channel; otherwise, we generate a fresh private channel, insert it in the table and execute the remaining process. Intuitively, the Sapic + construct lock t; P translates to ProVerif as: get lock_tbl(=t,x_n) in in(x_n,y); P else new n; insert lock_tbl(t,n); P Similarly, unlock t; P consists of a look up for a private channel for t and an output on this channel. Note that for the lock/unlock mechanism, it is irrelevant which term is sent on the private channels; hence we always output the constant 0.

A caveat remains: consider the process (lock t; P )|(lock t; Q). Assuming an empty table, the execution can start by executing the construct get lock_tbl(=t,x_n) for both locks, reducing into the two else branches (since the table is empty). Thus two fresh channels would be generated and inserted for t. To prevent this race condition, we consider a private channel glock that will act as a global lock to ensure that the else branch is executed before any other lookup in the table The translation for the Sapic + lookup and insert follows a similar structure, but as these two constructs are not blocking, the placement of input and output on private channels differs. See Appendix F.2 for the translation and its proof of correctness.

Translating queries

ProVerif translates security properties of various kinds (e.g. authentication, secrecy, noninterference, real-or-random secrecy) into either reachability queries (called correspondence query in ProVerif's manual) or equivalence queries. For reachability properties, we know that the state transformation preserves the set of traces. However, not all Sapic + queries can be translated into ProVerif reachability queries, as ProVerif permits only one quantifier alternation. Furthermore, the translation of special facts about communication or adversarial knowledge requires great care due to semantic differences. Note that GSVerif supports only reachability queries, hence support for equivalence queries is limited to protocols without state.

Reachability properties

In the latest ProVerif release, reachability properties can be described through a sorted first-order logic formula over atomic trace formulas as defined in Definition 1, similarly to Sapic + and Tamarin. There are, however, some differences in the facts and the fragment of the logic that prevent translation of all Sapic + queries to ProVerif queries and vice versa.

The first difference is that ProVerif only considers queries with at most one quantifier alternation. More specifically, a query must be of the form F 1 @i 1 ∧ . . . ∧ F n @i n ⇒ ϕ where ϕ is a quantifier-free trace formula and its disjunctive normal form (DNF) does not contain negations of facts F @i. All variables in F 1 @i 1 ∧ . . . ∧ F n @i n are quantified universally and remaining variables in ϕ are quantified existentially. For example, the following query in ProVerif syntax query x,y:my_type, z:bitstring, i,j,k:time; event(A(x))@i && event(B(y))@j =⇒ event(C(x,y,z))@k && k < j quantifies variables x, y, i, j universally and z, k existentially. In Sapic + 's syntax, this query is expressed as

All x y #i #j. A(x)@i & B(y)@j =⇒ Ex z #k. C(x,y,z)@k & k < j
The second difference is the set of allowed facts and their semantics. Facts in ProVerif include events, as illustrated by the previous example, message facts of the form mess(c,t) that hold when a term t has been sent on channel c, and attacker facts of the form attacker(t) that hold when the attacker can deduce the term t.

Though message and attacker facts may seem very similar to the K fact, their semantics are incomparable. Like for the K fact, an attacker can trigger mess(c,t) provided it can deduce c and t. However, mess(c,t) is also triggered when the output and input rules on private channels are executed.

Unfortunately, the attacker fact does not correspond to a K fact either: K(t)@i holds when the attacker did deduce t at timestamp i (e.g., to execute an input on a public channel); whereas attacker(t)@i holds if t is deducible at the timestamp i. This difference in semantics has important ramifications. First, two K facts cannot hold at the same timestamp but two attacker facts can. Second, and more importantly, it makes the translation of queries impossible when a K fact occurs in the conclusion of the query. Consider the process new a; new b; out(c,(a,b)); event A and the following queries. query i,j:time; event(A)@i =⇒ attacker(a)@j.

All #i. A@i =⇒ Ex #j. K(a)@j
The first (ProVerif) query holds whereas the second (Sapic + ) does not. The query query i,j:time; event(A)@i =⇒ mess(c,a)@j does not hold either but as explained above, message facts cannot translate K facts either due to the internal communication.

The semantic issue of the K(t)@i fact versus the attacker fact only occurs when it is existentially quantified. When the fact is universally quantified, however, we can safely translate K(t)@i to attacker(t)@i. For example, the following All x y #i #j. A(x)@i & K(y)@j =⇒ Ex z #k. C(x,y,z)@k will be correctly translated into the query query x,y,z:bitstring, i,j,k:time; event(A(x))@i && attacker(y)@j =⇒ event(C(x,y,z))@k Therefore, we only allow universally quantified K facts in queries.

ProVerif also allows table facts checking whether an element occurs in a table and injective events. We obviously ignore table facts since tables are not part of our syntax. Injective events allow to express a correspondence query where the occurrence of some event can be injectively associated to another event. For example, inj-event(A) =⇒ inj-event(B) ensures that there are at least as many B events as there are A events. Such properties cannot be expressed in Sapic + 's first-order logic and would require to extend the query syntax. Sapic + , however, allows users to export a ProVerif query in the input file if injective queries are needed (avoiding a separate file).

Practical evaluation and case studies 6.1 The implementation

We integrated our translation procedures as a separate package that is distributed with and integrated into Tamarin, in contrast to SAPIC's original compiler [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], which is a separate program. The benefits are threefold: we benefitted from Tamarin's libraries for manipulating and parsing terms, we could integrate our translation into Tamarin's graphical user interface and, finally, Sapic + will instantly support future extensions to Tamarin's term algebra. The package is open source and compatible with MacOS and Linux. We provide a docker image robertkuennemann/sapicplusplatform [START_REF]Sapic+ tool chain[END_REF] that allows to run all the tools easily and reproduce our case studies (detailed instructions in Appendix A).

The code uses a common parsing infrastructure and shares code for typing and annotating code (e.g., to identify matching lock and unlocks). The translation code is highly modular and exploits template mechanisms for easily adjustable output to ProVerif,GSVerif and DeepSec. We added about 5500 lines of code for the exports and the optimizations. Once the ProVerif export and the modular interface were done, the DeepSec export required around 200 lines of code.

The user provides an input file in Tamarin's spthy-format, which can include a process, and can choose to either translate into the target language of choice, or use Tamarin's internal constraint solver.

The new workflow in action

We provide below several complex case studies of real-life protocols, some of which constitute their first formal analysis. We also provide some case studies that were adapted either from existing Sapic + or Tamarin models. As a whole, our set of case studies illustrate:

• how Sapic + allows leveraging ProVerif's high level of automation when Tamarin's automation is insufficient;

• how Sapic + allows using Tamarin to prove lemmas that cannot be proved by ProVerif so they can be used as axioms inside ProVerif;

• how DeepSec can be used when ProVerif cannot prove equivalence; • and finally that the Tamarin models produced by Sapic + can be analyzed as efficiently as dedicated and fine-tuned Tamarin models.

We note that there are cases where a direct encoding is preferable to a translation from Sapic + . One instance are protocols with complex state machines, which are more easily expressed in Tamarin. Fig. 5 summarizes the running times of some of our case studies on a 2019 13"-MacBook Pro with 16GB RAM.

Novel case studies

KEMTLS Many post-quantum secure alternatives to currently deployed key-exchange protocols are starting to appear. In the coming years, formal verification tools are likely to play an essential role in their standardization process. We present here an analysis of KEMTLS [START_REF] Schwabe | Post-quantum TLS without handshake signatures[END_REF], a recently proposed alternative for the core key exchange of TLS.

The protocol relies on two main ingredients: a signature scheme for the server certificate and a Key Encapsulation Mechanism (KEM). Intuitively, a KEM is an asymmetric encryption scheme that uses the parties' long-term public keys to encrypt an ephemeral secret, which can be used to derive a shared key. 4 KEMTLS derives a secret shared key with authentication of the server after ten messages and six intermediate keys. We used Sapic + to verify the protocol over three models:

• A first, basic KEMTLS model, for which we verify server authentication and Perfect Forward Secrecy (PFS) of the final key. ProVerif proves these properties in a few seconds, Tamarin in around a minute.

• The KEMTLS-NO-AEAD model sanity checks the security claims. Indeed, in KEMTLS, most messages are encrypted using authenticated encryption, but in its security proof, nothing is assumed about this primitive. We thus modeled a version of KEMTLS without any encryption, and proved that the same security properties hold.

• The KEMTLS-CA model, where we model the client authentication option. This option was proposed in Appendix C of [START_REF] Schwabe | Post-quantum TLS without handshake signatures[END_REF] to match the existing option of TLS, but was provided without a security proof. It allows a user to authenticate to a server with a long-term certificate. We proved using ProVerif (1 second) and Tamarin (20 minutes) mutual authentication for this extension. We were also able to prove unlinkability of clients, modelled as strong unlinkability in terms of trace equivalence as defined e.g. in [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF][START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], for three sessions using DeepSec, and an unbounded number of sessions with ProVerif.

LAKE Lightweight Authenticated Key Exchange (LAKE) is a recently standardized key exchange protocol designed for resource-constrained devices. It is a DH based key exchange, where authentication can either rely on a signature scheme and long-term public keys, or on a long-term DH share and its public group element. With Sapic + , we could develop correct models of this protocol quickly. We debugged and proved them with ProVerif's approximate version of the equational theory, before strengthening the guarantees using the same model but with Tamarin's more complete theory.

Our models include both authentication modes, the client being able to chose between them dynamically. In the LAKE-DH-FS model, we proved mutual authentication, KCI and PFS of the exchanged key.

In concurrent work [START_REF] Norrman | Formal analysis of EDHOC key establishment for constrained iot devices[END_REF], a different version of the LAKE IETF draft was also analyzed with Tamarin. While they consider more properties than us, we consider a model supporting two different authentication modes.

SSH It is a widely deployed protocol that notably allows logging in on a remote server, relying on a user's long-term signature key. In its basic version, it has been analyzed previously using computeraided verification tools, both symbolic [START_REF] Lafourcade | Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties[END_REF] and computational [START_REF] Cadé | From computationally-proved protocol specifications to implementations and application to SSH[END_REF]. The protocol supports an additional agent-forwarding feature, allowing SSH connections to be nested. Analyzing this feature is complex: a secure channel established using a long-term signature key is used to forward a signature request for the same long-term key. The protocol with a single depth nesting was analyzed with an interactive prover in the computational model [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF], but it relies on an external composition result.

The SSH model verifies authentication and secrecy. Interestingly, a previous Tamarin model [39] required 26 seconds while our Sapic + model is verified in three seconds. 5 Sapic + can thus compile models that are verified in the same order of magnitude as a handmade Tamarin model.

The SSH-NEST model contains one nested connection. This model is verified very efficiently using ProVerif, and takes around 5 minutes in Tamarin with the more precise DH modeling. The SSH-NEST(X) model supports an arbitrary depth nesting, but with checks to manually bound the depth to X. Without a fixed bound, we were unable to make ProVerif terminate. We ran ProVerif with a bound up to 5: verification takes 7 seconds for depth X = 1, and each increment in depth approximately triples the running time, up to a running time of 6 minutes for depth 5. We were unable to make Tamarin terminate. 6Privacy-Pass The Privacy-Pass protocol, proposed in [START_REF] Davidson | Privacy pass: Bypassing internet challenges anonymously[END_REF] and under standardization [START_REF] Celi | Privacy Pass Protocol Specification[END_REF], is a token-based authorization of clients to servers that aims to preserve client anonymity. A server issues tokens upon client requests and tokens can be spent only once. It is based on a complex cryptographic primitive, a Verifiable Oblivious Pseudo-Random Function (VOPRF), whose equational theory is not supported by DeepSec. With the Privacy-Pass model, we verified token unforgeability, using ProVerif and Tamarin, and unlinkability (as defined in [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF][START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]) of the clients using ProVerif.

Existing Models

We used the export feature on some existing Sapic protocol models to illustrate its ease of use, where with only minor modifications, all models were executable in ProVerif. In addition, we also ported an existing Tamarin model.

5G AKA A previous case study of the 5G AKA authentication standard was performed recently in Tamarin [START_REF] Basin | A formal analysis of 5g authentication[END_REF], leading to one of the most complex Tamarin analysis to date. On this model and with on a complicated handwritten oracle to guide the tool, they were able to verify 4 sanity check lemmas, 3 security properties and find 7 attack traces.

To illustrate the usability and interest of Sapic + , we have reimplemented their main model using the platform. We were able to design a model such that after adapting their handwritten oracle, Tamarin was able to prove the 3 security properties in around a minute on the model produced by Sapic + . In comparison, the original Tamarin model took 3 times longer to verify those 3 properties. This example thus give evidence that Sapic + can even on complex case studies produce models that are as fast, or even faster to verify than Tamarin fine-tuned ones.

Moreover, by manually adding a simple parameter to guide the resolution, ProVerif finds 6 of the 7 attack traces automatically, in contrast to the original model, which required a complex oracle to find these attack traces. The last attack can also be found by ProVerif, but requires editing the process to help the trace reconstruction terminate.

SGX report models With Sapic + , the modeling of the SGX report capability from [START_REF] Jacomme | Symbolic models for isolated execution environments[END_REF] carries over to ProVerif for free. On the models of AC, AKE and OTP, ProVerif always answered in a second and Tamarin in a few seconds. Some interesting results were that on the SOC protocol, ProVerif does not terminate, but Tamarin answered in seconds. On a flawed model of AC, the AC-F-sid model, ProVerif reports 'cannot be proved', while Tamarin successfully reconstructed the attack trace. Nevertheless, with minor modifications to the generated ProVerif model7 , we could ensure termination and attack reconstruction.

Others Finally, we imported the Scytl e-voting protocol [START_REF] Cortier | A formal analysis of the neuchatel e-voting protocol[END_REF] from the GSVerif benchmark [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF], and the secure device (SD) [START_REF] Arapinis | Statverif: Verification of stateful processes[END_REF][START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] and NSL models [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] from Sapic's repository. We verify the strong secrecy of the key in NSL for one session with DeepSec, where ProVerif reports 'cannot be proved'. On the Scytl protocol, ProVerif answers in a second and Tamarin in a minute, but ProVerif reports 'cannot be proved' on the single vote property (without further expert input) while Tamarin proves it.

Tamarin proofs of ProVerif axioms

Since its recent update [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF] ProVerif allows specifying axioms that can be used to prove a protocol by adding an extra assumption that may hold but that ProVerif cannot prove. An example of such a case is given in Example 6 of [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF], where an axiom is used to specify that an action can only occur once. Consider the following subprocess new stamp; in(c,xr); event S(stamp,xr); new r; out(c,sign(aenc(vote,(r,xr),pk (sk e),sk ))

On such a process, ProVerif cannot prove that the event S can only occur once with a given timestamp, due to its abstraction. As this fact is required to prove the expected security properties, the following axiom is needed:

All stamp xr xr2 #i #i2. S(stamp,xr)@i & S(stamp,xr2)@i2 =⇒ i=i2 & x=xr2
While ProVerif cannot prove this, this is the sort of formula that Tamarin typically handles well. We thus ported this example to Sapic + , successfully using Tamarin to prove the axiom, and ProVerif to prove with the axiom the expected security property, both being formally combined. Axioms are also typically how GSVerif [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] functions: its adds axioms about states, axioms that were proven correct by hand. Once again using Sapic + , we proved for the previous 5G example that the axiom generated by GSVerif did hold thanks to Tamarin.

Conclusion

We introduced Sapic + , a protocol verification platform that allows to transparently use three major verification tools, ProVerif, Tamarin and DeepSec, to efficiently verify protocols from a single protocol model. The translations are carefully optimized and proven correct, and we developed novel case studies of real life protocols. For ease-of-use, we made the entire tool chain available on Docker Hub [START_REF]Sapic+ tool chain[END_REF].

We plan to generalize some of our encodings (notably permitting destructors to occur anywhere in the process) and to devise new optimizations, in particular when exporting stateful protocols to ProVerif. We see potential in helping ProVerif terminate by deriving lemmas from a static analysis of the process.

A Docker instructions

These instructions define how to run the docker image.

Docker installations

• Linux: follow instructions at https://docs.docker.com/get-docker/

• MacOS, there is a binary docker for Mac, which can be installed as a package (https: //docs.docker.com/docker-for-mac/), or, if you have homebrew, via 'brew cask install docker'.

Sapic + image The docker image that automatically installs all the required tool and provide an easy access to Sapic + is available on dockerhub [START_REF]Sapic+ tool chain[END_REF].

After the installation of docker, the ready to use image can be pulled in a few seconds with the following command: user@PC $ docker pull protocolplatform/protocolplatform:latest latest: Pulling from protocolplatform/protocolplatform 69692152171a: Pull complete 205f84d8d925: Pull complete 4f4fb700ef54: Pull complete d40febe920a4: Pull complete 951aab113191: Pull complete 1ce93dea7c43: Pull complete 756e36a6a0ee: Pull complete 578a009fd5f1: Pull complete 0d7b23b7972f: Pull complete 2e58ea6824e9: Pull complete 5edd7e3a65e5: Pull complete c08c877fcea6: Pull complete 59ceebc22d18: Pull complete 9b00f0afd6bb: Pull complete f3379feff7e7: Pull complete 7ed5ec83d93c: Pull complete gest: sha256:540d7197a065bc6979289d462873e0c76a28f2bfac05a5e1e94853ed1e9b38d1 Status: Downloaded newer image for protocolplatform/protocolplatform:latest docker.io/protocolplatform/protocolplatform:latest To launch the docker, execute the command $ docker run protocolplatform/protocolplatform: latest, which should display a README with instructions on how to use the tools.

Re-building the image This is only needed for regenerating the image when we update the software. The docker building files are directly included inside the tamarin-prover repository [START_REF] Tamarin | [END_REF].

1. From the root of the repository, the docker image is built with $./etc/docker/build.sh.

2.

Once the main image is built, one can also run the case studies of the paper with $./etc/ docker/build-benchs.sh.

B Benchmarks

See Figures 6 and7.

C Pitfalls when carrying over models

We already discussed the following differences:

• ProVerif and Tamarin do not allow to make statements about the attacker knowledge in a completely equivalent manner. • Some equational theories in one tool only have approximate equivalents in the other.

The differences due to implementations choices are the following ones.

Pattern matching and bindings Tamarin supports general pattern matchings, where the pattern ⟨x, x, y⟩ will for instance expect twice the same value for x, and if y is previously bound, y would need to match this bound value.

ProVerif supports pattern matchings, with an explicit = to indicate that a variable should not be rebound but match the current value of the variable. For example, the pattern ⟨x, x, y⟩ will accept three distinct values, and rebind x to the second value. ⟨= x, x, y⟩ will expect the first value to be the previous binding of x, and then bind x to the second value.

We believe that such subtle behavior may be confusing, and therefore forbid rebinding of variables, and thus multiple occurrences of the same variable in a pattern matching. This syntactic restriction avoids confusion about the possible semantics, and enforces the behavior of ProVerif and Tamarin to coincide.

Destructors in conditionals In

ProVerif a conditional if t 1 = t 2 then P else Q will • transition to P if Msg(t 1 ), Msg(t 2 ) and t 1 = E t 2 , • transition to Q if Msg(t 1 ), Msg(t 2 ) and t 1 ̸ = E t 2 ,

and

• block if either ¬Msg(t 1 ) or ¬Msg(t 2 ), that is if a destructor fails.

In Sapic + (as in DeepSec) we prefer the condition for entering the else branch to be the negation of the condition for entering the if branch, i.e., ¬Msg(t 1 ), or ¬Msg(t 2 ) or t 1 ̸ = E t 2 . Note that this does not decrease expressivity as the behaviour of ProVerif can be encoded as let

x 1 = t 1 in let x 2 = t 2 in if x 1 = x 2 then P else Q. To ensure consistent semantics we actually translate the conditional if t 1 = t 2 then P else Q in Sapic + to let (= t 1 ) = t 2 in P else Q in ProVerif.
If general conditional formulae occur in the process, we need to redefine in ProVerif an equality function eq' consistent with our semantics that we use only in the conditional branchings formulas: fun eq'(bitstring,bitstring):bool reduc forall x:bitstring; eq'(x,x) = true otherwise forall x: bitstring or fail, y: bitstring or fail; eq'(x,y) = false.

Pairs In Tamarin, tuples are syntactic sugar for right nested tuples, i.e., ⟨x, y, z⟩ = ⟨z, ⟨y, z⟩⟩ >.

In ProVerif, there is a dedicated function symbol for each possible length of tuples, with corresponding projections. Then, ⟨x, y, z⟩ corresponds to (x, y, z) 3 . This small difference actually implies distinct behaviours for let bindings or pattern matching in inputs.. For instance, consider let ⟨x, y, z⟩ = m in • • • In the Sapic + style, this pattern would accept ⟨m, n, s, t⟩, as it would correspond to ⟨m, ⟨n, ⟨s, t⟩⟩⟩, and we would have z = ⟨s, t⟩. In ProVerif, this would only accept tuples of exactly length 3, and a four tuple would be rejected. This can lead to very different behaviour for a protocol, and both remove attacks or create false attacks.

To ensure a sound export, we translate tuples in Sapic + as nested pairs in ProVerif.

Matching in inputs

The pattern matching inside an input behaves differently in ProVerif and Sapic. For ProVerif, this is only a syntactic sugar where given a pattern p, in(t, p); P corresponds to in(t, x); let p = x in P else 0. Notably, the input is always executable, and the continuation may fail. The semantics of Sapic is different, as the matching is directly made in the input, and the input is not always executable. We defined Sapic + following the behaviour of Sapic + , as it was important to obtain the same behaviours for the equivalence semantics of ProVerif and DeepSec.

D Syntactic extensions

With Sapic + , we make several small syntactic extensions to Sapic, importing some useful features from ProVerif.

Types Sapic + provides some small typing capabilities, that can be used to sanity check the model. Function symbols can be declared with a type, and variables can also be bound with a type: functions: enc(bitstring,skey):bitstring new sk:skey; in(m:bitstring); out(enc(m,sk)).

A type inference algorithms allows both to sanity check the models, looking for incompatible typing annotations, and to ease the export to ProVerif. Notably, events in ProVerif need to be declared with the type of their arguments, that we can infer from the annotation in the process and the event usages.

Processes with explicit parameters Sapic allows to declare sub-processes that can be called inside the main process with the following syntax. Such declarations can lead to mistakes in the model. Indeed, assuming that P should only have access to skP and pk(skQ), we may use inside it by mistake skQ. Sapic + now supports the declaration of sub-processes with some explicit parameters, that are binding the sub-variables, improving the readability of the models. Explicit pattern matchings Sapic supports the same pattern matching capabilities as Tamarin. Thus, one can write processes of the form new sk; new token; P(sk) | in(enc(< token, m>,sk)). In big processes, implicit pattern matchings can make the model difficult to verify and understand. We thus add the capability to specify which variables correspond to a pattern match, and which variable are to be bound. We use the same notation as ProVerif, adding as a prefix the = symbol, for instance yielding new sk; P(sk) | in(enc(< =token, m>,=sk)).

Remark that to avoid modelling mistakes, we recommend that modellers do not use pattern matchings over function symbols, but rather rely on let bindings: new sk; P(sk) | in(cypher); let <=token,m> = dec(cypher,sk) in ...)

E Sapic + to Tamarin

We first 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 5 (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 6 (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:

• l, a, r do not contain fresh names and • r does not contain Fr-facts.

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 right-hand side Fresh : [] -[]→ [Fr(x : fresh)] The semantics of the rules is defined by a labelled transition relation. Definition 7 (Labelled transition relation). Given a multiset rewriting system R we define the

labeled transition relation → 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 8 (Executions). Given a multiset rewriting system R we define its set of executions as

exec msr (R) = ∅ A1 -→ 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 9 (Traces). The set of traces is defined as

traces msr (R) = [A 1 , . . . , A n ] | ∀ 0 ≤ i ≤ n. A i ̸ = ∅ and ∅ A1 =⇒ 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.

Definition 10 (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 }.

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.

E.1 Sapic + extensions

E.1.1 Let bindings with pattern matching

The original Sapic translation actually allows writing MSR rules directly inside processes. We use this feature to encode let bindings in a black box fashion w.r.t. to the proof of the Sapic translation to Tamarin.

Definition 12. Let P be a Sapic + process. We define the translation P let as follows:

let s = t in P else Q let := new b; [] -[]→ [Let(t, b)]; ([Let(s, b)] -[]→ []; P let ) |([Let(x, b)] -[ restr(∀fv (p).t ̸ = s) ]→ []; Q let )
where x is a fresh variable, and where P let is lifted homomorphically to the other constructs.

We show that the validity of this encoding by showing that the set of traces is the same on both side. Lemma 1. Let E D = ∅ and P be a Sapic + process. We then have:

traces pi ⊢ (P ) = traces pi ⊢ ( P let )
Proof. We first recall the difference between our semantics and the original Sapic semantics, where MSR rules can be inserted inside processes. Sapic + configurations (E, S, P ∪ # {let s = t in P else Q}, σ, L) are extended with a set of ground facts S MS ⊂ G, and the semantics are equipped with the additional rule:

(E, S, S MS , P ∪ # {[l] -[ a ]→ [r]; P }, σ, L) a ′ -→ (E, S, S MS ∪ # r ′ \ lfacts, P ∪ # {P τ }, σ, L) if ∃τ, l ′ , a ′ , r ′ . τ is grounding for [l] -[ a ]→ [r], [l ′ ] -[ a ′ ]→ [r ′ ] = E ([l] -[ a ]→ [r])τ, lfacts(l ′ ) ⊂ # S MS , pfacts(l ′ ) ⊂ # S MS ∀restr(ϕ) ∈ a ′ , ϕ holds
Remark that we allow rules to be labelled with restriction of the form restr(ϕ), where the rule can be executed if and only if ϕ is true.

In this semantics, we have that:

(E, S, S MS , { let s = t in P else Q let }, σ, L) - → (E ∪ b ′ , S, S MS , R 1 , σ, L) - → (E ∪ b ′ , S, S MS ∪ Let(t, b ′ ), R 1 , σ, L)
where b ′ is a fresh name and

R 1 := [] -[]→ [Let(t, b ′ )]; ([Let(s, b ′ )] -[]→ []; P let ) |([Let(x, b ′ )] -[ restr(∀fv (s).t ̸ = s) ]→ []; Q let )
Now, we remark that in this setting ∃τ, l ′ , a ′ , r ′ such that τ is grounding for

[Let(s, b ′ )] -[]→ [] and [l ′ ] -[ a ′ ]→ [r ′ ] = E ([Let(s, b ′ )] -[]→ [])τ and lfacts(l ′ ) ⊂ # S MS is equivalent to ∃τ.sτ = E t.
This is notably due to the fact that b ′ is fresh, and thus only Let(t, b ′ ) ∈ S MS can be matched on the left hand side. And further, we have that ∃τ.t = E sτ ⇔ ¬(∀fv (s).t ̸ = s).

So, there are only two possibilities:

(E ∪ b ′ , S, S MS ∪ Let(t, b ′ ), R 1 , σ, L) - → (E ∪ b ′ , S, S MS , P let τ, σ, L) if ∃τ.t = E sτ and (E ∪ b ′ , S, S MS ∪ Let(t, b ′ ), R 1 , σ, L) - → (E ∪ b ′ , S, S MS , Q let , σ, L) if for allτ.t ̸ = E sτ
We thus see that the, without other processes in parallel, possible reductions of let s = t in P else Q let are exactly the same as the reductions of let s = t in P else Q. We can immediately conclude here that traces pi ⊢ (P ) ⊂ traces pi ⊢ ( P let ). For the other direction, we remark that even though we split a single transition into two transitions, both are silents and do not influence and cannot be influenced by the execution in parallel of other processes. This is due to the fresh name inserted inside the facts. We thus also have that traces pi ⊢ (P ) ⊃ traces pi ⊢ ( P let ).

Reusing the translation from Sapic to Tamarin, described in [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]Fig. 4] and that we denote by Tam , we can build a translation from Sapic + to Tamarin that preserves the set of traces and thus the validity of the formulas. This translation also adds the restrictions required to make the translation correct.

Theorem 3. Let P be a process without destructor symbols, and φ a formula without In and Out facts. We have that:

P ⊨ φ ⇔ P let Tam ⊨ φ
Tam Proof. After using the trace preserving encoding of Lemma 1, we conclude by using Theorem 1 of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], that we can leverage as we now have a process that only contains constructs of the Sapic language.

E.1.2 Let bindings with destructor Definition 13. Let dest be a destructor symbol with an associated rule of the form dest(⃗ u) → x ∈ E D .

We define P dest as:

let x = dest( ⃗ t) in P else Q dest := let ⃗ u = ⃗ t in P dest else Q dest if
all variables in ⃗ u are fresh except for x, and where P dest is inductively propagated.

To show the correction of the encoding, we simply show the validity of the syntactic sugar.

Lemma 2. traces pi (P ) = traces pi ( P dest )

Proof. By definition of the application of a rewrite rule to a term, which can only be applied if we can unify the argument of the destructor with the arguments of the rewrite rule, we have that:

∃τ.xτ = E dest( ⃗ t) ⇔ ∃τ.⃗ uτ = E ⃗ t
This directly implies the equivalence of the executability condition of the two let bindings in P dest .

Corollary 1. Let P be a process with destructor symbols only as head function symbols of right hand side term of let constructs, and φ a formula without In and Out facts. We have that:

P ⊨ φ ⇔ P dest let Tam ⊨ φ Tam
Proof. Direct application of Theorem 1 of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], Lemma 1 and Lemma 2.

E.2 Sapic optimizations

E.2.1 Path Compression

Some rules produced by the original Sapic translation can be compressed, for instance:

[s 1 , Fr(x)] -[]→ [s 2 ] ∪ [s 2 , Fr(y)] -[]→ [s 3 ] ⇒ [s 1 , Fr(x), F r(y)] -[]→ [s 3 ]
We try to provide a general algorithm to compress as much as possible the set of rules produced by Sapic + , and thus improve the performances.

We must consider in which cases compressing two rules, one of which produces some fact and one consumes it, does not alter the possible set of traces. We provide bellow a general algorithm to compress a set of rules of the form

[{s 1 } ∪ # F r 1 ∪ # In 1 ] -[ E 1 ]→ [R 1 ]
where intuitively s 1 is the control state of the protocol, and multisets of fresh facts F r 1 and input facts In 1 may be required. We first express, in an algorithmic form, a condition under which two rules can be merged. In this Section, we actually refer to E 1 for hide(E 1 ).

canMerge r 1 r 2 • • = let [P 1 ] -[ E 1 ] → [R 1 ] = r 1 in let [P 2 ] -[ E 2 ] → [R 2 ] = r 2 in if r1
or r2 contain any persistent state then False if E 1 ̸ = ∅ and E 2 ̸ = ∅ then (* we cannot merge rules if it makes events be simulataneous *) False else if Out ∈ R 1 and In ∈ P 2 then (* we cannot merge rules if the first one give knowledge that may be needed for the other one *) False else if #R 1 > 1 and E 2 ̸ = ∅ then (* we cannot merge rules if we are breaking asynchronous behavior (i.e u->v,w, and v-E->t cannot be compressed, else an event that could have happened with w before E cannot do so anymore. *) False else if E 1 ̸ = ∅ and In ∈ P 2 then (* we cannot merge rules if the second rule needs some input, that may be computable by the attacker only after the first rule raised an event. *) False else True Lemma 3. For any two rules

l := [{s 1 } ∪ # F r 1 ∪ # In 1 ] -[ E 1 ]→ [R 1 ] and r := [{s 2 } ∪ # F r 2 ∪ # In 2 ] -[ E 2 ]→ [R 2 ]
and any set of facts F such that s 2 ∈ R 1 , s 2 ̸ = s 1 , s 1 and s 2 not persistent and s 2 / ∈ F , if canMerge l r then traces msr (F ∪ l ∪ r)) = traces msr (F ∪ m)

where m := [{s 1 } ∪ # F r 1 ∪ # F r 2 ∪ # In 1 ∪ # In 2 ] -[ E 1 ∪ E 2 ]→ [R 1 ∪ R 2 \ {s 2 }]
Proof. Note that s 2 / ∈ F , so l is the only possible source of s 2 and l each application of r must be preceded by a different application of l. We assume that canMerge l r holds, and thus have that:

E 1 = ∅ ∨ E 2 = ∅ (i) ∧ Out ̸ ∈ R 1 ∨ In ̸ ∈ P 2 (ii) ∧ R 1 = {s 2 } ∨ E 2 = ∅ (iii) ∧ E 1 = ∅ ∨ In / ∈ P 2 (iv)
First, we prove that:

traces msr (F ∪ m) ⊆ traces msr (F ∪ l ∪ r)
Indeed, any application of m can be replaced by an application of l directly followed by an application of r, as for any facts set S such that lfacts(m) ⊆ # S:

S E1∪E2 -→ m S ∪ # R 1 ∪ # R 2 \ ({s 1 } ∪ # {s 2 } ∪ # F r 1 ∪ # F r 2 ∪ # In 1 ∪ # In 2 )
is replaced by

S E1 -→ l S ∪ # R 1 \ ({s 1 } ∪ # F r 1 ∪ # In 1 ) E2 -→ r S ∪ # R 1 ∪ # R 2 \ ({s 1 } ∪ # F r 1 ∪ # In 1 ∪ # {s 2 } ∪ # F r 2 ∪ # In 2 )
By (i), we have that either E 1 = ∅ or E 2 = ∅, which allows us to conclude.

Second, we prove that:

hide(traces msr (F ∪ l ∪ r)) ⊆ hide(traces msr (F ∪ m)

First, remark that as s 2 / ∈ F , for any execution e ∈ exec msr (F ∪ l ∪ r), there are more applications of l than r.

• Let us consider the case where there is no r.

-If E 1 ̸ = ∅, then, we can replace all occurrences of l by m (when l is executable, so is m), and it yields the same trace (as E 2 = ∅ by (i)).

-If E 1 = ∅ ∧ E 2 = ∅, then, we can also replace all occurrences of l by m.

-

If E 1 = ∅ ∧ E 2 ̸ = ∅, then by (iii), R 1 = s 2 .
And thus, l does not produce anything which is used in the trace, and we can simply remove all occurrences of l and preserve the executability of the trace.

• we now consider the last occurrence of r, along with its closest occurrence l.

-If E 2 = ∅ ∧ E 1 ̸ = ∅, we remove both l and r and insert m at the position of l in the execution.

-

If E 2 = ∅ ∧ E 1 = ∅ ∧ Out ∈ R 1 ,
we remove both l and r and insert m at the position of l in the execution. Out ∈ R 1 implies that In / ∈ P 2 by (ii), thus P 2 = {s 2 } ∪ # F r 2 . Hence, m can be executed at the position of l.

-

If E 2 = ∅ ∧ E 1 = ∅ ∧ Out / ∈ R 1 ∧
In ∈ P 2 , we remove both l and r and insert m at the position of r in the execution. As Out / ∈ R 1 , the application of l is useless for all rules between l and r, and we can indeed apply m at r and maintain the executability of the actions before.

-

If E 2 = ∅ ∧ E 1 = ∅ ∧ Out / ∈ R 1 ∧ In / ∈ P 2 ,
we remove both l and r and insert m at the position of l. m is indeed executable at this place, as P 2 only contains s 2 and fresh facts.

-If E 2 ̸ = ∅, then we remove both l and r and insert m at the position of r in the execution. By (i), we have that E 1 = ∅, and by (iii) we have that R 1 = {s 1 }. Thus, l is not required by any rules in between l and r, and we can indeed remove its execution, and only execute m instead of r.

We can thus apply the optimization on the set of MSR rules produced by the Sapic translation, and we preserve the set of traces. Remark that for translating the inputs, Sapic may behave in two different ways, depending on the lemmas that we have in the file:

• in all generality, and input is translated with an MSR rule labelled with an event InEvent, which is used in the α inev restriction( [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]).

• under some conditions, see [6, Appendix E], the α inev restriction is removed, and thus, the translation of input is with a rule that does not contain any event.

In the first case, two consecutive inputs will not be merged into a single rule, as we have events inside the labels, while in the second case, it is possible.

E.2.2 Secret channel optimization

When a channel is completely secret, we can simplify the translation, by essentially removing the rule that allows the attacker to intercept the messages, and making the communication through a dedicated fact. We can define the set of secret channels, by looking syntactically if the identifier of channel is a name that does not occur anywhere else.

Definition 14. Let P be a process. We denote by SecretChannels(P ) the set of names in N priv such that for any n ∈ SecretChannels(P ),

• there is a single occurrence of the form new n,

• all other occurences of n in P are either of the form in(n, M ) or out(n, M ) where n does not occur in M .

We then perform a simplification of the translation of Sapic from processes to MSR. We optimize the translation by removing the rules of the translation that corresponding to attacker communications, as the channel is secret.

Definition 15. We denote by

Tam the translation of Sapic defined in Figure 7 of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]. Let P be a protocol, we define T,secret P as Tam for which we change the definition on the in and out construct as follows when n ∈ SecretChannels(P ):

out(n, N ); Q, p, x T,secret P = [state p (x)] → [Msg(n, N ), state semi p (x)], [state semi p (x), Ack(n, N )] → [state p•1 (x)] ∪ P, p • 1, x Tam in(n, N ); P, p, x T,secret P = [state p (x), In(⟨n, N ⟩)] -[ InEvent(⟨n, N ⟩) ]→ [state p•1 (x ∪ vars(N ))], [state p (x), Msg(n, N )] → [state p•1 (x ∪ vars(N )), Ack(n, N )] ∪ P, p • 1, x ∪ vars(N )
Tam

For this modification we show that the soundness of the translation still holds, i.e. that Lemma 1 of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] still holds. Lemma 4. Let P be a protocol that does not contain any let bindings and destructors. traces pi ⊢ (P ) = hide(traces msr ( P, ∅ T,secret P

))

Proof. For n ∈ SecretChannels(P ), the difference between the set P, ∅ Tam and the set P, ∅ T,secret P , is that we removed rules of the form:

[state p (x), In(n)] -[ InEvent(n) ]→ [Out(N ), state p•1 (x)] [state p (x), In(⟨n, N ⟩)] -[ InEvent(⟨n, N ⟩) ]→ [state p•1 (x ∪ vars(N ))]
We remark that rules of the previous form can never be executed. Indeed, as n only occurs in channel name position, it never occurs inside a K fact. And thus, facts of the form In(n) or In(⟨n, N ⟩) can never be produced. We then easily conclude that traces msr ( P, ∅ Tam ) = traces msr ( P, ∅ T,secret P ), and with Lemma 1 of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF].

E.2.3 State encoding optimization

We show the soundness of encoding states with secret channels when the state is only accessed in a particular fashion. This is used both for the Tamarin and the ProVerif export.

Definition 16. Let P be a process and cell be a ground term. We say that t is a pure state if

• There is a single instance of insert t, t ′ for some t ′ not under a lock nor replication

• All other instances of insert t, t ′ should be followed by an unlock, i.e. insert t, t ′ ; unlock t for some t ′ , and should be necessarily preceded by the construct lock t; lookup t as x in else 0) for some x after possibly arbitrary many other actions that do not involve t.

• no other state identifier t ′ occurring in P can be unified with t, i.e., for all substitutions σ, t ̸ = t ′ implies tσ ̸ = E t ′ σ.

Definition 17. Let P be a process and t a pure state of P . We fix a fresh name n ∈ N priv in P . We first define an auxiliary translation function over a process and a set of bound names as: And we extend its application to multiset of processes. Let us define a bijective mapping f from configurations reachable in P to configurations reachable with the same observable trace in P st t . We show by induction on the last step of the execution that there exists a bijective mapping f (a bi-simulation actually) over configurations such that for all tr , if (∅, ∅, {P }, ∅, ∅) We first remark that in general, as t cannot be unified with any other state identifier, t uniquely identifies the state across any execution. And by defining n when all the names appearing in t are defined, substituting t by n in all state identifiers preserves the possible equalities between replications of t.

new
⇒ we first show the left to right implication. If the last step of the execution is a rule that does not involve states, the property trivially holds as the last step of the reduction can trivially be performed on the other side, and we inherit the required hypothesis by induction. Now, we branch depending on the last rule, that goes from configuration C to D, and we assume that P tr =⇒D and P st t tr =⇒f (C) with the above hypothesis over f (C). We need to construct f (D such that it meets the expected requirements.

• (E, S, P ∪ # {insert t, M ; P }, σ, L) -→ (E, S[n → M ], P ∪ # {P }, σ, L)

In this case, by induction hypothesis, there is {insert t, N ; P }, E ′ st' t ∈ P ′ , and we can perform the reduction: f (C) = (E ′ , S ′ , P ′ ∪ # {out(n, M )| P, E ′ st' t }, σ ′ , L ′ ) -→ (E ′ , S ′ , P ′ ∪ # { P st t } ∪ # { out(n, M ), E ′ st' t }, σ ′ , L ′ ) = f (D)

To show that this new configuration satisfy the induction hypothesis, there are two options. Either it is the lone insert, or it is an insert under the lock.

-In the first lone insert case, we know that t / ∈ L and that [t → M ] / ∈ S. This new configuration f (D) thus satisfies the induction hypothesis, as we now have out(n, M ) ∈ P ′ , and [n → M ] ∈ StoreA[n → M ] and t / ∈ L.

-In the other case, it is an insert under a lock, and we know as the state is pure that we in fact have P = unlock t; P ′ . Thus, the new configuration f (D) satisfies the induction hypothesis, as we now have out(n, M ) ∈ P ′ , and [n → M ] ∈ StoreA[n → M ] and unlock t; P ′ ∈ P.

• (E, S[n → M ], P ∪ # {lookup t as x in P }, σ, L) -→ (E, S, P ∪ # {P {M/x}}, σ, L) By induction hypothesis, we know that out(n, M ) ∈ P ′ , and that lookup t as x in P, E ′ st' t = in(n, x); P, E ′ st' t ∈ P. we can thus from f (C) perform the following reduction:

f (C) = (E ′ , S ′ , P ′ ∪ # {out(n, M )} ∪ # {in(n, x)| P, E ′ st' t }, σ ′ , L ′ ) -→ (E ′ , S ′ , P ′ ∪ # { P, E ′ st' t {M/x}}, σ ′ , L ′ ) = f (D)
As t is a pure state, so unlock t; P / ∈ P ∪ # {P {M/x}} and lookup t as xinP / ∈ P ∪ # {P {M/x}}. Further, t ∈ L, as this lookup must have been preceded by a lock. As we removed the output over n, out(n, M ) / ∈ P ∪ # {P {M/x}}, so this new configuration f (D) verifies the induction hypothesis.

• (E, S, P ∪ # {lock t; P }, σ, L) -→ (E, S, P ∪ # {P }, σ, L ∪ { t })

We have that t / ∈ L. So, out(n, M ) ∈ P ′ if and only if [t → M ] ∈ StoreA. We simply set f (D) = f (C). As t is a pure state, we know that P = lookup t as xinP ′ . So, for f (D) we also have out(n, M ) ∈ P ′ if and only if [t → M ] ∈ S, and thus the induction hypothesis is satisfied.

• (E, S, P ∪ # {unlock t; P }, σ, L) -→ (E, S, P ∪ # {P }, σ, L \ { t }) Because t is a pure state, we know that this unlock was preceded by an insert, and thus that [t → M ] ∈ S. Further, we obviously have that unlock t; P ∈ P ∪ # {unlock t; P }. By induction hypothesis, we know that in f (C), we have that out(n, M ) ∈ P ′ . We set f (D) = f (C). This new configuration satisfy the induction hypothesis, as we know have for D that t / ∈ L \ { t } and still have [t → M ] ∈ S, while out(n, M ) ∈ P ′ .

⇐ we now show the right to left implication. If the last step of the execution is a rule that does not involve an internal communication over channel n, or the addition of a out(n, M ) to set multiset, the property trivially holds. There are thus two interesting cases. Now, we branch depending on the last rule, that goes from configuration C ′ to D ′ , and we assume that P st t tr =⇒D ′ and that P tr =⇒f -1 (C ′ ) and with the above hypothesis over C ′ and f -1 (C ′ ).

• (E ′ , S ′ , P ′ ∪ # {out(n, M )|P ′ }, σ ′ , L ′ ) -→ (E ′ , S ′ , P ′ ∪ # {P ′ } ∪ # {out(n, M )}, σ ′ , L ′ )
We have two options regarding the processes set P of f -1 (C ′ ), which contains the pre-image of the state translation of {out(n, M )|P ′ }. Either insert t, M ; P ∈ P or insert t, M ; unlock t; P ∈ P. In both cases, we can make the reduction: • (E ′ , S ′ , P ′ ∪ # {in(n, x); P ′ } ∪ # {out(n, M )}, σ ′ , L ′ ) -→ (E ′ , S ′ , P ′ ∪ # {P ′ {M/x}}, σ ′ , L ′ ) By definition of the translation the processes set P of f -1 (C ′ ) contains the process {lock t; lookup t as x in P }. Further, as {out(n, M )} occurs in C ′ , we know by induction hypothesis that for f -1 (C ′ ) we have that [n → M ] ∈ S and t / ∈ L. We can thus reduce it with:

f -1 (C ′ ) -→ (E, S[t → M ], P ∪ # {P }, σ, L ∪ {t}) = f -1 (D ′ )
This new configuration satisfies the induction hypothesis, as {out(n, M )} does occur in D ′ , and even if [t → M ] ∈ S[t → M ], we have t ∈ L∪{t}, and as t is a pure state, unlock t; P / ∈ P (there must be an insert before) and lookup t as xinP / ∈ P.

We have demonstrated by induction the existence of a mapping satisfying our condition, that allows to show that the set of observable traces tr is indeed the same on both sides. This thus concludes the proof.

Remark that in practice, we perform the translation for each pure state t iteratively.

To complete the bijection, we thus only have to define the antecedent for such steps. For reductions that correspond to a partial execution of a translation, we simply map them to the same configuration as the previous one (f -1 (D ′ ) = f -1 (C ′ )), and it trivially preserves the induction hypothesis, as such steps never introduce a new out(n t , M ) in the multiset.

G Full semantics

Figure 1 :

 1 Figure 1: Protocol example in the applied π calculus

  let scen1 = in(c, <k 1,k 2>); !new sk ; (P(sk , k1)|Q(sk )). let scen2 = in(c, <k 1,k 2>); !new sk ; (P(sk , k2)|Q(sk )). equivalence scen1 scen2

  let scen1 = new sk ; (!new key ; P(sk ,key ) | !Q(sk )). let scen2 = !new sk ; (!new key ; P(sk ,key ) | !Q(sk )). equivalence scen1 scen2.

Figure 3 :

 3 Figure 3: Operational semantics (excerpt)

  Such a sequence of labels, together with the attacker knowledge σ of the resulting configuration defines a trace and denote the set of traces of a process P as traces pi (P ) = {(tr , σ) | ∃E, S, P, L. P tr =⇒(E, S, P, σ, L)} Moreover, we denote by tr ⇒ ⊢ the relation where In and Out facts are removed from the labels, and tr ⇒ ≈ the relation where we only keep the labels that are In and Out facts. Those relations yield the corresponding traces set traces pi ⊢ (P ) and traces pi ≈ (P ).

Example 1 .

 1 The process new a; (eventE(a) | out (c, h(a))) translates to Fr(a) -[]→ state 1 (a), state 2 (a) for the top-level new, and two rules for either side of the parallel: state 1 (a) -[ E(a) ]→ ∅ and state 2 (a), In(c) -[]→ Out(h(a)). In the latter rule, In(c) enforces that the channel c is known to the attacker before it can retrieve h(c). Using the predefined rule for freshness ∅ -[]→ Fr(x), we can rewrite ∅ to { Fr(b) } (for any b ∈ E) and proceed as follows: { Fr(b) }-→{ state 1 (b), state 2 (b) } E(b) ---→{ state 2 (b) }, producing the trace E(b).

Figure 4 :

 4 Figure 4: Benchmarks for path compression

  get lock_tbl(=t,x_n) in out(x_n,0) | P else 0

Figure 5 :

 5 Figure 5: Running time (seconds) of the case studies

Figure 7 :

 7 Figure 7: Benchmarks for the state facts option: running time (in seconds)

  let P = ... let Q = ... process (new skP; new skQ; !P | !Q)

  let P(skP,pkQ) = ... let Q(skQ,pkP) = ... process (new skP; new skQ; !P(skP,pk(skQ)) | !Q(skQ,pk(skP))

Definition 11 (

 11 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 }.

  S, P, σ, L) then (∅, ∅,P st t , ∅, ∅) tr =⇒f (C) = (E ′ , S ′ , P ′ , σ, L ′ ) such that, • S ′ = S \ [t → M ]; • L ′ = L \ {t}; • E ′ = E ∪ {n} if fn(t) ⊂ E and E ′ = E otherwise; • P ′ ⊃ P, E ′ st' t • out(n, M ) ∈ P ′ ifand only if [t → M ] ∈ StoreA, and t / ∈ L or unlock t; P ∈ P or lookup t as xinP ∈ P. And conversely if (∅, ∅, P st t , ∅, ∅)tr =⇒C ′ = (E ′ , S ′ , P ′ , σ, L ′ ) then (∅, ∅, {P }, ∅, ∅) tr =⇒f -1 (C ′ ) = (E, S, P, σ, L) with the same conditions.

f - 1

 1 (C ′ ) -→ (E, S[t → M ], P ∪ # {P }, σ, L \ {t}) = f -1 (D ′ )(remark that in one of the two cases, L\{t} = L) This configuration does satisfy the induction hypothesis, as we do have that out(n, M ) ∈ P ′ ∪ # {P ′ } ∪ # {out(n, M )}, and t / ∈ L \ {t} and [t → M ] ∈ S[t → M ].

  | out(t 1 , t 2 ); P output of t 2 on channel t 1 | insert t 1 , t 2 ; P set state t 1 to t 2 | in(t, x); P input on channel t a term bound to x | delete t; P delete state t | if ϕ then P else Q conditional | lookup t as x in P else Q read state t | let p = t in P else Q let binding

	⟨P, Q⟩ ::=
	(elementary processes)		(extended processes)
	0	null process	| event F ; P	event
	| new n; P	binding of a fresh name	| !P	replication
	| P | Q	parallel composition	(stateful processes)
			| lock t; P	lock a state
			| unlock t; P	unlock a state
		Figure 2: Syntax of our process calculus

(E, S, P, σ, L)

  Let P be a process without destructors symbols with a pure state t. We call n the fixed fresh name used in P st t . For the proof, we actually extend P, E st' t to some cases that do not occur in the normal translation: lookup t as x in P, E

	lock t; lookup t as x in P, E insert t, M ; unlock t; P, E st' t insert t, M ; P, E st' t :=	st' t :=	new a; P, E ∪ {a} st' := in(n, x); P, E t st' st' t out(n, M )| P, E t st' out(n, M )| P, E t	st' t	if fn(t) ⊂ E ∪ {a} else
	and where P We then define P st' is propagated inductively. t st t := P, ∅ st' t .
	Lemma 5. traces pi ⊢ (P ) = traces pi ⊢ ( P	st t )
	Proof. st' t unlock t; P, E st' t :=	:= in(n, x); P, E st' P, E t	st' t

a; P, E st' t := new a; new n; P, E ∪ {a, n}

We can represent a process as a binary tree and identify positions via sequences of 1 and

for the left and right branch, respectively,

We can extend this to arbitrary destructor terms in T (Fc, N , X ) simply by nesting several let expressions, one for each destructor symbol in the term.

The transformation can be extended to the case where destructors are defined with multiple rewrite rules dest(x i ) → u i by sequentially applying the transformation of dest(x i+1 ) → u i+1 on the else-branch of the translation of dest(x i ) → u i . Since our rewrite system is convergent, we can arbitrarily fix the order of application of rewrite rules.

In the symbolic model, we assume that keys generated by a KEM are uniformly sampled.

Timing obtained by running the SSH model of[START_REF] Lafourcade | Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties[END_REF] on the same laptop with the same version of Tamarin.

The model leads to over a thousand partial deconstructions.

Additonal lemmas and nounif instructions.

F Proverif export F.1 Without states

We introduce the semantics of ProVerif of in Fig. 8, dropping the part of the configuration dedicated to phases. A configuration E, P, A is given by a multiset P of processes, representing the current state of the process, a set of names E representing the free names of P and the names created by the adversary, and a set A of terms known by the adversary. The semantics of processes is defined through a reduction relation l -→ o where l is either the empty label or a label of the form msg(M, N ) or event(ev) with M, M being terms and ev being an event.

We remark that the classical semantics of ProVerif does not have conditionals if M = N then P else Q, because it can be encoded using a let binding with a equal function symbol destructor, let equal(M, N ) = true inP else Q. We however consider that it is now included in the semantics and the syntax, as it is simpler for our translation. We also add the prefix -P to all rule names, to not coincides with the rules names for our Sapic + semantics.

We denote by traces proverif (P ) the set of traces (observable events) of a process with respect to the ProVerif semantics.

F.2 Translation of non-static states

We rely on the cell semantics from the GSVerif extension [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF]. It allows to declare a channel over which all actions can be fired only once. Static states are translated using the encoding presented in Appendix E.2.3.

For non static states, each state identifier is associated with a corresponding secret name, where the association is stored inside a table state tbl. The secret name for an identifier is generated during the first access to the state, i.e., when trying to get the secret name inside the table fails and we go inside the state tbl. To ensure that two secret names are not created for the same channel, we must make those operations atomic through the use of a dedicated locking channel s.

Locks are modelled in a similar fashion.

Definition 18. Let P be a process such that on every path on the syntactic tree, each unlock is mapped injectively to a lock, without any other unlock in between nor parallel and replication operators (this corresponds to the general syntactic restriction over processes of [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]). We assume two table identifiers state tbl and lock tbl, as well as a secret channel s. We assume that for each state identifier t occurring in P , we have fresh variables c t , x t , y y ∈ X and a fresh name n t ∈ N priv .

lock t; P and where P P-st is inductively propagated.

To prove the validity of the translation, we require that the general syntactic conditions on lock t and unlock t given in [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] holds (we actually also need it for the export to Tamarin, it is a syntactic condition without which the language does not make sense). It ensures that on every possible path through the process tree, each unlock is injectively mapped to a single lock without replication or parallel between them. Lemma 6. Let P be a process with only the equality predicate. We denote by P PV the process out(s, 0); P P-st . We have that:

trans(traces proverif ( P PV ) = traces pi K (P )

Proof. We denote by tr ⇒ ProVerif the reduction relation corresponding to traces proverif . We show that there exists a bijective mapping f between configurations of P and P P-st such that, for all tr , (∅, ∅, {P }, ∅, ∅) tr =⇒C = (E, S, P, σ, L) ⇔ (∅, { P P-st }, ∅, ∅})

• t ∈ L if and only if there exists a unique n t ∈ E ProVerif such that lock tbl(t, n t ) ∈ T and {out(n t , 0)} / ∈ P ProVerif ;

• [t → M ] ∈ StoreA if and only if there exists a unique n t ∈ E ProVerif such that state tbl(t, n t ) ∈ T and {out(n t , M )} ∈ P ProVerif .

• P P-st ⊂ P ProVerif

We reason by induction on the last step of the reduction. ⇒ We branch depending on the last rule, that goes from configuration C to D, and we assume that (∅, ∅, {P }, ∅, ∅) tr =⇒D and P st t tr =⇒f (C) with the above hypothesis over f (C). We only consider reduction steps that concern a state operation, as the mapping is trivial for all others.

• (E, S[t → M ′ ], P ∪ # {insert t, M ; P }, σ, L) -→ (E, S[t → M ], P ∪ # {P }, σ, L) By induction hypothesis, the translation of the insert occurs in the processes of f (C) and as

there exists a unique n t ∈ E ProVerif such that state tbl(t, n t ) ∈ T and {out(n t , M ′ )} ∈ P ProVerif .

And we do have for f (D) that out(n t , M ) ∈ P ′ ProVerif , needed as we have in D the store S[t → M ]. The other hypothesis are inherited form D = f (C) by the induction hypothesis.

By induction hypothesis, the translation of the insert occurs in the processes of f (C) and as t does not appear in S, there does not exist state tbl(t, n t ) ∈ T and {out(n t , M ′ )} / ∈ P ProVerif . We can thus take the else branch, and reduce to:

And as in the previous case, this new configuration satisfies the induction hypothesis.

• (E, S[t → M ], P ∪ # {lookup t as x in P else Q}, σ, L) -→ (E, S, P ∪ # {P {M/x}}, σ, L)

By induction hypothesis, the translation of the lookup occurs in the processes of f (C) and as [t → M ] ∈ S[t → M ], there exists a unique n t ∈ E ProVerif such that state tbl(t, n t ) ∈ T and {out(n t , M )} ∈ P ProVerif . We can then perform the reduction:

This new configuration then meets the hypothesis, as we once again have P on one side and P {M/x} P-st on the other.

• (E, S, P ∪ # {lookup t as x in P else Q}, σ, L) -→ (E, S, P ∪ # {Q}, σ, L)

The translation of the lookup occurs in the processes of f (C). Further, by induction hypothesis, as t does not occur in S we have that there does not exist any state tbl(t, n t ) ∈ T . We can then perform the reduction:

And this new reduction does satisfy the induction hypothesis.

• We do not detail the lock and unlock cases, that are simpler occurrences of the previous cases, and also similar to the proof of Lemma 5.

⇐ We branch depending on the last rule, that goes from configuration C ′ to D ′ , and we assume that P st t tr =⇒D ′ and that P tr =⇒f -1 (C ′ ) and with the above hypothesis over C ′ and f -1 (C ′ ). We defined previously the bijection for all reduction steps that do not concern a translation of a process, or concerns the last step of the reduction of a translated process.

Standard operations: (E, S, P ∪ # {insert t1, t2; P }, σ, L) -→ (E, S[t1 → t2], P ∪ # {P }, σ, L) (E, S, P ∪ # {delete t; P }, σ, L) -→ (E, S[t → ⊥], P ∪ # {P }, σ, L) (E, S, P ∪ # {lookup t as x in P else Q }, σ, L) -→ (E, S, P ∪ # {P {u/x}}, σ, L)

if S(t ′ ) =E u is defined and t =E t ′ (E, S, P ∪ # {lookup t as x in P else Q }, σ, L) -→ (E, S, P ∪ # {Q}, σ, L) if S(t ′ ) is undefined for all t ′ =E t (E, S, P ∪ # {lock t; P }, σ, L) -→ (E, S, P ∪ # {P }, σ, L ∪ { t }) if t̸ ∈ E L (E, S, P ∪ # {unlock t; P }, σ, L) -→ (E, S, P ∪ # {P }, σ, L \ { t ′ | t ′ =E t })