学位论文 > 优秀研究生学位论文题录展示

安全协议的Athena方法研究

作　者: 李超
导　师: 董荣胜
学　校: 桂林电子科技大学
专　业: 计算机应用技术
关键词: 形式化分析串空间模型 Athena 类型缺陷攻击组合协议猜测攻击
分类号: TP393.04
类　型: 硕士论文
年　份: 2007年
下　载: 57次
引　用: 0次
阅　读: 论文下载

内容摘要

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

全文目录

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

安全协议的Athena方法研究

内容摘要

全文目录

相似论文