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

安全协议的形式化方法及其应用的研究

作　者: 华东明
导　师: 侯紫峰
学　校: 中国科学院研究生院（计算技术研究所）
专　业: 计算机系统结构
关键词: 安全协议身份认证密钥协商信道知识信念主体面向主体的软件工程可信计算可信平台模块
分类号: TP393.08
类　型: 博士论文
年　份: 2005年
下　载: 906次
引　用: 6次
阅　读: 论文下载

内容摘要

网络可以使人们在任意地点和任意时间、以任意方式访问共享网络资源,同时随着网络的迅猛发展和应用领域的不断扩大,网络面临着越来越多的安全威胁,为了保证网络的安全运行和资源的有效利用,作为网络安全服务基础的安全协议越来越受到重视,但由于安全协议本身的复杂性、相关理论和工程技术的不成熟以及人们认识能力的局限性,使得在现有安全协议中不可避免地存在着安全缺陷。为了设计出更可靠的安全协议,形式化方法成为描述、设计和分析安全协议的有效工具,并得到相当深入的研究、并获到比较广泛和成功的运用。目前,在无线局域网的安全协议中不同程度地存在着安全缺陷,其中在802.11中的安全机制存在着致命的安全漏洞。近几年来,为了基于可信平台特性建立未来具有高安全性的计算机系统,可信计算组提出了在计算机的硬件平台上引入安全芯片架构和通过提供硬件的安全特性来提高系统安全性的安全体系结构。本论文深入研究了安全协议面向主体的形式描述、设计和分析,并运用本论文中提出的安全协议面向主体的形式描述、设计和分析方法,分别研究了无线局域网中WAPI的认证和密钥协商协议以及可信计算中的OIAP协议。本论文的贡献表现在:(1)在安全协议面向主体的逻辑描述语言的研究中,将主体遵从安全协议相互通信的过程看成主体通过通信行为传递拥有、知识和信念以及主体的拥有、知识和信念随时序单调增加的过程;基于拥有、知识、信念、发送、接收和时序建立了描述安全协议的形式语言;给出它的Kripke语义模型和真值语义解释;在安全协议元素的形式化描述中,运用面向主体的方法描述了参与安全协议运行的主体的特性及其角色,比较清晰、准确和全面地描述了安全协议中消息的可辨认性和新鲜性、密钥的特性以及认证与密钥分发的目的,根据提供的不同安全服务,将安全协议中的密码机制抽象为不同信道;运用该形式语言以面向主体的方法对Needham-Schroeder对称密钥协议进行了形式化描述;将该语言与CKT5对安全协议逻辑描述的表达能力进行了比较。(2)在安全协议面向主体的设计逻辑的研究中,创建了基于面向主体以及知识和信念逻辑的安全协议设计逻辑,给出了关于知识和信念、安全主体、权威主体、发送、接收、拥有、消息的可辨认性、消息的新鲜性、消息源和主体身份认证、密钥验证和密钥协商的公理,给出了三段论推理规则;根据提供的不同安全服务,将安全协议中的密码机制抽象为不同信道,形式化地描述了细化规则、合成规则、转发规则、规范消息规则、关联规则、全信息规则和优化消息规则7个安全协议设计规则;将安全协议的设计分为安全协议目的的确定、分析主体的角色及其特性、密码机制的确定、安全协议目的的细化、分析安全协议设计的初始假设、运用规范消息、关联和全信息规则设计单个消息、根据优化消息优化安全协议7个步骤;根据给出的设计逻辑、设计规则和设计步骤形式

全文目录

摘要  4-6
英文摘要  6-10
目录  10-16
图目录  16-18
表目录  18-20
第一章引言  20-32
  1.1 本文的研究背景  20-29
    1.1.1 安全协议的发展  20-23
    1.1.2 安全协议形式化研究的发展  23-26
    1.1.3 无线局域网安全  26-28
    1.1.4 可信计算的发展  28-29
  1.2 本文的贡献  29-30
  1.3 论文的组织  30-32
第二章基本理论  32-46
  2.1 密码机制  32-39
    2.1.1 对称密钥密码系统  32-34
    2.1.2 公开密钥密码系统  34-36
    2.1.3 对称与公开密钥密码系统的比较  36
    2.1.4 重要公开密钥密码系统  36-39
  2.2 认知逻辑  39-42
    2.2.1 知识逻辑  39-41
    2.2.2 信念逻辑  41-42
    2.2.3 知识和信念的关系  42
  2.3 主体  42-46
    2.3.1 主体的定义  42-43
    2.3.2 多主体系统  43
    2.3.3 面向主体的软件工程  43-46
