杨锦翔，熊 焰，黄文超

（1.中国科学技术大学 网络空间安全学院，合肥 230022；2.中国科学技术大学 计算机科学与技术学院，合肥 230022）

0 概述

安全协议旨在通过应用密码原语在不安全的网络上提供安全通信。然而，安全协议的设计特别容易出错，研究者在5G［1］、TLS［2］等协议中都发现了设计上存在的缺陷。这使得安全协议的安全性验证成为一个热门的研究课题。

目前，已有许多对安全协议进行建模与分析的工作。最早的协议分析工具如Interrogator［3］和NRL Protocol Analyzer［4］，能够验证时序逻辑中的安全属性。一些通用的模型检测工具也已经被用于分析协议，如FDR［5］和Murphi［6］。最近，研究的重点转向了设计专门用于分析安全协议的模型检测工具，如Blanchet’s ProVerif［7］、AVISPA tool［8］、MaudeNPA［9］和Tamarin prover［10］。

虽然在安全协议的设计中利用形式化的方法能够成功地找到漏洞，但实现对安全协议的全自动分析仍然是一个挑战。smartVerif［11］是基于强化学习的一般性框架，其能提高目前最先进验证工具的自动化能力，但不足之处在于无泛化性，需要对每个安全协议训练一个对应的神经网络模型，每个安全协议的验证都需要从完全随机探索开始训练，因此验证效率较低。

本文基于无人工特征的强化学习模型对smartVerif框架进行优化。该优化方案通过Alpha Go zero［12］中将深度神经网络与蒙特卡洛树搜索相结合的形式，与smartVerif 中所使用的DQN 网络结构相比，只需要利用安全协议训练一个模型即可验证新的安全协议，无需重新训练网络。此外，关注形式化验证数据所包含的结构化信息，在向量表示方法中使用树型结构作为中间表达对形式化数据进行转换，同时考虑验证过程中的历史信息。……