基于多反例的安全协议漏洞挖掘方法

摘要

本发明公开了基于多反例的安全协议漏洞挖掘方法，包括以下步骤：S1、使用promela语言对需要验证的安全协议进行建模，并保存为.pml文件格式；S2、规约协议的安全性质，并以LTL形式表达；S3、通过查找反例的方式对安全协议进行验证；S4、消除相似反例：使用编辑距离法度量反例的权重序列，消除相似反例；随后使用对比攻击路径图的方法进一步消除相似反例；S5、使用统计方法对步骤S4剩余的反例集合进行处理。本发明在模型检测阶段引入权重概念，进一步对比反例中的权重序列，消除相似反例；在反例分析阶段利用统计方法来对大量冗长反例进行处理，使反例的分析过程更加自动化，提高安全协议分析的准确性和效率。