本文针对安全协议设计中的正确性验证问题，提出了一种在计算模型下对任意会话数进行协议证明的交互式证明框架。作者在Bana和Comon等人先前工作的基础上进行了扩展，原始工作只能分析固定会话数且缺乏证明机械化支持。论文首先定义了一个元逻辑以及相应的证明系统，用于推导安全属性。该证明系统仅处理协议执行的高层符号表示，类似于符号模型中的证明，但能够提供计算级别的安全保证。作者实现了这一方法，构建了名为Squirrel的交互式证明器，其输入是用应用π演算描述的协议。通过多个案例研究，覆盖了哈希、加密、签名、Diffie-Hellman指数运算等原语，以及认证、强机密性、不可链接性等安全属性，验证了该方法的有效性和通用性。该工作弥合了符号模型与计算模型之间的鸿沟，为协议安全性提供了可机械化验证的计算级保证，适用于协议设计者和形式化验证研究人员。

本文提出了一种基于强化学习（RL）的框架，用于提升 Tamarin 协议分析工具中的证明搜索效率。Tamarin 是广泛用于验证安全协议（如 EMV、5G、WPA2）的自动推理工具，但传统方法需要大量人工专家干预。受 AlphaZero 和 AlphaProof 启发，作者设计了一个无状态的 API，将 Tamarin 转化为经典 RL 环境，并通过蒙特卡洛树搜索（MCTS）结合神经网络启发式学习已完成子证明的模式。在 16 个案例研究（包括经典协议模型及最新发表中的复杂协议模型）上，该方法比 Tamarin 标准搜索自动找到更多证明，且生成的证明比标准启发式甚至人工编写的启发式更短。该框架可直接用于帮助 Tamarin 用户减少人工努力，同时提供标准化的程序化接口。实验结果表明，RL 方法在协议形式化验证领域具有巨大潜力。