这篇论文针对两个主流的协议形式化验证工具 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 倍。这项研究为安全协议分析工具的互操作和结果交叉验证奠定了基础，对形式化验证社区具有重要意义。

这篇论文将范畴论应用于密码学中的通用可组合性（UC）框架，以建立安全组合的严格数学理论。UC框架由Canetti提出，用于评估协议在并发环境中的安全性，但传统形式化依赖于交互式图灵机和复杂的概率论证明，难以扩展和验证。作者针对静态参与方和会话数量的系统，提出了一种范畴化表示：将协议、环境和对手建模为对象和态射，利用string diagrams（弦图）进行图形化推理，同时保持可翻译为代数方程的严谨性。该方法带来四个主要贡献：第一，通过弦图使组合定理的证明直观且简短，同时支持形式化验证；第二，范畴论抽象使结果超越交互式图灵机，适用于量子计算、领域特定语言等其他计算模型；第三，放宽了UC的某些限制，例如允许对手是计算网络而非单一图灵机，且证明其变体与标准UC等价，不损失表达力；第四，范畴论视角揭示了标准UC形式化中的若干小技术疏漏，并给出了修正。论文属于理论安全研究，为协议组合安全性提供了更通用、更严谨的数学基础，并为自动化验证和跨计算模型的安全性分析开辟了新途径。适合理论密码学、形式化方法和范畴论研究者深入研读。