A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

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 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 a large subset of Tamarin's features-including multiset rewrite rules, lemmas and restrictionsthereby 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 ProVerif front end accepts executable translations for 523 of 566 lemma tasks. Among non-XOR tasks with definitive results from both tools, 237 of 238 agree, with the remaining verdict explicitly flagged as using an incomplete model. Among the 344 tasks for which Tamarin returns a Boolean result and ProVerif completes with a logical result, ProVerif is faster in 316 cases (91.9 %), with median per-task runtime and peak-memory ratios of 6.74× and 6.13×, respectively.