论文题目: 安全协议形式化验证技术的研究与实现
论文类型: 博士论文
论文专业: 计算机科学与技术
作者: 李梦君
导师: 陈火旺,李舟军
关键词: 安全协议,安全性质,形式化验证,反例构造,逻辑,理论,合一化算法,安全协议
文献来源: 国防科学技术大学
发表年度: 2005
论文摘要: 协议是指两个或者两个以上的参与者为完成某一项特定任务相互约定的执行步骤和执行规则。协议的定义包含三层含义:(1)协议至少有两个参与者;(2)协议在参与者之间表现为消息交换和消息处理交替进行的一系列步骤;(3)协议的执行是为了能够完成某项任务或达成某种共识。 安全协议就是建立在密码体制基础上的—种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。 安全协议的正确性对网络应用的安全至关重要。安全协议攻击者的破坏和安全协议无穷多个会话的并发交叠运行使得安全协议运行时往往难以实现它的设计目标。形式化方法已被证明是分析和验证安全协议的有效手段,安全协议的形式化分析与验证已经成为当前形式化方法领域的一个研究热点。 本文以安全协议作为研究对象,以有效的形式化验证方法作为主要研究内容。本文的主要贡献包括: (1) 安全协议形式化建模、安全协议形式化验证方法和安全协议反例的自动构造算法。 Bruno Blanchet提出了基于Horn逻辑的安全协议模型,它是由基于线性逻辑的安全模型经过抽象解释和程序变换、并对带存在量词的公式进行Skolem化而得到的一个安全协议模型。基于进程代数的安全协议模型使用一组变换规则也可以转换为基于Horn逻辑的安全协议模型。在基于Horn逻辑的安全协议模型,没有描述消息的发送者和接受者,无法区分安全协议诚实角色与安全协议攻击者的形式化刻画。 在对基于Horn逻辑的安全协议模型进行深入分析的基础上,本文提出了基于Horn逻辑的安全协议扩展模型和基于进程代数的安全协议扩展模型。基于Bruno Blanchet的验证方法,本文提出了基于Horn逻辑的安全协议扩展模型的安全协议验证方法,从该方法的验证过程中能自动构造不满足安全性质的安全协议反例。 基于Horn逻辑的安全协议模型是对基于线性逻辑的安全模型进行抽象解释得到的模型。如果安全协议的验证过程表明基于Horn逻辑的安全协议模型满足安全性质,抽象解释保证安全协议满足安全性质;如果安全协议的验证过程表明基于Horn逻辑的安全协议模型不满足安全性质,由于抽象解释可能引入了虚假攻击,抽象解释并不保证安全协议一定不满足安全性质。自动构造不满足安全性质的安全协议反例有助于辨识虚假攻击,有助于分析安全协议出现漏洞的原因,以便对安全协议进行校正。基于Horn逻辑的安全协议扩展模型的安全协议验证过程,本文提出了不满足安全性质的安全协议反例的自动构造算法。
论文目录:
图索引
摘要
Abstract
第一章 绪论
1.1 研究背景
1.2 相关研究工作
1.2.1 类BAN逻辑方法
1.2.2 基于模型检验的方法
1.2.3 基于定理证明的方法
1.2.4 其它相关工作
1.3 研究对象与成果
1.4 本文结构
第二章 安全协议描述与安全协议模型
2.1 安全协议和安全协议攻击描述的标准方式
2.2 安全协议模型
2.2.1 基于线性逻辑的安全协议模型
2.2.2 基于进程代数的安全协议模型
2.2.3 抽象解释理论
2.2.4 基于Horn逻辑的安全协议模型
2.3 安全协议的扩展模型
2.3.1 基于进程代数的安全协议扩展模型
2.3.2 基于Horn逻辑的安全协议扩展模型
2.3.3 基于进程代数安全协议扩展模型到基于Horn逻辑安全协议扩展模型的转换
2.4 本章小结
第三章 安全协议验证与反例自动构造
3.1 保密性验证方法
3.2 不满足保密性的安全协议反例的自动生成
3.3 认证性验证方法与安全协议反例自动生成
3.4 简化的Needham-Schroeder公钥认证协议的验证与反例自动生成
3.5 一个有效的安全协议验证策略
3.6 本章小结
第四章 ACUN理论合一化问题的合一化算法
4.1 基本合一化问题和自由常数合一化问题的最一般合一化算子的求解算法
4.2 联合理论合一化问题和优化分解算法描述
4.3 一般合一化问题的合一化算法
4.3.1 带线性自由常数约束合一化问题的最一般合一化算子的求解算法
4.3.2 一般合一化问题的合一化算法
4.3.3 实例
4.4 本章小结
第五章 XOR安全协议的验证
5.1 保密性的验证方法
5.2 认证性的验证方法
5.3 验证简化的Needham-Schroeder公钥认证协议的变种协议
第六章 SPVT：—个安全协议验证工具原型
6.1 安全协议描述语言
6.2 基于进程代数安全协议扩展模型到基于Horn逻辑安全协议扩展模型的自动转换
6.3 与安全协议逻辑程序解形式不动点迭代计算和安全性质验证实现相关的几个算法
第七章 结束语
7.1 工作总结
7.2 工作展望
致谢
攻读博士学位期间发表的论文
攻读博士学位期间参与的科研项目
参考文献
发布时间: 2005-11-07
相关论文
- [1].计算机通信网安全协议的分析研究[D]. 张玉清.西安电子科技大学2000
- [2].安全协议的研究与设计[D]. 童华章.浙江大学2002
- [3].公平交换协议分析方法研究[D]. 邢育红.山东大学2005
- [4].电子商务协议形式化方法及模型检测技术的研究与应用[D]. 文静华.贵州大学2006