《毕业论文：Research and Application on Model Checking of Security Protocol》由会员分享，可在线阅读，更多相关《毕业论文：Research and Application on Model Checking of Security Protocol（28页珍藏版）》请在金锄头文库上搜索。
1、 I Research and Application on Model Checking of Security ProtocolAbstract: The security of security protocols is the foundation of the network security. Presently the analysis of security of security protocols using the formal method has become a hotspot of research. This dissertation makes a resea
2、rch on the theory and technique of the formal analysis of the security protocols and focuses on the running-mode analysis method based on the model checking technology. Furthermore this method is used to analyze and design practical security protocols. The researches are summarized as follows:The ba
3、ckground and significance of the cryptographic protocol security analysis are introduced, and we also summarize the three classifications of the formal analysis methods.We introduce the running-mode analysis based on the two-party security protocol, and found it will be simplified the running modes
4、from seven to five. We introduce the running-mode analysis based on the three-party security protocol including only one server which acts as the trusted third party. Then we find there are four form running modes when the protocols run.Furthermore, the running-mode analysis based on the two-party s
5、ecurity protocol is used to analyze on public-key protocol of Needham-Schroeder (NS). The properties we choose may not adapt to the model, we need to change the models behavior or the verification parameter.Finally, we compare the model checking with other formal analysis methods and give the conclu
6、sions.Keywords: security protocol, model checking, formal analysis, running-mode analysis II 安全协议模型检测技术的研究与应用摘要：安全协议的安全性是网络安全的重要基础，运用形式化方法分析安全协议的安全性己成为目前研究的主要热点。本文主要研究运用形式化技术分析安全协议的理论与技术，对基于模型检测技术的运行模式分析法进行深入的研究，并把其应用到实用安全协议的分析与设计中去。本文的主要研究内容包括：（1）系统介绍安全协议的背景和密码协议安全性分析的重要意义。概述协议形式化分析的三种思路；（2）在两方密码协议
7、运行模式的基础上，将七种运行攻击模式简化为五种。（3）介绍基于一个可信第三方的三方密码运行模式，给出四种组合形式的运行模式。（4）运用运行模式法成功分析了 NS 公钥协议，找出协议漏洞，并对协议进行了改进。（5）将模型检测法与其他经典形式化分析法进行比较，给出结论。关键词：安全协议； 模型检测； 形式化分析； 运行模式分析III 目 录第 1 章 绪论11.1 安全协议的背景11.2 分析安全协议的安全性的困难性11.3 国内外研究现状21.4 常见的安全协议形式化分析方法31.5 本文的研究内容41.6 本文的组织结构4第 2 章 模型检测及基于模型检测的运行模式分析法52.1 模型检测的基
8、本思想及工作方式52.2 模型检测技术分析协议方法62.3 运行模式分析法的基本思想及其优点72.4 运行模式分析法简介72.4.1 分析协议的基本假设72.4.2 两方安全协议的运行模式分析法简介82.4.3 三方安全协议运行模式分析法9第 3 章 运行模式分析法的运用133.1 NSPK 协议.133.2 对 NSPK 协议的运行模式分析143.2.1 对 NSPK 协议的分析前提143.2.2 有限状态系统143.2.3 NSPK 协议的分析.143.2.4 改进协议163.2.5 结论17第 4 章 模型检测法与其它经典形式化方法的比较184.1 经典的形式化分析协议方法184.1.1
9、 BAN 逻辑及 BAN 类逻辑184.1.2 串空间模型184.1.3 CSP 模型与分析方法19IV 4.1.4 定理证明的方法204.2 常用的模型检测工具20结论23致谢24参考文献251第 1 章 绪 论1.1 安全协议的背景随着计算机网络的普及与发展，全球信息化已经成为社会发展的必然趋势。同时作为提供通信安全服务的安全协议也在网络信息传递中发挥着越来越重要的作用。安全协议1，又称为密码协议，是在协议中应用加密解密的手段隐藏或获取信息，以达到在网络环境中提供各种安全服务的目的。运用安全协议人们可以解决一系列的安全问题，例如：完成信息源和目标的认证；信息的完整性，防止窜改；密钥的安全分
10、发，保证通讯的安全性；公证性和及时性，保证网络通讯的时效性与合法性；不可抵赖性；授权，实现权限的有效传送，等等。其中认证协议是其它安全目标的基础。Needham-Schroeder 协议2是最为著名的早期的认证协议，许多广泛使用的认证协议都是以 Needham-Schroeder 协议为蓝本而设计的。Needham-Schroeder 协议可分为对称密码体制和非对称密码体制下的两种版本，分别简称为 NSSK 协议和 NSPK协议。这些早期的经典安全协议是安全协议分析的“试验床” ，亦即每当出现一个新的形式化分析方法，都要先分析这几个安全协议，验证新方法的有效性。同时，学者们也经常以它们为例，说
11、明安全协议的设计原则和各种不同分析方法的特点。本文也是以分析 Needham-Schroeder 协议作为重点。1.2 分析安全协议的安全性的困难性已有的安全协议往往被证实并不如它们的设计者所期望的那样安全，同时网络系统仍然面临着各种新、旧手段的威胁。这种复杂的网络环境使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击，从而达到破坏网络安全的目的，因此，安全协议的安全性成为网络安全的关键。在分析协议的安全性时，常用的方法是对协议施加各种可能的攻击来测试其安全性。协议攻击的目标通常有三个：第一是协议中采用的密码算法；第二是算法和协议中采用的密码技术；第三是协议本身。这里我们主要研究对协议自身
12、的攻击，而假设协议中所采用的密码算法和密码技术均是安全的。2安全协议的安全性分析过程是很复杂的，到目前为止，没有一个安全协议是百分百安全的，任何的安全性都是有条件的，或是基于某种假设之上的，谁也不可能对某一协议的安全性给出百分百的证明，因此期望运用形式化分析工具找出所有的漏洞的想法是不切实际的。安全协议设计与分析的困难性在于：（1）安全目标本身的微妙性。例如，表面上十分简单的“认证目标” ，实际上十分微妙。关于认证性的定义，至今存在各种不同的观点；（2）协议运行环境的复杂性。实际上，当安全协议运行在一个十分复杂的公开环境时，攻击者处处存在。我们必须形式化地刻画安全协议的运行环境，这当然是一项艰
13、巨的任务；（3）攻击者模型的复杂性。我们必须形式化地描述攻击者的能力，对攻击者和攻击行为进行分类和形式化的分析；（4）安全协议本身具有“高并发性”的特点。因此，安全协议的分析变得更加复杂并具有挑战性。由于安全协议的分析具有上述特点，因此有必要借助形式化的分析方法或者工具来完成对安全协议的分析。安全协议的形式化分析技术，通俗的讲，是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。安全协议的分析技术可以令协议分析者通过对协议进行建模抽象，将协议的运行环境进行假设，从而将注意力主要集中在分析协议在不同条件下运行时自身属性的满足情况。形式分析的方法不仅能发现现有的攻击方法对协议
14、构成的威胁，而且通过对安全协议的分析，能发现协议中细微的漏洞，从而发现安全协议新的攻击方法。1.3 国内外研究现状Needham-Schroeder 是最早提出对安全协议进行形式化分析思想的学者。在这一领域做出突出贡献的是 Dolev 和 Yoa，他们最早将模型检测技术应用到安全协议验证中。1996 年 Lowe 采用进程代数，使用 FRD 模型检测工具对 Needham-Schroder公钥认证协议进行检测并成功地发现了协议的漏洞。1997 年 Lu 和 Smolka 也使用FRD 验证了 SET 协议中 5 个错误性质。2000 年，Bneerecetli 用信念逻辑验证了Anderw 协
15、议的安全性质。在国内，模型检测方法已经用于对在安全电子商务协议和安全认证协议的分析。但是在现有文献中，大多数用到的都是模型检测器 SMV 和 SPIN，从而不可避免的出现了状态空间爆炸问题。就目前来看，在协议形式化分析方面比较成功的研究思路可以分为三种：第一3种思路是基于推理知识和信念的模态逻辑；第二种思路是基于状态搜索工具和定理证明技术；第三种思路是基于新的协议模型发展证明正确性理论。在下一节中，将对这三种思路以及思路中的常见形式化方法进行一一概述。在这当中最引人注目的就是第二种思路中的模型检测方法，这种方法的好处在于它有全自动化的检测过程，并且如果一个性质不满足，它能给出这个性质不满足的理
16、由。我们即可据此对我们的系统描述进行改进。采用这种方法发现了协议的许多以前未发现的新的攻击，极大地促进了密码协议分析与设计的研究工作。1.4 常见的安全协议形式化分析方法（1）第一种思路是基于推理结构性方法，主要是运用逻辑系统从用户接收和发送的消息出发，通过一系列的推理公理推证协议是否满足其安全说明。用于安全协议形式化分析的逻辑系统可分为两类：一类是基于知识的，另一类是基于信仰的。这些逻辑系统通常由一些命题和推理公理组成，命题表示主体对消息的知识或信仰，而运用推理公理可以从已知的知识和信仰推导出新的知识和信仰。基于推理结构性方法是分析安全协议的最为重要的方法之一，它们分析并验证了许多重要的安全协议，其中包括分析经典的 Needham-Schroeder 私钥协议、Lowe-Needham-Schroeder公钥协议等。其中最重要的方法是 BAN 逻辑方法。（2）第二种思路是基于状态搜索工具
