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