| 【中文题名】 | 安全协议形式化验证方法的研究 |
| 【英文题名】 | |
| 【学科专业】 | 计算机应用技术 |
| 【论文级别】 | 硕士论文 |
| 【投稿时间】 | 2007-8-29 |
| 【中关键词】 | 安全协议,形式化方法,串空间模型,理想,秘密性, |
| 【英关键词】 | security protocol,formal method,strand space,ideal,secrecy, |
| 【分类导航】 | 工业技术>自动化技术、计算机技术>计算技术、计算机技术>计算机的应用>> |
| 【论文摘要】 |
安全协议也称密码协议，是建立在密码体制基础上的高互通的消息交换协议，它运行在计算机通信网或分布式系统中，其目的是在网络环境中提供各种安全服务。安全协议是构建安全网络环境的基石，它的正确性对于网络安全极其关键。然而由于安全协议的执行具有高度不确定性，以致有些安全协议往往不如它们的设计者所期望的那样安全，存在很多缺陷和漏洞。
纵观国内外的研究成果，安全协议的安全性分析是揭示安全协议缺陷和漏洞的重要途径，分析方法从最初的非形式化的攻击检验，到多种形式化分析方法并存，已经出现了百家争鸣的景况。
本课题以基于串空间模型安全协议的形式化验证方法为主要研究内容，从理论和实践两个层面上研究了安全协议形式化验证的相关技术。主要工作包括：
●在深刻理解安全协议基本概念的基础上，从安全协议形式化验证方法所应用的技术手段、技术特点入手，对安全协议的形式化验证方法进行了总结和分类。并对安全协议形式化验证若干热点研究方向进行了归纳和展望。
●在归纳现有串空间模型理论的基础上，深入分析了串空间模型内认证协议正确性的含义，并提出了基于串空间模型安全协议形式化验证的三种典型方法。最后，还指出串空间模型... |
| 【论文题纲】 |
|
摘要 |
4-5 |
|
ABSTRACT |
5-6 |
|
1 前言 |
6-9 |
|
1.1 课题研究背景和意义 |
6-7 |
|
1.2 研究的目标、内容和方案 |
7-8 |
|
1.3 本文的结构安排 |
8-9 |
|
2 安全协议及其形式化分析 |
9-21 |
|
2.1 安全协议 |
9-12 |
|
2.1.1 协议与安全协议 |
9 |
|
2.1.2 安全协议的安全属性 |
9-11 |
|
2.1.3 安全协议的缺陷 |
11-12 |
|
2.2 安全协议的形式化分析 |
12-21 |
|
2.2.1 形式化方法概述 |
12 |
|
2.2.2 形式化分析涵义 |
12-13 |
|
2.2.3 安全协议形式化分析思路 |
13-14 |
|
2.2.4 基本假设 |
14-15 |
|
2.2.5 形式化分析方法的现状 |
15-19 |
|
2.2.6 安全协议形式化分析的热点研究方向和发展趋势 |
19-21 |
|
3 串空间模型理论及其协议分析方法 |
21-33 |
|
3.1 串空间模型理论的基础知识 |
21-27 |
|
3.1.1 消息空间和代数假定 |
21-22 |
|
3.1.2 基本概念 |
22-23 |
|
3.1.3 丛和结点关系 |
23-25 |
|
3.1.4 攻击者描述 |
25-26 |
|
3.1.5 协议正确性的含义 |
26-27 |
|
3.1.6 协议描述 |
27 |
|
3.2 理想与诚实理论 |
27-28 |
|
3.2.1 理想 |
27 |
|
3.2.2 诚实 |
27-28 |
|
3.3 认证测试理论 |
28-31 |
|
3.3.1 基本概念 |
29-30 |
|
3.3.2 三种重要的认证测试方法 |
30 |
|
3.3.3 认证测试规则 |
30-31 |
|
3.4 基于串空间模型3种典型的安全协议形式化分析方法 |
31-33 |
|
3.4.1 基于极小元理论的串空间方法 |
31 |
|
3.4.2 基于理想与诚实理论的串空间方法 |
31-32 |
|
3.4.3 基于认证测试理论的串空间方法 |
32-33 |
|
4 基于串空间模型几个典型协议的形式化分析 |
33-62 |
|
4.1 基于极小元理论 NSL协议的形式化分析 |
33-41 |
|
4.1.1 NSL 协议串空间 |
33-34 |
|
4.1.2 NSL 协议响应者的认证性 |
34-38 |
|
4.1.3 NS 协议的脆弱性分析 |
38 |
|
4.1.4 NSL 协议响应者的秘密性 |
38-40 |
|
4.1.5 NSL 协议发起者的秘密性 |
40 |
|
4.1.6 NSL 协议发起者的认证性 |
40-41 |
|
4.2 基于理想与诚实理论 Yahalom 改进协议的形式化分析 |
41-49 |
|
4.2.1 Yahalom 协议串空间 |
42-44 |
|
4.2.2 秘密性 |
44-45 |
|
4.2.3 认证性分析 |
45-49 |
|
4.3 基于认证测试理论 X.509 三消息改进协议的形式化分析 |
49-53 |
|
4.3.1 X.509 三消息改进协议的串空间 |
50 |
|
4.3.2 发起者对响应者的认证性 |
50-52 |
|
4.3.3 响应者对发起者的认证性 |
52-53 |
|
4.4 基于认证测试理论 Yahalom 改进协议的形式化分析 |
53-57 |
|
4.5 基于认证测试理论 NSL 协议的形式化分析 |
57-60 |
|
4.6 方法总结与对比分析 |
60-62 |
|
4.6.1 与非串空间方法的对比分析 |
60-61 |
|
4.6.2 三种串空间形式化方法的特点与异同 |
61-62 |
|
5 总结与展望 |
62-64 |
|
5.1 研究总结 |
62-63 |
|
5.2 进一步的工作 |
63-64 |
|
致谢 |
64-65 |
|
参考文献 |
65-68 |
|
附录 |
68-69 |
|
| 【DOI】 | LunWen.ID:2.2008.375821 |
