(19)中华 人民共和国 国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202111327343.5 (22)申请日 2021.11.10 (71)申请人 中国人民解 放军战略支援 部队信息 工程大学 地址 450001 河南省郑州市高新区科 学大 道62号 (72)发明人 顾纯祥　田凯　魏福山　石雅男　 李光松　杨本朝　 (74)专利代理 机构 郑州睿信知识产权代理有限 公司 41119 代理人 陈浩 (51)Int.Cl. H04L 9/40(2022.01) G06N 20/00(2019.01) (54)发明名称 一种网络安全协议 脆弱性分析方法 (57)摘要 本发明涉及一种网络安全协议脆弱性分析 方法， 属于网络安全自动化分析技术领域。 本发 明首先对目标协议进行状态机推断； 然后提取目 标状态机的有效执行路径(状态转移路径)； 再基 于应用Pi演算对状态转移路径形式化建模， 说明 协议参与者的行为与交互， 通过对状态机每一步 状态转移进行形式化建模， 完成对安全协议程序 实现的状态机转移路径的自动化 建模； 将目标协 议自动转化为可用于形式化分析的符号模型， 实 现协议状态机到形式化分析脚本的自动化转化。 最后利用形式化分析工具对协议实现进行脆弱 性自动化分析挖掘。 本发明避免了依赖人工分析 的问题， 能够利用形式化分析具体对其脆弱性进 行自动分析， 大 大提高了分析效率。 权利要求书1页 说明书8页 附图6页 CN 114039783 A 2022.02.11 CN 114039783 A 1.一种网络安全协议 脆弱性分析 方法， 其特 征在于， 该 方法包括以下步骤： 1)获取目标协议， 对目标协议进行状态机推断； 2)对推断出目标协议状态机进行路径搜索， 提取 出目标协议状态转移路径； 3)对提取 出的状态转移路径进行 形式化建模； 4)根据目标协议特点和目标协议状态机对目标协议中的组件进行 形式化建模； 5)根据形式化建模组件利用形式化分析工具对形式化建模的路径进行分析， 确定目标 协议的攻击路径， 实现对目标协议的安全性分析。 2.根据权利要求1所述的网络安全协议脆弱性分析方法， 其特征在于， 所述步骤1)中的 状态机推断包括成员查询过程和等价查询过程； 所述成员查询过程指的是在成员查询阶 段， Learner根据给定的字母表利用有限状态机学习算法生成一轮测试消息， 由Mapper将测 试消息转化为SUL能够接收的消息并发送给SUL， SUL对接收到的消息进行响应； 通过多轮消 息查询与重置， 根据从SUL收到的响应提出假设； 所述等价查询过程指的是检查成员查询过 程中提出的假设与实际状态机是否一致， 若不一致， 则返回一个反例， 供成员查询过程重新 提出假设， 若一 致， 则认为当前状态机推断近似等 价于真实 实现。 3.根据权利要求2所述的网络安全协议脆弱性分析方法， 其特征在于， 所述成员查询过 程中采用的有限状态机学习算法为 L*算法或者T TT算法。 4.根据权利要求2所述的网络安全协议脆弱性分析方法， 其特征在于， 所述等价查询过 程中采用W 算法。 5.根据权利要求1或2所述的网络安全协议脆弱性分析方法， 其特征在于， 所述步骤2) 中采用启发式广 度优先搜索算法对推断出的状态机进行路径搜索。 6.根据权利要求1或2所述的网络安全协议脆弱性分析方法， 其特征在于， 所述步骤3) 中的形式化建模 采用Pi演算实现。 7.根据权利要求6所述的网络安全协议脆弱性分析方法， 其特征在于， 在采用Pi演算对 状态转移路径进行建模时， 将每一次状态转换建模成为子进程， 整条状态转移路径为子进 程的组合。 8.根据权利要求1或2所述的网络安全协议脆弱性分析方法， 其特征在于， 所述的形式 化分析工具采用ProVerif、 A VISPA、 SPIN或Tamari n。 9.根据权利要求1或2所述的网络安全协议脆弱性分析方法， 其特征在于， 所述步骤4) 中的组件 包括有数据类型&常量、 消息、 密码原语、 时间、 查询和辅助进程。 10.根据权利要求9所述的网络安全协议脆弱性分析方法， 其特征在于， 所述步骤4)中 采用Pi演算和形式化分析工具实现对组件的建模。权　利　要　求　书 1/1 页 2 CN 114039783 A 2一种网络安全协议脆弱性分析方 法 技术领域 [0001]本发明涉及 一种网络安全协议脆弱性分析方法， 属于网络安全自动化分析技术领 域。 背景技术 [0002]随着信息革命的不断推进， 网络成为人们生活中不可或缺的一部分。 敏感信息在 网络上的安全传输 问题关系着个人、 企业乃至 国家的发展。 安全协议以密码算法为基础在 互联网络中为用户提供信息保护服务， 是信息安全领域的一项重要内容。 网络安全协议是 营造网络安全环境的基础， 是构建安全网络的关键技术。 设计并保证网络安全协议的安全 性和正确性能够从基础上保证网络安全， 避免因网络安全等级不够而导致网络数据信息丢 失或文件损坏等信息泄露问题。 在计算机网络应用中， 人们对计算机通信的安全协议进行 了大量的研究， 以提高网络信息传输的安全性。 [0003]以应用最为广泛的TLS协议为例， TLS协议先后遭受了降级攻击、 重协商攻击、 POODLE攻击、 DROWN攻击、 ROBOT攻击等各类攻击。 近年来， 针对TLS协议的攻击以其实现安全 性分析为主流方 向， 出现了CCS中间人攻击， HeartBleed攻击等针对TLS协议实现的攻击方 法。 [0004]常用的协议实现的分析方法有模糊测试、 符号执行、 模型学习等， 这些方法从代码 或执行行为分析协议实现的安全性。 上述方法首先从协议代码或执行行为中提取抽象模 型， 然后对模型进行检查， 寻找违反规范的情形， 从而找出隐藏的漏洞。 模型学习凭借其思 路直观、 自动化程度高的优势已经成为当前主流的协议分析方法。 协议的模型学习 是一种 黑盒测试方法， 通过发送不同消息序列到目标系统， 并观察相应的输出从而推导协议状态 机， 进而对得到的状态机进行分析， 检测是否存在逻辑漏洞或者 其它冗余的状态。 [0005]模型学习理论最早由Angluin在1987年提出， 其主要思想是通过著名的MAT (Minimally  Adequate  Teacher)框架使用成员查询与等价查询学习系统的有限状态机。 Peled等人发现MAT框架可以用于学习软件或是硬件的黑盒模型。 近年来， 模型学习被应用 在网络协议安全性分析领域。 2015年， Joeri  de Ruiter等人通过协议状态模糊测试对TLS 协议实现了较高程度的自动化分析， 从协议实现层面 自动提取9个TLS协议实现的状态机， 并找到3个违反规范的行为。 而后模型 学习被应用于各种协议的状态机推断。 [0006]已有的研究对状态机分析多依赖人工分析， 对于复杂的状态机分析效率较低且分 析效果不够理想。 虽然有研究者将模型检测的方法引入到协议的状态机分析之中， 但模型 检测仅能够验证状态机的合规性， 无法对协议实现的安全性进行有效的分析。 协议的形式 化分析是对协议逻辑设计层面安全性分析 的重要方法， 它将协议抽象成数学模型， 通过程 式化的推演计算， 以检查协议是否满足其预期的安全目标。 近年来出现了较为有效的自动 化验证工具， 如ProVer if、 Tarmain等， 在安全协议的设计和分析中发挥了重要的作用。 但自 动化验证工具目前仅适用于协议逻辑设计分析， 由于协 议实现拥有比协 议标准更为复杂多 样的状态空间与执 行路径， 难以抽象成固定的符号模型， 很难 对其进行自动化分析。说　明　书 1/8 页 3 CN 114039783 A 3