一种基于IPv6下的安全协议的形式化验证方法

摘要

本发明公开了一种基于IPv6下的安全协议的形式化验证方法，涉及Ipv6网络安全领域，具体为一种针对安全协议的形式化验证方法，包括如下步骤：1）安全协议分析阶段提取安全协议所涉及的数据；2）安全协议简化阶段对提取的安全协议数据进行简化；3）安全协议形式化建模阶段使用Pi演算语法表示安全协议数据，进行形式化建模；4）自动化工具验证阶段使用Prolog编程语言描述形式化模型，使用ProVerif工具进行自动化验证，得到ProVerif工具输出的验证结果；5）可视化结果阶段对输出验证结果进行可视化显示，显示是否满足相应的安全目标。本发明主要应用于信息交换安全场合，针对IPv6网络环境安全，以SPFP协议为例进行形式化验证，有利于提高IPv6的移动网络环境的安全性。