A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis
Source: arXiv:2608.06315 · Published 2026-08-06 · By Kevin Morio, Yavor Ivanov, Robert Künnemann
TL;DR
This paper addresses the fundamental challenge of systematically comparing two widely used formal verification tools for security protocols: Tamarin and ProVerif. Although both tools aim to verify protocol security, they differ significantly in their underlying formalisms, semantics, and verification techniques, which has so far prevented rigorous cross-tool comparison on equivalent models. The authors develop a sound and partially complete translation from Tamarin’s multiset rewrite rule (MSR) models into ProVerif’s applied-pi calculus processes, including novel encodings of multiset semantics and simultaneous events. This translation enables expressing a large fragment of Tamarin’s features faithfully in ProVerif, allowing a direct comparison. They provide formal soundness and completeness proofs within the faithful translation fragment, ensuring that verified properties in ProVerif hold in Tamarin and certain exists-trace properties are preserved. Best-effort encodings such as XOR are handled separately and lie outside these guarantees. On a large evaluation set of 121 publicly available Tamarin models, the translation covers 562/566 lemma tasks, showing very high agreement (99.6%) on definitive results and demonstrating that ProVerif is substantially faster and more memory efficient for most tasks. This practical and theoretical contribution fills a long-standing gap by bridging the conceptual and semantic divide between these influential tools, enabling rigorous comparative analyses and mutual cross-validation.
Key findings
- Translation covers 562 of 566 lemma tasks across 121 Tamarin models evaluated.
- Among 247 non-XOR lemma tasks with definitive results from both tools, 246 (99.6%) yields identical results.
- ProVerif is faster than Tamarin on 334 out of 362 tasks (92.3%) where Tamarin returns Boolean and ProVerif returns logical results.
- Median per-task runtime ratio (Tamarin / ProVerif) is 6.74x; peak-memory ratio is 6.24x.
- Soundness theorem ensures any ProVerif verification within the faithful fragment holds in the original Tamarin model.
- Completeness guarantees preservation of exists-trace properties not involving attacker knowledge.
- Certain constructs such as XOR are translated as best-effort approximations outside soundness guarantees.
- Tamarin’s logic fragment is strictly more expressive than ProVerif’s; certain lemmas require query rewriting or splitting.
Threat model
The adversary is modeled within the standard symbolic Dolev-Yao attacker capabilities accessible to both Tamarin and ProVerif: it can intercept, replay, and fabricate messages arbitrarily on the network, but cannot break cryptographic primitives beyond the assumed equational theories. The analysis assumes perfect cryptography and no side-channels. The adversary does not control internal protocol state directly but can influence protocol execution via network messages.
Methodology — deep read
The authors begin by defining a precise threat model scoped to symbolic protocol verification: an adversary can intercept, fabricate, and replay messages as modeled by Tamarin and ProVerif semantics, but cannot compromise cryptography beyond the Dolev-Yao assumptions. The goal is to faithfully represent Tamarin models in ProVerif’s applied-pi calculus to compare verification results and performance.
They collect a diverse dataset of 121 Tamarin models representing various protocols and security properties, yielding 566 lemma verification tasks. lemmas are specifications of security properties expressed as trace properties in Tamarin’s rich two-sorted first-order logic with explicit timepoints.
The core technical contribution is a sound translation of Tamarin’s multiset rewrite rules (MSRs) to ProVerif processes. Each Tamarin rule is converted to a ProVerif subprocess, running under replication to simulate multiple rule applications. Persistent and linear facts in Tamarin translate into ProVerif tables for monotonic storage, with lookups and insertions representing premise and conclusion of rules. Special fact symbols In, Out, and Fr translate directly to ProVerif’s input, output, and name creation constructs, respectively.
To overcome ProVerif’s limited pattern-matching, the authors introduce private auxiliary destructors which partially decompose complex terms to extract variables matched in Tamarin premises. They also encode multiset rewrite semantics using table entries augmented with unique identifiers to model fact multiplicities and linear consumption.
Lemma translation adapts Tamarin’s general trace formulas into ProVerif’s more restricted single-alternation quantified Boolean formula (SA-QBF) fragment by rewriting and splitting lemmas when needed. Injective properties are decomposed into combinations of correspondence and uniqueness queries.
The translation is accompanied by formal soundness proofs showing that properties satisfied by the resulting ProVerif model also hold in the original Tamarin semantics for the faithful fragment, and completeness results that capture which existential trace properties without attacker knowledge are preserved. Best-effort features, especially XOR and partial Diffie-Hellman, fall outside these guarantees.
The system is implemented and tested on the 121 Tamarin models. The evaluation measures coverage, correctness agreement on equivalently translated lemmas, and performance metrics including runtime and memory use. Results show near-perfect agreement on non-XOR tasks and major performance advantages for ProVerif, notably faster executions (median speedup over 6x) and reduced peak memory usage (median factor 6x reduction).
Reproducibility is partially supported by detailed formal definitions and proofs, though code and data release status is not explicitly stated. One concrete example demonstrated is the Lowe fix of the Andrew Secure RPC protocol, where the Tamarin model is translated automatically, checked by ProVerif, and verification times compared.
Overall, the methodology combines formal semantics alignment, syntactic and semantic encoding innovations, soundness and completeness reasoning, and extensive empirical benchmarking to rigorously bridge and compare two divergent protocol verification frameworks.
Technical innovations
- Novel systematic translation of Tamarin multiset rewrite rules into ProVerif processes using tables augmented with unique identifiers to encode multiset and linear fact semantics.
- Introduction of private auxiliary destructors enabling ProVerif to emulate Tamarin’s complex pattern matching within rule premises.
- Formula rewriting techniques that decompose Tamarin’s richer trace lemmas into ProVerif’s SA-QBF fragment queries enabling sound and complete property translation.
- Characterization and formal proof of a faithful translation fragment where soundness (correctness of verified properties) and completeness (preservation of existential trace properties without attacker knowledge) hold.
- Best-effort encodings of features not natively supported by ProVerif, especially XOR, with explicit identification of their limitations.
Datasets
- Tamarin benchmark collection — 121 models — publicly available set from Tamarin protocol verification community
Baselines vs proposed
- Tamarin: median runtime = X seconds (not specified) vs ProVerif: median runtime = X/6.74 seconds
- Tamarin: median peak memory = Y MB (not specified) vs ProVerif: median peak memory = Y/6.24 MB
- Agreement on 247 non-XOR tasks with definitive results: Tamarin and ProVerif agree on 246 tasks (99.6%)
Limitations
- Translation excludes or only best-effort supports XOR and Diffie-Hellman primitives, which are common in cryptographic protocols.
- ProVerif’s SA-QBF logic fragment restricts expressiveness relative to full Tamarin first-order trace formulas, requiring lemma rewriting and sometimes splitting.
- Over-approximations (e.g., use of replication and monotonic tables) may lead to incomplete modeling of linearity or ordering in some cases.
- Evaluation results do not include adversarial attack scenarios crafted specifically to exploit translation gaps.
- Reproducibility and code availability are not explicitly stated, which may hinder independent verification.
- No explicit distribution shift or out-of-sample model generalization tests are reported.
Open questions / follow-ons
- How to extend faithful translation support for XOR and Diffie-Hellman operations within the ProVerif framework?
- Can the translation and comparison methodology be generalized to other protocol verification tools or more expressive cryptographic primitives?
- What are the implications of observed semantic gaps for protocol design guidance and tool selection in practical verification scenarios?
- How do the translation and verification results hold up under adversarial modeling beyond standard Dolev-Yao assumptions or under compositional protocol settings?
Why it matters for bot defense
Although this work operates primarily within the domain of formal security protocol verification—distinct from classical CAPTCHA and bot-defense mechanisms—the methodological insights into translating and comparing two distinct symbolic verification frameworks are relevant for bot-defense researchers pursuing formally vetted protocol or authentication challenge designs. Captcha system designers requiring guarantees about protocol soundness and equivalence under alternative symbolic models may benefit from the demonstrated systematic translation approach and its rigorously established soundness guarantees. Moreover, performance trade-offs observed between Tamarin and ProVerif can inform engineering decisions regarding verification toolchains used to validate bot-defense protocols or cryptographic puzzles embedded in CAPTCHAs. The ability to cross-validate properties and explore performance scaling yields useful lessons for practical CAPTCHA lifecycle assurance.
Cite
@article{arxiv2608_06315,
title={ A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis },
author={ Kevin Morio and Yavor Ivanov and Robert Künnemann },
journal={arXiv preprint arXiv:2608.06315},
year={ 2026 },
url={https://arxiv.org/abs/2608.06315}
}