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

论文题目: 安全协议的形式化方法及其应用的研究

论文类型: 博士论文

论文专业: 计算机系统结构

作者: 华东明

导师: 侯紫峰

关键词: 安全协议,身份认证,密钥协商,信道,知识,信念,主体,面向主体的软件工程,可信计算,可信平台模块

文献来源: 中国科学院研究生院（计算技术研究所）

发表年度: 2005

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

论文目录:

摘要

英文摘要

目录

图目录

表目录

第一章 引言

1.1 本文的研究背景

1.1.1 安全协议的发展

1.1.2 安全协议形式化研究的发展

1.1.3 无线局域网安全

1.1.4 可信计算的发展

1.2 本文的贡献

1.3 论文的组织

第二章 基本理论

2.1 密码机制

2.1.1 对称密钥密码系统

2.1.2 公开密钥密码系统

2.1.3 对称与公开密钥密码系统的比较

2.1.4 重要公开密钥密码系统

2.2 认知逻辑

2.2.1 知识逻辑

2.2.2 信念逻辑

2.2.3 知识和信念的关系

2.3 主体

2.3.1 主体的定义

2.3.2 多主体系统

2.3.3 面向主体的软件工程

第三章 一种面向主体的安全协议形式描述语言

3.1 安全协议描述的研究现状

3.1.1 认证

3.1.2 协议安全特性

3.1.3 协议需求

3.1.4 协议目的

3.2 面向主体的形式语言

3.2.1 语法

3.2.2 语义

3.3 主体

3.4 角色

3.5 消息

3.6 信道

3.7 密钥

3.8 密码协议目的

3.8.1 身份认证协议的目的

3.8.2 密钥协商协议的目的

3.9 NSSK 协议的形式化描述

3.9.1 主体的特性和角色

3.9.2 形式化描述

3.10 与CKT5的比较

3.11 结论

第四章 一种面向主体的安全协议设计逻辑

4.1 安全协议设计的研究现状

4.1.1 安全协议设计的形式化研究

4.1.2 安全协议设计的非形式化研究

4.1.3 安全协议的设计规则

4.2 面向主体的逻辑

4.2.1 面向主体的形式语言

4.2.2 公理集

4.2.3 推理规则

4.3 安全协议的设计规则

4.3.1 细化规则

4.3.2 合成规则

4.3.3 转发规则

4.3.4 规范消息规则

4.3.5 关联规则

4.3.6 全信息规则

4.3.7 优化消息规则

4.4 安全协议的设计步骤

4.4.1 目的的确定

4.4.2 主体角色与特性的分析

4.4.3 密码机制的确定

4.4.4 目的的细化

4.4.5 初始假设的分析

4.4.6 消息的设计

4.4.7 安全协议的优化

4.5 一个新的基于对称密钥机制安全协议的设计

4.5.1 目的的确定

4.5.2 主体角色与特性的分析

4.5.3 密码机制的确定

4.5.4 目的的细化

4.5.5 初始假设的分析

4.5.6 消息的设计

4.5.7 安全协议的优化

4.6 一个新的基于公钥密码机制的安全协议的设计

4.6.1 目的的确定

4.6.2 主体角色与特性的分析

4.6.3 密码机制的确定

4.6.4 目的的细化

4.6.5 初始假设的分析

4.6.6 消息的设计

4.6.7 安全协议的优化

4.7 与BSW 逻辑的比较

4.8 结论

第五章 一种面向主体的安全协议分析逻辑

5.1 安全协议逻辑分析的研究现状

5.1.1 BAN 逻辑

5.1.2 GNY 逻辑

5.1.3 VO 逻辑

5.2 语法

5.2.1 面向主体的形式语言

5.2.2 分析安全协议的逻辑

5.3 语义

5.3.1 计算模型

5.3.2 真值语义解释

5.4 逻辑的可靠性

5.5 安全协议的目的

5.5.1 身份认证协议的目的

5.5.2 密钥协商协议的目的

5.6 安全协议的分析步骤

5.7 NSSK 协议的形式化分析

5.7.1 主体角色与特性

5.7.2 形式化描述

5.7.3 初始假设

5.7.4 形式化分析

5.8 与BAN 类型逻辑的比较

5.9 结论

第六章 WAPI 中的认证和密钥协商协议

6.1 WLAN 中安全协议的现状

6.2 WAI的系统结构

6.3 WAI的协议步骤

6.4 WAPI 和802.11i 的比较

6.5 WAI协议的形式化分析

6.5.1 主体角色与特性

6.5.2 形式化描述

6.5.3 初始假设

6.5.4 形式化分析

6.5.5 改进分析

6.6 结论

第七章 可信计算中的OIAP 协议

7.1 可信计算的研究现状

7.2 可信平台的基本特性

7.2.1 保护能力

7.2.2 完整性度量

7.2.3 完整性报告

7.2.4 可递信任

7.3 TPM 的系统结构

7.4 TPM 的授权协议

7.5 OIAP 的会话过程

7.6 OIAP 的形式化分析

7.6.1 主体角色和特性

7.6.2 形式化描述

7.6.3 初始假设

7.6.4 形式化分析

7.6.5 改进分析

7.7 结论

第八章 总结与展望

参考文献

致谢

作者简历

发布时间: 2006-12-27

相关论文

• [1].多方安全协议的形式化分析方法研究与应用[D]. 汪学明.贵州大学2008
• [2].安全协议形式化分析理论与方法[D]. 范红.中国人民解放军信息工程大学2003
• [3].安全协议分析的形式化理论与方法[D]. 王焕宝.合肥工业大学2006
• [4].可信平台模块安全性分析与应用[D]. 陈军.中国科学院研究生院（计算技术研究所）2006
• [5].基于串空间模型的安全协议形式化验证方法的研究[D]. 李谢华.上海交通大学2007
• [6].串空间理论及其在安全协议分析中的应用研究[D]. 龙士工.贵州大学2007
• [7].安全协议及其BAN逻辑分析研究[D]. 杨世平.贵州大学2007
• [8].无线网络安全协议的形式化分析方法[D]. 张帆.西安电子科技大学2007

标签：安全协议论文;  身份认证论文;  密钥协商论文;  信道论文;  知识论文;  信念论文;  主体论文;  面向主体的软件工程论文;  可信计算论文;  可信平台模块论文;