公开(公告)号：CN103259788B

公开(公告)日：2016-02-10

申请号：CN201310152401.4

申请日：2013-04-27

Applicant: 天津大学

Inventor： 李晓红 ,  沈岗 ,  胡静 ,  韩卓兵 ,  谢肖飞 ,  张程伟

IPC: H04L29/06

Abstract: 本发明涉及信息交换安全技术领域，为尽快发现在协议建模过程中存在的错误或者协议本身存在的缺陷，从而尽快修复安全协议的缺陷并再次验证，直至安全协议的安全属性得以满足，为此，本发明采用的技术方案是，针对安全协议的形式化建模及验证方法，包括如下步骤：1、对安全协议进行总结和分析，使用Pi演算对这些信息进行描述，获得安全协议的形式化模型；2、使用Proverif工具进行自动化验证，对验证的结果进行细化分块，并将发现的攻击路径进行图形化；3、将细化分块后的验证结果和图形化的攻击路径整合，最终得到一份完整的协议验证结果报表。本发明主要应用于信息交换安全场合。

公开(公告)号：CN105049420A

公开(公告)日：2015-11-11

申请号：CN201510351022.7

申请日：2015-06-23

Applicant: 天津大学

Inventor： 李晓红 ,  方坤丁 ,  沈岗 ,  胡静 ,  谢肖飞 ,  张程伟

IPC: H04L29/06

CPC classification number: H04L63/08

Abstract: 本发明公开了一种基于扩展的UML模型为框架的安全协议形式化验证方法，首先提取软件工程建模的关键步骤，并分析安全协议建模过程，构建基于UML的轻量级形式化框架；之后根据框架所提供的步骤，提出安全协议的形式化验证方法，逐步进行UML模型向Pi演算的自动转换，以及转换后的验证规则；即首先进行领域分析，选取合适的UML模型进行领域建模，之后利用扩展机制对UML模型进行相应扩展，丰富其对协议的描述能力。再将模型进行解析和关键词的抽取，指定匹配规则进行自动的形式化转换；最后利用集成的验证工具对模型进行安全属性的验证，找出协议模型中存在的漏洞，进行模型精化。与现有技术相比，本发明具有模型直观、建模方法简单、协议表达自然分析、利于模型检测和精化等特点。

公开(公告)号：CN103259788A

公开(公告)日：2013-08-21

申请号：CN201310152401.4

申请日：2013-04-27

Applicant: 天津大学

Inventor： 李晓红 ,  沈岗 ,  胡静 ,  韩卓兵 ,  谢肖飞 ,  张程伟

IPC: H04L29/06

Abstract: 本发明涉及信息交换安全技术领域，为尽快发现在协议建模过程中存在的错误或者协议本身存在的缺陷，从而尽快修复安全协议的缺陷并再次验证，直至安全协议的安全属性得以满足，为此，本发明采用的技术方案是，针对安全协议的形式化建模及验证方法，包括如下步骤：1、对安全协议进行总结和分析，使用Pi演算对这些信息进行描述，获得安全协议的形式化模型；2、使用Proverif工具进行自动化验证，对验证的结果进行细化分块，并将发现的攻击路径进行图形化；3、将细化分块后的验证结果和图形化的攻击路径整合，最终得到一份完整的协议验证结果报表。本发明主要应用于信息交换安全场合。