FlagThis

Abstract

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- pi calculus that provides fast but potentially incomplete results. 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- pi 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 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 Tamarins features can be expressed in ProVerifs formalism while precisely characterizing the cases where this is not possible. The translation supports an extensive subset of Tamarins featuresincluding multiset rewrite rules, lemmas and restrictionsthereby aligning the semantics of the two formalisms. We compare the expressiveness of Tamarins 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.