Search papers, labs, and topics across Lattice.
This paper introduces a sound translation mechanism from Tamarin to ProVerif, facilitating a rigorous comparative analysis of these two formal verification tools for security protocols. By employing novel techniques for formula rewriting and encoding multiset rewrite semantics, the authors ensure that properties verified in ProVerif are soundly preserved from Tamarin, while also identifying cases where faithful translation is not achievable. The evaluation demonstrates that ProVerif significantly outperforms Tamarin in runtime efficiency, achieving agreement on the majority of tasks while maintaining soundness and completeness for a substantial subset of properties.
ProVerif outpaces Tamarin in verification speed by over 92%, while ensuring soundness in the majority of comparative tasks.
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.
