| 【中文题名】 | 网络安全认证协议自动分析系统 |
| 【英文题名】 | The Automatic Analysis System for Network Authentication Protocols |
| 【学科专业】 | 计算机软件与理论 |
| 【论文级别】 | 硕士论文 |
| 【投稿时间】 | 2007-10-29 |
| 【中关键词】 | 网络安全,安全协议,形式化分析,模型检测,SPIN,时态逻辑 |
| 【英关键词】 | Network Security,Cryptographic protocol,Formal method,Model Checking,SPIN,Time Logic, |
| 【分类导航】 | 工业技术>自动化技术、计算机技术>计算技术、计算机技术>计算机的应用>计算机网络>一般性问题 |
| 【论文摘要】 |
网络协议的安全性分析和验证是当今计算机安全领域中研究的重大课题。协议安全性分析包括非形式化和形式化两种方法，形式化方法是安全协议分析和验证的主要方法。我们以大量的协议形式化建模研究为基础，以网络安全认证协议为研究对象，采用模型检测技术，开发了网络安全认证协议自动分析系统。该系统功能主要是用来对认证协议进行自动建模与验证。本系统分为用户界面模块、自动分析建模模块以及自动验证模块。用户界面模块为用户提供了直观的GUI界面，以可见即可得的方式对网络认证协议进行录入，用这种方式形成系统所接收的原语言——PDL(Protocol Description Language)；自动建模分析子模块设计了认证协议的形式化分析算法，对认证协议进行建模与性质规约；自动验证子模块内嵌SPIN，对建模过程进行自动验证并返回验证结果。本系统完成了对双方公钥类型和三方对称密钥类型协议的自动建模与验证，并成功地发现了N-S、Helsinki、TMN等协议的攻击漏洞。针对状态爆炸问题，本系统采用了atomic和steps、顺序重定向、缩减随机数变量的取值范围以及偏序规约等多项优化策略，实验结果表明系统采用优化策略具有有效性。此外，系... |
| 【论文题纲】 |
|
摘要 |
3-4 |
|
ABSTRACT |
4-7 |
|
第一章 引言 |
7-11 |
|
1.1 研究背景 |
7-8 |
|
1.2 研究思路 |
8-9 |
|
1.3 论文组织 |
9-11 |
|
第二章 安全协议及其分析方法 |
11-20 |
|
2.1 安全协议 |
11-14 |
|
2.1.1 安全协议的概念 |
11-12 |
|
2.1.2 安全协议的历史 |
12-14 |
|
2.1.3 安全协议的分类 |
14 |
|
2.2 安全协议的分析方法 |
14-20 |
|
2.2.1 安全协议的非形式化分析 |
14-16 |
|
2.2.2 安全协议形式化分析 |
16-20 |
|
第三章 模型检测及相关技术 |
20-31 |
|
3.1 模型检测 |
20-21 |
|
3.2 几个重要的术语 |
21-22 |
|
3.3 模型检测工具SPIN |
22-23 |
|
3.4 模型检测工具对网络认证协议的安全性分析 |
23-25 |
|
3.4.1 Promela对认证协议的建模 |
24 |
|
3.4.2 时态逻辑 |
24-25 |
|
3.4.3 验证 |
25 |
|
3.5 利用SPIN对N-S协议进行形式化的分析 |
25-31 |
|
3.5.1 套用Promela对认证协议建模的五个步骤 |
25-30 |
|
3.5.2 利用LTL对N-S协议性质的描述 |
30 |
|
3.5.3 利用SPIN对N-S协议进行验证 |
30-31 |
|
第四章 网络安全认证协议自动分析系统的设计 |
31-52 |
|
4.1 网络安全认证协议自动分析系统概述 |
31-35 |
|
4.1.1 系统简介 |
31-34 |
|
4.1.2 系统功能 |
34-35 |
|
4.2 系统实现 |
35-52 |
|
4.2.1 整体设计 |
35-36 |
|
4.2.2 模块设计 |
36-52 |
|
第五章 系统特点及其优化策略 |
52-61 |
|
5.1 系统描述语言PDL |
52-55 |
|
5.2 效率性 |
55 |
|
5.3 自动化设计 |
55 |
|
5.4 功能可扩展性 |
55-56 |
|
5.5 用户界面设计 |
56 |
|
5.6 解决状态爆炸问题之策略 |
56-61 |
|
5.6.1 atomic和steps |
56-57 |
|
5.6.2 顺序重定向 |
57-58 |
|
5.6.3 缩减随机数变量的取值范围 |
58-59 |
|
5.6.4 偏序规约技术 |
59-61 |
|
第六章 其它相关工作 |
61-67 |
|
6.1 认证逻辑 |
61-63 |
|
6.2 FDR |
63 |
|
6.3 MURφ |
63-64 |
|
6.4 NRL |
64-65 |
|
6.5 ATHENA |
65-66 |
|
6.6 ISBELL |
66-67 |
|
第七章 结论与展望 |
67-70 |
|
7.1 结论 |
67-68 |
|
7.2 进一步工作方向 |
68-70 |
|
致谢 |
70-71 |
|
参考文献 |
71-76 |
|
攻读学位期间的研究成果 |
76 |
|
| 【DOI】 | LunWen.ID:2.2008.376503 |
