论文摘要
近年来,安全协议形式化分析及自动化验证技术越来越受到人们的关注,但是对基于安全协议形式化分析理论的攻击过程重构技术的研究还处于初始阶段,而攻击重构技术不仅能够验证协议形式化方法的有效性,而且能够为攻击敌方网络提供参考方法。本文基于安全协议进程代数理论和一阶逻辑理论对安全协议攻击重构技术进行了深入研究,本文的主要工作包括以下几个方面:1.深入分析了针对安全协议的不同攻击方法,对各种攻击方法的危害性进行了分析比较。研究了安全协议形式化分析方法中的攻击重构技术,对各种技术进行了优缺点比较;2.在分析比较各种攻击方法和形式化方法的基础上,采用进程代数理论和一阶逻辑理论对安全协议进行建模,通过加入消息收发对象信息、会话标识信息以及协议步骤信息,提出了适于对攻击过程进行重构的安全协议模型。给出安全协议进程代数语法语义和安全协议一阶逻辑语法语义,同时给出两套语法语义之间的转换规则,并证明转换规则的推导一致性;3.为实现协议攻击序列的自动构造,基于一阶逻辑提出了攻击重构机制,对逻辑推导中的各种情况进行了深入讨论。通过规则分类策略,将逻辑推导中出现的规则按照属性的不同进行了分类;通过合一化分类策略,将推导中的合一化运算与攻击者的攻击行为联系起来;通过推导信息记录策略,对规则的分类信息、合一化分类信息、消息项的收发对象以及会话标识符进行记录;通过逻辑推导解释策略将一阶逻辑中的推导步骤解释为攻击者对协议安全性质的攻击过程。最后结合NS公钥协议详细阐述了各种策略的具体应用;4.根据提出的安全协议模型和攻击重构策略,设计了攻击重构算法,改进了规则合一化、蕴含检验和规则化简算法,各种算法相互配合能够实现攻击过程的重构;5.基于验证和攻击重构算法,设计开发出协议验证原型工具ASPV-AR,详细介绍了原型系统的体系结构和各模块的功能及接口。最后,给出ASPV-AR的性能测试。