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

关于密码协议的形式化分析方法的研究

作　者: 李晨
导　师: 许春香
学　校: 电子科技大学
专　业: 信息与通信工程
关键词: 密码协议密码学技术形式化方法
分类号: TP393.08
类　型: 硕士论文
年　份: 2010年
下　载: 37次
引　用: 0次
阅　读: 论文下载

内容摘要

随着信息技术的快速发展和广泛应用,诸如电子商务这类需要高度安全性的应用逐渐普及,建立安全信道的重要性可想而知。在网络这个特殊的大环境里,两个互相不认识的主体如果想要达成某种通信目的,必须要在密码技术保障的前提下进行。虽然现阶段对密码协议的分析方法的研究已经有了很多观点,但是还没有一种被广泛认同的可以作为工业标准的方法,所以对于密码协议的形式化分析方法仍然是一个开放性的热点问题,而且具有重要的理论意义。本文首先介绍了密码学领域的一些基本概念,密码协议的分类,以及在密码协议中需要用到的一些重要的密码学技术:保密性,数据完整性,抗抵赖性以及消息认证性。为了使得分析方法的设计更加具有针对性,本文假设所讨论的协议都是在底层密码技术安全的前提下进行的;然后,本文通过分析密码协议形式化方法的主流观点,总结出这些观点存在的缺陷。接着通过对一些经典的攻击方式的分析,引出本文的主题,即对密码协议安全性分析的形式化方法,提出这套方法的依据在于Bellare和Rogaway对于密码协议安全的公式化定义,以及作者在学习过程中总结出的一些密码协议的设计原则。这个形式化方法分为五个模块,首先对协议进行前四个模块的检验,然后在第五个模块中对协议进行安全性证明。本文通过对大量相关文献的研究,深深的体会到对于密码协议安全性证明的困难性。所以本文所采用的证明方式基于不同于传统密码学证明的逻辑方式,并不是将攻击者攻破协议的行为归约到攻破数学难题上,而是归约到对已知假设的否定上,每个步骤在逻辑上都严密合理。接下来利用这套方法对一些工业协议例如SSH,Kerberos以及STS协议进行分析;最后,对密码协议的研究做出总结和展望。

全文目录

摘要  4-5
ABSTRACT  5-8
第一章绪论  8-13
  1.1 密码协议相关的密码技术  8-9
  1.2 密码协议简介  9-10
    1.2.1 密码协议的概念  9
    1.2.2 密码协议的历史  9
    1.2.3 对于密码协议的直观描述  9-10
  1.3 国内外研究现状  10-11
  1.4 论文主要工作、创新点及组织结构  11-13
    1.4.1 论文主要工作和创新点  11
    1.4.2 论文组织结构  11-13
第二章密码协议的常见缺陷以及相应的攻击  13-23
  2.1 攻击者的模型  13-14
  2.2 分析密码协议的主要困难  14
  2.3 对于密码协议的常见攻击  14-22
    2.3.1 重放攻击  15-18
    2.3.2 中间人攻击  18-20
    2.3.3 平行会话攻击  20-21
    2.3.4 类型攻击  21-22
    2.3.5 攻击方法难以穷尽  22
  2.4 本章小结  22-23
第三章密码协议形式化分析方法  23-35
  3.1 计算观点  23-26
    3.1.1 相互认证的目标：匹配对话  23
    3.1.2 相互认证成功的定义  23-24
    3.1.3 MAP1 协议以及其安全性证明  24-26
    3.1.4 对计算观点的分析  26
  3.2 逻辑符号观点  26-33
    3.2.1 BAN 逻辑  26-27
    3.2.2 BAN 逻辑框架介绍  27-29
    3.2.3 BAN 逻辑分析举例  29-32
    3.2.4 BAN 逻辑的缺陷以及提出新的形式化方法的必要性  32-33
  3.3 状态探查观点  33
  3.4 对这三种观点的理解  33-34
  3.5 本章小结  34-35
第四章一种新的密码协议形式化分析方法  35-56
  4.1 对密码协议的非形式化分析方法  35-39
    4.1.1 非形式化分析方法简介  35-37
    4.1.2 提出非形式化分析方法的原因  37
    4.1.3 非形式化分析方法的作用  37-39
  4.2 形式化分析方法的基本框架  39
  4.3 系统各子模块的功能说明  39-55
    4.3.1 模块1：对协议进行符号化  39-40
    4.3.2 模块2：对消息本身进行的源认证  40-42
    4.3.3 模块3：新鲜性标识符对于各个主体的关联验证  42-44
    4.3.4 模块4：进行Wenbo Mao 规则检验  44-46
    4.3.5 模块5：对协议进行安全性证明  46-55
  4.4 本章小结  55-56
第五章新形式化分析方法的实践应用  56-71
  5.1 形式化分析方法的应用  56
  5.2 对SSH 协议的分析  56-59
    5.2.1 SSH 协议简介  56
    5.2.2 SSH 协议的整体架构  56-57
    5.2.3 SSH 传输层协议  57-58
    5.2.4 对SSH 传输层协议的安全性进行安全性分析  58-59
  5.3 对Kerberos 协议的分析  59-63
    5.3.1 Kerberos 协议简介  59
    5.3.2 Kerberos 协议的总体结构  59-60
    5.3.3 认证服务交换  60
    5.3.4 与TGS 运行协议  60-61
    5.3.5 与应用服务器运行协议  61
    5.3.6 对Kerberos 协议的安全性进行形式化分析  61-63
  5.4 对工作站-工作站（STS）协议的分析  63-69
    5.4.1 STS 协议简介  63-65
    5.4.2 对STS 协议的安全性进行形式化分析  65-69
  5.5 本文提出的形式化方法的优缺点  69-70
  5.6 本章小结  70-71
第六章总结和展望  71-72
致谢  72-73
参考文献  73-76

相似论文

Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
卡箱式高速公路联网收费通行IC卡管理系统的设计与实现,TP311.52
基于Z规格的软件缺陷形式化方法,TP311.53
基于Hoare逻辑的软件形式化验证技术研究,TP311.52
基于形式化方法的统一软件模型及其应用,TP311.52
教育信息网中的统一认证授权平台研究与实现,TP393.08
面向软件复用的组件形式化开发,TP311.52
基于串空间模型的形式化方法的扩展与应用,TP393.08
密码学算法安全性研究,TN918.1
委托代理电子投票协议研究,TP399-C2
UML建模的形式化方法研究和应用,TP311.52
电子商务安全协议的一种形式化分析方法,TP393.08
形式化方法的理论及其影响,B812
基于行为时序逻辑模型检测的研究与应用,TP311.52
基于SPIN/Promela的UML模型验证工具设计与实现,TP311.52
Petri网在密码协议建模和分析中的应用,TN918.1
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
THP事务协调协议的形式化分析与验证,TP311.52
基于PVS的自稳定算法形式化分析,TP338.8
数字签名应用研究,TN918.2