1、 I 目 录第 1 章 绪论 .11.1 安全协议的背景 .11.2 分析安全协议的安全性的困难性 .11.3 国内外研究现状 .21.4 常见的安全协议形式化分析方法 .31.5 本文的研究内容 .41.6 本文的组织结构 .4第 2 章 模型检测及基于模型检测的运行模式分析法 .52.1 模型检测的基本思想及工作方式 .52.2 模型检测技术分析协议方法 .62.3 运行模式分析法的基本思想及其优点 .72.4 运行模式分析法简介 .72.4.1 分析协议的基本假设 .72.4.2 两方安全协议的运行模式分析法简介 .82.4.3 三方安全协议运行模式分析法 .9第 3 章 运行模式分析法
2、的运用 .133.1 NSPK 协议 .133.2 对 NSPK 协议的运行模式分析 .143.2.1 对 NSPK 协议的分析前提 .14II 3.2.2 有限状态系统 .143.2.3 NSPK 协议的分析 .143.2.4 改进协议 .163.2.5 结论 .17第 4 章 模型检测法与其它经典形式化方法的比较 .184.1 经典的形式化分析协议方法 .184.1.1 BAN 逻辑及 BAN 类逻辑 .184.1.2 串空间模型 .184.1.3 CSP 模型与分析方法 .194.1.4 定理证明的方法 .204.2 常用的模型检测工具 .20结论 .23致谢 .24参考文献 .251安
3、全协议模型检测技术的研究与应用摘要：安全协议的安全性是网络安全的重要基础，运用形式化方法分析安全协议的安全性己成为目前研究的主要热点。本文主要研究运用形式化技术分析安全协议的理论与技术，对基于模型检测技术的运行模式分析法进行深入的研究，并把其应用到实用安全协议的分析与设计中去。本文的主要研究内容包括：（1）系统介绍安全协议的背景和密码协议安全性分析的重要意义。概述协议形式化分析的三种思路；（2）在两方密码协议运行模式的基础上，将七种运行攻击模式简化为五种。（3）介绍基于一个可信第三方的三方密码运行模式，给出四种组合形式的运行模式。（4）运用运行模式法成功分析了 NS 公钥协议，找出协议漏洞，并
4、对协议进行了改进。（5）将模型检测法与其他经典形式化分析法进行比较，给出结论。关键词：安全协议； 模型检测； 形式化分析； 运行模式分析2Research 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
5、 has become a hotspot of research. This dissertation makes a research 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 s
6、ecurity protocols. The researches are summarized as follows:The background 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 sec
7、urity protocol, and found it will be simplified the running modes from seven to five. We introduce the running-mode analysis based on the three-party security protocol 3including only one server which acts as the trusted third party. Then we find there are four form running modes when the protocols
8、run.Furthermore, the running-mode analysis based on the two-party security 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 mo
9、del checking with other formal analysis methods and give the conclusions.Keywords: security protocol, model checking, formal analysis, running-mode analysis 第 1 章 绪 论1.1 安全协议的背景随着计算机网络的普及与发展，全球信息化已经成为社会发展的必然趋势。同时作为提供通信安全服务的安全协议也在网络信息传递中发挥着越来越重要的作用。安全协议 1，又称为密码协议，是在协议中应用加密解密的手段隐藏或获取信息，以达到在网络环境中提供各种安全
10、服务的目的。运用安全协议人们可以解决一系列的安全问题，例如：完成信息源和目标的认证；信息的完整性，防止窜改；密钥的安全分发，保证通讯的安全性；公证性和及时性，保证网络通讯的时效性与合4法性；不可抵赖性；授权，实现权限的有效传送，等等。其中认证协议是其它安全目标的基础。Needham-Schroeder 协议 2是最为著名的早期的认证协议，许多广泛使用的认证协议都是以 Needham-Schroeder 协议为蓝本而设计的。 Needham-Schroeder 协议可分为对称密码体制和非对称密码体制下的两种版本，分别简称为 NSSK 协议和 NSPK协议。这些早期的经典安全协议是安全协议分析的“
11、试验床” ，亦即每当出现一个新的形式化分析方法，都要先分析这几个安全协议，验证新方法的有效性。同时，学者们也经常以它们为例，说明安全协议的设计原则和各种不同分析方法的特点。本文也是以分析 Needham-Schroeder 协议作为重点。1.2 分析安全协议的安全性的困难性已有的安全协议往往被证实并不如它们的设计者所期望的那样安全，同时网络系统仍然面临着各种新、旧手段的威胁。这种复杂的网络环境使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击，从而达到破坏网络安全的目的，因此，安全协议的安全性成为网络安全的关键。在分析协议的安全性时，常用的方法是对协议施加各种可能的攻击来测试其安全性。协议
12、攻击的目标通常有三个：第一是协议中采用的密码算法；第二是算法和协议中采用的密码技术；第三是协议本身。这里我们主要研究对协议自身的攻击，而假设协议中所采用的密码算法和密码技术均是安全的。安全协议的安全性分析过程是很复杂的，到目前为止，没有一个安全协议是百分百安全的，任何的安全性都是有条件的，或是基于某种假设之上的，谁也不可能对某一协议的安全性给出百分百的证明，因此期望运用形式化分析工具找出所有的漏洞的想法是不切实际的。安全协议设计与分析的困难性在于：（1）安全目标本身的微妙性。例如，表面上十分简单的“认证目标” ，实际上十分微妙。关于认证性的定义，至今存在各种不同的观点；（2）协议运行环境的复杂
13、性。实际上，当安全协议运行在一个十分复杂的公开环境时，攻击者处处存在。我们必须形式化地刻画安全协议的运行环境，这当然是一项艰巨的任务；（3）攻击者模型的复杂性。我们必须形式化地描述攻击者的能力，对攻击者和攻击行为进行分类和形式化的分析；5（4）安全协议本身具有“高并发性”的特点。因此，安全协议的分析变得更加复杂并具有挑战性。由于安全协议的分析具有上述特点，因此有必要借助形式化的分析方法或者工具来完成对安全协议的分析。安全协议的形式化分析技术，通俗的讲，是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。安全协议的分析技术可以令协议分析者通过对协议进行建模抽象，将协议的运行
14、环境进行假设，从而将注意力主要集中在分析协议在不同条件下运行时自身属性的满足情况。形式分析的方法不仅能发现现有的攻击方法对协议构成的威胁，而且通过对安全协议的分析，能发现协议中细微的漏洞，从而发现安全协议新的攻击方法。1.3 国内外研究现状Needham-Schroeder 是最早提出对安全协议进行形式化分析思想的学者。在这一领域做出突出贡献的是 Dolev 和 Yoa，他们最早将模型检测技术应用到安全协议验证中。1996 年 Lowe 采用进程代数，使用 FRD 模型检测工具对 Needham-Schroder公钥认证协议进行检测并成功地发现了协议的漏洞。1997 年 Lu 和 Smolka
15、 也使用FRD 验证了 SET 协议中 5 个错误性质。2000 年， Bneerecetli 用信念逻辑验证了Anderw 协议的安全性质。在国内，模型检测方法已经用于对在安全电子商务协议和安全认证协议的分析。但是在现有文献中，大多数用到的都是模型检测器 SMV 和 SPIN，从而不可避免的出现了状态空间爆炸问题。就目前来看，在协议形式化分析方面比较成功的研究思路可以分为三种：第一种思路是基于推理知识和信念的模态逻辑；第二种思路是基于状态搜索工具和定理证明技术；第三种思路是基于新的协议模型发展证明正确性理论。在下一节中，将对这三种思路以及思路中的常见形式化方法进行一一概述。在这当中最引人注目
16、的就是第二种思路中的模型检测方法，这种方法的好处在于它有全自动化的检测过程，并且如果一个性质不满足，它能给出这个性质不满足的理由。我们即可据此对我们的系统描述进行改进。采用这种方法发现了协议的许多以前未发现的新的攻击，极大地促进了密码协议分析与设计的研究工作。61.4 常见的安全协议形式化分析方法（1）第一种思路是基于推理结构性方法，主要是运用逻辑系统从用户接收和发送的消息出发，通过一系列的推理公理推证协议是否满足其安全说明。用于安全协议形式化分析的逻辑系统可分为两类：一类是基于知识的，另一类是基于信仰的。这些逻辑系统通常由一些命题和推理公理组成，命题表示主体对消息的知识或信仰，而运用推理公理
17、可以从已知的知识和信仰推导出新的知识和信仰。基于推理结构性方法是分析安全协议的最为重要的方法之一，它们分析并验证了许多重要的安全协议，其中包括分析经典的 Needham-Schroeder 私钥协议、 Lowe-Needham-Schroeder公钥协议等。其中最重要的方法是 BAN 逻辑方法。（2）第二种思路是基于状态搜索工具和定理证明技术，可以分为三类：一般目的的验证语言和模型检测工具，如通信顺序进程 CSP 和其验证工具 FDR；单一代数理论模型，如 Dolev-Yao 模型、Merrit 模型、Meadows 模型等；特殊目的的专家系统，如 NRL 分析器和 Interrogator。
18、这种思路是近几年研究的焦点，大量一般目的的形式化方法被用于这一领域，取得了大量成果，突出的成果有：Lowe 使用进程代数CSP 发现了 Needham-Schroeder 公钥协议的十七年未发现的漏洞；Schneider 用进程代数 CSP 归范了大量的安全性质；基于进程代数 CSP，Lowe 和 Roscoe 分别发展了不同的理论和方法把大系统中协议安全性质的研究约化为小系统中协议安全性质的研究；Abadi 及 Gordon 发展推演密码协议的 Spi 演算，J.Mitchell 等把 Spi 演算与他们发展的工具 Mur 结合，有可能把 MIT 群体的基于算法复杂性的协议安全理论与进程代数
19、有机结合。总之，这种思路至今仍是热点。在这些成果中最重要的就是 CSP和模型检测技术的结合。而本文也是以这种思路中的模型检测法为研究重点。（3）第三种思路是推广或完善协议模型，根据该模型提出有效的分析理论。如前所述，基于推理结构性的形式化分析方法不能解决秘密性，而且缺乏清晰的语义，甚至有时很难明确指出信仰逻辑在证明什么。另一方面，由于基于攻击结构性的形式化分析方法不得不对随着协议的增大而呈指数增长的协议状态空间进行搜索，其所需的时间和空间往往超过可用资源。为解决上述问题而提出的第三种思路是推广或完善协议模型，根据该模型提出有效的分析理论。在这方面主要包括 Bolignano提出的 human-
20、readable 证明法、Paulson 归纳法、 Thayer、Herzon 及 Guttman 提出的7Strand Space（串空间）理论等等。在这些理论中，human-readable 证明法将重点放在区分主体的可信度上，以及它们所扮演的角色、信仰、控制结构、使用临时特征表示认证属性等，并运用强有力的不变式技术和攻击者知识公理使得认证过程类似基于模型的验证方法，且可自动实现，该方法已用于多种认证协议的分析中，验证结论可以从一个协议应用到另一个协议。串空间集 NRL 协议器、Schneider 的秩函数以及 Paulson 的归纳法思想于一体，是相当简洁、优美的，是一种新型的有效的协议
21、形式化方法。1.5 本文的研究内容本文在研究安全协议的形式化分析方法的基础上，重点研究了基于模型检测技术的运行模式分析法，主要围绕 NS 认证协议的模型检测方法进行深入的研究，对该议进行安全性分析，找出协议漏洞，并做改进。然后将模型检测法与其他经典形式化分析方法进行对比，分析各方法的优缺点，最后给出模型检测方法的总体结论。1.6 本文的组织结构全文的章节如下：第一章：简要介绍安全协议的背景、研究现状及几种常见的形式化分析方法。第二章：重点介绍基于模型检测的运行模式分析法。第三章：使用两方运行模式分析法对NS协议的安全性进行分析。第四章：将模型检测法与其它经典形式化分析方法进行对比，给出总体结论；将常用的模型检测工具SPIN 和SMV 进行对比，给出结论。8
