A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis
2026-08-06 • Cryptography and Security
Cryptography and Security
AI summaryⓘ
The authors compare two tools, Tamarin and ProVerif, used to check the security of communication protocols. While Tamarin is thorough but slower, ProVerif is faster but may miss some issues. They created a way to translate Tamarin's models into ProVerif's format to directly compare them, proving that in many cases the results match reliably. Their tests showed ProVerif is usually faster and agrees with Tamarin most of the time, especially for tasks that don't involve certain tricky operations like XOR. This work helps users understand when the faster tool can be trusted to give correct answers.
TamarinProVerifsecurity protocolsformal verificationmultiset rewrite rulesapplied-pi calculussoundnesscompletenessXOR encodingmodel translation
Authors
Kevin Morio, Yavor Ivanov, Robert Künnemann
Abstract
Tamarin and ProVerif are two prominent tools for the formal verification of security protocols. They share the same high-level goal but 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-pi calculus that provides fast but potentially incomplete results. We present a sound translation from Tamarin to ProVerif that enables a rigorous comparison of the two tools. It introduces novel techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, supporting an extensive subset of Tamarin's features, including multiset rewrite rules, lemmas, and restrictions, while precisely characterizing the cases where faithful translation is not possible. We provide formal proofs: within the faithful fragment, soundness ensures that any property verified in ProVerif also holds in the original Tamarin model, and completeness ensures that exists-trace properties not involving attacker knowledge are preserved. Best-effort encodings, in particular XOR, are reported separately and are outside these guarantees. Finally, we evaluate 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.74x and 6.24x, respectively.