基于串空间模型的形式化方法的扩展与应用

论文摘要

安全协议是实现信息安全的基础,是网络安全通信的核心技术,它的正确性对网络的安全起着非常重要的作用,因此其自身的安全性问题已成为安全研究的重要内容。然而怎样保证安全协议的安全性,怎样设计协议才能使之满足安全性的要求,都是安全协议研究领域需要不断探索的问题。为了分析安全协议的安全性,研究人员提出了形式化分析的方法,并利用这类方法找出了许多协议的缺陷和攻击,对安全协议的设计和分析提供了很大的帮助。但是,出于安全的考虑,现在的安全协议加入了很多新的密码运算,而一些形式化分析方法在设计时没有对这些运算进行定义,所以无法用来分析某些安全协议。因此,本文以串空间模型、诚实理想和认证测试方法为基础,对这些问题进行了深入的研究,取得了一些的成果。论文的主要研究内容有以下几个方面:首先,对串空间模型、诚实理想及认证测试方法在经典安全协议分析中的应用做了深入研究,并通过对这些协议形式化的分析发现了其中存在的安全缺陷和攻击,给出了相应的攻击方式,并以分析结果为依据对这些协议提出了具体的改进方案。其次,在对串空间模型、诚实理想及认证测试方法深入研究的基础上,指出它们对加入了签名运算和哈希运算的安全协议不能有效分析,因此要对串空间模型、诚实理想及认证测试方法进行扩展。主要扩展了串空间中自由假设、子项关系以及入侵者模型,扩展了诚实理想的相关定义和定理,扩展了认证测试方法中的分量、测试分量、转换边、被转换边、输出测试方法、输入测试方法以及主动测试方法。最后,通过对一个不可否认电子邮件传输协议的分析,验证了扩展后的诚实理想及认证测试方法的准确性。

论文目录

• 摘要
• Abstract
• 第1章 引言
• 1.1 课题的研究背景及意义
• 1.2 安全协议形式化分析方法
• 1.3 本文的主要研究内容
• 1.4 文章安排
• 第2章 形式化分析方法基础
• 2.1 基本术语
• 2.2 串和串空间
• 2.3 丛和因果次序
• 2.4 子项
• 2.5 入侵者模型
• 2.5.1 入侵者初始密钥集
• 2.5.2 入侵者串
• 2.6 协议分析举例
• 2.6.1 协议串空间
• 2.6.2 协议分析
• 2.7 本章小结
• 第3章 串空间理论的发展
• 3.1 诚实与理想
• 3.2 认证测试理论
• 3.2.1 基本概念
• 3.2.2 认证测试方法分类
• 3.2.3 认证测试方法步骤
• 3.3 改进型Otway-Rees 协议分析
• 3.3.1 改进后的Otway-Rees 协议
• 3.3.2 改进型Otway-Rees 协议的串空间模型分析
• 3.4 本章小结
• 第4章 串空间理论的扩展
• 4.1 串空间模型扩展的必要性
• 4.2 串空间模型扩展
• 4.2.1 消息项扩展
• 4.2.2 自由假设扩展
• 4.2.3 子项关系扩展
• 4.2.4 攻击者模型扩展
• 4.3 诚实与理想的扩展
• 4.4 认证测试理论
• 4.4.1 基本概念扩展
• 4.4.2 认证测试方法的扩展
• 4.4.3 认证测试规则的扩展
• 4.5 本章小结
• 第5章 应用实例分析
• 5.1 一种电子邮件传输的非否认协议
• 5.1.1 协议及协议中的假设与说明
• 5.1.2 协议的仲裁
• 5.1.3 协议的串空间模型
• 5.2 用扩展后的认证测试方法分析协议
• 5.2.1 协议的验证
• 5.3 用扩展后的诚实理想分析协议
• 5.4 本章小结
• 总结与展望
• 参考文献
• 致谢
• 攻读学位期间取得学术成果