A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis

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.

Source: arXiv:2608.06315v1 - http://arxiv.org/abs/2608.06315v1 PDF: https://arxiv.org/pdf/2608.06315v1 Original Link: http://arxiv.org/abs/2608.06315v1