(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202211083948.9 (22)申请日 2022.09.06 (71)申请人 中国科学技术大学 地址 230000 安徽省合肥市金寨路96号 (72)发明人 黄文超　熊焰　汪万森　孟昭逸　 苏诚　熊峰　方贤进　 (74)专利代理 机构 安徽思沃达知识产权代理有 限公司 342 20 专利代理师 王茜 (51)Int.Cl. H04L 69/00(2022.01) H04L 43/18(2022.01) G06N 20/00(2019.01) (54)发明名称 一种网络安全协议的自动形式化验证方法 (57)摘要 本发明公开了一种网络安全协议的自动形 式化验证方法， 包括步骤： 一、 输入协议模型； 二、 初始树构建； 已依据静态策略路径选择执行六、 否则执行三； 三、 依据静态策略进行路径选择； 四、 依据静态策略进行路径检查； 路径循环执行 二； 完整且正确输出验证结果； 正确但不完整执 行五； 五、 定理树合并， 已依据静态策略路径选择 执行六、 否则执行三； 六、 依据动态策略进行路径 选择； 七、 依据动态策略进行路径检查； 路径循环 时训练神经网络优化证明策略再返回二； 路径完 整且正确时输出验证结果； 路径 正确但不完整时 执行八； 八、 定理树合并： 定理树合并， 已依据静 态策略进行了路径选择执行六、 否则执行三。 本 发明全过程都自动化， 准确性高， 效率高。 权利要求书2页 说明书6页 附图3页 CN 115460297 A 2022.12.09 CN 115460297 A 1.一种网络安全协议的自动形式化验证方法， 其特 征在于， 该 方法包括以下步骤： 步骤一、 输入协议模型： 输入网络安全协议形式化模型； 步骤二、 初始树构建： 构建形式化验证的底层框架， 自动提取网络安全协议形式化模型 中的证明目标， 构建初始定理树； 判断是否已依据静态策略进 行了路径选择， 是就执行步骤 六、 否则执 行步骤三； 步骤三、 依据静态策略进行路径选择： 根据预设的静态策略进行证明路径的选择； 步骤四、 依据静态策略进行路径检查： 使用循环检测算法判断证明路径的完整性和正 确性； 当证明路径中存在循环 时， 返回执行步骤二； 当证明路径完整且正确时， 网络安全协 议成功完成验证， 系统自动终止， 输出验证结果； 当证明路径正确但不完整时， 执 行步骤五； 步骤五、 定理树合并： 根据当前证明路径， 使用信息获取模块进一步构建新的定理子 树， 并与之前轮次的定理树合并， 对定理树进行扩展； 扩展完成后， 判断是否已依据静态策 略进行了路径选择， 是就执 行步骤六、 否则返回执 行步骤三； 步骤六、 依据动态策略进行路径选择： 根据预设的动态策略进行证明路径的选择； 步骤七、 依据动态策略进行路径检查： 使用循环检测算法判断证明路径的完整性和正 确性； 当证明路径中存在循环时， 可能导致协 议验证过程无法终止， 给予该证明路径神经网 络反馈， 并训练神经网络优化证明策略， 再返回执行步骤二； 当证明路径完整且正确时， 网 络安全协议成功完成验证， 系统自动终止， 输出验证结果； 当证明路径正确但不完整时， 执 行步骤八； 步骤八、 定理树合并： 根据当前证明路径， 使用信息获取模块进一步构建新的定理子 树， 并与之前轮次的定理树合并， 对定理树进行扩展； 扩展完成后， 判断是否已依据静态策 略进行了路径选择， 是就执 行步骤六、 否则返回执 行步骤三。 2.按照权利要求1所述的一种网络安全协议的自动形式化验证方法， 其特征在于： 步骤 一中所述网络安全协议形式化模型使用多重集 合复写规则表示。 3.按照权利要求1所述的一种网络安全协议的自动形式化验证方法， 其特征在于： 步骤 三中所述预设的静态策略包括以下任意 一种： 第一种、 按照约束引入的先后顺序进行证明路径节点选择， 优先选择先引入的约束对 应的证明路径 节点； 第二种、 按照约束类型进行证明路径节点选择， 优先选择链型约束对应的证明路径节 点， 次优选择析取约束对应的证明路径节点， 再次之选择事实约束或动作约束对应的证明 路径节点， 攻击者相关约束的证明路径 节点最后选择； 第三种、 优先选择链型约束对应的证明路径节点， 次优选择析取约束对应的证明路径 节点， 剩下几个类型 的约束对应的证明路径节点处于同等优先级， 按照引入约束的顺序进 行选择。 4.按照权利要求1所述的一种网络安全协议的自动形式化验证方法， 其特征在于： 步骤 六中所述预设的动态策略为DQN强化学习网络、 DDQN强化学习网络或Dueling  DQN强化学习 网络， 步骤六中所述根据预设的动态策略进行证明路径的选择时， 根据DQN强化学习网络、 DDQN强化学习网络或Dueling  DQN强化学习网络评估定理树各节点成功完成验证的概率， 并根据评估结果自动选择 出证明路径。 5.按照权利要求1所述的一种网络安全协议的自动形式化验证方法， 其特征在于： 步骤权　利　要　求　书 1/2 页 2 CN 115460297 A 2四和步骤七中所述循环检测算法为基于约束含义的循环检测算法， 采用该循环检测算法判 断证明路径的完整性和正确 性时的方法为： 去除约束中的时间点编号和项编号， 得到简化 后的约束； 并略过即使简化形式相同也可能存在不同的含义的特殊约束； 当两个约束简化 形式相同时， 判断为两个约束的含义是相同的， 对证明过程的影响也是相似的； 当这样的约 束在某条证明路径中出现过多次 时， 判断为证明路径中存在循环。 6.按照权利要求5所述的一种网络安全协议的自动形式化验证方法， 其特征在于： 所述 即使简化形式相同也可能存在不同的含义的特殊约束包括攻击者相关约束、 时间点比较约 束和时间点引入约束。 7.按照权利要求5所述的一种网络安全协议的自动形式化验证方法， 其特征在于： 所述 当这样的约束在某条证明路径中出现过多次时， 判断为证明路径中存在循环， 其中， 多次为 三次以上。权　利　要　求　书 2/2 页 3 CN 115460297 A 3