用强化学习自动找安全协议证明，更快更短。
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
- 基于AlphaZero思想，用神经网络引导蒙特卡洛搜索
- 16个案例中自动找到更多证明，且证明长度更短
- 无需调参即插即用，适合安全协议研究者
Tamarin和ProVerif等工具在分析复杂现实协议（如EMV、5G、WPA2）方面已取得显著成果，甚至发现零日漏洞。然而，验证过程仍耗时耗力，需大量人工干预。本文提出一种受AlphaZero和AlphaProof启发的强化学习框架，用于Tamarin的证明搜索。我们设计了一个无状态API，将Tamarin变为经典强化学习环境，通过神经启发式函数引导蒙特卡洛树搜索（MCTS），学习已完成子证明的模式。在16个案例中评估，包括经典与前沿协议模型，该方法自动找到的证明数量超过Tamarin标准搜索，且生成的证明比标准和人工启发式方法更短。该流程可开箱即用，降低用户人力成本，并提供程序化接口。本工作展示了强化学习在Tamarin领域的巨大潜力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。