做安全协议验证的团队终于有了减少人工的利器——RL框架自动生成更短证明，Tamarin用户可以直接集成到现有工作流中，值得一试。
本文提出一个基于强化学习的框架，借鉴AlphaZero和AlphaProof的思路，为安全协议分析工具Tamarin实现新的证明搜索方式。该框架通过无状态API将Tamarin转化为经典RL环境，并用蒙特卡洛树搜索结合神经网络启发式，从已完成子证明中学习。在16个案例研究中，该方法比Tamarin标准搜索找到更多自动证明，且生成的证明比标准及人工设计的启发式更短。该框架可直接用于辅助Tamarin用户，减少人工工作量，展示了RL方法在协议验证领域的潜力。
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
Tools like Tamarin and ProVerif have achieved notable success in analyzing and verifying complex real-world protocols such as EMV, 5G, and WPA2, even detecting zero-day exploits. Despite these successes, verifying such protocols remains a time-consuming, challenging task, often requiring significant human effort and expertise. In this paper, we present a reinforcement learning (RL) framework inspired by AlphaZero and AlphaProof that implements a new style of proof search for Tamarin. We have developed a stateless API for Tamarin that acts as a classical RL environment. We guide a Monte Carlo Tree Search (MCTS) by a neural heuristic that learns from completed subproofs. We evaluate our framework on 16 case studies, ranging from classical protocol models to challenging state-of-the-art protocol models from recent publications. Our method finds more proofs automatically than Tamarin's standard search and produces shorter proofs than both the standard and human-engineered heuristics. Our pipeline is applicable out of the box to assist Tamarin users in active research, reducing the human effort required. Moreover, our standardized interface provides a programmatic way for users to interact with Tamarin. Finally, our work demonstrates the promising potential of adapting RL-based methods to the Tamarin domain.