一种属性驱动的安全协议符号化模型检测方法和系统

    公开(公告)号:CN112818569A

    公开(公告)日:2021-05-18

    申请号:CN202110416348.9

    申请日:2021-04-19

    摘要: 本发明提供一种属性驱动的安全协议符号化模型检测方法、系统和介质。所述方法包括:步骤S1、分别获取所述安全协议的状态机模型和进程演算模型;步骤S2、配置所述安全协议的时序性质,所述时序性质由时序逻辑的时间算子和逻辑运算符来描述;步骤S3、基于所述状态机模型对所述时序性质进行验证,以获取存在的反例;步骤S4、基于所述反例精化所述时序性质得到安全性质,调用ProVerif安全协议验证器,基于所述进程演算模型对所述安全性质进行验证。所述方法能够提高传统模型检测在安全协议时序性验证方面的正确性,有效避免虚假反例的情况,弥补了安全协议形式化验证工具无法对时序性建模与分析的问题。

    一种基于OSPF的安全路由协议方法和系统

    公开(公告)号:CN114157419B

    公开(公告)日:2023-08-08

    申请号:CN202111438825.8

    申请日:2021-11-29

    IPC分类号: H04L9/08 H04L45/12 H04L45/16

    摘要: 本发明提出一种基于OSPF的安全路由协议方法和系统。所述方法包括:步骤S1、OSPF协议报文的发送方和接收方进行随机数协商,所述OSPF为开放最短路径优先协议;步骤S2、所述发送方采用杂凑值对待发送的所述OSPF协议报文进行封装加固,将经封装加固的OSPF协议报文发送至所述接收方,并为所述经封装加固的OSPF协议报文分配发送序号;步骤S3、所述接收方在接收到所述经封装加固的OSPF协议报文后,提取所述经封装加固的OSPF协议报文的所述发送序号,并将所述发送序号与接收端维持的接收序号进行比较。

    一种基于序列重建的异常事件自动检测方法和系统

    公开(公告)号:CN114356743B

    公开(公告)日:2022-06-07

    申请号:CN202210234545.3

    申请日:2022-03-11

    IPC分类号: G06F11/34 G06N3/04 G06N3/08

    摘要: 本发明提出一种基于序列重建的异常事件自动检测方法和系统。所述方法包括:步骤S1、利用预定义的事件模板,从多源日志中确定离散事件序列,所述离散事件序列由同一用户的多个事件日志按照时间顺序拼接而成;步骤S2、对所述离散事件序列进行拆分处理来获取若干原始子序列,并通过对所述若干原始子序列进行特征嵌入,进一步获取无监督检测模型的输入子序列,所述无监督检测模型包括LSTM编码器、变分组件和LSTM解码器,用于基于所述输入子序列生成所述离散事件序列的重建子序列;步骤S3、基于所述原始子序列和所述离散事件序列的重建子序列,利用评判准则来判断所述多个事件的异常属性。

    一种双向认证的网络管理协议方法和系统

    公开(公告)号:CN113839969B

    公开(公告)日:2022-03-15

    申请号:CN202111427310.8

    申请日:2021-11-29

    IPC分类号: H04L9/40 H04L9/08

    摘要: 本发明提出一种双向认证的网络管理协议方法和系统。步骤S1、设备接入双向认证;步骤S2、控制操作的双向认证:设备网管向被管理设备下发配置数据、启用/关闭端口、终端的报文采用步骤S1中的协商的密钥进行加密传输;步骤S3、测试操作的双向认证:设备网管向被管理设备发送测试命令或者是被管理设备向网管系统返回的测试结果的报文,采用步骤S1中的协商的密钥进行加密传输;步骤S4、查询操作的双向认证:设备网管从被管理设备获取状态、配置、性能数据的报文,采用步骤S1协商的密钥进行加密传输;步骤S5、主报操作的双向认证:被管理设备主动向设备网管上报事件或消息的报文,采用步骤S1协商的密钥进行加密传输。

    一种双向认证的局域网安全接入协议方法和系统

    公开(公告)号:CN113839787A

    公开(公告)日:2021-12-24

    申请号:CN202111427308.0

    申请日:2021-11-29

    IPC分类号: H04L9/32 H04L29/06

    摘要: 本发明提出一种双向认证的局域网安全接入协议方法和系统。所述方法包括:发现阶段:局域网安全接入协议两端相互发送邻居间发送发现报文,相互发现对端上线情况,同时比较所述域网安全接入协议两端的MAC地址,所述两端包括两个通信实体即设备A和设备B,所述MAC地址较大的一端设备B主动进入协商阶段;协商阶段:由MAC地址较大的一端设备B主动进入协商阶段,并经历协商等待状态、协商结束等待状态后最终进入协商成功状态;MAC地址较小的一端设备A收到起始应答成功报文后,进入协商结束等待状态,并最终达到协商成功状态;保活阶段:由MAC地址较小的一端设备A定时主动发起客户端保活报文,服务端回复服务端保活消息进行保活。

    一种属性驱动的安全协议符号化模型检测方法和系统

    公开(公告)号:CN112818569B

    公开(公告)日:2021-07-02

    申请号:CN202110416348.9

    申请日:2021-04-19

    摘要: 本发明提供一种属性驱动的安全协议符号化模型检测方法、系统和介质。所述方法包括:步骤S1、分别获取所述安全协议的状态机模型和进程演算模型;步骤S2、配置所述安全协议的时序性质,所述时序性质由时序逻辑的时间算子和逻辑运算符来描述;步骤S3、基于所述状态机模型对所述时序性质进行验证,以获取存在的反例;步骤S4、基于所述反例精化所述时序性质得到安全性质,调用ProVerif安全协议验证器,基于所述进程演算模型对所述安全性质进行验证。所述方法能够提高传统模型检测在安全协议时序性验证方面的正确性,有效避免虚假反例的情况,弥补了安全协议形式化验证工具无法对时序性建模与分析的问题。

    一种形式化验证方法及系统

    公开(公告)号:CN115687166B

    公开(公告)日:2023-04-07

    申请号:CN202310009947.8

    申请日:2023-01-05

    IPC分类号: G06F11/36

    摘要: 本发明公开了一种形式化验证方法及系统,属于计算机软件设计及测试技术领域。该方法包括:在Isabelle环境中执行如下操作:构建以状态机表示的操作系统的基本执行模型;根据基本执行模型,使用元语言对所述操作系统的功能点需求进行描述,得到操作系统的需求形式化规范,并进行正确性进行验证;使用状态单子描述操作系统的数据结构及算法流程,得到操作系统的设计形式化规范,并对设计符合性进行验证;采用Simpl语言描述操作系统的源代码,以得到操作系统的源代码形式化规范;利用Simpl霍尔逻辑进行正确性及符合性进行验证。本发明具有较高的通用性,便于自动化实现,可应用于各类安全关键领域的操作系统验证。