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 章 模型检测及基于模型检测的运行模式
8、分析法 .52.1 模型检测的基本思想及工作方式 .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 章
9、 模型检测法与其它经典形式化方法的比较 .184.1 经典的形式化分析协议方法 .184.1.1 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 和 Sm
15、olka 也使用FRD 验证了 SET 协议中 5 个错误性质。2000 年， Bneerecetli 用信念逻辑验证了Anderw 协议的安全性质。在国内，模型检测方法已经用于对在安全电子商务协议和安全认证协议的分析。但是在现有文献中，大多数用到的都是模型检测器 SMV 和 SPIN，从而不可避免的出现了状态空间爆炸问题。就目前来看，在协议形式化分析方面比较成功的研究思路可以分为三种：第一3种思路是基于推理知识和信念的模态逻辑；第二种思路是基于状态搜索工具和定理证明技术；第三种思路是基于新的协议模型发展证明正确性理论。在下一节中，将对这三种思路以及思路中的常见形式化方法进行一一概述。在这当中
16、最引人注目的就是第二种思路中的模型检测方法，这种方法的好处在于它有全自动化的检测过程，并且如果一个性质不满足，它能给出这个性质不满足的理由。我们即可据此对我们的系统描述进行改进。采用这种方法发现了协议的许多以前未发现的新的攻击，极大地促进了密码协议分析与设计的研究工作。1.4 常见的安全协议形式化分析方法（1）第一种思路是基于推理结构性方法，主要是运用逻辑系统从用户接收和发送的消息出发，通过一系列的推理公理推证协议是否满足其安全说明。用于安全协议形式化分析的逻辑系统可分为两类：一类是基于知识的，另一类是基于信仰的。这些逻辑系统通常由一些命题和推理公理组成，命题表示主体对消息的知识或信仰，而运用
17、推理公理可以从已知的知识和信仰推导出新的知识和信仰。基于推理结构性方法是分析安全协议的最为重要的方法之一，它们分析并验证了许多重要的安全协议，其中包括分析经典的 Needham-Schroeder 私钥协议、 Lowe-Needham-Schroeder公钥协议等。其中最重要的方法是 BAN 逻辑方法。（2）第二种思路是基于状态搜索工具和定理证明技术，可以分为三类：一般目的的验证语言和模型检测工具，如通信顺序进程 CSP 和其验证工具 FDR；单一代数理论模型，如 Dolev-Yao 模型、Merrit 模型、Meadows 模型等；特殊目的的专家系统，如 NRL 分析器和 Interroga
18、tor。这种思路是近几年研究的焦点，大量一般目的的形式化方法被用于这一领域，取得了大量成果，突出的成果有：Lowe 使用进程代数CSP 发现了 Needham-Schroeder 公钥协议的十七年未发现的漏洞；Schneider 用进程代数 CSP 归范了大量的安全性质；基于进程代数 CSP，Lowe 和 Roscoe 分别发展了不同的理论和方法把大系统中协议安全性质的研究约化为小系统中协议安全性质的研究；Abadi 及 Gordon 发展推演密码协议的 Spi 演算，J.Mitchell 等把 Spi 演算与他们发展的工具 Mur 结合，有可能把 MIT 群体的基于算法复杂性的协议安全理论与
19、进程代数有机结合。总之，这种思路至今仍是热点。在这些成果中最重要的就是 CSP和模型检测技术的结合。而本文也是以这种思路中的模型检测法为研究重点。（3）第三种思路是推广或完善协议模型，根据该模型提出有效的分析理论。如4前所述，基于推理结构性的形式化分析方法不能解决秘密性，而且缺乏清晰的语义，甚至有时很难明确指出信仰逻辑在证明什么。另一方面，由于基于攻击结构性的形式化分析方法不得不对随着协议的增大而呈指数增长的协议状态空间进行搜索，其所需的时间和空间往往超过可用资源。为解决上述问题而提出的第三种思路是推广或完善协议模型，根据该模型提出有效的分析理论。在这方面主要包括 Bolignano提出的 h
20、uman-readable 证明法、Paulson 归纳法、 Thayer、Herzon 及 Guttman 提出的Strand Space（串空间）理论等等。在这些理论中，human-readable 证明法将重点放在区分主体的可信度上，以及它们所扮演的角色、信仰、控制结构、使用临时特征表示认证属性等，并运用强有力的不变式技术和攻击者知识公理使得认证过程类似基于模型的验证方法，且可自动实现，该方法已用于多种认证协议的分析中，验证结论可以从一个协议应用到另一个协议。串空间集 NRL 协议器、Schneider 的秩函数以及 Paulson 的归纳法思想于一体，是相当简洁、优美的，是一种新型的有
21、效的协议形式化方法。1.5 本文的研究内容本文在研究安全协议的形式化分析方法的基础上，重点研究了基于模型检测技术的运行模式分析法，主要围绕 NS 认证协议的模型检测方法进行深入的研究，对该议进行安全性分析，找出协议漏洞，并做改进。然后将模型检测法与其他经典形式化分析方法进行对比，分析各方法的优缺点，最后给出模型检测方法的总体结论。1.6 本文的组织结构全文的章节如下：第一章：简要介绍安全协议的背景、研究现状及几种常见的形式化分析方法。第二章：重点介绍基于模型检测的运行模式分析法。第三章：使用两方运行模式分析法对NS协议的安全性进行分析。第四章：将模型检测法与其它经典形式化分析方法进行对比，给出
22、总体结论；将常用的模型检测工具SPIN 和SMV 进行对比，给出结论。56第 2 章 模型检测及基于模型检测的运行模式分析法2.1 模型检测的基本思想及工作方式模型检测是一种面向有穷状态并发系统的验证技术，是形式化验证中很重要的一种方法。它的研究始于八十年代初，当时 larke，Emerson 等人提出了用于描述并发系统性质的 CTL 逻辑，设计了检测有穷状态系统是否满足给定 CTL 公式的算法，并实现了一个原型系统 EMC。这一工作为对并发系统的性质自动进行验证开辟了一条新的途径，成为近二十年来计算机科学基础研究的一个热点。模型检测是一种关于系统性质验证算法的方法，它通过状态空间搜索的方法来
23、检测一个给定的计算模型是否满足某个时序逻辑公式表示的特定的性质。对于有穷状态系统，该问题是可判定的，即用计算机程序可以在有限时间内自动确定。模型检测技术的优点是自动化程度高，不需要使用者掌握大量的逻辑知识。当所设计的系统不满足某个性质时，模型检测工具可以返回一个反例，通过对反例的解读可以得到性质不成立的原因，为系统的修正提供重要线索。因此模型检测在形式化验证领域越来越受到重视。目前模型检测已被应用于计算机硬件、通信协议、安全认证协议等方面的分析与验证中，取得了令人瞩目的成功。但同时由于模型检测是基于对系统状态空间的穷举搜索，其状态的数目往往随并发分量的增加呈指数增长。因此当一个系统的并发分量较
24、多时，直接对其状态空间进行搜索实际上是不可行的，这就是所谓的状态爆炸问题。由于软件涉及无穷数据域上的运算，所以状态爆炸问题十分突出，已成为模型检测应用于软件系统的一个具有挑战性的难题。模型检测大致可分为以下3个步骤：（1）是系统建模，在此阶段需要把系统结构用形式化语言描述出来，即将系统的状态集合及状态迁移关系进行形式化描述。具体使用哪种描述语言要根据模型检测工具来确定，每个不同的模型检测工具都有各自的建模语言。系统建模的关键在于正确地描述好系统的状态迁移关系，这是进行规范验证的前提条件，因为迁移关系描述有误则不能保证规范验证的结果是可靠的。此外，还要注意尽量使用精简的方式来描述系统，避免因为引入过多变量而造成的系统状态爆炸问题。 （2）建立规范，通常将需要验证的系统性质表示为时态规范，即时态逻辑表达式。对硬件或软件系统，时态逻辑能够断言系统随着时间演变的行为变化。不同的模型检测工具对规范的描述有不同的要求。如SPIN中的规范必
