这篇论文针对两个主流的协议形式化验证工具 Tamarin 和 ProVerif 提出了首个从 Tamarin 到 ProVerif 的忠实的（sound）翻译方法，以支持系统性的对比分析。Tamarin 基于多集重写规则，验证是可靠且完备的；而 ProVerif 基于应用 pi 演算的扩展，验证速度更快但可能不完整。两者的底层形式化体系和验证技术差异很大，导致难以直接比较。作者开发了一种新翻译方法，包含公式重写、多集重写语义的编码以及对同时事件的处理，能够支持 Tamarin 的绝大多数特性，包括多集重写规则、引理和限制。同时，论文精确刻画了无法忠实翻译的情况，并通过形式化证明保证了在忠实翻译片段内的可靠性（soundness）和完整性（completeness）：若 ProVerif 验证成功，则原 Tamarin 模型中也成立；若 Tamarin 中存在某条轨迹，除非涉及攻击者知识，否则该轨迹在 ProVerif 中也被保留。对于非线性（XOR）等最佳努力编码，论文会单独报告，且不在上述保证范围内。实验部分在 121 个 Tamarin 模型上评估了翻译过程，共覆盖 566 个引理任务中的 562 个。在非 XOR 且两个工具都给出确定性结果的任务中，247 个里有 246 个结论一致，剩余的一个明确标注为使用了不完整模型。在 Tamarin 返回布尔结果且 ProVerif 返回逻辑结果的 362 个任务中，ProVerif 在 334 个任务（92.3%）上运行更快，每个任务的中位数运行时间比为 6.74 倍，峰值内存比为 6.24 倍。这项研究为安全协议分析工具的互操作和结果交叉验证奠定了基础，对形式化验证社区具有重要意义。