该论文关注的是一个长期被忽视但至关重要的问题：密码学协议形式化验证工具（尤其是 Tamarin、ProVerif 及同类协议验证器）在实际使用中的可用性问题。作者指出，尽管这类工具被广泛用于分析复杂安全协议（如 TLS、SSH、信号协议、认证与密钥交换协议等）的安全性质，但关于『真实用户如何使用这些工具、在哪些环节遇到困难』的实证研究仍相当匮乏，工具设计者往往缺乏来自一线的反馈依据。为此，作者开展了一项以人为中心的探索性研究（human-centered exploratory study），通过问卷调查的形式，系统性收集了具备实际使用经验的用户反馈。受访群体包括研究人员、研究生以及工业界从业者，均具有使用 Tamarin、ProVerif 或相关工具的动手经验，覆盖面兼顾学术与工程两侧。研究结果揭示了贯穿整个验证工作流的多个可用性障碍：其一，当验证过程出现不终止（non-termination）或性能瓶颈时，用户难以进行有效的调试与定位，缺乏可操作的诊断信息；其二，缺乏系统化方法将形式化模型与真实世界协议实现进行对照校验，用户很难判断『模型是否忠实反映了真实协议』，这直接影响验证结论的可信度；其三，当证明失败但没有给出具体攻击路径（concrete attack）时，用户普遍采取的经验性应对策略是简化模型、补充辅助引理（helper lemmas）、或反复回溯并调整建模抽象层次，整个过程高度依赖个人经验与试错，缺少方法学支撑。此外，受访者明确提出了对可操作诊断、更清晰的结果解释、可视化能力以及对重复性证明任务自动化的需求。作者的核心论断是：这些持续存在的可用性挑战，根源在于『协议层面的推理方式』与『验证器的形式化模型、证明过程及诊断输出』之间存在语义与认知上的鸿沟。基于上述发现，论文提炼出一组具体的设计优先级，用于提升密码协议验证工具的可访问性、可解释性与易用性。该工作属于典型的可用性/人机交互与形式化方法交叉研究，适合形式化验证工具开发者、协议安全研究者、以及需要将形式化验证引入工程流程的安全团队阅读。

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