AI 中文总结
本文提出从安全协议验证工具Tamarin到ProVerif的可靠翻译，支持二者严格对比，经121个模型评估，ProVerif在多数任务中更快，非异或任务一致性达99.6%。
AI 中文摘要
Tamarin和ProVerif是两款用于安全协议形式化验证的知名工具，二者虽拥有相同的高级目标，但底层形式体系与验证技术差异显著，导致系统对比颇具挑战：Tamarin采用多重集重写规则，具备可靠且完备的验证能力；ProVerif则应用应用π演算的扩展版本，可提供快速但可能不完备的结果。本文提出一种从Tamarin到ProVerif的可靠翻译，为两款工具的严格对比提供支持。该翻译引入了公式重写、编码多重集重写语义及处理并发事件的新技术，支持Tamarin的广泛功能子集，包括多重集重写规则、引理和限制，同时明确界定了无法实现忠实翻译的情形。我们提供了形式化证明：在忠实片段内，可靠性确保ProVerif中验证的任何属性也适用于原始Tamarin模型，完备性确保不涉及攻击者知识的存在性跟踪属性得到保留。异或（XOR）等尽力而为的编码单独报告，不受上述保证约束。最后，我们在121个Tamarin模型上对该翻译进行评估，翻译覆盖566项引理任务中的562项；在两款工具均给出确定结果的非异或任务中，247项里有246项一致，剩余结果被明确标记为使用不完备模型；在Tamarin返回布尔结果且ProVerif完成逻辑结果的362项任务中，ProVerif在334项中速度更快（占比92.3%），每项任务的中位数运行时比率和峰值内存比率分别为6.74倍和6.24倍。
英文摘要
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 techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, supporting a large 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 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.74x and 6.13x, respectively.
Comments21 pages, 5 figures, 5 tables. Full version of the corresponding ACM CCS '26 paper
