目前的形式化方法已经成功地用于发现许多安全协议中的设计缺陷。然而，由于协议的状态空间很大或无限大，对其进行自动分析仍然是一个挑战。本研究提出了一种新的通用框架SmartVerif，它突破了现有验证方法自动化能力的极限。我们的主要技术贡献是SmartVerif内部的动态策略，它可以用来智能地搜索证明路径。与现有静态策略的非平凡性和易出错性设计不同，我们的动态策略设计简单灵活，它可以根据安全协议自动优化自身，而无需任何人工干预。通过优化后的策略，SmartVerif可以定位和证明支持引理，从而提高了验证成功的概率。设计该策略的意义在于，当随机策略被给定时，表示支持引理的节点处于错误证明路径上，且概率较低。因此，我们通过引入强化学习算法来实现这一策略。我们还提出了几种解决SmartVerif实现中其他技术问题的方法。实验结果表明，SmartVerif能够自动验证本文研究的所有安全协议。案例分析也验证了动态策略的有效性。

       本研究由中国科学技术大学在本项目的支持下完成，发表在CCF A类推荐会议Usenix Security 2020，原文可由链接https://www.usenix.org/system/files/sec20summer_xiong_prepub.pdf查看。