10:02arXiv cs.LG@Matthias Cosler, Cas Cremers, Bernd Finkbeiner, Mohamed Ghanem, Niklas Medinger本文提出一个基于强化学习的框架,借鉴AlphaZero和AlphaProof的思路,为安全协议分析工具Tamarin实现新的证明搜索方式。该框架通过无状态API将Tamarin转化为经典RL环境,并用蒙特卡洛树搜索结合神经网络启发式,从已完成子证明中学习。在16个案例研究中,该方法比Tamarin标准搜索找到更多自动证明,且生成的证明比标准及人工设计的启发式更短。该框架可直接用于辅助Tamarin用户,减少人工工作量,展示了RL方法在协议验证领域的潜力。论文强化学习安全协议验证Tamarin蒙特卡洛树搜索自动证明推荐理由:做安全协议验证的团队终于有了减少人工的利器——RL框架自动生成更短证明,Tamarin用户可以直接集成到现有工作流中,值得一试。原文