安全协议的Athena方法研究

论文摘要

Athena方法是安全协议分析领域中的一种新的形式化分析方法。本文首先对其进行了深入分析,然后针对安全协议形式化分析领域中的两个重要问题——类型缺陷攻击问题、组合协议猜测攻击问题及Athena方法在分析这两个问题中遇到的困难,对该方法进行了扩展。取得的主要成果如下:(1)对Athena方法进行了深入研究,分析了Athena方法对串空间模型所做的扩展,对Athena方法的逻辑和验证算法进行了深入分析,并通过实验说明其分析协议的有效性和高效性。(2) Athena方法建立在强类型抽象假设的基础上,但在协议的实际执行过程中,这样的假设并不现实。因此本文去除这一假设,对原有的Athena方法进行了相应的扩展,引入了组合项,增加了攻击者强制类型转换的能力,同时扩展了Athena方法中的内在项、目标及目标绑定等概念,并对相关内容进行修改。用扩展后的方法对NSL协议进行分析,发现了一处在APV中无法发现的类型缺陷攻击。(3)针对组合协议猜测攻击问题,对Athena方法进行扩展。引入了串空间模型中理想的概念,并在此基础上提出了一种跨协议影响的关系,以描述从协议对主协议的影响,增加了攻击者猜测密钥的能力,提出了猜测验证目标及猜测验证绑定的概念,对Athena方法中的状态、推理规则、后继状态函数等进行了扩展。用扩展后的Athena方法对一个认证协议实例和EKE协议的组合运行问题进行了分析,发现了认证协议实例在组合协议环境下存在的一处猜测攻击。

论文目录

• 摘要
• Abstract
• 第一章 概述
• 1.1 研究背景
• 1.2 国内外研究现状
• 1.2.1 安全协议形式化分析方法
• 1.2.2 相关研究工作
• 1.3 研究内容及意义
• 1.4 论文安排
• 第二章 Athena 方法分析研究
• 2.1 串空间模型基础
• 2.1.1 消息项及消息间的关系
• 2.1.2 串空间的构成
• 2.1.3 丛与结点的因果依赖关系
• 2.1.4 项、加密与攻击者串
• 2.2 串空间模型的扩充
• 2.3 Athena 的逻辑
• 2.3.1 语法
• 2.3.2 语义
• 2.3.3 安全性质描述
• 2.4 验证算法
• 2.4.1 算法的本质
• 2.4.2 推理规则
• 2.4.3 后继状态函数
• 2.4.4 消减规则
• 2.4.5 搜索算法
• 2.6 小结
• 第三章 APV 的分析及应用
• 3.1 APV 的协议建模方法
• 3.2 基于APV 的Otway-Rees 协议建模与分析
• 3.2.1 协议原型
• 3.2.2 协议的 APV 规格
• 3.2.3 实验结果
• 3.3 基于APV 的Woo-Lam 单向认证协议建模与分析
• 3.3.1 协议原型
• 3.3.2 协议的 APV 规格
• 3.3.3 实验结果
• 3.4 其他实验结果
• 3.5 小结
• 第四章 针对类型缺陷攻击的 Athena 方法扩展
• 4.1 问题提出
• 4.2 类型缺陷攻击的定义
• 4.3 串空间模型的扩展
• 4.3.1 消息项的扩展
• 4.3.2 攻击者模型的扩展
• 4.4 Athena 方法的扩展
• 4.4.1 内在项关系的修改
• 4.4.2 目标以及目标绑定的扩展
• 4.4.3 后续状态函数的扩展
• 4.5 实例分析
• 4.6 小结
• 第五章 针对组合协议猜测攻击的 Athena 方法扩展
• 5.1 问题提出
• 5.2 组合协议猜测攻击的定义
• 5.3 串空间模型的扩展
• 5.3.1 混合串空间
• 5.3.2 消息项扩展
• 5.3.3 攻击者模型的扩展
• 5.3.4 理想及其生成算法
• 5.4 Athena 方法的扩展
• 5.4.1 状态表示法的扩展
• 5.4.2 推理规则的扩展
• 5.4.3 后继状态函数的扩展
• 5.4.4 算法伪代码
• 5.5 实例分析
• 5.6 小结
• 第六章 结束语
• 参考文献
• 致谢
• 攻读硕士学位期间发表或录用的论文