中国人民解放军军事科学院系统工程研究院张京京获国家专利权
买专利卖专利找龙图腾,真高效! 查专利查商标用IPTOP,全免费!专利年费监控用IP管家,真方便!
龙图腾网获悉中国人民解放军军事科学院系统工程研究院申请的专利一种网络协议组合形式化验证方法获国家发明授权专利权,本发明授权专利权由国家知识产权局授予,授权公告号为:CN118802337B 。
龙图腾网通过国家知识产权局官网在2025-10-28发布的发明授权授权公告中获悉:该发明授权的专利申请号/专利号为:202410837150.1,技术领域涉及:H04L9/40;该发明授权一种网络协议组合形式化验证方法是由张京京;张龙;马琳茹;黄志坚;熊欢;张建宇设计研发完成,并于2024-06-26向国家知识产权局提交的专利申请。
本一种网络协议组合形式化验证方法在说明书摘要公布了:本发明提出一种网络协议组合形式化验证方法,属于形式化验证技术领域。所述方法在网络协议设计阶段,针对网络协议所需要的信息安全性、功能安全性和密码学可靠性进行有效形式化验证,使得网络协议代码在实现前即被检测出潜在安全缺陷,且所述潜在安全缺陷中不存在虚假反例。
本发明授权一种网络协议组合形式化验证方法在权利要求书中公布了:1.一种网络协议组合形式化验证方法,其特征在于: 所述方法在网络协议设计阶段,针对网络协议所需要的信息安全性、功能安全性和密码学可靠性进行有效形式化验证,使得网络协议代码在实现前即被检测出潜在安全缺陷,且所述潜在安全缺陷中不存在虚假反例; 所述方法包括: 步骤S1、获取网络协议设计文档Doc,对网络协议设计文档Doc进行应用PI演算形式化建模,从而得到第一形式化模型,通过自动化验证器ProVerif对第一形式化模型执行针对信息安全性的自动化验证,得到具有信息安全性保障的网络协议设计文档DocS; 步骤S2、对网络协议设计文档DocS进行基于Promela语言的经典模型检测建模,从而得到第二形式化模型,通过自动化验证器SPIN对所述第二形式化模型执行针对功能安全性的自动化验证,得到反例集合π,所述反例集合π包括真实反例和虚假反例; 步骤S3、对反例集合π中的各个反例进行分类,针对不同类别的反例采用不同的验证方式执行虚假反例筛除,得到仅包括违反网络协议功能安全性的真实反例集合π’,并利用真实反例集合π’修正网络协议设计文档DocS,从而得到具有信息安全性、功能安全性保障的网络协议设计文档DocSS; 步骤S4、对网络协议设计文档DocSS进行应用Blanchet演算形式化建模,从而得到第三形式化模型,通过自动化验证器CryptoVerif对所述第三形式化模型执行针对密码学可靠性的自动化验证,得到具有信息安全性、功能安全性、密码学可靠性保障的网络协议设计文档DocSSS。
如需购买、转让、实施、许可或投资类似专利技术,可联系本专利的申请人或专利权人中国人民解放军军事科学院系统工程研究院,其通讯地址为:100141 北京市丰台区大成路13号;或者联系龙图腾网官方客服,联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。
以上内容由龙图腾AI智能生成。
1、本报告根据公开、合法渠道获得相关数据和信息,力求客观、公正,但并不保证数据的最终完整性和准确性。
2、报告中的分析和结论仅反映本公司于发布本报告当日的职业理解,仅供参考使用,不能作为本公司承担任何法律责任的依据或者凭证。

皖公网安备 34010402703815号
请提出您的宝贵建议,有机会获取IP积分或其他奖励