安全协议攻击序列重构技术研究

论文摘要

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

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景及意义
• 1.2 安全协议基本概念
• 1.2.1 安全协议及其安全性质
• 1.2.2 安全协议攻击的分类
• 1.2.3 安全协议攻击描述
• 1.2.4 安全协议攻击实例
• 1.3 安全协议自动化验证中攻击重构技术现状
• 1.3.1 基于模型检测的方法
• 1.3.2 基于定理证明的方法
• 1.3.3 基于一阶逻辑的方法
• 1.3.4 其它方法
• 1.3.5 总结
• 1.4 论文组织结构
• 第二章 适于攻击重构的安全协议模型
• 2.1 Blanchet安全协议模型
• 2.1.1 Blanchet安全协议模型
• 2.1.2 SPVT安全协议模型
• 2.2 改进的安全协议模型
• 2.2.1 基本假设
• 2.2.2 安全协议进程代数模型
• 2.2.3 安全协议一阶逻辑模型
• 2.2.4 安全协议进程代数模型到一阶逻辑模型的转换
• 2.3 本章小结
• 第三章 安全协议一阶逻辑模型中攻击重构机制
• 3.1 机制总体设计思想
• 3.2 规则属性及规则分类
• 3.2.1 密码学函数定义
• 3.2.2 协议规范规则
• 3.2.3 攻击者知识及能力规则
• 3.3 动作及动作属性
• 3.4 逻辑推导记录
• 3.4.1 设计思想
• 3.4.2 逻辑推导记录机制
• 3.5 逻辑推导的解释
• 3.5.1 消息项映射函数
• 3.5.2 操作置换规则
• 3.6 攻击重构策略
• 3.7 合理性证明
• 3.8 应用举例
• 3.9 本章小结
• 第四章 攻击重构关键算法设计
• 4.1 总体设计思想
• 4.2 安全性验证算法中推导信息的记录
• 4.2.1 规则正规合一化算法
• 4.2.2 规则蕴含算法
• 4.2.3 规则化简算法
• 4.2.4 不动点计算和逻辑推导算法
• 4.3 攻击重构算法
• 4.3.1 推导过程重构算法
• 4.3.2 相关变量统一算法
• 4.3.3 攻击过程输出算法
• 4.4 本章小结
• 第五章 协议验证原型系统设计与实现
• 5.1 需求分析
• 5.1.1 功能分析
• 5.1.2 性能分析
• 5.2 设计思路及体系结构
• 5.2.1 设计思路
• 5.2.2 体系结构
• 5.2.3 工作流程
• 5.2.4 数据结构定义
• 5.3 用户界面部分
• 5.3.1 基本功能
• 5.3.2 组成结构
• 5.3.3 功能实现
• 5.4 协议编译部分
• 5.4.1 基本功能
• 5.4.2 组成结构
• 5.4.3 功能实现
• 5.5 不动点计算和逻辑推导部分
• 5.5.1 基本功能
• 5.5.2 组成结构
• 5.5.3 功能实现
• 5.6 攻击重构部分
• 5.6.1 基本功能
• 5.6.2 组成结构
• 5.6.3 功能实现
• 5.7 实验结果
• 5.8 本章小结
• 第六章 结束语
• 6.1 论文工作总结
• 6.2 下一步工作展望
• 参考文献
• 作者简历 攻读硕士学位期间完成的主要工作
• 致谢