A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis Full Version Kevin Morio∗

Yavor Ivanov

Robert Künnemann

kevin.morio@cispa.de CISPA Helmholtz Center for Information Security Saarbrücken, Germany

yavorivanov.yi@gmail.com CISPA Helmholtz Center for Information Security Saarbrücken, Germany

robert.kuennemann@cispa.de CISPA Helmholtz Center for Information Security Saarbrücken, Germany

arXiv:2608.06315v1 [cs.CR] 6 Aug 2026

Abstract

in a formal language, then employing symbolic methods to either discover attacks or establish their absence. Two prominent tools in this domain are Tamarin [26] and ProVerif [6]. While both tools pursue the same high-level objective, their divergent input languages and verification methodologies present significant barriers to leveraging their complementary strengths. Tamarin models protocols using multiset rewrite rules (MSRs), whereas ProVerif employs the applied-𝜋 calculus. ProVerif typically exhibits superior performance due to an abstraction step that avoids backtracking, though this may result in spurious attacks. Tamarin employs constraint solving, which may be less efficient and does not always guarantee automatic termination, yet it eliminates spurious attacks and provides interactive proof guidance. These fundamental differences render switching between tools nontrivial. In this work, we present a sound translation from Tamarin to ProVerif that enables systematic comparative analysis of these tools. Our translation provides a common ground for directly comparing their verification capabilities, identifying the core logic fragment they share, and understanding which formalism features have practical impact. Our soundness guarantee ensures that any property verified in ProVerif within the faithful translation fragment also holds in the original Tamarin model. We use a Tamarin model of Lowe’s fix of the Andrew Secure RPC protocol as the case study to show the intended workflow: start with a previously published stateful Tamarin model, translate it automatically, and use ProVerif as a fast backend for non-injective and injective agreement. Nevertheless, the fundamental differences between Tamarin and ProVerif preclude a complete translation. Tamarin’s logic fragment is strictly more expressive than ProVerif’s, necessitating careful handling of property specifications. Where feasible, we systematically rewrite Tamarin lemmas into logically equivalent ProVerif queries that preserve the intended semantics. Certain Tamarin built-ins, specifically multiset and bilinear-pairing, admit no translation. Diffie-Hellman support is partial, and XOR is translated only as a best-effort approximation outside the soundness theorem. We evaluate our approach on 121 Tamarin models, addressing the following research questions: RQ1 What common core logic fragment do Tamarin and ProVerif share for security properties? RQ2 What novel encodings enable expressing Tamarin’s features in ProVerif? RQ3 To what extent do helping lemmas from Tamarin improve verification in ProVerif? RQ4 What are the performance trade-offs between the tools on comparable models?

Protocol verification tools enable the formal modeling and automatic verification of security protocols. Two prominent tools in this area are Tamarin and ProVerif. While they share the same high-level goal, they differ significantly in their underlying formalisms and verification techniques, making a systematic comparison challenging. Tamarin uses multiset rewrite rules with sound and complete verification, whereas ProVerif employs an extension of the applied𝜋 calculus that provides fast but potentially incomplete results. In this work, we present a sound translation from Tamarin to ProVerif that enables a rigorous comparison of the two tools. Our translation introduces novel techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, showing how Tamarin’s features can be expressed in ProVerif’s formalism while precisely characterizing the cases where this is not possible. The translation supports an extensive subset of Tamarin’s features—including multiset rewrite rules, lemmas and restrictions—thereby aligning the semantics of the two formalisms. We compare the expressiveness of Tamarin’s logic fragment with that of ProVerif, identifying which properties can be faithfully translated. Moreover, we provide formal soundness and completeness proofs: within the faithful translation fragment, soundness ensures that any property verified in ProVerif also holds in the original Tamarin model, while completeness ensures that exists-trace properties not involving attacker knowledge are preserved by the translation. Best-effort encodings, in particular XOR, are reported separately and are outside these guarantees. Finally, we conduct an extensive evaluation of our translation on 121 Tamarin models. The translation covers 562 of 566 lemma tasks. Among non-XOR tasks with definitive results from both tools, 246 of 247 agree, with the remaining verdict explicitly flagged as using an incomplete model. Among the 362 tasks for which Tamarin returns a Boolean result and ProVerif completes with a logical result, ProVerif is faster in 334 cases (92.3 %), with median per-task runtime and peak-memory ratios of 6.74× and 6.24×, respectively.

1

Introduction

The design and verification of security protocols present significant challenges. The complexity of protocol interactions and the subtlety of attack vectors make manual analysis error-prone, motivating the development of automated verification tools. Such tools enable rigorous checking of whether protocols satisfy their intended security guarantees by expressing both the protocol and desired properties ∗ This is an extended version of [27].

1

Kevin Morio, Yavor Ivanov, and Robert Künnemann

SAPiC+

[12]

Tamarin

[12]

[12]

This work

DeepSec

language that requires strong modeling discipline and should ideally be produced by compiling from a more high-level language. Nevertheless, a substantial body of Tamarin models, e.g., TLS [16], WPA2 [18] and Signal [17], suggests that modelers are not at all averse to using MSRs as an input language. Cheval et al. [12] extend this approach to a platform, so that a single protocol specification (in a revised version of SAPiC, SAPiC+) translates to three different symbolic protocol verification tools: Tamarin, ProVerif and DeepSec. The differences between SAPiC+ and ProVerif, both descendants of the applied-𝜋 calculus, mainly concern the encoding of explicit state (in ProVerif) and term algebra with destructor symbols (in SAPiC+). Our translation of Tamarin’s security properties to ProVerif queries builds on their work. SAPiC+ allows embedding MSRs in a process, but thus far only the translation to Tamarin supports this feature. We thus integrate our MSR-to-ProVerif translation to add this missing piece to the SAPiC+-to-ProVerif translation.

ProVerif

Figure 1: Overview of related work and our contribution.

Contributions. This work makes the following contributions: • A sound translation from Tamarin to ProVerif incorporating novel encodings for multiset rewrite semantics and simultaneous events • A characterization of the common core logic fragment shared by both tools • Systematic identification of semantic gaps and their practical implications • A large-scale empirical study (121 models), including the Lowe case study, demonstrating significant overlap in verified results and practical performance gains

Translation from MSR to applied-𝜋. The only work translating from MSRs to applied-𝜋 was written well before Tamarin was developed. Bistarelli et al. [5] thus focus on a theoretical connection with little regard to the size of the model or the efficiency of verification. They relate first-order multiset rewriting to an (unnamed) process algebra that borrows from the 𝜋-calculus and the Calculus of Communicating Systems (CCS), and they show that trace properties like secrecy and authentication are preserved. For the most basic interactions, i.e., network input and output, their translation is similar to ours; however, it is limited to MSRs where (1) roles can be clearly identified (i.e., no setup or out-of-band state synchronization); (2) roles are linear (no conditionals, no state machines), and (3) roles are finite (no replication). Moreover, the intruder model is considered to be part of the protocol description. This is in contrast to Tamarin and ProVerif, where the intruder model is part of the semantics for optimization reasons. In this early work, protocols were still analyzed by hand. Altogether, these limitations facilitate the translation and soundness proof to the point where they share very little structure with our work. In contrast to prior work, our approach soundly and comprehensively translates Tamarin’s MSRs to ProVerif’s applied-𝜋 calculus while addressing scalability and applicability.

Outline. We discuss related work in Section 2 and provide background on Tamarin and ProVerif in Section 3. Our translation approach is presented in Section 4. The soundness argument is developed in Section 5. Implementation details are provided in Section 6. We evaluate our approach in Section 7 and conclude in Section 8.

2

Related Work

We review prior work on formal verification tools, translations between their respective formalisms, relevant external feature extensions of ProVerif, and comparative analyses of verification tools. Figure 1 gives an overview of the translations between these tools and situates our contribution. Protocol Verification Tools. Over the years, several approaches have been proposed to formally model and verify security protocols (see [3] for a survey). Among the most widely used protocol verification tools are Tamarin [26] and ProVerif [6, 8]. DeepSec [14] is used for bounded analysis of equivalence properties such as privacy and anonymity. DeepSec and ProVerif both employ a dialect of the applied-𝜋 calculus [1], which extends Milner’s 𝜋-calculus with the ability to send free terms, making it well-suited for modeling the ‘perfect cryptography’ assumption of the Dolev-Yao model and concurrent communication between parties. In contrast, Tamarin’s multisetrewriting calculus is very similar to term-rewriting, with Tamarin forcing a specific structure onto terms, describing the overall system state as a multiset of ‘fact’-terms. Term rewriting has also been used directly to analyze cryptographic protocols in Maude-NPA [21].

ProVerif Extensions. ProVerif does not support the faithful representation of algebraic properties due to the lack of an associative function symbol. This limits the modeling of certain cryptographic primitives, such as XOR operations and Diffie-Hellman exponentiation. Küsters and Truderung [23, 24] describe a reduction step from protocols using XOR and Diffie-Hellman exponentiation to protocols without them, which can then be analyzed by ProVerif. Since this reduction is a separate protocol-dependent step requiring user intervention, it is outside the scope of our automatic translation approach. It is, however, orthogonal to our translation from Tamarin to ProVerif and can be applied to the translated ProVerif models as a post-processing step.

Translation from applied-𝜋 to Tamarin. There are two prior works translating from applied-𝜋 to MSR—the opposite of the direction we are interested in. Kremer and Künnemann [22] provide a translation from the Stateful Applied Pi Calculus (SAPiC), an extension to the applied-𝜋 calculus adding state access, to MSRs supported by Tamarin. The authors suggest thinking of MSR as a low-level

Comparative Analysis of Verification Tools. Although numerous protocol-verification tools have been developed, systematic comparative studies remain limited. Early pairwise comparisons examined specific tools like Scyther and ProVerif on selected protocols [19], while performance-based evaluations compared execution time and 2

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

unary fact symbol Fr. Terms being received or sent are represented by In and Out, respectively.

memory consumption across multiple tools including Tamarin and ProVerif [25]. Recent comprehensive surveys have evaluated the latest versions of major tools [2], yet these studies often face challenges due to incompatible input languages and divergent modeling assumptions. While translation frameworks like SAPiC+ [12] now enable cross-tool verification, systematic model-level comparisons under semantically equivalent specifications remain scarce. Our translation-based approach addresses this gap by enabling direct, large-scale empirical comparison between Tamarin and ProVerif on semantically equivalent models.

3

Example 1. [ !Ltk(𝐴, 𝑘), In(𝑥) ] −[ Enc(𝑥, 𝑘) ]→ [ Out(senc(𝑥, 𝑘)) ] This rule models that agent 𝐴 receives a message from the network, encrypts it with its long-term key 𝑘, and transmits the ciphertext. An exclamation mark in front of a fact symbol indicates that it is persistent and can be consumed arbitrarily often. For example, freshness Fr is a linear fact, whereas !Ltk is a persistent fact. In Example 1, !Ltk(𝐴, 𝑘) is therefore a persistent fact recording that 𝑘 is 𝐴’s long-term key, while the action fact Enc(𝑥, 𝑘) labels the encryption step.

Background

We briefly recall the main concepts of Tamarin [26] and ProVerif [6]. We present the two formalisms separately and emphasize the translation links between MSRs and processes, Tamarin action facts and ProVerif events, as well as lemmas and queries.

3.1

Traces. For a fact multiset 𝑀, let lfacts(𝑀) and pfacts(𝑀) denote its linear and persistent facts, respectively, and let set (𝑀) discard multiplicities. We mark multiset inclusion, difference, and union with a # superscript: ⊂ # , \# , and ∪# . From here on, R denotes a finite set of Tamarin MSRs, ru = 𝑙 −[ 𝑎 ]→ 𝑟 a single rule, G the set of ground facts, G # the multisets of ground facts, and ginsts𝐸 (R) the set of ground instances of R modulo an equational theory 𝐸. We define a labeled transition relation →ginsts𝐸 ( R ) ⊆ G # ×G # ×G # as a rewriting step between multisets of ground facts, with 𝑆 ∈ G # denoting the current state. Rewriting is possible if all facts in 𝑙 are in 𝑆 and replaces all linear facts in 𝑙 with all facts in 𝑟 . Formally:

Tamarin

Terms. In Tamarin, messages are represented by abstract terms composed of function symbols that represent cryptographic primitives. The terms are drawn from an order-sorted term algebra, where each term is assigned a sort. The sorts form a partially ordered set with a top sort, msg, and two incomparable subsorts: fresh and pub. The sort fresh (fresh names) models random values such as keys and nonces. The sort pub (public names) models known constants, such as the identities of protocol parties. For each sort 𝑠, there is a countably infinite set of variables V𝑠 . The union of all such sets is the set of variables V. Keys and nonces are constants from a countably infinite set of names N , divided into public (attacker) names PN and secret (protocol) names FN . Given a set of variables V, the set of terms T (Σ, PN, FN, V), short T , is thus constructed over N and V and applications of function symbols in the signature Σ on terms. Let 𝑓 ∈ Σ𝑛 denote a function symbol with arity 𝑛, alternatively written as 𝑓 /𝑛. When we apply a substitution 𝜎, i.e., a well-sorted partial function from V to T , to a term, we substitute each variable 𝑣 in the domain of 𝜎 by the term 𝜎 (𝑣). Let vars(𝑡) denote the set of variables occurring in a term 𝑡 and vars+ (𝑡) denote the set of variables occurring in 𝑡 if 𝑡 is not a variable, i.e., vars+ (𝑡) = ∅ if 𝑡 ∈ V and vars+ (𝑡) = vars(𝑡) otherwise. To equip terms with a meaning, Tamarin allows the user to define a set of equations 𝐸 ⊆ T × T , for instance, sdec(senc(𝑦, 𝑥), 𝑥) = 𝑦 to model encryption. Tamarin then considers terms modulo the equivalence relation =𝐸 defined as the smallest equivalence relation that (1) contains 𝐸, (2) is closed under application of function symbols, and (3) is closed under substitution of variables by terms. For instance, 𝑓 (sdec(senc(𝑔(𝑚), 𝑘), 𝑘)) =𝐸 𝑓 (𝑔(𝑚)).

𝑙 −[ 𝑎 ]→ 𝑟 ∈ ginsts𝐸 (R)

lfacts(𝑙) ⊆# 𝑆

pfacts(𝑙) ⊆ set (𝑆)

𝑎