第三章一种面向主体的安全协议形式描述语言  46-62
  3.1 安全协议描述的研究现状  46-49
    3.1.1 认证  46-47
    3.1.2 协议安全特性  47
    3.1.3 协议需求  47
    3.1.4 协议目的  47-49
  3.2 面向主体的形式语言  49-54
    3.2.1 语法  49-51
    3.2.2 语义  51-54
  3.3 主体  54
  3.4 角色  54-55
  3.5 消息  55-56
  3.6 信道  56-57
  3.7 密钥  57-58
  3.8 密码协议目的  58
    3.8.1 身份认证协议的目的  58
    3.8.2 密钥协商协议的目的  58
  3.9 NSSK 协议的形式化描述  58-60
    3.9.1 主体的特性和角色  59
    3.9.2 形式化描述  59-60
  3.10 与CKT5的比较  60-61
  3.11 结论  61-62
第四章一种面向主体的安全协议设计逻辑  62-88
  4.1 安全协议设计的研究现状  62-67
    4.1.1 安全协议设计的形式化研究  62-64
    4.1.2 安全协议设计的非形式化研究  64-66
    4.1.3 安全协议的设计规则  66-67
  4.2 面向主体的逻辑  67-72
    4.2.1 面向主体的形式语言  67-68
    4.2.2 公理集  68-72
    4.2.3 推理规则  72
  4.3 安全协议的设计规则  72-75
    4.3.1 细化规则  73
    4.3.2 合成规则  73
    4.3.3 转发规则  73
    4.3.4 规范消息规则  73-74
    4.3.5 关联规则  74
    4.3.6 全信息规则  74
    4.3.7 优化消息规则  74-75
  4.4 安全协议的设计步骤  75-76
    4.4.1 目的的确定  75
    4.4.2 主体角色与特性的分析  75
    4.4.3 密码机制的确定  75
    4.4.4 目的的细化  75
    4.4.5 初始假设的分析  75-76
    4.4.6 消息的设计  76
    4.4.7 安全协议的优化  76
  4.5 一个新的基于对称密钥机制安全协议的设计  76-81
    4.5.1 目的的确定  76
    4.5.2 主体角色与特性的分析  76
    4.5.3 密码机制的确定  76
    4.5.4 目的的细化  76-79
    4.5.5 初始假设的分析  79-80
    4.5.6 消息的设计  80-81
    4.5.7 安全协议的优化  81
  4.6 一个新的基于公钥密码机制的安全协议的设计  81-86
    4.6.1 目的的确定  81
    4.6.2 主体角色与特性的分析  81
    4.6.3 密码机制的确定  81
    4.6.4 目的的细化  81-84
    4.6.5 初始假设的分析  84-85
    4.6.6 消息的设计  85-86
    4.6.7 安全协议的优化  86
  4.7 与BSW 逻辑的比较  86-87
  4.8 结论  87-88
第五章一种面向主体的安全协议分析逻辑  88-114
  5.1 安全协议逻辑分析的研究现状  88-92
    5.1.1 BAN 逻辑  88-91
    5.1.2 GNY 逻辑  91
    5.1.3 VO 逻辑  91-92
  5.2 语法  92-102
    5.2.1 面向主体的形式语言  92-95
    5.2.2 分析安全协议的逻辑  95-102
  5.3 语义  102-106
    5.3.1 计算模型  102-104
    5.3.2 真值语义解释  104-106
  5.4 逻辑的可靠性  106-107
  5.5 安全协议的目的  107-108
    5.5.1 身份认证协议的目的  107
    5.5.2 密钥协商协议的目的  107-108
  5.6 安全协议的分析步骤  108
  5.7 NSSK 协议的形式化分析  108-111
    5.7.1 主体角色与特性  108
    5.7.2 形式化描述  108-109
    5.7.3 初始假设  109-110
    5.7.4 形式化分析  110-111
  5.8 与BAN 类型逻辑的比较  111-112
  5.9 结论  112-114
第六章 WAPI 中的认证和密钥协商协议  114-136
  6.1 WLAN 中安全协议的现状  114-118
  6.2 WAI的系统结构  118-119
  6.3 WAI的协议步骤  119-120
  6.4 WAPI 和802.11i 的比较  120-124
  6.5 WAI协议的形式化分析  124-134
    6.5.1 主体角色与特性  124
    6.5.2 形式化描述  124-127
    6.5.3 初始假设  127-128
    6.5.4 形式化分析  128-133
    6.5.5 改进分析  133-134
  6.6 结论  134-136
第七章可信计算中的OIAP 协议  136-150
  7.1 可信计算的研究现状  136-137
  7.2 可信平台的基本特性  137-139
    7.2.1 保护能力  137
    7.2.2 完整性度量  137
    7.2.3 完整性报告  137-138
    7.2.4 可递信任  138-139
  7.3 TPM 的系统结构  139-143
  7.4 TPM 的授权协议  143-144
  7.5 OIAP 的会话过程  144
  7.6 OIAP 的形式化分析  144-148
    7.6.1 主体角色和特性  144-145
    7.6.2 形式化描述  145-146
    7.6.3 初始假设  146
    7.6.4 形式化分析  146-148
    7.6.5 改进分析  148
  7.7 结论  148-150
第八章总结与展望  150-154
参考文献  154-162
致谢  162-164
作者简历  164

安全协议的形式化方法及其应用的研究

内容摘要

全文目录

相似论文