针对安全协议的形式化建模及验证方法

摘要

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

主权项

一种针对安全协议的形式化建模及验证方法，其特征是，包括如下步骤：1)、对安全协议进行总结和分析，提取出安全协议所涉及的资源、协议参与者交互过程和安全属性，使用Pi演算对这些信息进行描述，通过Pi演算来定义协议的资源、安全属性和协议参与者的交互过程，最后完成安全协议形式化模型的建模，使该安全协议形式化模型能被Proverif工具进行自动化验证；2)、根据得到的安全协议形式化模型作为输入，使用Proverif工具进行自动化验证，对验证的结果进行细化分块，并将发现的攻击路径进行图形化；3)、将细化分块后的验证结果和图形化的攻击路径整合，最终得到一份完整的协议验证结果报表，使其能帮助安全协议研究人员较快的发现并修复安全协议存在的缺陷；验证结果细化分块是根据Proverif帮助文档对验证结果的具体结构进行分析，从而得到源码经编译后的主程序，验证的属性个数，验证属性的假设和结果，如果验证结果不满足相关的安全属性，则会给出相应的反例，反例中包含对应的目标反例、攻击路径和相应的攻击跟踪，而攻击路径图形化则是先将相应的攻击轨迹转化成易于理解的信息交互过程，并将该信息交互过程以信息交互图的形式进行显示，最终生成验证结果报表。