𝑆→ − ginsts𝐸 ( R ) (𝑆 \# lfacts(𝑙)) ∪# 𝑟

Definition 1 (Executions and Traces). An execution of a set of rules R is a sequence of transitions from multisets of ground facts labeled by action-fact multisets starting with the empty multiset 𝑎1

𝑎𝑛

[ ] −−→ginsts𝐸 ( R ) 𝑆 1 · · · −−→ginsts𝐸 ( R ) 𝑆𝑛 , such that no fresh name is chosen twice, i.e., for the special fact symbol Fr, we have 𝑆𝑖+1 \# 𝑆𝑖 = [ Fr(𝑛) ] and 𝑆 𝑗+1 \# 𝑆 𝑗 = [ Fr(𝑛) ] implies 𝑖 = 𝑗. The set of executions is denoted by execsmsr (R). The set of traces tracesmsr (R) is the projection on the action labels in execsmsr (R) including empty action multisets. The set of weak traces wtracesmsr (R) is also the projection on the action labels in execsmsr (R) but excluding empty action multisets. Definition 2 (Reachable state). A state 𝑆 is reachable if it can be 𝑎 reached from the initial state 𝑆 0 by a chain of → − ginsts𝐸 ( R ) transitions: 𝑎1

𝑎𝑛

𝑆 0 −−→ginsts𝐸 ( R ) . . . −−→ginsts𝐸 ( R ) 𝑆𝑛 = 𝑆 .

Protocol Model. The protocol’s behavior is modeled as a system of labeled multiset rewrite rules (MSRs) of the form ru = 𝑙 −[ 𝑎 ]→ 𝑟 , where prems(ru) = 𝑙 are the premises of the rule, concls(ru) = 𝑟 the conclusions and acts(ru) = 𝑎 the actions that label the rule. The facts in 𝑎 are called action facts and annotate the trace. These rules rewrite a multiset of ground facts from the set G, where a fact F(𝑡 1, . . . , 𝑡𝑘 ) of arity 𝑘 is ground if all 𝑘 terms 𝑡 1, . . . , 𝑡𝑘 are ground and terms are ground if they contain no variables. There are predefined fact symbols for special purposes. The fact that a name 𝑛 ∈ FN is fresh (i.e., was not used before) is marked with the

Tamarin combines a user-defined set of rules describing the protocol itself with the built-in rules for message deduction MD depicted in Figure 2. These rules represent a standard Dolev-Yao attacker who obtains knowledge (!K) by eavesdropping on the network (Out), creating fresh names (Fr), or using public values. The knowledge can be used to construct new terms by applying function symbols. Network communication is mediated by Out and In: MDOut turns a protocol output Out(𝑥) into attacker knowledge !K(𝑥), and MDIn lets the attacker provide any known term to a protocol rule by producing In(𝑥). The action fact K(𝑥) on MDIn 3

Kevin Morio, Yavor Ivanov, and Robert Künnemann

[ Out(𝑥) ] −−−−→ [ !K(𝑥) ]

(MDOut)

[ Fr(𝑥 : fresh) ] −−−−→ [ !K(𝑥 : fresh) ]

(MDFresh)

[ ] −−−−→ [ !K(𝑥 : pub) ]

(MDPub)

[ !K(𝑥 1 ), . . . , !K(𝑥𝑘 ) ] −−−−→ [ !K(𝑓 (𝑥 1, . . . , 𝑥𝑘 )) ]

When the process encounters an instance of the term g(𝑡 1, . . . , 𝑡𝑛 ), it tries to rewrite it according to one of the rules in def(g). If it succeeds, it returns the term 𝑡 ∈ T . If none of the rules are applicable, the destructor application fails and the process blocks. Destructors can also be defined as private, in which case they can occur in the process but are not available to the adversary.

(MDApp)

K(𝑥 )

[ !K(𝑥) ] −−−−→ [ In(𝑥) ]

(MDIn) Example 2. Let the constructor senc/2 model symmetric encryption. Decryption can be described with an additional constructor sdec/2 and the equation sdec(senc(𝑚, 𝑘), 𝑘) =𝐸 𝑚, as in Tamarin. Alternatively, decryption can be described with a destructor sdec/2 defined through the rewrite rule sdec(senc(𝑚, 𝑘), 𝑘) → 𝑚. If we supply an invalid key to the destructor, it will fail and block the execution, whereas sdec(senc(𝑚, 𝑘), 𝑘 ′ ) with 𝑘 ≠ 𝑘 ′ is a valid term, albeit irreducible. Hence, the destructor can model an encryption scheme that detects valid ciphertexts.

Figure 2: The set of message deduction rules MD.

records this use of attacker knowledge in the trace. Executions and traces are accordingly defined over ginsts𝐸 (R ∪ MD ∪ { Fresh }), where the built-in rule Fresh : [ ] → − [ Fr(𝑥 : fresh) ] creates fresh names; to ease notation, we keep writing R in the subscripts. Trace Properties. Properties are expressed as lemmas in the form of trace properties. These are specified as trace formulas over a two-sorted first-order logic that supports quantification over both messages and timepoints. Thus, in addition to the sort msg that ranges over terms, a second sort temp is used for timepoints. Trace atoms have the form F(𝑡®)@𝑖, referring to Tamarin action facts at trace timepoints. Tamarin supports both universal (all-trace) and existential (exists-trace) trace properties. The former requires that the property holds for all traces, while the latter only requires the existence of at least one such trace. The Lowe case study in Section 4 uses all-trace secrecy and agreement properties.

Protocol Model. Both the implementation of ProVerif and its underlying calculus have gone through several iterations. For the purpose of this work, it suffices to consider the core language as described in [7]. Its syntax is shown in Figure 3c. For readability, we omit types in the presentation. The implementation uses the default type bitstring throughout. The empty process 0 terminates a process definition. In the grammar, a semicolon separates a construct from its continuation; the calculus has no general sequential composition. The process out(𝑐, 𝑡); 𝑃 outputs 𝑡 on channel 𝑐 and continues as 𝑃, while in(𝑐, 𝑥); 𝑃 receives a message from 𝑐, binds it to 𝑥, and continues as 𝑃. The process 𝑃 | 𝑄 runs 𝑃 and 𝑄 in parallel, and the replication !𝑃 runs arbitrarily many copies of 𝑃. The restriction new 𝑛; 𝑃 creates a fresh name 𝑛 scoped to 𝑃 and then executes 𝑃. The construct let 𝑥 = 𝑡 in 𝑃 else 𝑄 evaluates 𝑡: on success, it binds the result to 𝑥 and executes 𝑃; otherwise, it executes 𝑄. Evaluation can fail because of an incorrect destructor application. The construct if 𝐸 then 𝑃 else 𝑄 similarly executes 𝑃 when 𝐸 evaluates to true and 𝑄 otherwise. In both constructs, an omitted else branch means 𝑄 = 0, so failed evaluation terminates execution. The event construct enables the specification of trace properties. Events are written as F(𝑡 1, . . . , 𝑡𝑛 ) where F ∈ Σ𝑛fact is an event symbol and 𝑡 1, . . . , 𝑡𝑛 are terms. They do not influence the execution of a process. Events record that a certain point in the protocol execution was reached with certain values, specified as the event’s arguments. Tables provide a mechanism for persistent storage in ProVerif models. Once a value has been added to a table, it cannot be deleted or replaced. Tables are declared with a number of columns 𝑛; processes can append a row of 𝑛 values (with insert) or retrieve an arbitrary row that matches a pattern (with get). If there is a match, 𝑃 is executed, otherwise the (optional) process 𝑄 is executed. Note that the declared tables are not accessible by the attacker.

Definition 3 (Tamarin’s two-sorted first-order logic). Let 𝑖, 𝑖 ′ ∈ V𝑡𝑒𝑚𝑝 (timepoint variables), 𝑤 ∈ V𝑚𝑠𝑔 (term variables), and 𝑓 ∈ Σ𝑛 . Furthermore, 𝑡 1, . . . , 𝑡𝑛 ∈ T . Tamarin’s trace formula logic is defined by the grammar in Figure 3a. To determine if a trace formula 𝜑 holds, Tamarin converts it into an equivalent guarded trace property. First, 𝜑 is transformed into negation normal form (NNF), where negations apply only to trace atoms, and the remaining operations are ∧, ∨, ∃, or ∀. A formula in NNF is a guarded trace formula if it has the form ∃® 𝑥 . (F@𝑖) ∧ 𝜓 or ∀® 𝑥 . ¬(F@𝑖) ∨ 𝜓 , where 𝜓 is itself a guarded trace formula and the trace atom F@𝑖, called the guard, ensures that all quantified variables are instantiated with terms or indices that occur in the trace, 𝑥® ⊆ vars(F@𝑖) ∩ (V𝑚𝑠𝑔 ∪ V𝑡𝑒𝑚𝑝 ). A guarded trace formula that contains only terms in V ∪ PN and where all variables are quantified is called a guarded trace property.

3.2

ProVerif

Terms. In ProVerif, cryptographic primitives are specified as constructor symbols, which correspond directly to Tamarin’s function symbols. ProVerif supports destructors, which can also be used to define cryptographic operators and the relationships between them, much like, and as an alternative to, equations in Tamarin. We define the set of terms T to contain all constructor terms, i.e., all terms without destructor symbols. This definition aligns with the previous definition of T for Tamarin. Like in Tamarin, equational theories can be defined as a finite set of equations 𝐸 ⊆ T × T . By contrast, a destructor g is a partial function T 𝑛 → T (for some arity 𝑛 ∈ N) that a process can apply. The semantics are provided by an ordered list of rewrite rules def(g), each of the form g(𝑡 1, . . . , 𝑡𝑛 ) → 𝑡.

Traces. We define a labeled transition relation →𝑝𝑣 ⊆ C × L × C, where C denotes a process configuration and 𝑙 ∈ L a label, as a reduction relation between process configurations. A process configuration C = (E, P, T, A) is defined in a way similar to [13, Appendix F.1, Fig. 8], where • E contains the free names of P and names created during execution by the protocol or adversary; 4

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

⟨𝐹 ⟩ ::= 𝐼 [ ⇔ 𝐼 ] ⟨𝐼 ⟩ ::= 𝐷 [ ⇒ 𝐼 ] ⟨𝐷⟩ ::= 𝐶 (∨ 𝐶) ∗

⟨𝑞⟩ ::= 𝐹 ∧ . . . ∧ 𝐹 | 𝐹 ∧ . . . ∧ 𝐹 =⇒ 𝐻

⟨𝐶⟩ ::= 𝑁 (∧ 𝑁 ) ∗

⟨𝐻 ⟩ ::= 𝐹 | 𝐻 ∧𝐻 | 𝐻 ∨𝐻 | 𝐹 =⇒ 𝐻 | 𝐶 | ⊥

⟨𝑁 ⟩ ::= [¬] 𝐴 ⟨𝐴⟩ ::= (𝐹 ) | [∃ | ∀] 𝑙 + . 𝐹 | F(𝑡 1, . . . , 𝑡𝑛 )@𝑖 | 𝑡 = 𝑡′ | 𝑖 <¤ 𝑖 ′ | 𝑖  𝑖′ | ⊥

⟨𝐹 ⟩ ::= F(𝑡 1, . . . , 𝑡𝑛 )@𝑖 | attacker(𝑡)@𝑖 ⟨𝐶⟩ ::= 𝑡 ◦𝑒 𝑡 ′ with ◦𝑒 ∈ {=, ≠} ¤ , <, ¤ ̸ } | 𝑖 ◦𝑡 𝑖 ′ with ◦𝑡 ∈ {≤,

⟨𝑙⟩ ::= 𝑖 | 𝑤 (a) Tamarin’s trace formula grammar.

(b) ProVerif’s trace formula grammar.

⟨𝑃, 𝑄⟩ ::= 0 | out(𝑐, 𝑡); 𝑃 | in(𝑐, 𝑥); 𝑃 | 𝑃 |𝑄 | !𝑃 | new 𝑛; 𝑃 | let 𝑥 = 𝑡 in 𝑃 else 𝑄 | if 𝐸 then 𝑃 else 𝑄 | event(𝑓𝑒 (𝑡 1, . . . , 𝑡𝑛 )); 𝑃 | insert tbl(𝑣 1, . . . , 𝑣𝑛 ); 𝑃 | get tbl(𝑝 1, . . . , 𝑝𝑛 ) in 𝑃 else 𝑄 (c) ProVerif’s process calculus grammar.

Figure 3: Grammars for Tamarin and ProVerif. Tamarin’s full trace formula logic is shown to illustrate its expressiveness. ProVerif’s grammar shows the SA-QBF fragment used for correspondence and reachability queries, omitting phases and native injective correspondences. Injective agreement is instead handled by the two-query SA-QBF encoding of Section 4.2. • P is a multiset of processes representing the current state of the process; • Tis the set of table entries 𝑇 (𝑀1, . . . , 𝑀𝑛 ) inserted during the process execution up to this point; and • A is a set representing the adversary knowledge. The set E is partitioned into the disjoint sets N𝑝𝑢𝑏 and N𝑝𝑟𝑖𝑣 , for public (attacker) names and private (protocol) names, respectively. We transition between process configurations by applying reduction rules from [13, Figure 8]. The label 𝑙 is either empty (𝜖), an event, or a mess label. Executions of out and new add terms to the adversary knowledge. Notably, the set A can be saturated by applications of the App rule. This rule corresponds to the adversary obtaining terms by applying constructors and destructors to terms from its knowledge set.

Trace Properties. In ProVerif, trace properties are categorized into reachability and correspondence properties, both of which start with the keyword query (see Figure 3b). A query contains events emitted by the process or attacker predicates attacker(𝑡)@𝑖, stating that the attacker can derive term 𝑡 at timepoint 𝑖. Reachability properties are of the form query F1 && . . . && F𝑛 , where F𝑖 are events. They ensure the existence of at least one trace in which all the events F1, . . . , F𝑛 occur and are hence comparable to Tamarin’s exists-trace lemmas. Correspondence properties are of the form query F1 && . . . && F𝑛 −→ 𝐻 , where F1, . . . , F𝑛 are events and the hypothesis 𝐻 is a quantifier-free trace formula over trace atoms. They are universally quantified over all traces and are comparable to Tamarin’s all-trace lemmas. Thus, a correspondence query reads: whenever the premise events F1, . . . , F𝑛 occur together, the conclusion 𝐻 must also be justified in the same trace. The disjunctive normal form of 𝐻 must not contain negated events. Internally, ProVerif translates reachability queries into correspondence queries with the conclusion ⊥, so all queries can be treated as implications. In contrast to Tamarin, ProVerif only allows a single quantifier alternation. The variables occurring in the premise are universally quantified, while the variables occurring in the conclusion but not in the premise are existentially quantified. This convention is the main syntactic difference the lemma translation must manage: Tamarin exposes quantifiers explicitly, while ProVerif infers them from where variables occur in the query.

Definition 4 (Executions and Traces). A ProVerif execution is a sequence of reduction rule applications starting with the initial process configuration C0 = (E0, {𝑃 }, ∅, A0 ) 𝑙1

𝑙𝑛

C0 − → → C1 · · · −→ → C𝑛 . The transitions in the execution are annotated with the labels of the applied rules. The set of executions is denoted by execspv (𝑃). The set of traces tracespv (𝑃) is the projection on the labels in execspv (𝑃) including empty labels (𝜖). The set of weak traces wtracespv (𝑃) is also the projection on the labels in execspv (𝑃) but excluding the empty labels 𝜖. In contrast to Tamarin, which annotates transitions by multisets of action facts, ProVerif uses atomic labels such as events and message labels. To ease the comparison of both tools, we implicitly lift ProVerif’s atomic labels to singleton multisets of labels.

Definition 6 (SA-QBF). Figure 3b presents the syntax of ProVerif’s logic fragment we target, which we call SA-QBF (single-alternation quantified Boolean formulas). This fragment captures ProVerif’s correspondence and reachability queries, excluding phases and native injective correspondences. The translation of injective agreement remains in this fragment by decomposing the source property into correspondence and uniqueness queries (Section 4.2). When a timepoint inequality between 𝑖 and 𝑗 occurs in the conclusion

Definition 5 (Reachable configuration). A ProVerif configuration 𝑙

C is reachable if there is a chain of → − → transitions starting at the initial configuration C0 such that 𝑙1

𝑙𝑛

C0 − → → . . . −→ → C𝑛 = C . 5

Kevin Morio, Yavor Ivanov, and Robert Künnemann

Table 1: Correspondence between Tamarin and ProVerif constructs. The channel 𝑐 is a global public channel in ProVerif. Tamarin source construct

ProVerif target construct

Storage fact F(𝑡®) Premise fact F(𝑡®) Conclusion fact F(𝑡®) In(𝑡 ) Out(𝑡 ) Fr(𝑛) Action fact F(𝑡®) All-trace lemma Exists-trace lemma

Table entry F𝑡𝑏𝑙 (𝑡®) get F𝑡𝑏𝑙 (𝑡®) insert F𝑡𝑏𝑙 (𝑡®) in(𝑐, 𝑡 ) out(𝑐, 𝑡 ) new 𝑛 Event event(F(𝑡®) ) Correspondence query Reachability query

Each subprocess emulates Tamarin MSR semantics using ProVerif’s table construct. For each fact symbol F with arity 𝑛 in Tamarin, we create a corresponding ProVerif table F𝑡𝑏𝑙 with the same arity (the multiset encoding of Section 4.4 adds one further identifier column). Modifications of the protocol state in Tamarin through facts are then emulated by inserting and looking up entries in these tables. Since tables in ProVerif are monotonic, this is an over-approximation. We discuss in Section 4.4 how we overcome this limitation. The special fact symbols In, Out and Fr, whose semantics are defined through the built-in intruder deduction rules MD in Figure 2, are treated differently. These facts have direct counterparts in ProVerif: in, out and new. Tamarin supports pattern matching on facts in a rule’s premise     F(ℎ(𝑥)) → − Out(𝑥) .

of a formula, where 𝑖 and 𝑗 are the time variables associated with facts F and G, respectively, the following two conditions must hold: (1) F@𝑖 occurs in the premise or F is an event; (2) G@𝑗 occurs in the conclusion or G is an event.

In contrast, ProVerif permits only tuple patterns and equality tests in inputs (in) and table lookups (get), but no matching under other constructors such as ℎ(𝑥). To emulate this behavior, we introduce private auxiliary destructors that extract variables from patterns. These destructors are translation helpers used only inside the generated process; they are private, not attacker operations, and not additional cryptographic capabilities. If exposed to the attacker, they would otherwise allow them, for example, to look inside encrypted messages. We create such destructors for each variable 𝑣 and top-level function application 𝑡 occurring in a pattern in the premise of a rule. Let 𝑔𝑣,𝑡 denote the destructor extracting 𝑣 from 𝑡 with the rewriting rule 𝑔𝑣,𝑡 (𝑡) → 𝑣. For the above example, we introduce the destructor 𝑔𝑥,ℎ (𝑥 ) and obtain

Remark 1. ProVerif queries must conform to SA-QBF as presented in Figure 3b. In particular: (1) reachability queries do not support disjunctions, (2) correspondence queries do not support conjunctions at the top level, and (3) negation is not supported in queries. These restrictions necessitate query rewriting and splitting for certain Tamarin lemmas (see Section 4.2). ProVerif also supports phases and native injective correspondences beyond SA-QBF; neither is needed for the exact encodings used here.

4

Translation

Our translation serves two purposes: (1) enabling practical use of ProVerif on Tamarin models, and (2) providing a rigorous foundation for comparative analysis. The translation challenges we address reveal fundamental differences between the formalisms. We introduce novel encoding techniques that bridge these gaps where possible and precisely characterize the remaining limitations. The translation is composed of three main parts: process generation, property translation, and bridging semantic gaps between the two tools. Table 1 summarizes the main syntactic correspondences. The remainder of this section expands these correspondences and explains the cases where they require additional encoding.

4.1

get F𝑡𝑏𝑙 (auxℎ (𝑥 ) ) in let 𝑥 = 𝑔𝑥,ℎ (𝑥 ) (auxℎ (𝑥 ) ) in out(𝑐, 𝑥) for an auxiliary variable auxℎ (𝑥 ) not occurring elsewhere. To formally define the translation, we introduce a sequencing operator that applies a process expression to each element of an ordered multiset, using a fixed lexicographical order for names, terms, and facts. Definition 7 (Sequencing Operator). Let 𝑋 be an ordered multiset, 𝑒 : 𝑋 → Process a process expression, and 𝑃 a follow-up process. The sequencing operator seq is defined as

Rule Translation

Given a set of MSRs R = {ru1, . . . , ru𝑛 }, we translate each rule to a subprocess in ProVerif. These subprocesses run in parallel and are replicated to allow multiple applications. The translated process of a rule ru is denoted by ⟦ru⟧. At a high level, premises of a Tamarin rule become ProVerif inputs or table lookups, action facts become ProVerif events, and conclusions become outputs or table insertions. We then translate R to the process

  𝑃  seq 𝑒 (𝑥); 𝑃 ≔ 𝑒 (𝑦); seq 𝑒 (𝑥); 𝑃   𝑥 ∈ # 𝑋 \# [ 𝑦 ] 𝑥 ∈ #𝑋 

if 𝑋 = ∅ if 𝑦 = min 𝑋

For example, for the names 𝑎, 𝑏, 𝑐 ∈ N , we have seq new 𝑥; 0 = new 𝑎; new 𝑏; new 𝑐; 0

⟦R⟧ ≔ ! ⟦ru1 ⟧ | · · · | ! ⟦ru𝑛 ⟧ .

𝑥 ∈ # {𝑎,𝑏,𝑐 }

Next, let aux(𝑡) be 𝑡 if 𝑡 ∈ V and a fresh auxiliary variable aux𝑡 otherwise. We can define the translation of Storage facts (all facts except In, Out, and Fr) and input facts that may contain patterns.

The replication of each subprocess is an over-approximation, but we do not lose precision, since ProVerif’s Horn clause abstraction acts as an implicit top-level replication, which can be pushed down the parallel composition. 6

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

Definition 8 (Translation of Storage facts).

lemma in the case study. The header, auxiliary destructors, and the instrumentation of Section 4.4 are omitted for brevity. The lefthand side uses Tamarin’s concrete syntax for multiset rewriting: the multisets before, between, and after the arrow are the premises, action facts, and conclusions, respectively. The two get commands implement premise facts stored in ProVerif tables, in implements the network input, the event commands implement Tamarin action facts, and the final insert/out commands implement the conclusion facts.

⟦F(𝑡 1, . . . , 𝑡𝑛 )⟧; 𝑃 := get F𝑡𝑏𝑙 (aux(𝑡 1 ), . . . , aux(𝑡𝑛 )) in seq let 𝑣 = 𝑔𝑣,𝑡𝑖 (aux𝑡𝑖 ) in

1≤𝑖 ≤𝑛, 𝑣 ∈vars+ (𝑡𝑖 )

𝑃 For input and output facts, we use a single public channel 𝑐 for all communication to emulate Tamarin’s global network model. Definition 9 (Translation of input facts). Let 𝑐 be the public channel.

4.2

⟦In(𝑡)⟧; 𝑃 := in (𝑐, aux(𝑡));

Lemma Translation

Tamarin lemmas are translated into ProVerif queries, all-trace lemmas as correspondence queries and exists-trace lemmas as reachability queries. Since the two tools use different logics for expressing properties (Figure 3), a direct translation is not always possible. While Tamarin’s logic fragment is strictly more expressive than ProVerif’s SA-QBF, we follow a systematic rewriting approach that allows us to translate a large class of Tamarin lemmas to logically equivalent ProVerif queries. Operationally, the translation turns Tamarin action facts F(𝑡®)@𝑖 into ProVerif events of the same shape and then arranges them into the query form described in Section 3: all-trace implications become correspondences, while exists-trace goals become reachability queries. The Lowe case study illustrates both the direct correspondence translation and a stronger property that requires decomposition. The verified non-injective agreement lemma for role A has the correspondence shape

seq let 𝑣 = 𝑔𝑣,𝑡 (aux(𝑡)) in

𝑣 ∈vars+ (𝑡 )

𝑃 Observe that the get and in processes have no else branches. This emulates the behavior of a rule being applicable only if all facts of its premise satisfy the patterns and are present in the current protocol state. ProVerif denotes variables that are matched instead of bound by prepending the variable name with ‘=’. This becomes relevant when a variable occurs both in a pattern and directly in the fact. In this case, we prefix it with ‘=’ in the get or in to indicate that it is matched, as shown in Figure 4. The two remaining parts of the translation are action facts and the handling of public variables. Action facts are directly translated to ProVerif events. Tamarin allows public variables (variables of sort pub) in action facts and Out facts that are not bound in the premise of a rule, which ProVerif does not support. We define a generic function pubv that returns the set of public variables in a term or fact as a term list. We prepend in(𝑐, pubv(·)) to action facts and Out facts such that the ProVerif attacker can instantiate the public variables.

∀𝐴 𝐵 𝑡 𝑖. CommitA(𝐴, 𝐵, 𝑡)@𝑖 =⇒ (∃𝑗 . RunningB(𝐴, 𝐵, 𝑡)@𝑗 ∧ 𝑗 < 𝑖) ∨ (∃𝑟 . Reveal(𝐴, 𝐵)@𝑟 ). The injective variant additionally excludes a distinct second commit for the same payload:

Definition 10 (Rule Translation). A rule ru = 𝑙 −[ 𝑎 ]→ 𝑟 is translated to the following process.

∀𝐴 𝐵 𝑡 𝑖. CommitA(𝐴, 𝐵, 𝑡)@𝑖 =⇒ (∃𝑗 . RunningB(𝐴, 𝐵, 𝑡)@𝑗 ∧ 𝑗 < 𝑖

⟦ru⟧ ≔ seq ⟦F⟧;

∧ ¬∃𝐴′ 𝐵 ′ 𝑖 ′ . CommitA(𝐴′, 𝐵 ′, 𝑡)@𝑖 ′ ∧ 𝑖 ′ ≠ 𝑖)

F∈ #𝑙 | Storage,In

∨ 𝑅(𝐴, 𝐵),

seq new 𝑛; Fr(𝑛) ∈ #𝑙

where 𝑅 abbreviates the disjunction of key-reveal exceptions. Although the nested uniqueness condition exceeds SA-QBF, it can be eliminated. Abstracting from the Lowe event names, let 𝐶𝑖 denote a commit, 𝑊 𝑗 its matching running witness, and 𝐶𝑖′′ a second commit with the same uniqueness key. The formula is equivalent to the conjunction of two supported correspondences:

seq (in(𝑐, pubv(𝑒)); event 𝑒); 𝑒 ∈ #𝑎

seq (in(𝑐, pubv(F)); insert F); F∈ # 𝑟 | Storage

seq (in(𝑐, pubv(𝑡)); out(𝑐, 𝑡)); Out(𝑡 ) ∈ # 𝑟

𝐶𝑖 =⇒ (∃𝑗 . 𝑊 𝑗 ∧ 𝑗 < 𝑖) ∨ 𝑅(𝐴, 𝐵),

0

𝐶𝑖 ∧ 𝐶𝑖′′ =⇒ 𝑖 = 𝑖 ′ ∨ 𝑅(𝐴, 𝐵).

The translated process first checks for the presence of all facts in the premise of the rule. Then, it draws all fresh names specified by Fr facts. Next, it translates each action fact by first inputting the public variables and then raising the corresponding ProVerif event. Finally, it applies all conclusions by inserting the corresponding table entries and performing all outputs, again inputting public variables first. This order ensures that ProVerif emits events only after the premises are met and never produces an output or table insertion before the corresponding action events. Figure 4 illustrates the translation on Lowe AS rule A_2, which produces the Commit_A event used by the non-injective agreement

For the forward implication, the first query drops uniqueness; applying the original formula to the first commit yields the second query because, absent 𝑅, its uniqueness conjunct forces the second commit to coincide. Conversely, absent 𝑅, the first query supplies a running witness and the second establishes uniqueness of the commit, reconstructing the original conjunctive witness branch. The escape disjuncts must occur in both queries: omitting them from the uniqueness query would reject duplicate commits that the original property excuses after a reveal. As in Section 4.4, the second query is emitted using equality of rule-instance identifiers. 7

Kevin Morio, Yavor Ivanov, and Robert Künnemann

Tamarin Rules

ProVerif Translation

rule A_2 : [ ! Key ( $A , $B ,~ sk ) , StateASend ( $A , $B ,~ sk ,~ na ) , In ( senc ( < '2 ' ,~ na , kabp , $B > ,~ sk )) ] - -[ Secret ( $A , $B , kabp ) , Commit_A ( $A , $B , < 'A ' , 'B ' ,~ sk , kabp >) ] - > [ Out ( senc ( < '3 ' ,~ na > , kabp )) , StateAReceive ( $A , $B ,~ sk ,~ na , kabp ) ]

let rA_2 = get tKey (A , B , sk ) in get tStateASend (st , =A , =B , =sk , na ) in in ( publicChannel , v0 : bitstring ); let (=v2 ) = g_var_v2_3 ( v0 ) in let (=na ) = g_var_na_4 ( v0 ) in let kabp = g_var_kabp_5 ( v0 ) in let (=B) = g_var_B_6 ( v0 ) in let (=sk ) = g_var_sk_7 ( v0 ) in new stA : bitstring ; let t = (vA , (vB , (sk , kabp ))) in event eSecret (A , B , kabp ); event eCommit_A (A , B , t ); insert tStateAReceive ( stA ,A ,B ,sk ,na , kabp ); out ( publicChannel , senc (( v3 , na ), kabp )).

Figure 4: Translation slice from the Lowe case study. Rule A_2 consumes the server’s encrypted response and the initiator’s local state, emits the secrecy and agreement events used by the case-study lemmas, records the new local state in a ProVerif table, and sends the third protocol message. Headers, auxiliary destructors, and the rule-instance identifier and DistinctFact instrumentation are omitted for clarity. hypothesis of Corollary 2. KU is an internal annotation of the same attacker deduction check and follows the same polarity test.

Both components are standard correspondences over the instrumented events, so their soundness follows from the correspondence translation and the exact rule-identifier equality argument of Remark 3; the equivalence above transfers this result to the source property. We do not use ProVerif’s native inj-event. It requires an injective mapping from commits to earlier matching runs, so distinct runs can justify duplicated commits with equal parameters. Tamarin’s formula forbids those duplicates unless an escape disjunct holds. Thus, inj-event is strictly weaker in the verification direction covered by Theorem 1, whereas the two-query encoding is equivalent to the source formula. As a validation check, native inj-event agreed with Tamarin in all nine decided cases of a tenlemma sample; the remaining case timed out. We first define the root target fragment for our formula rewriting.

Definition 12 (T-UKF and P-UKF). Let T-UKF be the restriction of TSA-QBF to formulas 𝜑 for which every K atom in NNF(¬𝜑) occurs positively, and P-UKF the corresponding ProVerif logic fragment. For our lemma translation, we can further extend the supported fragment in the following way: If 𝜑 is a formula in Tamarin’s full logic fragment that can be rewritten into ¬𝜓 , 𝜓 1 ∧ . . . ∧ 𝜓𝑛 , or 𝜓 1 ∨ . . . ∨ 𝜓𝑛 with 𝜓𝑖 ∈ T-UKF, then it can be translated into a negated query or multiple separate queries whose results can be combined to reconstruct the original semantics. For each generated query, the translation records whether its result is used directly or inverted and emits instructions for recombining multiple queries. All rewrites are selected from formula structure; protocol, rule, lemma, and event names do not select an encoding. The rewriting approach is based on two key observations about the differences between the logics. First, ProVerif does not support disjunctions in reachability queries. Hence, we split top-level disjunctions in exists-trace lemmas into separate ProVerif queries:

Definition 11 (TSA-QBF). Let TSA-QBF be the restriction of Tamarin’s logic fragment from Definition 3 to that of ProVerif from Definition 6, with K(𝑚)@𝑖 replacing attacker(𝑚)@𝑖.

(∃𝑥 𝑖. A(𝑥)@𝑖) ∨ (∃𝑦 𝑗 . B(𝑦)@𝑗) Before discussing the rewriting approach, we highlight a key semantic difference between K facts and ProVerif attacker predicates that influences the supported fragment. attacker(𝑚)@𝑖 holds whenever 𝑚 is deducible from the attacker’s knowledge at timepoint 𝑖, whereas K(𝑚)@𝑖 records that the attacker explicitly derived and used 𝑚. Hence, K(𝑚)@𝑖 implies attacker(𝑚)@𝑖, and once attacker(𝑚) holds, it remains true. K facts can thus be seen as a subset of attacker facts, which we make precise in Definition 22. Accordingly, the soundness condition is polarity-based: after negating an all-trace property and putting it in negation normal form, every K atom must occur positively. The translation renders each accepted K or KU atom as attacker. Premise-side existentials are prenexed into ProVerif’s universal query variables, while conclusion-only variables receive ProVerif’s implicit existential quantification. A negated K conclusion is first rewritten as a leading-negation reachability query. Residual negative knowledge atoms are rejected. Thus, the K case is exactly the positive-atom

becomes query x: bitstring, i: time. A(x)@i. query y: bitstring, j: time. B(y)@j. The original semantics are preserved: the lemma holds if and only if at least one of the resulting queries is satisfied. The generated output includes the corresponding recombination instruction. Similarly, ProVerif does not support top-level conjunctions in correspondence queries. Hence, we split top-level conjunctions in Tamarin formulas for all-trace lemmas into separate ProVerif queries. The lemma holds if and only if all resulting queries are satisfied. This distribution is used only when the resulting obligations are independently checkable. The second class of differences arises from ProVerif’s lack of support for negation in queries. We eliminate supported negations by the exact logical equivalences in Table 2; the first group converts between all-trace and exists-trace lemmas and records result inversion 8

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

Table 2: Representative exact lemma rewrites. Quantifiers abbreviate closures over all variables in scope. A top-level negation is implemented by inverting the generated query result; a list denotes separately checked queries whose results are conjoined. Transformation

Original

Rewritten

All-trace to exists-trace

∀𝜑 =⇒ ¬∃𝜓

¬(∃𝜑 ∧ ∃𝜓 )

Exists-trace to all-trace

∃𝜑 ∧ ¬∃𝜓

¬(∀𝜑 =⇒ ∃𝜓 )

Negated ∃ to all-trace

¬(∃𝜑 ∧ ¬∃𝜓 )

∀𝜑 =⇒ ∃𝜓

Positive-witness exists-trace

∃ (𝜑 ∧

Ó

Independent obligations

∀𝜑 =⇒ (𝜓 ∧ 𝜒 )

{ ∀𝜑 =⇒ 𝜓, ∀𝜑 =⇒ 𝜒 }

(𝜑 ∧ ¬𝜓 ) =⇒ 𝜒

𝜑 =⇒ ( 𝜒 ∨ 𝜓 )

𝜑 =⇒ (¬𝜓 ∨ 𝜒 )

(𝜑 ∧ 𝜓 ) =⇒ 𝜒

Move ¬ to conclusion Move ¬ to premise

𝑘 ¬𝜓𝑘 )

¬(∀𝜑 =⇒

A@𝑖 ∧ B@𝑗 =⇒ 𝑗 < 𝑖 ∨ 𝑖 = 𝑗. It also translates a forbiddenevent restriction whose opened body is a quantifier-free positive event formula. For example, ¬∃® 𝑥 . 𝑃 ∧ (𝑄 1 ∨ 𝑄 2 ) becomes the two prohibitions 𝑃 ∧ 𝑄 1 =⇒ ⊥ and 𝑃 ∧ 𝑄 2 =⇒ ⊥. The translation computes positive disjunctive normal form and emits one prohibition per branch, with expansion capped at 16 branches. Restriction conclusions containing nested implications remain unsupported and are omitted with an explicit warning, because ProVerif rejects nested queries in restrictions. Moreover, there are restrictions that can be translated but require deeper reasoning that is outside the scope of our automatic translation. For example, the restriction ¬∃𝑥 𝑖.Neq(𝑥, 𝑥)@𝑖,

Ô

𝑘 𝜓𝑘 )

which expresses the inequality of two terms, cannot be directly translated to ProVerif due to the negation. An equivalent formulation is ∀𝑥 𝑦 𝑖.Neq(𝑥, 𝑦)@𝑖 =⇒ 𝑥 ≠ 𝑦 can be translated. Uniqueness restrictions of the form ∀𝑥 𝑖 𝑗 . A(𝑥)@𝑖 ∧ A(𝑥)@𝑗 ⇒ 𝑖  𝑗 need no rewriting, as timepoint equalities in restrictions are directly supported by ProVerif. If the events carry rule-instance identifiers (Section 4.4), the equality is translated, like any other temporal equality, as an equality of the identifier variables. Tamarin allows regular lemmas to be reused as axioms in the verification of other lemmas. We translate reusable lemmas to ProVerif axioms. The limitations that apply to restriction translation also apply to axiom translation, as ProVerif axioms do not support negations either. The ProVerif build used in the evaluation supports timepoints in restrictions and axioms. Tamarin supports inductive reasoning for proving lemmas with the use_induction attribute. This is directly translated to ProVerif’s [inductive] query directive.

when a negation is moved to the top level. The implementation also translates all-trace nonexistence properties by using the leadingnegation reachability form. For the narrow event-free exists-trace case, the implementation instead uses attacker(()) as an alwaystrue premise: the empty tuple is public and always constructible, while ProVerif has no dedicated true query atom. The generated query then asks whether the forbidden event must occur under this premise and inverts the correspondence result. For an exists-trace property with a positive witness and a disjunction of possible violations, the translation negates the full property and emits one correspondence from that witness to the complete violation disjunction, again inverting the result. The disjunction is deliberately not split: every alternative must refer to the same premise witness. The translation also distributes independent all-trace conjuncts, moves supported guards from a premise to the conclusion, and recognizes an exact two-query conditional-existence decomposition whose no-match query retains the positive matching branch. These structural cases extend coverage without allowing separately generated queries to choose witnesses independently. The second table group moves negated subformulas between premises and conclusions of implications. In particular, the last rule is frequently used to convert secrecy properties expressing that the attacker does not know a secret unless it has been leaked.

4.3

4.4

Bridging Semantic Gaps

Multiset Semantics. One of the fundamental differences between Tamarin and ProVerif is that Tamarin’s MSRs operate on multisets of facts, whereas ProVerif’s tables are sets without delete operations. Hence, once a fact is added to a table, it remains there for the rest of the protocol execution. This leads to an over-approximation of the protocol behavior, as a ProVerif process can use the same fact multiple times, whereas Tamarin can consume it only once. To avoid this, for each linear storage fact in the right-hand side of a rule, we create a fresh value and add it as the first argument of the corresponding table entry. For each linear storage fact in the left-hand side of a rule, we then match on the fact together with its fresh value and add a DistinctFact(st, args) event for each such fact. We then add a restriction that ensures that no two such events have the same identifier and arguments.

Restriction & Axiom Translation

Tamarin restrictions are translated to ProVerif restrictions in a straightforward manner similar to lemmas. However, since ProVerif restrictions also do not support negations and there is no possibility to handle a leading negation, we can only split top-level conjunctions into separate restrictions. This limits the class of Tamarin restrictions that can be translated. The implementation does recognize temporal negations of the form ¬∃𝑖 𝑗 . A@𝑖 ∧ B@𝑗 ∧ 𝑖 < 𝑗, rewriting them to the equivalent universal ordering constraint

∀𝑠𝑡 𝑥 𝑖 𝑗 . DistinctFact(𝑠𝑡, 𝑥)@𝑖∧ DistinctFact(𝑠𝑡, 𝑥)@𝑗 ⇒ 𝑖 = 𝑗 The fresh identifier therefore preserves Tamarin’s multiset semantics in ProVerif. 9

Kevin Morio, Yavor Ivanov, and Robert Künnemann

Simultaneous Action Facts. Tamarin permits multiple action facts in a single rule that occur at the same timepoint. In contrast, ProVerif assumes a total order on events. We can simulate simultaneous action facts by introducing a fresh rule-instance identifier that ties all events in the translated process together. All queries having the same time variable for multiple action facts are rewritten to use distinct time variables for each action fact, with the additional identifier tying them together. For example, a formula

in the evaluation supports explicit temporal variables. For formulas with explicit timepoints, however, ProVerif does not insert this conclusion-before-premise order implicitly: a correspondence B@𝑗 =⇒ A@𝑖 constrains 𝑖 and 𝑗 only through explicit temporal constraints or through options such as conclBeforePremise. Without such a constraint, the formula asks only that whenever B occurs, some A occurs in the same trace. In contrast, Tamarin employs the standard logical interpretation of =⇒ without any implicit temporal ordering. When verifying B@𝑗 =⇒ A@𝑖, Tamarin searches for counterexamples by attempting to satisfy B@𝑗 ∧ ¬A@𝑖—the expected logical negation. Consequently, in Tamarin, the formula B@𝑗 =⇒ A@𝑖 is satisfied even when event B precedes event A temporally. However, this interpretation requires careful handling of trace prefixes. Without additional constraints, a prefix trace containing only event B would constitute a counterexample. To address this, we must add a progress restriction that ensures certain events are reached, thereby preventing incomplete trace prefixes from invalidating the property. The same prefix issue arises for an unguarded correspondence whose conclusion refers to a later event of the same rule. Translated cross-fact same-action properties instead use the completion event described above, without adding a progress restriction. The implication cases used by the translation are covered by the satisfaction relations in the proof; the following experiment only checks the interaction with ProVerif’s documented implementation behavior and progress restrictions. To validate our understanding of these semantic differences, we conducted a controlled experiment using a minimal model that permits events A, B, and C to occur only in that sequence. We included a progress restriction A =⇒ C to ensure that all considered traces terminate with event C. This progress restriction is preserved during translation between the tools. ProVerif successfully verified all three queries. In particular, we found that A =⇒ B, B =⇒ C, and A =⇒ C all hold. This matches the explicit-timepoint behavior described above: the progress restriction is treated as a liveness condition, filtering traces in which A occurs without a corresponding C, rather than as a precedence constraint. Thus, the experiment supports the implementation-side assumptions used for progress-restricted examples, while the formal guarantee remains limited to the faithfully translated fragment of Theorem 1.

∀𝑥 𝑖. A(𝑥)@𝑖 ∧ B(𝑥)@𝑖 =⇒ ∃𝑗 . C(𝑥)@𝑗 is rewritten into ∀𝑥 𝑟 𝑖 1 𝑖 2 . A(𝑟, 𝑥)@𝑖 1 ∧ B(𝑟, 𝑥)@𝑖 2 ⇒ ∃𝑗 . C(𝑥)@𝑗 . This translation preserves the semantics of the original formula, as the only way for both A(𝑟, 𝑥)@𝑖 1 and B(𝑟, 𝑥)@𝑖 2 to hold is if 𝑟 is instantiated to the same fresh value. Sequential emission also exposes a prefix between two events of the same translated rule. If a final correspondence observes one action fact in its premise and requires a different fact from the same Tamarin action in its conclusion, a shared identifier alone does not show that the second event has already been emitted. For these cross-fact same-action conclusions, affected rules emit RuleCompleted(𝑟 ) after all ordinary action events, and the translated conclusion is guarded by this completion event. A same-fact tautology does not require the event, and rules whose action facts are not involved in such a conclusion do not emit it. The completion event excludes prefixes that stop partway through the translated action. It is not a source-level timepoint and imposes no progress or liveness restriction. Temporal Equalities. In Tamarin, two action facts occur at the same timepoint exactly when they belong to the same rule instance; in ProVerif, two distinct events never share a timepoint. The ruleinstance identifiers introduced above make this expressible: we translate a timepoint equality 𝑖  𝑗 between distinct action facts as an equality between their identifier variables, and a negated equality as a disequality. Where the equality merely pins a quantified time variable, as in ∃𝑗 . B@𝑗 ∧ 𝑖  𝑗, we instead eliminate it and reuse the rule-instance-identifier rewriting for simultaneous action facts described above. Each event occurrence in a query receives its own identifier variable. Two occurrences share an identifier variable exactly when they are asserted to stem from the same rule instance. This sharing is derived from the identity of the original source binders: copied occurrences of one source timepoint retain one provenance, whereas independently scoped binders remain distinct even if they have the same printed hint. Since the identifiers are introduced by the translation and are invisible in the source lemma, this identifier-sharing discipline is the translation’s obligation, not the user’s.

Relating K-Facts and mess Facts. ProVerif also supports the predicate mess(𝑐, 𝑚), which we may view as recording that a message 𝑚 has been communicated on a channel 𝑐. Because the action fact K(𝑚) labels MDIn when In(𝑚) is produced but not yet consumed, Tamarin’s semantics allow visible action facts to occur between these two points in a trace. We therefore experimented with encoding K facts as mess(𝑐, 𝑚) facts and with adding restrictions to keep this separation between emission and consumption explicit. In our experiments, neither approach yielded a practical solution: restrictions caused significant verification overhead, and the encodings did not reliably preserve the intended semantics. Consequently, this mess-based encoding is not part of the translation and is outside the proof scope. It is distinct from the supported translation of K/KU atoms in T-UKF formulas to attacker predicates (Definition 12).

Semantic Differences in the Implication Connective. Our analysis revealed an interesting semantic distinction in the interpretation of the =⇒ connective between Tamarin and ProVerif. While both tools support this connective—Tamarin in all-trace lemmas and ProVerif in correspondence queries—their semantic interpretations differ subtly but importantly. The ProVerif manual [10, p.55] describes non-temporal correspondences such as B =⇒ A as requiring the conclusion event A to occur before the premise event B. The ProVerif build used 10

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

5

Table 3: Overview of excluded models.

Soundness & Completeness

We show that our translation is sound for model/property instances in the faithful translation fragment: if the property of such an instance holds in the ProVerif translation of a Tamarin model, then it also holds in the original Tamarin model.

Criterion

Definition 13 (Faithful translation fragment). A model/property instance (R, 𝐸, 𝜑) is in the faithful translation fragment when the satisfaction-preserving rewritings of Sections 4.2 and 4.4 reduce 𝜑 to a finite conjunction of T-UKF formulas, the model (R, 𝐸) uses only the MSR constructs mapped in Table 1 and detailed in Section 4, and its equational theory is classified as faithfully translated in Section 6. Built-ins for which no translation to ProVerif exists, such as Tamarin’s multiset and bilinear-pairing built-ins and Diffie-Hellman models requiring inverse, are outside this fragment. Models using XOR can be translated, but the best-effort encoding is not part of this fragment. Furthermore, each rewritten component is simultaneity-free: every time variable indexes exactly one trace atom, and no timepoint equality relates distinct trace atoms. Lemmas with simultaneous action facts are supported through the rewriting of Section 4.4, which produces simultaneity-free formulas over identifier-instrumented events. The detailed argument is given in Remark 3.

∀

msr tracespv (⟦R⟧) |=𝑃𝑉 (R) |=𝑇𝐸 𝜑 𝐸 ⟦𝜑⟧ ⇒ traces

For the converse direction, we show that satisfiability is preserved: if a property without K facts is satisfied by some Tamarin trace, it is satisfied by some trace of the translation. This covers exists-trace lemmas. For all-trace lemmas, the converse of Theorem 1 does not hold in general: the translation over-approximates Tamarin’s traces—for example, by executions stopping between the events of a single rule—so ProVerif may report spurious counterexamples. This is consistent with ProVerif’s over-approximating design; a ProVerif proof remains conclusive by Theorem 1.

Invalid DH pattern matching Well-formedness warnings

93 35

Pot. unsound

Models with stored proofs Duplicate models Archived / obsolete models Translated from other formalisms

37 27 23 19

Avoid distortion

Not verifiable

Usage and Warnings. Translation is invoked via tamarin-prover -m=proverif, producing a self-contained ProVerif model with all necessary destructors, names, tables, and parallel composition of translated rules. The intended workflow is to keep Tamarin as the source model and use the generated ProVerif file primarily as a fast backend artifact; the file remains inspectable and editable, but its control flow follows the table-based state-machine structure of the source MSRs rather than a handwritten process style. The implementation provides systematic warnings to guide result interpretation: When an exact structural normalization produces multiple queries or an inverted result (Section 4.2), it records how the query results must be combined. Colliding bound timepoint names are alpha-renamed automatically before query generation. When a property remains outside the supported fragment, the implementation reports the precise rejected shape and emits no approximate query. Separately, if an axiom or restriction cannot be translated, the generated model is marked and the user is warned that any verifier outcome concerns an incomplete model.

Theorem 2 (Completeness for existential properties). For (R, 𝐸, 𝜑) in the faithful translation fragment such that 𝜑 itself is simultaneityfree, belongs to TSA-QBF, and contains no K facts: ∃

tracesmsr (R) |=𝑇𝐸 𝜑 ⇒ tracespv (⟦R⟧) |=𝑃𝑉 𝐸 𝜑 Both proofs are provided in Appendix B.6.

6

Out of scope

Built-in Theories. The implementation distinguishes faithfully translated theories from features that cannot be translated and features that are translated only as best-effort approximations. Ordinary constructors, user equations accepted by both tools, private helper destructors, and the encodings for MSR state are part of the faithful translation fragment defined in Definition 13. Tamarin’s multiset and bilinear-pairing built-ins cannot be translated. The same holds for Diffie-Hellman models requiring inverse. Models using any of these features are excluded from the comparison. Diffie-Hellman support uses a best-effort translation derived from SAPiC+ , and XOR support is partial. As discussed in Section 7.4, the XOR encoding is not covered by Theorem 1 because ProVerif cannot faithfully represent associative symbols and the self-inverse XOR equation. When XOR is used, the implementation emits a warning that the resulting verification results may be unsound.

Theorem 1 (Soundness). For every (R, 𝐸, 𝜑) in the faithful translation fragment:

∃

Reason

327 113 46 12

No lemmas / rules 29 Requires preprocessor flags 22 Errors / timeout during preprocessing 2

For a rewritten source property, ⟦𝜑⟧ denotes the conjunction of its translated components. Soundness applies to each T-UKF component and lifts to the source property through conjunction and the stated satisfaction equivalence.

∀

Count

Unsupported built-ins / DH inv SAPiC models Observational equivalence Accountability lemmas

Implementation

The translation is integrated with Tamarin’s export framework and builds on the ProVerif export module from SAPiC+ [12]. It supports MSR features including multiset rewrite rules with pattern matching, restrictions, helping lemmas, and the security-property fragment characterized in Definition 13. The implementation is distributed as part of Tamarin’s export functionality.

7

Evaluation

We analyze 121 Tamarin models, examining both where the tools achieve consistent results and where they systematically diverge. 11

Kevin Morio, Yavor Ivanov, and Robert Künnemann

Table 4: Comparison of Tamarin and ProVerif outcomes on the 562 successfully translated lemma tasks, using the candidatepatched ProVerif toolchain. Entries marked ∗ are best-effort XOR cases outside the soundness theorem. Tamarin Result

ProVerif Result

Total

True

False

None

OOM

Timeout

185 19∗ 18 –

1† 46 – –

35 4 2 2

61 11 9 4

38 11 4 –

49 –

12∗

Universal properties (all-trace)

450

True False OOM Timeout Existential properties (exists-trace)

320 91 33 6 112

True OOM Total successfully translated lemmas

–

11 –

19 4

17 –

108 4 562

OOM = Out of Memory. “None” is a logical inconclusive result; OOM and timeout are resource outcomes. Dashes (–) indicate zero cases. ∗ Due to best-effort XOR translation outside the soundness theorem (see Section 7.4). † The dp3t::upload_auth incomplete-model result discussed in Section 7.4.1.

Our evaluation serves two purposes: (1) validating that the translation allows a meaningful comparison, and (2) revealing insights about the tools’ relative capabilities.

and two no-step regression properties (true to inconclusive); all other paired verdicts are identical.

7.1

7.2

Key Findings

Our analysis reveals a substantial common core between the tools. Among non-XOR tasks, 246 of 247 definitive pairs agree; the remaining pair is explicitly flagged because ProVerif decides an incomplete translation of the dp3t model (Section 7.4.1). Best-effort XOR results remain outside the faithful fragment, with 34 agreements and 31 disagreements among definitive pairs. The four in-fragment functional lemmas are inconclusive under the candidate-patched build. The primary bottleneck is ProVerif’s termination rate on more complex lemmas. Throughout, ProVerif demonstrates significant performance advantages (faster verification, lower memory usage). These results, enabled by our translation, provide the first large-scale empirical comparison of Tamarin and ProVerif on semantically equivalent models. As described in Section 4.2, certain Tamarin lemmas require splitting into multiple ProVerif queries due to top-level disjunctions (in exists-trace lemmas) or conjunctions (in all-trace lemmas), while others require negation handling where the ProVerif result must be negated to obtain the result for the original lemma. In our evaluation, we used a wrapper that automatically interprets and combines the results from split queries according to the appropriate logical connective and negates results when necessary. The generated output includes the same reconstruction instructions, so users invoking the translation directly need not infer the connective or result polarity unaided. Unless stated otherwise, the outcome counts use our candidate liveness patch for restrictions with event conclusions. Our reliablechannel encoding requires ProVerif’s extended restriction semantics. The developers confirmed our report and fixed the issue in working_dev_branch commit 8122b55c; official releases remain on master. Our evaluation predates this fix and runs on our own candidate patch. Compared with the pinned build, the patch changes only four functional reachability queries (false to inconclusive)

Dataset & Scope of Comparison

Our dataset is based on the largest curated set of Tamarin models to date: the example directory in Tamarin’s code base. This diverse collection includes feature showcases, regression tests, and, importantly, the models of various conference publications. To enable a meaningful comparative analysis, we excluded several categories of models (shown in Table 3) and obtained a representative set of 121 models for our comparison. The resulting dataset contains 53 publication- or thesis-origin models (40 core published case-study models from major venues and 13 derived feature or test variants), together with 7 classic protocol models, 18 SPORE models, 4 literature benchmarks, and 39 internal or synthetic pedagogical models (121 total). The models average 208 lines of code overall, while the core published case studies average 381 lines. This dataset exhibits a survivorship bias: models are typically included only if their analysis (e.g., verification or attack discovery) terminates without user interaction. Exceptions exist, including legacy models, models created to showcase new features or to highlight bugs, and “model suites” that use Tamarin’s macro language to produce different variants of the same protocol in different threat models. Some models also come with manually constructed proofs; in such cases, both the original model and a corresponding proofannotated version—often one per proven lemma—are preserved. First, we exclude models that are out of scope for this work. This includes models using Tamarin built-ins that cannot be faithfully translated (multiset, bilinear-pairing, diffie-hellman with inverse). Moreover, we discard all SAPiC models, as their translation has already been evaluated in prior work [12]. We also exclude models using observational equivalence (diff mode). Although ProVerif also supports observational equivalence, Tamarin and ProVerif implement it too differently for a direct translation. Finally, we exclude models focusing on accountability properties, as they require a different treatment. In total, this includes 498 models. 12

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

property of XOR to deduce 𝑥 from 𝑥 ⊕ 𝑦 and 𝑦, which Tamarin’s XOR theory handles but ProVerif’s approximation cannot. The other Tamarin-false all-trace lemmas yield 4 inconclusive results, 11 outof-memory results, and 11 timeouts in ProVerif. Since these XOR cases are outside that fragment, they are not counterexamples to Theorem 1. The practical reason for including XOR is empirical: many XOR lemmas do not exercise the unsupported associative or self-inverse reasoning. Across the 29 evaluated XOR models, both tools agree on 34 of the 65 lemmas for which both tools return a Boolean result; the remaining 31 are the XOR disagreements reported in Table 4. Other XOR lemma runs do not produce a comparable result because one tool returns None, runs out of memory, or times out. The implementation warning described in Section 6 marks these verdicts as outside the formal guarantee, so they can be used as fast diagnostics but not as standalone soundness evidence. When Tamarin is resource-bound on all-trace tasks, ProVerif returns true in 18 cases, inconclusive in 4, out-of-memory in 13, and times out in 4; ProVerif has no false results in these rows. For the 108 exists-trace lemmas that Tamarin verifies, ProVerif agrees in 49 cases and returns “false” for 12, all of which are besteffort XOR translations; a false reachability result is a proof of unsatisfiability within ProVerif’s abstraction, not a failed search. The remaining runs are 11 inconclusive results, 19 out-of-memory results, and 17 timeouts; four inconclusive results are the functional lemmas discussed next. For the four exists-trace lemmas on which Tamarin runs out of memory, ProVerif also runs out of memory. Across all transformation families, 246 of 247 non-XOR definitive pairs agree. The injective-agreement encoding yields agreement in all 34 definitive pairs; ten additional injective-agreement tasks are resource-bound. The only non-XOR disagreement is the flagged dp3t cell.

Second, we exclude models whose soundness of the verification result cannot be guaranteed. This includes models using ambiguous and therefore invalid pattern matching on DH terms, e.g., (𝑔𝑎 )𝑏 = (𝑔𝑏 )𝑎 cannot uniquely determine whether 𝑥 = 𝑔𝑎 or 𝑥 = 𝑔𝑏 . We also exclude models with critical well-formedness warnings in Tamarin (not subterm convergent equations, missing facts, unbound variables), as we cannot be sure that Tamarin gives the correct result in this case. This category contains 128 models. Third, to avoid distortion of the dataset, we exclude models with stored proofs, duplicates of the same model (e.g., used as both feature showcase and regression test), models marked as archived or obsolete, as well as translations from SAPiC+. This category encompasses 106 models. Fourth, we discard models without rules or lemmas (used for regression and feature tests), models that require a specific set of preprocessor flags to be evaluated, and models producing errors or timeouts during precomputation. This encompasses 53 models. These exclusions provide a meaningful basis for comparison.

7.3

The Common Core Logic Fragment

The 121 models contain 566 lemma tasks. Our translation generates queries for 565 tasks. The ProVerif front end accepts 562 tasks (99.3 %), leaving four outside the executable translation. The sole static property failure, dp3t::soundness, has a quantifier alternation that the structural normalizer cannot translate without changing its witness dependencies. ProVerif rejects the three generated queries for the Okamoto model because its equational theory is non-convergent, which Tamarin supports [20]; the model was designed to demonstrate that extension. We do not count inconclusive or resource-bound tasks as translation failures. These cases define the expressiveness boundary. The translation handles the narrow event-free exists-trace shape, shared positive witnesses, compound all-trace properties, and same-action completion patterns described in Section 4.2. Within the supported fragment, accepted knowledge atoms use ProVerif’s attacker predicate. This covers secrecy, authenticationwith-reveal, and source lemmas. It also handles bound-name collisions by alpha-renaming, temporal-negation restrictions, all-trace nonexistence, and the correspondence-plus-uniqueness form of injective agreement.

7.4

7.4.1 Failure Cases and Mitigation Paths. Three qualifications explain the cells where the tools do not reach the same definitive result. First, XOR can change the result because the current encoding does not preserve all XOR reasoning. For the nonce_secrecy lemma of NSLPK3xor, Tamarin finds the expected attack, whereas ProVerif verifies the secrecy query under the best-effort approximation. For the executable lemma of CH07, Tamarin witnesses the expected execution trace, whereas ProVerif proves the corresponding query unreachable under the best-effort encoding. These cases justify the warning emitted for XOR models: their results are useful diagnostics but not faithful-translation evidence. Future versions could incorporate ProVerif-specific XOR reductions, such as those of Küsters and Truderung [23], before invoking ProVerif on the translated model; the practical coverage of such reductions on our 31 XOR disagreements has not been quantified in this work. Second, the four non-XOR exists-trace cases on which ProVerif is inconclusive do not reflect a limitation of the translation. The functional lemmas in mixvote_ShHh and aletheaDR_ShHh (and their SmHh variants) each encode an honest end-to-end vote-counting execution requiring 13 action facts. Tamarin finds the trace, whereas ProVerif is inconclusive when using our candidate liveness patch for restrictions with event conclusions. The pinned build’s unreachable verdicts result from the locally reproduced restriction-handling defect; all all-trace results in the affected theories are unchanged under the candidate patch. Third, dp3t::upload_auth is false in ProVerif but true

Verification Outcome

Having established the expressive boundary of both tools, we now examine how they perform. We separate formally guaranteed results from best-effort XOR results, which are interpreted only as empirical cross-checks. Table 4 gives a comprehensive overview of the verification results categorized by all-trace (correspondence queries) and exists-trace properties (reachability queries). For all-trace lemmas, Tamarin verifies 320 lemmas, of which ProVerif also verifies 185; ProVerif returns one false result on the incomplete dp3t translation, 35 inconclusive results, 61 out-of-memory results, and 38 timeouts. ProVerif also confirms 46 of Tamarin’s 91 counterexamples. In 19 cases, ProVerif verifies a lemma for which Tamarin finds an attack. These cases are exclusively from models using Tamarin’s built-in XOR theory and are expected results of our best-effort translation: the attacker must exploit the self-inverse 13

Kevin Morio, Yavor Ivanov, and Robert Künnemann

Table 5: Lowe case-study results. In the agreeing-total row, times are summed and memory is the per-lemma peak maximum; injective-agreement measurements use the candidate-patched ProVerif build. Tamarin Lemma

Time (s) secrecy noninjectiveagreement_A noninjectiveagreement_B injectiveagreement_A injectiveagreement_B

agree agree agree agree agree

Agreeing total

Memory (MiB)

Time (s)

Memory (MiB)

0.768 0.298 4.076 2.762 22.033

89.8 81.6 129.9 157.1 324.2

0.048 0.049 0.048 0.148 0.170

12.6 12.7 13.1 14.7 15.6

29.937

324.2

0.463

15.6

where each In fact is inherently consumed exactly once, enabling this setting is obligatory to maintain semantic equivalence. Disabling precision has asymmetric soundness implications: for all-trace lemmas, verified results remain sound (the overapproximation still holds), but for exists-trace lemmas, only disproven results are reliable—verified traces may rely on input reuse not possible in Tamarin. To assess the practical impact, we compare the default evaluation setting with an otherwise identical run that omits preciseActions. The two evaluation settings agree on 223 of 225 paired Boolean results. In both disagreements, Tamarin and ProVerif with preciseActions verify the property, whereas ProVerif without this directive reports a counterexample: injective_agree in NSLPK3 and injectiveagreement_A in Otway-Rees. Moreover, 105 Boolean results obtained with the default setting become inconclusive without precision. Thus, preciseActions is required to prevent spurious input reuse and preserve the source MSR semantics, rather than being merely a proof-search optimization.

in Tamarin only after four time-ordering restrictions with nested implications are dropped, so the recorded restriction_missing verdict is for an incomplete, weaker model rather than a faithful disagreement; dp3t::soundness is separately excluded because its formula is not translated. The same unsupported restriction shape occurs in robert; those translated tasks are resource-bound rather than disagreements, timing out after 7200 s in the final run.

7.5

ProVerif

Outcome

Impact of Translation Features

We characterize the impact of several key features of both ProVerif and our translation. For each feature comparison, we rerun all 566 tasks and assess verdict preservation on the tasks for which both evaluation settings return Boolean results. First, we are interested in the effectiveness of our formula rewriting and novel encoding techniques for multiset rewriting and simultaneous events introduced in Section 4. Second, we analyze the impact of ProVerif’s precision settings as described in [10]. Third, we investigate whether ProVerif benefits from helping lemmas written specifically for Tamarin.

Incomplete Models. Of the 562 translations, 380 use complete translated models (294 all-trace and 86 exists-trace), while 182 omit at least one axiom or restriction (156 all-trace and 26 exists-trace). Specifically, 130 omit an axiom (118 all-trace and 12 exists-trace), and 77 omit a restriction (61 all-trace and 16 exists-trace). These categories overlap. Reusable axioms are helping lemmas and do not change process traces, although their omission may affect proof search and termination. Omitting a restriction can only enlarge the trace set. Consequently, verified all-trace results and disproven exists-trace results remain conservative, whereas disproven alltrace results and verified exists-trace results may depend on the incomplete model. Among the 77 accepted translations with a missing restriction, ProVerif disproves exactly one all-trace lemma and verifies no exists-trace lemma. The sole non-conservative logical verdict is dp3t::upload_auth, the only definitive non-XOR disagreement; we exclude it from the faithful comparison set.

Encoding Techniques. Among the 562 successfully translated lemmas (450 all-trace, 112 exists-trace), 85 all-trace lemmas produce multiple ProVerif queries, including the correspondence-plusuniqueness encoding of injective agreement; no exists-trace lemma produces multiple queries. The reconstructed result is inverted for 36 all-trace and 76 exists-trace lemmas. Source-timepoint splitting is used in 45 all-trace and 13 exists-trace lemmas. This shows that our rewriting and encoding techniques are widely applicable in practice. To assess the impact of our multiset encoding, we compare the default evaluation setting with an otherwise identical run in which this encoding is disabled. The two evaluation settings agree on 247 of 267 paired Boolean results. In all 20 disagreements, Tamarin and ProVerif with the default setting verify a complete, non-XOR all-trace property, whereas ProVerif without the multiset encoding reports a counterexample. These spurious counterexamples show that the encoding is necessary to enforce the linear consumption of facts and preserve the source MSR semantics.

Helping Lemmas. We investigated whether ProVerif benefits from helping lemmas written for Tamarin, as both tools use very different reasoning methods. We compare the default evaluation setting with a run that omits translated helping lemmas. The two evaluation settings agree on all 330 paired Boolean results. Among resource-bound results, 18 out-of-memory results become timeouts and six timeouts become out-of-memory results; no task crosses between a logical and resource-bound outcome. Overall, these feature comparisons show that the multiset encoding and preciseActions

Precision in ProVerif. By default, ProVerif’s Horn clause abstraction ignores the number of repetitions of actions, potentially allowing multiple executions of constructs that should execute only once—for example, an input in(𝑐, 𝑥) can be reused multiple times, leading to false attacks [10, pp. 91]. ProVerif provides the directive set preciseActions = true that ensures each action executes at most once per process instance [11]. For translations from MSRs, 14

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

Execution Time Distribution

Memory Usage Distribution Tamarin (n=362)

70

Medians: Tamarin: 0.616 s ProVerif: 0.053 s

50

P90: Tamarin: 2.84 s ProVerif: 0.99 s

40 30

Number of Tasks

Number of Tasks

60

Tamarin (n=362)

100

ProVerif (n=362)

ProVerif (n=362) Medians: Tamarin: 102.1 MiB ProVerif: 13.4 MiB

80

P90: Tamarin: 166.3 MiB ProVerif: 48.9 MiB

60

40

20 20

10 0

10−2

10−1

100

101 Time (s, log scale)

102

0

103

101

102 Memory (MiB, log scale)

103

Figure 5: Performance on the 𝑛 = 362 tasks where Tamarin returns a Boolean result and ProVerif completes with a logical result. (Left) Execution time: ProVerif median 0.053 s and P90 0.99 s vs. Tamarin median 0.616 s and P90 2.84 s. (Right) Peak memory: ProVerif median 13.4 MiB and P90 48.9 MiB vs. Tamarin median 102.1 MiB and P90 166.3 MiB.

are required for Boolean verdicts to soundly reflect the source MSR model, whereas Tamarin-specific helping lemmas do not improve ProVerif’s Boolean results or termination.

7.6

it is 13.4 MiB versus 102.1 MiB. The corresponding runtime P90 values are 0.99 s versus 2.84 s; the memory P90 values are 48.9 MiB versus 166.3 MiB. Of the 28 Tamarin-faster tasks, 21 exercise its auto-source feature [15]; the other seven include injective and reachability queries, so the advantage is workload-dependent rather than confined to one feature family. Overall, ProVerif demonstrates consistently lower resource requirements, making it well-suited for rapid prototyping.

Performance Characterization

Each lemma and query was verified independently in a containerized environment. All tasks were evaluated with a timeout of at most 7200 s and a memory limit of at most 96 GiB. Tamarin used 12 configured CPUs per task. ProVerif is single-threaded and therefore used one CPU per task. We measured the total wall clock running time and peak memory usage during verification. In a separate translation-overhead measurement, translating all 121 models took about 72 s in total, with a median translation time of 0.22 s per model. Figure 5 shows a comparison between Tamarin’s and ProVerif’s performance across the evaluation. The Lowe case study demonstrates the practical value behind these aggregate numbers. The model has 206 lines and 7 rules, comes from the SPORE protocol library, and captures Lowe’s fix of the Andrew Secure RPC protocol. A systematic scan found 179 complete, agreeing, Boolean, non-XOR tasks; Lowe leads both the individual-task time comparison and the multi-lemma groups, while remaining a published case study with security-meaningful agreement lemmas. As shown in Table 5, ProVerif is 64.7× faster across all five agreeing all-trace lemmas, well above the 6.74× median per-task speedup reported below. The correspondenceplus-uniqueness encoding also translates both injective-agreement lemmas, and the candidate-patched build verifies both in agreement with Tamarin. The strongest row, injectiveagreement_B, is 129.6× faster and saves 21.863 s; it is the largest relative and absolute time saving among all complete, definitive, non-XOR agreements. Across the five displayed lemmas, the recorded totals are 0.463 s for ProVerif and 29.937 s for Tamarin. The exists-trace Session_key_honest_setup lemma is excluded from that total because Tamarin returns true while ProVerif is logically inconclusive. Among the 362 tasks in Figure 5, ProVerif is faster in 334 cases (92.3 %). The median per-task time ratio is 6.74×, and the median per-task memory ratio is 6.24×. The marginal median runtime is 0.053 s for ProVerif versus 0.616 s for Tamarin; for peak memory,

8

Conclusion

In this work, we presented a sound translation from Tamarin to ProVerif that enables systematic comparative analysis of these prominent verification tools. Through novel techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, we bridged key formalism gaps, revealing both the similarities and fundamental differences between the tools. Our comparative analysis identified a substantial common core logic fragment. Across 121 models, 562 of 566 lemma tasks (99.3 %) are translated and accepted by the ProVerif front end. The tools agree on 246 of 247 definitive non-XOR pairs; the sole exception is the flagged dp3t verdict on an incomplete model. Best-effort XOR is separate, with 34 agreements among 65 definitive pairs. ProVerif returns true for 18 all-trace tasks on which Tamarin runs out of memory; these resource-bound Tamarin cases are not counted as definitive cross-tool comparisons. These results expose the tradeoff between ProVerif’s speed and Tamarin’s expressiveness and provide a methodology for combining backends within explicit fragment boundaries.

Acknowledgments We thank Julian Biehl for the foundational rule-translation design and implementation in his Master’s thesis [4]. This paper was edited for grammar using ChatGPT.

References [1]

15

Martín Abadi and Cédric Fournet. 2001. Mobile values, new names, and secure communication. In Conference Record of POPL 2001: The 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. ACM, 104–115.

Kevin Morio, Yavor Ivanov, and Robert Künnemann

[2]

[3]

[4] [5]

[6]

[7] [8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

S. Abed et al. 2024. A Comparative Study of Protocols’ Security Verification Tools: AVISPA, Scyther, ProVerif, and Tamarin. In Computer and Network Security. Springer, 183–196. Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In 42nd IEEE Symposium on Security and Privacy, SP 2021. IEEE, 777–795. Julian Biehl. 2022. Translating Multiset-Rewrite Rules to ProVerif. MA thesis. Saarland University. Stefano Bistarelli, Iliano Cervesato, Gabriele Lenzini, and Fabio Martinelli. 2005. Relating multiset rewriting and process algebras for security protocol analysis. Journal of Computer Security, 13, 1, 3–47. Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001). IEEE Computer Society, 82–96. Bruno Blanchet. 2016. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Found. Trends Priv. Secur., 1, 1-2, 1–135. Bruno Blanchet. 2022. The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. In Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, HCVS/VPT@ETAPS 2022, 14–22. Bruno Blanchet, Vincent Cheval, and Véronique Cortier. 2022. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. In 2022 IEEE Symposium on Security and Privacy (SP). IEEE, 69–86. Bruno Blanchet, Ben Smyth, Vincent Cheval, and Marc Sylvestre. 2023. ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. https: //bblanche.gitlabpages.inria.fr/proverif/manual.pdf. Vincent Cheval, Véronique Cortier, and Mathieu Turuani. 2018. A Little More Conversation, a Little Less Action, a Lot More Satisfaction: Global States in ProVerif. In 31st IEEE Computer Security Foundations Symposium, CSF 2018. IEEE Computer Society, 344–358. Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. 2022. SAPIC+: protocol verifiers of the world, unite! In 31st USENIX Security Symposium, USENIX Security 2022. USENIX Association, 3935–3952. Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. 2022. SAPIC+: protocol verifiers of the world, unite! IACR Cryptol. ePrint Arch., 2022, 741. Full version of [12]. Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice. In 2018 IEEE Symposium on Security and Privacy, SP 2018. IEEE Computer Society, 529–546. Véronique Cortier, Stéphanie Delaune, Jannik Dreier, and Elise Klein. 2022. Automatic generation of sources lemmas in Tamarin: Towards automatic proofs of security protocols. J. Comput. Secur., 30, 4, 573–598. Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A Comprehensive Symbolic Analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017. ACM, 1773–1788. Cas Cremers, Charlie Jacomme, and Aurora Naska. 2023. Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. In 32nd USENIX Security Symposium, USENIX Security 2023. USENIX Association, 1235–1252. Cas Cremers, Benjamin Kiesl, and Niklas Medinger. 2020. A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters. In 29th USENIX Security Symposium, USENIX Security 2020. USENIX Association, 1–17. Nitish Dalal, Jenny Shah, Khushboo Hisaria, and Devesh Jinwala. 2010. A Comparative Analysis of Tools for Verification of Security Protocols. Int. J. Commun. Netw. Syst. Sci., 3, 10, 779–787. Jannik Dreier, Charles Duménil, Steve Kremer, and Ralf Sasse. 2017. Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols. In Principles of Security and Trust - 6th International Conference, POST 2017. Springer, 117–140. Santiago Escobar, Catherine Meadows, and José Meseguer. 2007. Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Springer, 1–50. Steve Kremer and Robert Künnemann. 2014. Automated Analysis of Security Protocols with Global State. In 2014 IEEE Symposium on Security and Privacy. IEEE, 163–178. Ralf Küsters and Tomasz Truderung. 2008. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. In Proceedings of the 15th ACM conference on Computer and communications security. ACM, 129–138. Ralf Küsters and Tomasz Truderung. 2009. Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009. IEEE Computer Society, 157–171. Pascal Lafourcade and Maxime Puys. 2015. Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties. In

[26]

[27]

[28]

A

Foundations and Practice of Security - 8th International Symposium, FPS 2015. Springer, 137–155. Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification - 25th International Conference, CAV 2013. Springer, 696–701. Kevin Morio, Yavor Ivanov, and Robert Künnemann. 2026. A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis. In Proceedings of the 2026 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 21 pages. Benedikt Schmidt, Simon Meier, Cas Cremers, and David A. Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 25th IEEE Computer Security Foundations Symposium, CSF 2012. IEEE Computer Society, 78–94.

Open Science

We provide a companion artifact containing the evaluation data, analysis and runner scripts, and a Docker recipe for building the evaluation image from public sources. The artifact is available at: https://doi.org/10.5281/zenodo.21827126 Artifacts Provided. Our artifact includes: (1) the 566-task evaluation inventory extracted from Tamarin’s protocol examples; (2) complete evaluation results with outcomes, execution times, and memory usage for both tools; (3) Python and shell scripts for running tasks, merging results, reconstructing the reported statistics, and regenerating the performance figure; and (4) a Docker recipe that obtains Tamarin from its public develop branch and builds the exact ProVerif revision and candidate patch used in our experiments. Reproducibility. The included README.md documents the dataset and result formats, the evaluation procedure, and the analysis commands. The numerical claims can be reconstructed immediately from the supplied JSONL file. The supplied Docker recipe and instructions build the evaluation image needed to rerun verification from public sources. Licensing. The implementation and evaluation scripts are GPL3.0 licensed. The evaluation inventory and result data are released under CC0-1.0.

B Soundness and Completeness Proofs B.1 Auxiliary Definitions Let C be a ProVerif configuration and Red be one of ProVerif’s reduction rules ([13, Figure 8]). We denote the transition from configuration C to configuration C ′ with the reduction rule Red and label 𝑙 by 𝑙

C→ − →Red C ′, where 𝑙 may be omitted depending on the rule. Similarly, for MSR 𝑎 states, we write 𝑆 → − ri 𝑆 ′ for a rewriting step from 𝑆 to 𝑆 ′ with the ground rule instance ri = ru𝜎 ∈ ginsts𝐸 (R ∪ MD ∪ {Fresh}) of a rule ru under a grounding substitution 𝜎. In Tamarin, the attacker knowledge consists of the terms 𝑚, for which there are !K(𝑚) facts in the current MSR state. During execution, the attacker can raise a K(𝑚) fact to show that it has explicit knowledge of the term 𝑚, i.e., that it has deduced it at some previous timepoint. We can use such facts in trace formulas to ask if the attacker has raised such an event at a given time. In ProVerif, the attacker knowledge consists of the terms contained in the set A, which is part of the process configuration. We can ask if the 16

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

attacker has knowledge of a term 𝑚 through attacker(𝑚), but, as mentioned before, A also contains messages that are deducible.

For ProVerif, we extend the above definition to executions of ProVerif processes. For all but the following additional case, we project the execution to the corresponding trace.

Definition 14 (Attacker knowledge in ProVerif). The adversary can deduce 𝑚 from a process configuration C as defined in [9, Sec. 2.3.1] if there exists a configuration C ′ = (E ′, P, T, A ′ ) with 𝑚 ∈ A ′ reachable from C by only applying App and New.

Definition 18 (Satisfaction relation for ProVerif). The satisfaction relation |=𝑃𝑉 𝐸 is defined by extending Definition 17 to ProVerif ex𝑙1

Based on this notion, we define two functions: deducible(·) and known(·). For a ProVerif configuration C, deducible(C) returns all the terms deducible by the adversary from C. For an MSR state 𝑆, known(𝑆) = { 𝑚 | !K(𝑚) ∈ 𝑆 } returns the set of all messages known to the adversary in the MSR state 𝑆. Let ri ∈ ginsts𝐸 (R) be a ground instance of an MSR. We define the set of ProVerif table entries inserts(ri) as follows  F𝑡𝑏𝑙 (𝑡 1, . . . , 𝑡𝑛 ) F(𝑡 1, . . . , 𝑡𝑛 ) ∈ concls(ri)| Storage ,

(𝑒, 𝜃 ) |=𝑃𝑉 𝐸 attacker(𝑚)@𝑖

Similarly to Schmidt et al. [28], for closed formulas 𝜑, we overload notation and write 𝑡𝑟 |=𝐸 𝜑 if (𝑡𝑟, 𝜃 ) |=𝐸 𝜑 for all 𝜃 . In the following, we refer to the unfiltered traces as strong traces, in contrast to the weak traces of Definition 1. Next, we recall a lemma from [28, Appendix C, Section E, Lemma 19]. Lemma 1. For all equational theories 𝐸, strong MSR traces 𝑡𝑟𝑚𝑠𝑟 , corresponding weak MSR traces 𝑤𝑡𝑟𝑚𝑠𝑟 and closed formulas 𝜑: 𝑡𝑟𝑚𝑠𝑟 |=𝑇𝐸 𝜑 ⇔ 𝑤𝑡𝑟𝑚𝑠𝑟 |=𝑇𝐸 𝜑

Definition 15 (Applicability of a translated process). Let C be a ProVerif configuration and 𝑟 ∈ R be a rule with grounding substitution 𝜎. Then ⟦𝑟𝜎⟧ is applicable in C if all sub-processes of the premise (the first two lines in Definition 10) of ⟦𝑟𝜎⟧ can be executed starting from C: (1) All ground instances of the premises have a corresponding table entry. (2) The attacker has explicit knowledge of all terms it needs to input to the process.

We also adapt the above lemma to ProVerif. The statement follows by the same proof. Lemma 2. For all equational theories 𝐸, strong ProVerif traces 𝑡𝑟 𝑝𝑣 , corresponding weak ProVerif traces 𝑤𝑡𝑟 𝑝𝑣 and closed formulas 𝜑 that do not contain attacker facts: 𝑃𝑉 𝑡𝑟 𝑝𝑣 |=𝑃𝑉 𝐸 𝜑 ⇔ 𝑤𝑡𝑟 𝑝𝑣 |=𝐸 𝜑

The condition that 𝜑 does not contain attacker facts can be relaxed, but this form of the statement is sufficient for our purposes. Definition 19 (Silencing facts in traces). Let 𝑡𝑟 be an MSR or ProVerif trace and F a fact symbol. We define the trace 𝑡𝑟 ≠F as the trace 𝑡𝑟 in which the facts with symbol F have been made silent, i.e., every such fact is removed from the multiset at each index of 𝑡𝑟 .

Satisfaction Relation

We introduce a satisfaction |=𝐸 w.r.t. an equational theory 𝐸. For a trace 𝑡𝑟 , let idx (𝑡𝑟 ) ≔ { 1, . . . , |𝑡𝑟 | } denote its index set. Definition 16 (Valuation). Let D𝑠 be the domain associated to sort 𝑠; we set Dmsg to the set of ground terms and Dtemp to the set of trace indices N. A function 𝜃 from V to Dmsg ∪ Dtemp is called a valuation if it respects sorts, i.e., 𝜃 (V𝑠 ) ⊆ D𝑠 for all sorts 𝑠. For a term 𝑡, 𝑡𝜃 denotes the application of the homomorphic extension of 𝜃 to 𝑡 where variables outside the domain of 𝜃 remain unchanged.

Lemma 3. For all equational theories 𝐸, Tamarin traces 𝑡𝑟 , corresponding Tamarin traces 𝑡𝑟 ≠K and closed formulas 𝜑 that do not contain K facts: 𝑡𝑟 |=𝑇𝐸 𝜑 ⇔ 𝑡𝑟 ≠K |=𝑇𝐸 𝜑 To obtain a proof for the lemma, one needs to modify the proof of Lemma 1 by performing induction on the number of K transitions in 𝑡𝑟 , instead of the number of silent actions in 𝑡𝑟 . We can use the above definition and a slightly adapted proof of the previously cited lemma to obtain the following result for formulas in SA-QBF

Definition 17 (Satisfaction relation). We define the satisfaction relation (𝑡𝑟, 𝜃 ) |=𝐸 𝜑 between a trace 𝑡𝑟 , a valuation 𝜃 , and a formula 𝜑 inductively as follows: the remaining connectives (∨, ⇒, ∀) and the derived comparisons 𝑖 ≤¤ 𝑗 (i.e., 𝑖 <¤ 𝑗 ∨ 𝑖  𝑗) and 𝑖 ̸  𝑗 are defined as usual. (tr, 𝜃 ) |=𝐸 ⊥

never

(tr, 𝜃 ) |=𝐸 F@𝑖 (tr, 𝜃 ) |=𝐸 𝑖 <¤ 𝑗

if 𝜃 (𝑖) ∈ idx (tr) and F𝜃 ∈𝐸 tr 𝜃 (𝑖 )

if 𝜃 (𝑖) ∈ {1, . . . , 𝑛} and 𝑚𝜃 ∈ deducible(C𝜃 (𝑖 ) ).

where F𝑡𝑏𝑙 is a ProVerif table corresponding to the fact symbol F. After the successful execution of the process ⟦ri⟧, inserts(ri) ⊆ T holds for the resulting configuration, which corresponds to the MSR state after applying ri.

B.2

𝑙𝑛

ecutions. For an execution 𝑒 = C0 − → → C1 · · · −→ → C𝑛 , we add the following case:

Lemma 4. For all equational theories 𝐸, ProVerif traces 𝑡𝑟 , corresponding ProVerif traces 𝑡𝑟 ≠mess and closed formulas 𝜑 ∈ SA-QBF:

if 𝜃 (𝑖) < 𝜃 ( 𝑗)

𝑃𝑉 𝑡𝑟 |=𝑃𝑉 𝐸 𝜑 ⇔ 𝑡𝑟 ≠mess |=𝐸 𝜑

(tr, 𝜃 ) |=𝐸 𝑖  𝑗

if 𝜃 (𝑖) = 𝜃 ( 𝑗)

(tr, 𝜃 ) |=𝐸 𝑡 1 = 𝑡 2

if 𝑡 1𝜃 =𝐸 𝑡 2𝜃

To obtain a proof for the lemma, one needs to modify the proof of Lemma 1 by performing induction on the number of mess transitions in 𝑡𝑟 , instead of the number of silent actions in 𝑡𝑟 .

(tr, 𝜃 ) |=𝐸 ¬𝜑

if not (tr, 𝜃 ) |=𝐸 𝜑

(tr, 𝜃 ) |=𝐸 𝜑 ∧ 𝜓

if (tr, 𝜃 ) |=𝐸 𝜑 and (tr, 𝜃 ) |=𝐸 𝜓

(tr, 𝜃 ) |=𝐸 ∃® 𝑥 : 𝑠®.𝜑

if ∃® 𝑢 ∈ D𝑠1 × · · · × D𝑠 |𝑥® | .

Definition 20 (Satisfiability). Let Tr be a set of traces and |=𝐸 a satisfaction relation. A formula 𝜑 is satisfiable for Tr, written Tr ∃ |=𝐸 𝜑, if ∃ tr ∈ Tr, 𝜃 . (tr, 𝜃 ) |=𝐸 𝜑 .

(tr, 𝜃 [𝑥® ↦→ 𝑢]) ® |=𝐸 𝜑 17

Kevin Morio, Yavor Ivanov, and Robert Künnemann

Definition 21 (Validity). Let Tr be a set of traces and |=𝐸 a satisfaction relation. A formula 𝜑 is valid for Tr, written Tr ∀ |=𝐸 𝜑, if

of the same atom, which are mapped to the same position. Therefore, 𝜎 ′ preserves all action occurrences and temporal orderings, ensuring 𝜑 is satisfied on lex(𝑡𝑟 ). □

∀ tr ∈ Tr, 𝜃 . (tr, 𝜃 ) |=𝐸 𝜑 .

B.3

Corollary 1. Let Tr be a set of traces and 𝜑 be a closed formula satisfying the conditions of Lemma 5. If Tr ∀ |=𝐸 𝜑, then lex(Tr) ∀ |=𝐸 𝜑.

Proof Overview

Proof. Every trace in lex(Tr) is lex(𝑡𝑟 ) for some 𝑡𝑟 ∈ Tr. The claim follows from Lemma 5. □

The proof establishes a weak simulation between the LTS induced by the MSR system R and its ProVerif translation ⟦R⟧, where (1) initial states are related, and (2) each visible MSR transition corresponds to ProVerif transitions producing a lexicographically ordered trace. Our trace comparison ignores Tamarin’s K facts and ProVerif’s mess facts: the former are translated to attacker and compared via deducibility rather than trace inclusion, while the latter do not affect SA-QBF satisfaction (Lemma 4). The weak simulation maintains a state equivalence relating Tamarin’s !K facts to ProVerif’s attacker knowledge, enabling soundness for T-UKF and the preservation of exists-trace properties for K-free TSA-QBF formulas.

B.4

B.5

Definition 22 (State relation). Let C = (E, P, T, A) be a process configuration and 𝑆 be an MSR state. We relate 𝑆 to C, i.e., 𝑆 ∼ C, if the following conditions hold: (1) 𝑆 | Storage ⊆𝑡𝑏𝑙 T (2) known(𝑆) ⊆ deducible(C)

Trace Comparison

In the above definition, 𝑆 | Storage ⊆𝑡𝑏𝑙 Tmeans that all grounded Storage facts in the MSR state 𝑆 have a corresponding table entry stored in T. In particular, 𝑆 | Storage ⊆𝑡𝑏𝑙 T if and only if, for each Storage fact F(𝑡 1, . . . , 𝑡𝑛 ) ∈ 𝑆, we have a matching entry F𝑡𝑏𝑙 (𝑡 1, . . . , 𝑡𝑛 ) ∈ T, where the table name F𝑡𝑏𝑙 corresponds to the fact symbol F. These conditions help us in two ways. The first condition helps us show that if a rule instance ri ∈ ginsts𝐸 (R) is applicable to 𝑆, then ⟦ri⟧ is applicable to C. Moreover, it guarantees that the process configuration after the execution of ⟦ri⟧ contains table entries simulating the conclusions that the execution of ri inserted into the corresponding MSR state. The second condition helps us prove that if K(𝑚) holds for a given timepoint, attacker(𝑚) also holds at the same timepoint.

To simplify the comparison between Tamarin and ProVerif traces, we lift ProVerif traces to sequences of singleton sets of facts. For Tamarin traces, we consider them as sequences of sets of facts since the multiset semantics cannot impact formula satisfaction. Overloading notation, we write lex(𝑡𝑟𝑚𝑠𝑟 ) to denote the lifting of a Tamarin trace 𝑡𝑟𝑚𝑠𝑟 to a sequence of singleton sets of facts ordered lexicographically. For example, with 𝑡𝑟𝑚𝑠𝑟 = ({𝐴, 𝐵}, {𝐶}), we have lex(𝑡𝑟𝑚𝑠𝑟 ) = ({𝐴}, {𝐵}, {𝐶}). We also lift the function to sets of traces. Lemma 5 (Valuation Translation). Let 𝑡𝑟 = (𝑎 1, . . . , 𝑎𝑛 ) be a trace and 𝜑 be a simultaneity-free formula (Definition 13), i.e., each time variable of 𝜑 indexes exactly one trace atom and no timepoint equality relates distinct trace atoms. The formulas produced by the lemma translation satisfy these conditions after the rewriting of Section 4.4 (see Remark 3). Let 𝜎 be a valuation that satisfies 𝜑 on trace 𝑡𝑟 . Then there exists a valuation 𝜎 ′ that satisfies 𝜑 on trace lex(𝑡𝑟 ) defined as follows: For each time variable 𝑖 where F@𝑖 appears in 𝜑 and 𝜎 (𝑖) = 𝑘: 𝜎 ′ (𝑖) =

𝑘 −1 ∑︁

State Relation

Each step of the simulation needs to assume the two models are in a relation in order to prove that this relation is retained. We thus define a relation between MSR states (multisets) and ProVerif states (process configurations).

B.6

Weak Simulation

Let R be a set of MSRs. We denote the set of weak traces with K actions removed as wtracesmsr ≠K (R) and the set of weak traces with pv mess actions removed as wtraces≠mess (⟦R⟧). Theorem 3 (Weak Trace Inclusion). Let R be a set of MSRs. Then

|𝑎 ℓ | + poslex (F, 𝑎𝑘 )

pv

lex(wtracesmsr ≠K (R)) ⊆ wtraces ≠mess (⟦R⟧) .

ℓ=1

Proof. Let 𝑆® ∈ execsmsr (R) be an execution of length 𝑚 with ® ∈ weak trace 𝑤𝑡𝑟𝑚𝑠𝑟 . We show that there exists an execution C execspv (⟦R⟧) of length 𝑛 with weak trace 𝑤𝑡𝑟 𝑝𝑣 such that

where poslex (F, 𝑎𝑘 ) denotes the position of F in the lexicographic ordering of 𝑎𝑘 . Proof. For any F@𝑖 in 𝜑 with 𝜎 (𝑖) = 𝑘 we have F ∈ 𝑎𝑘 by definition of 𝜎. By the definition of 𝜎 ′ this places F at position 𝜎 ′ (𝑖) in lex(𝑡𝑟 ). For any constraint 𝑖 < 𝑗 in 𝜑 where 𝜎 (𝑖) = 𝑘 1 and 𝜎 ( 𝑗) = 𝑘 2 :

𝑆𝑚 ∼ C𝑛 𝑤𝑡𝑟 𝑝𝑣 = lex(𝑤𝑡𝑟𝑚𝑠𝑟 ) ® The proof is by induction on the length 𝑚 of the execution 𝑆. Base case (𝑚 = 0): By the definitions of the initial states 𝑆 0 and C0 ,

• Since 𝜎 satisfies 𝑖 < 𝑗, we have 𝑘 1 < 𝑘 2 Í1 • 𝜎 ′ (𝑖) ≤ 𝑘ℓ=1 |𝑎 ℓ | Í 2 −1 ′ • 𝜎 ( 𝑗) ≥ 𝑘ℓ=1 |𝑎 ℓ | + 1 • Since 𝑘 1 < 𝑘 2 , we have 𝜎 ′ (𝑖) < 𝜎 ′ ( 𝑗)

∅ = 𝑆 0 ⊆𝑡𝑏𝑙 T0 = ∅ ∅ = known(𝑆 0 ) ⊆ deducible(C0 ) ,

Timepoint disequalities 𝑖 ≠ 𝑗 are preserved since satisfying them requires 𝑘 1 ≠ 𝑘 2 , and timepoint equalities relate only occurrences

and thus 𝑆 0 ∼ C0 . Moreover, 𝑤𝑡𝑟𝑚𝑠𝑟 = 𝜖 = 𝑤𝑡𝑟 𝑝𝑣 . 18

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

Inductive hypothesis (𝑚 = 𝑘): We assume that the statement holds for all executions of length 𝑘. Inductive step (𝑚 = 𝑘 + 1): Let 𝑆® be an execution of length 𝑘 + 1 𝑎 with 𝑆𝑘 → − 𝑟𝜎 𝑆𝑘+1 for a rule 𝑟 and a grounding substitution 𝜎. By ® of length applying the induction hypothesis, we get an execution C ′ ′ 𝑗 with 𝑆𝑘 ∼ C𝑗 and 𝑤𝑡𝑟 𝑝𝑣 = lex(𝑤𝑡𝑟𝑚𝑠𝑟 ). We show that there exists a configuration C𝑗+𝑙 such that 𝑆𝑘+1 ∼ C𝑗+𝑙 and 𝑤𝑡𝑟 𝑝𝑣 = lex(𝑤𝑡𝑟𝑚𝑠𝑟 ) by a case distinction on the rule 𝑟 . Case 𝑟 ∈ R: First, we show that ⟦𝑟𝜎⟧ is applicable in C𝑗 . From 𝑆𝑘 ∼ C𝑗 , it follows that 𝑆𝑘 | Storage ⊆𝑡𝑏𝑙 T𝑗 . Since 𝑟𝜎 is applicable in 𝑆𝑘 , prems(𝑟𝜎) |Storage ⊆ 𝑆𝑘 and hence prems(𝑟𝜎) |Storage ⊆𝑡𝑏𝑙 T𝑗 . Since 𝑟𝜎 is applicable in 𝑆𝑘 , prems(𝑟𝜎)| In ⊆ 𝑆𝑘 . An In fact can only be added to the state through a previous application of the MDIn rule. Since the premise of the MDIn rule !K is a persistent fact, it is still in 𝑆𝑘 . Thus, for all In(𝑡) ∈ 𝑆𝑘 we have 𝑡 ∈ known(𝑆𝑘 ). From 𝑆𝑘 ∼ C𝑗 follows known(𝑆𝑘 ) ⊆ deducible(C𝑗 ). If there exists a term 𝑡 for In(𝑡) ∈ prems(𝑟𝜎) for which the ProVerif attacker does not have explicit knowledge, the term can be deduced in a series of transitions starting from C𝑗 . These transitions have no effect on the weak trace. After 𝑝 < 𝑙 transitions, we reach a configuration C𝑗+𝑝 with 𝑡 ∈ A. By Definition 10, we know that each In(𝑡) fact is translated to an in(𝑐, 𝑡) process for the public channel 𝑐. The ProVerif attacker can thus send all the terms over 𝑐 where they can be received by the corresponding process. Hence, ⟦𝑟𝜎⟧ is applicable in C𝑗 . Now, we show how to get from C𝑗+𝑝 to C𝑗+𝑙 , the configuration after the application of ⟦𝑟𝜎⟧. The initial process is always a replication. With C = C𝑗+𝑝 and C ′ = C𝑗+𝑝+1 we have

Since no new !K facts are added to the state, we have known(𝑆𝑘+1 ) = known(𝑆𝑘 ). Hence, 𝑆𝑘+1 ∼ C𝑗+𝑙 . Case 𝑟 = MDIn: MDIn is the only rule that adds K actions to the trace. Since we filter out the K actions when comparing traces, they are not observable. In ProVerif, we simulate this rule by staying in C𝑗 . Hence, in both cases the observable behavior is the same with respect to our weak-trace comparison. The application of MDIn does not add storage or !K facts to 𝑆𝑘+1 . Therefore, 𝑆𝑘+1 | Storage = 𝑆𝑘 | Storage and known(𝑆𝑘+1 ) = known(𝑆𝑘 ). Consequently, 𝑆𝑘+1 ∼ C𝑗 . Case 𝑟 = MDOut: The application of MDOut adds a !K fact to 𝑆𝑘+1 . Hence, known(𝑆𝑘+1 ) = known(𝑆𝑘 ) ∪ {𝑚}. In ProVerif, we simulate this rule by staying in C𝑗 . Since MDOut is applicable in 𝑆𝑘 , we know that Out(𝑚) ∈ 𝑆𝑘 . Hence, there exist a rule 𝑟 ∗ ∈ R and a grounding substitution 𝜎 ∗ such that 𝑟 ∗ 𝜎 ∗ added Out(𝑚) to the state at a previous timepoint. Therefore, ⟦𝑟 ∗ 𝜎 ∗ ⟧ has also been executed earlier including the corresponding out process. By the semantics of ProVerif’s Out transition, we know that 𝑚 was added to the knowledge of the attacker and thus 𝑚 ∈ deducible(C𝑗 ). The application of MDOut does not add storage facts to 𝑆𝑘+1 . Therefore, 𝑆𝑘+1 | Storage = 𝑆𝑘 | Storage . Consequently, 𝑆𝑘+1 ∼ C𝑗 holds. Case 𝑟 = MDFresh: MDFresh allows the attacker to learn a previously generated fresh name through the rule Fresh. Its application adds a !K fact to 𝑆𝑘+1 . Hence, known(𝑆𝑘+1 ) = known(𝑆𝑘 ) ∪ {𝑚}. In ProVerif, we simulate this behavior with a single New transition adding the name to the knowledge of the attacker. There is no observable behavior in either case. The application of MDFresh does not add storage facts to 𝑆𝑘+1 . Therefore, 𝑆𝑘+1 | Storage = 𝑆𝑘 | Storage . Consequently, 𝑆𝑘+1 ∼ C𝑗+1 holds. Case 𝑟 = MDApp: MDApp allows the attacker to construct a message from its knowledge. Its application adds a !K fact to 𝑆𝑘+1 . Hence, known(𝑆𝑘+1 ) = known(𝑆𝑘 )∪{𝑓 (𝑚 1, . . . , 𝑚𝑝 )} for a function symbol 𝑓 and !K(𝑚𝑖 ) ∈ 𝑆𝑘 . As 𝑆𝑘 ∼ C𝑗 , we know that 𝑚𝑖 ∈ deducible(C𝑗 ). Thus, the attacker can deduce them in a finite number 𝑞 of steps and add them to its knowledge. In ProVerif, we simulate this behavior with a App transition adding the term 𝑓 (𝑚 1, . . . , 𝑚𝑝 ) to its knowledge. There is no observable behavior in either case. The application of MDApp does not add storage facts to 𝑆𝑘+1 . Therefore, 𝑆𝑘+1 | Storage = 𝑆𝑘 | Storage . Consequently, 𝑆𝑘+1 ∼ C𝑗+𝑞 holds. Case 𝑟 = Fresh: Fresh allows for generating fresh names by adding a Fr(𝑛) fact to the state. At this time, we do not know how the generated name will be used. It can either be used by another protocol rule that requires a fresh fact in its premise or by MDFresh to allow the attacker to generate a fresh name. In ProVerif, the former case is simulated by a Restr transition and the latter by a New transition. Hence, we stay in C𝑗 . There is no observable behavior in either case. The application of Fresh does not add storage or !K facts to 𝑆𝑘+1 . Therefore, 𝑆𝑘+1 | Storage = 𝑆𝑘 | Storage . Consequently, 𝑆𝑘+1 ∼ C𝑗 holds. Case 𝑟 = MDPub: MDPub allows the attacker to learn public names. Its application adds a !K fact to 𝑆𝑘+1 . Hence, known(𝑆𝑘+1 ) = known(𝑆𝑘 ) ∪ {𝑚}. In ProVerif, the attacker knows all public names from the start and thus 𝑚 ∈ deducible(C𝑗 ). Hence, we stay in C𝑗 . There is no observable behavior in either case. The application of MDPub does not add storage facts to 𝑆𝑘+1 . Therefore, 𝑆𝑘+1 | Storage = 𝑆𝑘 | Storage . Consequently, 𝑆𝑘+1 ∼ C𝑗 holds.

C = (E, P, T, A) → − →Repl C ′ = (E, P ∪ {⟦𝑟𝜎⟧}, T, A) , which leaves the trace unchanged. Next, we execute the process ⟦𝑟𝜎⟧ step by step following Definition 10 closely without interleaving steps from other processes. From the two requirements of applicability, all required table entries exist and terms are known to the attacker (line 1 in Definition 10). In the next step, fresh names are generated for each fresh fact in the premise of 𝑟 (line 2). We continue with the emission of action facts (line 3) for each action in 𝑎 in lexicographical order. If the action contains public variables, they are received from the ProVerif attacker. Similarly, storage facts from the conclusion are added to the table (line 4). Finally, the output facts are emulated by the out process (line 5). From the above, only the events are observable in the trace. Since the events are ordered lexicographically, the weak trace of the process is a lexicographical ordering of the weak trace of the MSR: 𝑤𝑡𝑟 𝑝𝑣 = lex(𝑤𝑡𝑟𝑚𝑠𝑟 ). We assume that after the execution of ⟦𝑟𝜎⟧, we are in the configuration C𝑗+𝑙 . It remains to show that 𝑆𝑘+1 ∼ C𝑗+𝑙 . From Definition 10 we know that for each storage fact in the conclusion of 𝑟𝜎, there is a corresponding insert in ⟦𝑟𝜎⟧, i.e., concls(𝑟𝜎) |Storage =𝑡𝑏𝑙 inserts(𝑟𝜎). Thus, at the end of the execution of ⟦𝑟𝜎⟧, we have T𝑗+𝑙 = T𝑗 ∪ inserts(𝑟𝜎). From 𝑆𝑘 ∼ C𝑗 we know that 𝑆𝑘 | Storage ⊆𝑡𝑏𝑙 T𝑗 . The transition from 𝑆𝑘 to 𝑆𝑘+1 adds the storage facts in concls(𝑟𝜎) to the state. The table entries that correspond to these facts are exactly inserts(𝑟𝜎). From T𝑗+𝑙 = T𝑗 ∪ inserts(𝑟𝜎) follows that C𝑗+𝑙 contains a corresponding table entry for each storage fact in 𝑆𝑘+1 , i.e., 𝑆𝑘+1 | Storage ⊆𝑡𝑏𝑙 T𝑗+𝑙 . 19

Kevin Morio, Yavor Ivanov, and Robert Künnemann

In the last two cases (Fresh and MDPub), the execution 𝑆® can stutter since both rules have empty premises and can thus be applied infinitely often. Since the rules have no observable actions, the weak trace remains unchanged. The same holds for the ProVerif execution, as we stay in the same configuration for both rules. Hence, we can ignore these two cases of possible stuttering of the MSR LTS as weak simulation only requires the observable actions to be matched. □

serialization of simultaneous action facts (handled by Lemma 5). By Lemmas 1 and 2, the empty steps do not influence the satisfaction of the formula and can be ignored. Hence, the satisfaction only depends on finding appropriate valuations for the time variables. Let wtr (𝑡) and wtr (𝑡 ′ ) be the weak traces obtained from 𝑡 and ′ 𝑡 , respectively. If 𝑡 does not contain any K facts, then wtr (𝑡 ′ ) = lex(wtr (𝑡)), and thus we get a satisfying valuation 𝜃 ∗ by Lemma 5 with (wtr (𝑡 ′ ), 𝜃 ∗ ) |=𝐸 𝜑. With Lemma 2, we get a valuation 𝜃 ′ such that (𝑡 ′, 𝜃 ′ ) |=𝐸 ⟦𝜑⟧. Let us now assume 𝑡 and 𝜑 contain K facts. We first show that if

We proved weak simulation between Tamarin and ProVerif without considering K and mess facts, respectively. Recall that this is not problematic as mess facts are not part of SA-QBF and K facts are translated to attacker facts, which do not appear in the trace.

(𝑡, 𝜃 ) |=𝐸 K(𝑚)@𝑖, then there exists a valuation 𝜃 ′ such that ® 𝜃 ′ ) |=𝐸 attacker(𝑚)@𝑖 ( C,

Remark 2. The reverse inclusion does not hold in general. A ProVerif execution may stop between the events of a single translated rule, producing a strict prefix of the lexicographic image of a Tamarin action multiset, and, without the instrumentation of Section 4.4, table entries may be consumed more often than the corresponding linear facts. The encodings of Section 4.4 mitigate the latter in the implementation but lie outside the formal statement.

The only rule that produces K(𝑚) is MDIn. Moreover, we know that (K(𝑚)@𝑖)𝜃 is in 𝑡 at index 𝜃 (𝑖). Let 𝑆® be the MSR execution that produces 𝑡. Then there is a corresponding transition from the ® MSR state 𝑆𝜃 (𝑖 ) −1 to 𝑆𝜃 (𝑖 ) with the rule MDIn. By construction, C contains a configuration C𝑗 −1 such that 𝑆𝜃 (𝑖 ) −1 ∼ C𝑗 −1 . Therefore, known(𝑆𝜃 (𝑖 ) −1 ) ⊆ deducible(C𝑗 −1 ). Since MDIn is applicable in 𝑆𝜃 (𝑖 ) −1 , it includes !K(𝑚), i.e., 𝑚 ∈ known(𝑆𝜃 (𝑖 ) −1 ). Consequently, 𝑚 ∈ deducible(C𝑗 −1 ). Thus, attacker(𝑚) holds at the next timepoint with 𝜃 ′ (𝑖) = 𝑗. To reconstruct the valuation for the other time variables, we proceed similarly. If (𝑡, 𝜃 ) |=𝐸 F@𝑖, then a rule 𝑟 is applicable in ® contains a configuration 𝑆𝜃 (𝑖 ) −1 with F ∈ acts(𝑟 ). By construction, C C𝑗 −1 such that 𝑆𝜃 (𝑖 ) −1 ∼ C𝑗 −1 and such that ⟦𝑟 ⟧ is applicable. The next |acts(𝑟 )| transitions produce the corresponding action facts in lexicographical order in 𝑡 ′ . Let 𝑛 be the position of F in lex(acts(𝑟 )). Then we set 𝜃 ′ (𝑖) = 𝑗 + 𝑛 − 1. This construction preserves the relative order of the timepoints. Hence, we get a valuation 𝜃 ′ such ® 𝜃 ′ ) |=𝐸 ⟦𝜑⟧. that ( C, □

Remark 3 (Instrumented translation and formula rewriting). The implementation additionally instruments events with rule-instance identifiers (Section 4.4): each translated rule instance draws a fresh identifier and passes it as an additional argument to all of its events. The construction above extends verbatim, as the identifier is one further fresh name and the extra event argument does not affect the simulation. To exclude artificial mid-action prefixes for a cross-fact same-action conclusion, the translation may guard it with an internal RuleCompleted event that is emitted after the serialized source action and removed by projection to source events. Over such instrumented traces, the formula rewriting of Section 4.4 preserves satisfaction: (1) one-point elimination of definite timepoint equalities is a logical equivalence; (2) splitting a shared time variable into per-event time variables tied by a common identifier variable is exact, since two action facts occur at the same Tamarin timepoint if and only if they belong to the same rule instance; and (3) translating a surviving timepoint equality (resp. disequality) between distinct events as an equality (resp. disequality) of the corresponding identifier variables is exact for the same reason. The rewritten formulas contain exactly one trace atom per time variable and no timepoint equalities between distinct atoms, as required by Lemma 5.

Next, we combine our results to show soundness and completeness of our translation. Theorem 2 (Completeness for existential properties). For (R, 𝐸, 𝜑) in the faithful translation fragment such that 𝜑 itself is simultaneityfree, belongs to TSA-QBF, and contains no K facts: ∃

∃

tracesmsr (R) |=𝑇𝐸 𝜑 ⇒ tracespv (⟦R⟧) |=𝑃𝑉 𝐸 𝜑 Proof. Fix 𝑡𝑟 ∈ tracesmsr (R) and a valuation 𝜃 with (𝑡𝑟, 𝜃 ) |=𝑇𝐸 𝜑. Since 𝜑 contains no K facts and is simultaneity-free, we have ® ∈ ⟦𝜑⟧ = 𝜑. By Corollary 2, there are a ProVerif execution C execspv (⟦R⟧), obtained via the construction of Theorem 3, and a ® 𝜃 ′ ) |=𝑃𝑉 𝜑. Hence tracespv (⟦R⟧) ∃ |=𝑃𝑉 𝜑. □ valuation 𝜃 ′ with ( C, 𝐸 𝐸

With this construction, we can now show that satisfaction of closed formulas is preserved from MSR traces to ProVerif traces. Corollary 2 (MSR to ProVerif Satisfaction). Let R be a set of MSRs ® be the ProVerif execution oband 𝑡 ∈ tracesmsr (R) a trace. Let C tained after the construction in Theorem 3. If there exists a valuation 𝜃 such that (𝑡, 𝜃 ) |=𝐸 𝜑 for a closed, simultaneity-free formula 𝜑 in negation normal form whose K atoms occur only positively—this covers K-free formulas in TSA-QBF as well as negation normal forms of ¬𝜓 for 𝜓 ∈ T-UKF—then there exists a valuation 𝜃 ′ such ® 𝜃 ′ ) |=𝐸 ⟦𝜑⟧. that ( C,

Due to semantic differences between attacker knowledge in Tamarin and ProVerif, soundness is guaranteed for T-UKF components (Definition 12), whose counterexample formulas contain K atoms only positively. The faithful translation fragment is their satisfaction-preserving conjunctive rewrite closure (Definition 13); the model and equational-theory conditions are enforced by the theorem hypotheses. We prove the result componentwise and lift it through conjunction. ProVerif’s Horn clause resolution is sound but incomplete, so properties proven valid by the verification procedure are semantically valid, though the converse does not hold.

® We note Proof. Let 𝑡 ′ be the trace obtained from projecting C. that 𝑡 and 𝑡 ′ differ only in the presence of K facts in 𝑡, the mess labels in 𝑡 ′ (which do not affect SA-QBF satisfaction by Lemma 4), the number of empty steps between action facts, and the lexicographic 20

A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

Hence, we fix 𝑡𝑟 ∈ tracesmsr (R) and a valuation 𝜃 such that

Theorem 1 (Soundness). For every (R, 𝐸, 𝜑) in the faithful translation fragment: pv

traces (⟦R⟧)

∀

(𝑡𝑟, 𝜃 ) |=𝑇𝐸 ¬𝜑 .

∀ msr |=𝑃𝑉 (R) |=𝑇𝐸 𝜑 𝐸 ⟦𝜑⟧ ⇒ traces

® ∈ execspv (⟦R⟧) be the corresponding ProVerif execution Let C constructed following Theorem 3. Let 𝑡𝑟 ′ be the projection of the ® labels of C. Since 𝜑 ∈ T-UKF, the negation normal form of ¬𝜑 contains K atoms only positively, and it is simultaneity-free because 𝜑 is in the faithful translation fragment (Definition 13); hence Corollary 2 applies, and we obtain the existence of a valuation 𝜃 ′ such that (𝑡𝑟 ′, 𝜃 ′ ) |=𝑃𝑉 𝐸 ⟦¬𝜑⟧. As ⟦·⟧ replaces K atoms by attacker atoms, ⟦¬𝜑⟧ = ¬⟦𝜑⟧, which concludes the proof. □

Proof. By Definition 13, 𝜑 rewrites to a finite conjunction of T-UKF components. Since the rewritings preserve satisfaction and ⟦𝜑⟧ is the conjunction of the translated components, it suffices to establish the claim for an arbitrary component, again denoted by 𝜑. We prove the contraposition of the above statement: ∃

∃

tracesmsr (R) |=𝑇𝐸 ¬𝜑 ⇒ tracespv (⟦R⟧) |=𝑃𝑉 𝐸 ⟦¬𝜑⟧

21

Related documents

• Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin#238520
• On How to Avoid the Indeterminacy of Translation#762143
• Proof-Theoretic Semantics and Inquisitive Logic#770237
• More Troubles for Comesana and Tal#731050
• Part Two:. Texts in Translation#229891