文献综述报告-范文

论文文献综述

论文题目：中学教学数学审美能力的培养

班级：数学102班姓名：黄强学号：1020151211

1. 前言

信息技术的飞速发展和网络技术的全面应用，将世界带入了一个计算机和网络深入千家万户的信息时代。随着网络应用的迅速发展，信息安全的问题日益重要。信息安全不但关系国家的政治安全、经济安全、军事安全、社会稳定，也关系到社会中每一个人的数字化生存的质量。由于系统的设计缺陷、网络协议的脆弱性，以及人为因素造成的各种漏洞，都可能被攻击者加以利用进行网络攻击。信息安全问题已经成为全球性问题，没有信息安全，就没有真正的政治经济的安全。信息革命是否得以保障决定了信息革命给人类带来的高效率和高效益是否真正实现。西方发达国家十分重视信息安全，美国多年来一直将信息安全技术列为国防重点项目，并已形成庞大的信息安全产业。欧洲、日本、加拿大、澳大利亚和以色列等国也在信息安全领域投入巨资，拥有相当规模的信息安全产业。信息安全涵盖了很多的方面，比如操作系统安全，数据库安全，网络安全等等。

当前，以Internet 为代表的国际互联网的热潮正在向社会的每一个角落渗，因此网络安全成为目前人们关注的一个热点。网络安全主要有两个方面的内容：密码算法和密码协议。密码协议又称为安全协议。它们构成了网络安全体系的两个层次：密码算法为网络上传递的消息提供高强度的加密解密操作和其他辅助算法，而密码协议则在这些算法的基础上为各种网络安全性方面的需求提供实现方案。安全协议是基于密码算法的更高一层的算法，它为有安全需求的各方提供了一个步骤序列，以使它们能够安全地完成实体之间的认证、在实体之间安全地分配密钥或其他各种秘密、确认发送和接收的消息的非否认性等。网络安全不能单纯依靠安全的密码算法。安全协议是网络安全的一个重要组成部分。近年来，安全协议越来越多地用于保护因特网上传送的各种交易。网络协议的安全性分析和验证是当今计算机安全领域的热点和重大课题。

经验告诉我们，设计和分析一个正确的安全协议是一项十分困难的任务。即使我们只讨论安全协议中最基本的认证协议，其中参加协议的主体只有两三个，交换的消息只有3～5条，设计一个正确的、符合认证目标的、没有冗余的认证协议也很不容易[1][2]¨ 。许多安全协议在提出之初被认为是足够安全的，然而在一段时间内被证明有漏洞。如：Needham-Schroeder[3]协议是最为著名的早期的认证协议，该协议可分为对称密码体制和非对称密码体制下的两种版本，分别简称为NSSK协议和NSPK协议。从1978年NSPK协议问世以来，到Lowe于1996年发现NSPK协议的安全缺陷，已经过去了大约l7年之久。安全协议设计的困难性和安全协议分析的微妙性，由此可见一斑。这些漏洞严重的威胁了网络安全。

目前越来越多的安全协议不断地涌现，伴随着相应协议的漏洞也会不断产生。因此对协议进行安全分析找出协议漏洞并修改相应协议成为当前的热点也是难点。安全协议的分析设计方法大概可分为形式化和非形式化两种方法。非形式化的方法根据已知的各种攻击方法来对协议进行攻击，以攻击是否有效来检验密码协议是否安全，是早期的密码协议安全分析所采用形式。长期以来，密码学专家一直依赖经验性的指导原则来设计密码协议，但事实表明非形式化的设计方法很容易忽略掉一些微妙的直觉难以发现的漏洞。这种方法只是停留于发现协议中是否存在已知的缺陷，而不能全面客观地分析密码协议。因此在密码协议的分析过程中引入形式化方法就成为必然。

2. 安全协议及安全协议形式化分析领域研究现状

2.1 安全协议发展的20年

1、从1978年Needham-Schroeder协议的诞生算起，安全协议的发展已经历经20余年了。除了NSSK 协议和NSPK协议之外，早期著名的经典安全协议还有Otway-Rees协议[4]、Yahalom 协议[5]、大嘴青蛙协议[5]等，以及一些重要的实用协议，如Keberos协议[6]、CCITTX。509协议[7]等。

2、1983年，Dolev和Yao发表了安全协议发展史上的一篇重要的论文[8]。该论文的主要贡献有两点。第一点是将安全协议本身与安全协议所具体采用的密码系统分开，在假定密码系统是“完善”的基础上讨论安全协议本身的正确性、安全性、冗余性等课题。从此，学者们可以专心研究安全协议的内在安全性质了。亦即，问题很清楚地被划分为两个不同的层次：首先研究安全协议本身的安全性质，然后讨论实现层次的具体细节，包括所采用的具体密码算法等等。第2点贡献是，Dolev和Yao建立了攻击者模型。他们认为，攻击者的知识和能力不能够低估，攻击者可以控制整个通信网络。Dolev和Yao认为攻击者具有如下能力：(1)可以窃听所有经过网络的消息；(2)可以阻止和截获所有经过网络的消息；(3)可以存储所获得或自身创造的消息；(4)可以根据存储的消息伪造消息，并发送该消息；(5)可以作为合法的主体参与协议的运行。

Dolev和Yao的工作具有深远的影响。迄今为止，大部分有关安全协议的研究工作都遵循Dolev和Yao的基本思想。

3、1990年，Boyd[9]通过实例指出，如果应用序列密码，则在NSSK 协议中，密文消息4与5之间的差别只有1个比特，协议极易受到攻击。

4、1993年，Van Oorschot[10]给出了关于认证协议的6种不同形式的认证目标：Ping认证、实体认证、安全密钥建立、密钥确认、密钥新鲜性、互相信任共享密钥。

5、1996年，Gollmann[11]正式提出讨论认证协议的目标

6、1997年，Clark和Jacob[12]对安全协议进行了概括和总结，列举了一系列有研究意义和实用价值的安全协议。他们将安全协议进行如下分类：

(1)无可信第三方的对称密钥协议。属于这一类的典型协议包括以下ISO系列协议[13]：ISO对称密钥一遍单边认证协议、ISO 对称密钥二遍单边认证协议、ISO 对称密钥二遍相互认证协议、ISO 对称密钥三遍相互认证协议、Andrew安全RPC协议等[14]。

(2)应用密码校验函数(CCF)的认证协议。属于这一类的典型协议包括以下ISO系列协议[15]：ISO应用CCF的一遍单边认证协议、ISO 应用CCF的二遍单边认证协议、ISO 应用CCF的二遍相互认证协议、ISO 应用CCF的三遍相互认证协议。

(3)具有可信第三方的对称密钥协议[3]。属于这一类的典型协议包括NSSK 协议、Otway-Rees协议、Yahalom 协议、大嘴青蛙协议、Denning-Sacco[16]协议、Woo-Lam 协议等。

(4)对称密钥重复认证协议。属于这一类的典型协议有Kerberos协议版本5、Neuman-Stubblebine协议[17]、Kao-Chow重复认证协议[18]等。

(5)无可信第三方的公开密钥协议。属于这一类的典型协议包括以下ISO系列协议[16]：ISO公开密钥一遍单边认证协议、ISO 公开密钥二遍单边认证协议、ISO 公开密钥二遍相互认证协议、ISO 公开密钥三遍相互认证协议、ISO公开密钥二遍并行相互认证协议、Diffie-Hellman[17]协议等。

(6)具有可信第三方的公开密钥协议属于这一类的典型协议有NSPK协议[3]等。

7、1996年，Lowe[21]先采用CSP(通信顺序进程)方法和模型校验技术对安全协议进行形式化分析。他应用CSP模型和CSP模型校验工具FDR分析NSPK协议，并令人惊讶地发现了一个近l7年来未知的攻击。

8、Lowe的论文发表不久，Roscoe[22]对CSP和FDR的组合作了进一步的研究。他们认为，CSP+FDR是形式化分析安全协议的一条新途径。模型校验技术是验证有限状态系统的自动化分析技术，是一种安全协议的自动验证工具。Lowe等学者应用CSP方法的成功，促进了这一领域的发展。Schneider发表了一系列关于CSP方法应用的论文，应用CSP方法讨论安全协议的安全性质、匿名等问题；分析了各种安全协议，例如NSPK协议、非否认协议等。

9、美国卡内基.梅隆大学以Clarke教授为首的研究小组，长期从事定理证明和自动校验的研究。他们提出了一种通用的模型校验器，构造了一种新型的模型及其代数理论，并证明了该模型的有效性。Marrero，Clarke和Jha[23]应用该方法对NSPK协议进行分析。得到了与Lowe相同的结论[21]。Mitchell[24]的方法是通过状态计数工具Murphi分析安全协议，从安全协议可能到达的状态，分析安全协议是否安全。他应用Murphi分析了一系列著名的安全协议，成功地发现了所有己知的攻击。

10、Thayer，Herzog和Guttman[25-27]提出了串空间(strand space)模型，这是一种结合定理证明和协议迹的混合方法。事实证明，串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。

11、Perrig和Song[28]等人对串空间模型进行了重要的扩展，将其增强和优化，并将串空间模型推广到分析三方安全协议。Song应用串空间模型，研制出安全协议自动检验工具— —A曲ena。Athena结合定理证明和模型校验技术，证明从一些初始状态开始，进行回退搜索。初始状态是满足某种安全属性的。

2.2 安全协议形式化分析的历史与现状

网络环境被视为是不安全的，网络中的攻击者可以获取、修改和删除网上信息，并可控制网上用户，因此网络协议是易受攻击的。而协议形式化分析长期以来被视为分析协议安全性的有效工具。最早提出对安全协议进行形式化分析思想的是Needham和Schroeder[3]，他们提出了为进行共享和公钥认证的认证服务器系统的实现建立安全协议，这些安全协议引发了安全协议领域的许多重要问题的研究。1981年Denning & Sacco在文献[16]中指出了NS私钥协议的一个错误，使得人们开始关注安全协议分析这一领域的研究。真正在这一领域首先做出工作的是Dolev和Yao[8]，紧随其后，Dolev，Even和Karp在20世纪七八十年代开发了一系列的多项式时间算法，用于对一些协议的安全性进行分析。Dolev和Yao所作的工作是十分重要的。此后的协议形式化分析模型大多基于此或此模型的变体。如Interrogator、NRL协议分析器和Longley-Rigby工具。

在此基础上发展起来的大多数形式化分析工具都采用了状态探测技术，即定义一个状态空间，对其探测已确定是否存在一条路经对应于攻击者的一次成功的攻击。有些工具中用到了归纳定理推证技术，如在NRL协议分析其中运用此技术证明搜索的空间规模已经可以确保安全性。在形式化分析技术出现的早期阶段，它已成功地发现了协议中不为人工分析所发现的缺陷等。如NRL协议分析器发现了Simmons Selective Broadcast协议的缺陷，Longley-Rigby工具发现了banking协议的缺陷等。

尽管如此，直到1989年，Burrows、Abadi和Needham提出了BAN逻辑之后才打破了形式化分析技术这一领域的神秘感，并从此逐步引起人们广泛的关注。BAN逻辑采用了与状态探测技术完全不同的方法，它是关于主体拥有的知识与信仰以及用于从已有信仰推知新的信仰的推理规则的逻辑。这种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接受消息从最初的信仰逐渐发展到协议运行最终要达到的目的—认证双方的最终信仰。BAN逻辑的规则十分简洁和直观，因此易于使用。BAN逻辑成功地对Needham-Schroeder协议、Kerberos协议等几个著名的协议进行了分析，找到了其中已知的和未知的漏洞。BAN逻辑的成功极大的激发了密码研究者对安全协议形式化分析的兴趣，并导致许多安全协议形式化方法的产生。

但BAN逻辑还有许多不足，出现这样的尴尬局面：当逻辑发现协议中的错误时，每个人都相信那确实是有问题；但当逻辑证明一个协议是安全的时，却没人敢相信它的正确性。

协议形式化分析技术目前主要有三类。第一类是以BAN逻辑为代表的基于推理结构性方法，第二类是基于攻击结构性方法，第三类是基于证明结构性方法。沿着第一个思路，Brackin推广了GNY逻辑并给出了该逻辑的高阶逻辑（HOL）理论，之后利用HOL理论自动证明在该系统内与安全相关的命题。第二种思路是近年来的研究焦点，大量一般目的的形式化方法被用于这一领域，并取得了大量成果。Lowe在文献[21]中证明了可用Ruscoe的模型检测程序FDR发现对Needham-Schroeder公钥协议的一个中间人攻击行为，这引发了人们将协议形式化分析研究的热点集中于基于Dolev-Yao模型的状态检测和定理推证技术上。Mitchell和Stern使用Dill的MurF模型检测程序对Needham-Schroeder公钥协议、TMN和Kerberos协议进行分析；基于进程代数CSP(Communicating Sequential Processes)，Lowe和Roscoe分别发展了不同的理论和方法把大系统中的协议安全性值得研究约化为小系统中的协议安全性质的研究；Millen开发的CAPSL(Common Authentication Protocol Specification Language)为协议形式化分析工具提供通用说明语言，标志着不同形式化分析技术的日趋成熟与集成；Bolignano使用Coq来分析大协议取得实效。第三种思想是推广和（或）完善协议模型，根据该模型提出有效地分析理论。顺应此趋势，Thayer和Herzog给出了Dolev-yao模型的深度理论说明，在文献[25]中提出了融合协议形式化分析中的多种思想和技术的Strand Space的概念，Paulson的归纳方法也是有力的。

3. 形式化方法的概述

安全协议的分析设计方法大概可分为形式化和非形式化两种方法。非形式化的方法我们在前面已经分析了他的缺陷，形式化的方法是当前对安全协议验证的主要方法和手段。形式化方法[29][30][31][32][33][34][35][36][37][38][39][40]原则上就是采用数学与逻辑的方法描述和验证系统。其描述主要包括三方面：一是系统行为的描述，也称建模(modeling)。即通过构造系统的模型来描述系统及其行为模式；二是系统性质的描述，也称规范或规约(specification)。即表示系统满足的一些性质如安全性、活性等。它们可以用一种或多种(规范)语言来描述。这些语言包括命题逻辑、一阶逻辑、高阶逻辑、时序逻辑、自动机、(并发)状态机、代效、进程代数、丌一演算、演算，特殊的程序语言。以及程序语言的子集等。三是系统的验证(verification)。形式化验证主要包括两类方法。一类是以逻辑推理为基础的演绎验证(deductive verification)。另一类是以穷尽搜索为基础的模型检测(model-checking)。用形式化的方法对安全认证协议[41][42][43][44][45][46][47]进行分析和验证要从以下几个方面着手。

3.1 模型检测及相关技术

模型检测[48][49][50][51][52][53]使用状态空间搜索的办法来全自动地检验一个有穷状态系统是否满足其设计规范。这类方法的优点在于它有全自动化的检测过程且验证速度快、效率高，并且如果一个性质不满足能给出这个性质不满足的理由，并指导对协议描述的进行改进。该方法自提出以来发展非常迅速，其理论与技术得到了工业界和学术界的广泛关注[54]。目前许多世界著名大公司如AT&T、Fujitsu、Inter、IBM、Microsoft、Lucent、Motorola、Siemens等纷纷在其产品设计和开发过程中使用模型检测技术，并在许多复杂的实例研究中发挥了重要的作用。

模型检测是一种基于算法的性质验证方法。即对于一类给定的有穷状态并发程序(系统)和表示系统性质(或规范)的某种时序逻辑公式，能否找到一算法，判定系统类中的任一给定系统是否满足公式类中任意给定的一个时序逻辑式。如图1所示，模型检测算法的输入包括二部分，分别是待验证系统的模型M 和系统待检测性质的描述Y，如模型M 满足性质Y。则算法输出“true”；否则给出反例说明M 为何不满足Y。系统建模、性质描述和算法验证是模型检测技术的三个主要步骤。最初的模型检测算法由E。M，Clarke、E。A，Emerson、Queille，Sifakis等人在20世纪80年代初期提出[55]，他们采用分支时序逻辑CTL来描述系统的性质，又称为CTL模型检测；稍后又出现了线性时序逻辑LTL模型检测。

图一

由于模型检测基于状态搜索的基本思想，搜索的可穷尽性要求系统模型状态数有穷。故不能直接对无穷状态系统进行验证。因此对于一般系统来说，首先需要有一个从任意状态到有限状态的建模过程。即使对于有穷状态系统，模型检测也会面临“状态空间爆炸(state space explosion)”的严重问题。CTL或LTL模型检测方法一般采用列表或表格等方式显式表示状态空间，这些状态空间图的大小与系统模型的状态数成正比，而模型的状态数与并发系统的大小成指数关系。因此随着所要检测的系统的规模增大，所要搜索的状态空间呈指数增大，算法验证所需的时间／空间复杂度将超过实际所能承受的程度。

如何有效缓解“状态爆炸”是模型检测能被广泛使用的一个重要前提，在这方面已有一些重要的方法被相继提出，主要包括符号(模型检测)方法、抽象技术、偏序归约，分解与组合以及对称、归纳、On-the-fly方法等[56]。

目前，模型检测与其它方法的结合也取得了一些显著的成果。如模型检测与定理证明方法相结合；模型检测与测试方法相结合；模型检测与概率论方法相结合。

3.2 模型检测工具Spin

常用模型检测工具有：SPIN、SMV、CWB、DESIGN／CPN，UPPAAL，KRONOS，HYTECH等，这些工具的选用与所验证的系统以及系统性质的表示有很大的关系，其中SPIN [57][58][59][60][61][62][63][64]是一种著名的分析验证并发系统（特别是数据通讯协议）逻辑一致性的工具，其目标是对软件而不是硬件高效验证。 G.J. Holzmann因开发SPIN的杰出贡献， 20##年荣获ACM “Software System Award”。

SPIN的开发研究始于上世纪八十年代初，1980年Bell 实验室推出第一个验证系统Pan[65]（Protocol analyzer），它严格限制于对安全性验证；1983 年，Pan被更名为Trace，意味着验证方法从基于进程代数转变为基于自动机理论；1989年推出SPIN的第一个版本，作为一个小型的实例验证系统用来对协议进行验证[66]；1994 年SPIN提出了基于Partial-order reduction的静态归约技术STREM[67]（Static Reduction Method），次年利用内嵌算法[68] 扩充了由LTL公式到自动机自动转换的功能；1997 年提出对软件验证的Minimized Automata[69]思想，在某些情况下，能指数级地减少对内存的需求；1999 年在SPIN 3.3中，提出了Statement Merging技术，能大大地减少对内存的需求及缩短SPIN的验证时间；2000 年在自动模型抽取中引入Property-base Slicing技术，20##年SPIN 4.0 中通过一个模型抽取器的使用，能直接支持对嵌入的C语言代码的检测。目前，最高版本为SPIN 4.2.0。

待验证的系统用Promela（PROcess MEta LAnguage）建模后，进行语法检查，SPIN能通过随机或交互方式模拟此系统的执行，SPIN也可从系统的高级规约中生成一个优化的on-the-fly验证程序（C程序），此验证程序选择优化算法进行编译、运行得到验证结果。若在检测过程中，发现了相背correctness claim的反例，那返回到交互模拟执行状态再继续仔细诊断，确定产生反例的原因。生成的相应C程序，可以穷尽系统状态空间验证。SPIN不仅可以作为LTL模型检测系统，对所有用LTL描述的系统性质进行验证，还可on-the-fly高效地验证很多勿需用LTL刻画的safety properties和 liveness properties，同时还能验证invariants（assertions）正确性、是否存在死锁（deadlock）。SPIN模拟与验证流程见图二（其中XSPIN是用Tcl/Tk书写的驱动执行SPIN的图形前端界面）：

3.3 Promela 建模

Promela是模型检测工具spin提供的一种直观的设计规约语言，用于明确地描述（规约）系统设计选择要求，而不考虑具体实现细节，它是一种系统的描述语言。Promela提供对并发系统进行抽象的机制，而不考虑与进程交互无关的细节，相关进程行为用Promela建模。随着对Promela所建模型的逐步精化，相应地整个并发系统要经过一系列的验证步骤。一旦某个模型的正确性被SPIN所验证，那么此结论就可用于随后精化模型的构建和验证^[20]。

Promela基于Dijkstra的非确定性卫式命令语言，语法类似于C语言，并借鉴Hoare的CSP思想。它的建模方式是以进程为单位，进程异步组合，同步则需要进行显式的声明。进程描述的基本要素包括赋值语句，条件语句，通讯语句，非确定性选择和循环语句。Promela程序由进程、信息通道和变量组成。进程是全局对象，而信息通道和变量相对于一个进程可说明为全局的，也可说明为局部的。进程刻画系统的行为，通道和全局变量用来定义进程执行的环境。

3.4 时态逻辑

由于并发执行的程序在执行过程中各程序交替点的不确定性所引起对各程序的走停点及交替过程的不确定性、使得并发程序的描述与时间变化密切相关。在时态逻辑中，时间并不是显式地表述，相反，在公式中可能会描述某个指定状态最终（ eventually）会到达，或者会描述某个错误状态从不（never）进入。性质eventually， never可以用时态算子说明，这些算子也可以和逻辑连接词（∨、∧、）结合在一起或嵌套使用，构成更复杂的时态逻辑公式来描述并发系统的性质。

3.4.1计算树逻辑（CTL*）

CTL*公式由路径算子和时态算子组成。路径算子用来描述树中的分支结构，路径算子A（“All”，对于所有的路径）和E(“Exist”，存在某条路径)分别表示从某个状态出发的所有路径或某些路径上具有某些性质（描述分枝情况）。时态算子描述经由树的某条路径的性质（描述状态的前后关系），时态算子具体有：X（“neXt”）、 F(“Future”) 、G（“Gobal”）、U（“Until”）、R（“Release”），直观含义分别为（其中Φ、Ψ为原子命题）：

①XΦ对于某条路径为真，如果Φ在该路径的当前状态的下一个状态为真；

②FΦ对于某条路径为真，如果在该路径的某个状态Φ为真；

③GΦ对于一条路径为真，如果在该路径的所有状态Φ都为真；

④ΦUΨ对于某条路径为真，如果Ψ在该路径的某个状态为真，而Φ在这个状态以前的所有状态都为真（U为二元操作算子）；

⑤ΦRΨ对于某条路径为真，如果Ψ在该路径的某个状态及以后所有状态为真，而Φ在这个状态以前的所有状态都为假（R为二元操作算子）。

CTL*中有二类公式：状态公式（其值在某个指定的状态上为真）和路径公式(其值沿着某指定的路径为真)。

（1）CTL*语法

CTL*是由下述规则生成的状态公式集（设AP为原子命题集，p为原子命题）：

①若pAP，则p是一个状态公式；

②若f， g 是状态公式，则f， f∨g， f∧g是状态公式；

③若f是一个路径公式，则Ef， Af是状态公式。

对应路径公式的语法规则如下：

④若f是状态公式，则f 也是路径公式；

⑤若f， g 是路径公式，则f， f∨g， f∧g， Xf， Ff， Gf， fUg， fRg是路径公式。

（2）CTL*的语义

Kripke结构M用三元组 <S，R，L>表示，路径ⁱ表示无穷状态序列= s₀ s₁ s₂_。。。中从s_i开始的后缀。

设f是一个状态公式，则M，s╞f表示在M中状态s满足f，

设g是一个路径公式，则M， ╞g表示在 M中路径满足g。“╞”的递归定义如下(设f₁、f₂为状态公式，g₁、g₂为路径公式)：

M，s╞ppL(s)

M，s╞f₁ M，s? f₁

M，s╞f₁∨f₂ M，s╞f₁ 或M，s╞f₂

M，s╞f₁∧f₂ M，s╞f₁ 且 M，s╞f₂

M，s╞E g₁ $，＝s s₁ s₂_。。。，M， ╞g₁

M，s╞A g₁"，＝s s₁ s₂_。。。，M， ╞g₁

M， ╞f₁$s，＝s s₁ s₂_。。。且 M，s╞f₁

M， ╞g₁ M， ? g₁

M， ╞g₁∨g₂ M， ╞g₁ 或 M， ╞g₂

M， ╞g₁∧g₂ M， ╞g₁ 且M， ╞g₂

M， ╞X g₁ M， ¹╞g₁

M， ╞F g₁ $ k，k≥0，M， ^k╞g₁

M， ╞G g₁ " i，i≥0，M， ⁱ╞g₁

M， ╞ g₁U g₂$k ，k≥0，M， ^k╞g₂且"j ，0≤j<k，M， ^j╞g₁

M， ╞ g₁R g₂ "j，j≥0 ，若"i ，i<j，M， ⁱ ? g₁则 M， ^j╞g₂

容易看出只使用操作算子∨、、X、U、E足以表达其它CTL*公式：

①f∧g(f∨g)

②f R g(f U g)

③F fTrue U f

④G fF f

⑤A(f) E( f)

3.4.2 CTL和LTL

CTL和LTL[70][71][72][73][74][75][76][77]是二种模型检测工具中常用的时态逻辑，模型检测工具SMV[78] 、SPIN[79]中性质描述分别使用CTL、LTL，它们都是CTL*的子逻辑。二者的区别在于：分支时态逻辑CTL是在状态的计算树上解释的，对应于计算树上的每一个状态，要考虑它的一切可能的后继状态（确定沿于某一给定状态的所有可能路径）；线性时态逻辑LTL则是在状态的线性序列上解释的，状态之间按照一个隐含的时间参数严格排序，对于每个状态都有唯一的后继状态。

CTL中路径算子和时态算子成对出现，而且路径算子后面必须有一个时态算子。使用下列规则对CTL*中的路径公式的语法加以限制即得CTL公式：

若f， g 是状态公式，则 Xf， Ff， Gf， fUg， fRg是路径公式。

对CTL公式存在线性时间的模型检测算法，即算法的最坏时间复杂度与│S│*│F│成正比，这里│S│是状态迁移系统的大小，│F│是CTL逻辑公式的长度。

形如A f 为LTL公式，路径公式f中被允许的状态子公式只能是原子命题，构建f的语法规则为：

若pAP，则p是一个路径公式；

若f， g 是路径公式，则f， f∨g， f∧g， Xf， Ff， Gf， fUg， fRg是路径公式（文献^[1]中LTL 的时态算子X、F、G分别用〇、◇、□表示）。

LTL模型检测的常用方法是将所要检测的性质即LTL公式的补转换成Büchi自动机，然后求其与表示系统的自动机的交，如果交为空，则说明系统满足所要检测的性质；否则生成对应反例(counterexample)，说明不满足的原因。

4. 小结

安全协议研究的进展十分可喜，取得了丰富的研究成果。特别是2O世纪9O年代以来，研究取得突破性进展，对安全协议若干本质性的问题有了更为深刻的认识。但是，这一领域还有许多问题有待解决。Meadows[80]提出了安全协议领域的若干公开问题。我们当前研究的协议大多数是认证协议，而电子商务协议、非否认协议、公平交换等是另一个重要的协议及形式化分析领域。

模型检测技术分析密码协议，开启了模型检测技术新的应用领域，并且取得了公认的成功，并使密码协议的形式分析跨越了BAN类逻辑所存在的缺陷，向前进了一大步。但模型检测技术分析密码协议仍然存在着不少问题。如在协议及其环境条件下，如果小系统是安全的，如何使得大系统也是安全的。尽管Gavin Lowe[26]提出一种将大系统中协议安全性质的研究，化为小系统中协议安全性质研究的方法，这是目前这一领域的最新理论研究成果，但是仍然有待于我们去研究；另一个为解决的问题就是状态爆炸问题。模型检测基于对系统状态空间的穷举搜索，对于并发系统，其状态数目往往随并发分量的增加成指数增长，当一个系统的并发分量较多时，直接对其状态空间进行搜索是不可行的。这一点也是我们需要继续去探讨的。

未来的研究趋势是如何扩充模型检测技术从而扩大可分析密码协议的种类，并和定理证明技术相结台，进而解决密码协议安全性分析问题。

5. 参考文献

[1] Qing SH. Cryptography and Computer Network Security. Bering: Tsinghua University Press， 2001， 127-147(in Chinese).

[2] Qing SH. Formal analysis of authentication protocols. Journal of Software， 1996， 7(Supplement)：107-114(in Chinese with English abstract).

[3] Needham R，Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM，1978，21(12)：993-999.

[4] Otway D，Rees O. Efficient and timely mutual authentication. Operating Systems Review，1987，21(1)：8-10.

[5] Burrows M ，Abadi M ，Needham R. A logic of authentication. In：Proceedings of the Royal Society of London A，Vol 426.1989.233-271.

[6] Miller SP，Neuman C，Schiller JI，Saltzer JH. Kerberos authentication and authorization system. Project Athena Technical Plan Section E.2.1，M IT，1987.

[7] CCITT.CCITT draft recommendation X.509.The Directory-Authentication Framework，Version 7，1987.

[8] Dolev D，Yao A. On the security of public key protocols. IEEE Transactions on Information Theory，1983，29(2)：198~208

[9] Boyd C. Hidden assumptions in cryptographic protocols. Proceedings of the IEEE，1990，137(6)：433- 436.

[10] van Oorschot PC. Extending cryptographic logics of belief to key agreement protocols. In：Proceedings of the 1st ACM Conferenceon Computer and Communications Security. ACM Press.1993.233—243.

[11] Gollmmm D. What do we mean by entity authentication? In：Proceedings of the IEEE Symposium on Security and Privacy. Los Alamitos：IEEE Computer Society Press.1996.46~54.

[12] Clark J，Jacob J.A survey of authentication protocol literature：Version 1.0.1997.http：//www—users.cs.york.ac.uk／～jac／under the link＼Security Protocols Review.

[13] ISO／IEC. Information technology--security techniques----entity authentication mechanisms part 2：Entity authentication using symmetric techniques.1993.

[14] Satyanarayanan M. Integrating security in a large distributed system.Technical Report，CMU-CS，CMU，1987.87-179.

[15] ISO／IEC. Information technology---security techniques----entity authentication mechanisms part 4：Entity authentication using cryptographic check functions.1993.

[16] Denning D，Sacco G. Timestamps in key distribution protocols. Communications of the ACM，1981，24(8)：533~536.

[17] Nenman BC，Stubblebine SG. A note on the use of timestamps as nonces. Operating Systems Review，1993，27(2)：10-14.

[18] Kao IL，Chow R. An efficient and secure authentication protocol using uncertified keys. Operating Systems Review，1995，29(3)：l4～21.

[19] ISO／IEC. Information technology~ security techniques----entity authentication mechanisms part 3：Entity authentication using a public key algorithm .1995.

[20] Difie W，Helhnan ME. New directions in cryptography. IEEE Transactions on Information Theory，1976，IT-22(6)：644-4554.

[21] Lowe G. Breaking an d fixing the Needham-Schroeder public-key protocol using FDR.Software-Concepts and Tools，1996，17：93-102.

[22] Roscoe A，Goldsmith M .The perfect ‘spy’ for model-checking cryptoprotocols. In：DIMACS Workshop on Design and Formal Verification of Security Protocols.1997.

[23] Marrero W，Clarke E，Jha S. A model checker for authentication protocols. In：DIMACS Workshop on Design and Formal Verification of Security Protocols.1997.

[24] Mitchell J，Mitchell M，Stern U. Automated analysis of cryptographic protocols using murphi. In：Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos：IEEE Computer Society Press，1997. 141~151.

[25] Thayer FJ，Herzog JC，Guttman JD. Strand spaces：Why is a security protocol correct? In：Proceedings of the 1998 IEEE Symposium on Security an d Privacy. Los Alamitos：IEEE Computer Society Press，1998. 160--171.

[26] Thayer FJ，Herzog JC，Guttman JD. Strand spaces：Proving security protocols correct. Journal of Computer Security，1999，7(2-3)：l9l—230.

[27] Thayer FJ，Herzog JC，Guttman JD. Strand spaces：Honest ideals on strand spaces. In：Proceedings of the 1998 IEEE Computer Security Foundations Workshop. Los Alamitos：IEEE Computer Society Press，1998. 66~77.

[28] Perrig A，Song D. Looking for diamonds in the desert-extending automatic protocol generation to three-party authentication and key agreement. In ：Proceedings of the 13th IEEE Computer Security Foundations Workshop. Los Alamitos：IEEE Computer Society Press，2000. 64-76.

[29] Pnueli A. Verification Engineering：A Future Profession. (A. M. Turing Award Lecture)sixteenth Annual ACM Symposium on Principles of Distributed Computing. San Diego，Aug. 1991

[30] 卿斯汉.安全协议. 第1版，北京: 清华大学出版社， 20##年: 1～149

[31] 肖美华薛锦云. 时态逻辑形式化描述并发系统性质. 海军工程大学学报，2004:16(5)；10-13

[32] 范红冯登国. 安全协议理论与方法. 第1版，北京: 科学出版社， 20##年: 1～227

[33] 冯登国，范红. 安全协议形式化分析理论与方法研究综述.中国科学院研究生报学报，2003: 20(4)

[34] 林贤金，胡山立. 认证协议供给与非形式化分析.小型微型计算机系统，2003，24(11)

[35] 卿斯汉. 一种电子商务协议形式化分析方法. 软件学报，2005：16(10).

[36] 刘克龙，卿斯汉，蒙扬.一种利用公钥体制改进Kerberos协议的方法.软件学报，2001:12(6)

[37] 肖美华，薛锦云. 基于SPIN/Promela 的并发系统验证.计算机科学，2004:31(8)

[38] 钱勇，谷大武，陈克菲. 公钥密码体制下认证协议的形式化分析研究. 小型微型计算机系统. 2002:23(2)

[39] 张磊，桑田，黄连生.从Woo-Lam协议到网络协议的抽象验证. 计算机研究与发展，2001:38(8)

[40] 肖德琴.形式化验证认证协议的研究. 计算机工程，1999: 25(特刊)

[41] Paul Syverson. A Taxonomy Of Replay Attacks. In Proceedings of the 7th IEEE Computer Security Foundations Workshop， pages 131.136.IEEE Computer Society Press， 1994.

[42] 季庆光，冯登国. 对几类重要网络安全协议形式化模型的分析. 计算机学报，2005:28(7)

[43] 卓继亮，李先贤，李建欣. 安全协议的攻击分类及其安全性评估. 计算机研究与发展， 2005:42(7) 1100-1107

[44] 王贵林，卿斯汉，周展飞. 认证协议的一些新攻击方法. 软件学报，2001:12

[45] 刘秀英，张玉清，杨波.三方密码协议运行模式分析. 中国科学院研究生院学报，2004：21（3）

[46] 刘秀英，张玉清，杨波.TMN协议的攻击及其分类研究.Computer Engineering，2004， 30(16)

[47] 卿斯汉. 安全协议20年研究进展. 软件学报，2003：14（10）

[48] Clarke E M Grumberg O Peled D A. Model checking. Cambridge Massachusetts: The MIT Press， 1999: 1-295

[49] Lowe G，Breaking and Fixing the Needham—Schroeder-Public Key Protocol using FDR In. Proc. of TACAS’96 Berlin: Springer Verlag，1996，l47～ 166

[50] 林惠民，张文辉模型检测：理论、方法与应用. 电子学报，2002. 12(A)

[51] 董威、王戟、齐治昌.并发和实时系统的模型检测技术.计算机研究与发展，2001，38(6)

[52] 戎枚，张广泉.模型检测新技术研究. 计算机科学，2003：30(5)

[53] 张玉清，王磊，肖国镇.Needham-Schroeder公钥协议的模型检测分析. 软件学报，2000:11(10)，1348-1352

[54] Pnueli A. Verification Engineering：A Future Profession. (A. M. Turing Award Lecture)sixteenth Annual ACM Symposium on Principles of Distributed Computing. San Diego，Aug. 1997

[55] Clarke E M， Emerson E A. Sistla A P. Automatic Verification of Finite-State Concurrent System Using Temporal Logic Specification. ACM Trans. on Prog. Lang，1986. 8(2): 244～263

[56] Clarke E M. Grumberg J O. Peled D A. Model Checking. M IT. 1999

[57] G.J. Holzmann， The SPIN Model Checker， Primer and Reference Manual， Addison-Wesley， 2003.

[58] G.J. Holzmann， The Model Checker Spin， IEEE Transaction on software engineering， Vol23， No. 5. 1-17，1997.

[59] Holzmann G J. The SPIN Model Checker. Addison—Wesley. 2003:1～535

[60] Paolo Maggi and Riccardo Sisto. Using SPIN to Verify Security Properties of Cryptographic Protocols. Model Checking of Software: 9th International SPIN Workshop， Grenoble， France， April 11-13， 2002. Proceedings

[61] XIAO Mei-hua，XUE Jin-yun. “Modeling and Verifying Cryptographic Protocols Using SPIN/Promela”. International Journal of Computer and Information Science，Vol. 06, No. 1, 1～ 12, 2005.

[62] Gerard J. Holzmann. The Model Checker SPIN. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING，1997:23(5)；

[63] http://netlib.bell-labs.com/netlib/spin

[64] 邵晨曦，胡香冬，熊焰.密码协议的SPIN建模和验证.电子学报，2002：30(12A)

[65] G.J. Holzmann， PAN-a protocol specification analyzer， Bell Laboratories Technical Memorandum，TM81-11271-5，May 1981.

[66] G.J. Holzmann， Design and Validation of Computer Protocols， N.J.: Prentice Hall， 1991.

[67] G.J.Holzmann and D.Peled，An improvement in formal verification， Proc. Forte94，Berne，Switzerland，1994.

[68] R.Gerth， D.Peled， M.Vardi， P.Wolper， Simple on-the-fly automatic verification of linear temporal logic，Proc.PSTV 1995，3-18，Warsaw，Poland.

[69] G.J.Holzmann and A.Puri，A Minimized Automaton Representation of Reachable States， Software Tools for Technology Transfer，Vol.2，No.3，270-278，November 1999， Springer-Verlag.

[70] LI Yong， Van Hung. Checking Temporal Duration Properties of Timed Automata. J. Com put. Sci. ＆ Technology ，2002: 17(6);689-698

[71] S. Schneider. Security properties and CSP. In IEEE Symp. Security and Privacy, 1996.

[72] R. Iosif C. Demartini and R. Sisto. Modeling and Validation of Java Multithreading Applications using SPIN. In Proceedings of the 4th SPIN workshop， Paris， France， November 1998.

[73] P. Gastin， P. Moro， and M. Zeitoun. Minimization of counterexamples in spin. In SPIN Workshop on Model Checking of Software， pages 92–108， 2004.

[74] 肖美华薛锦云. 基于SPIN/Promela 的并发系统验证. 计算机科学， 2004； 31(8)； 201～204

[75] 卿斯汉. 安全协议的设计与逻辑分析. 软件学报，2005：14（7）

[76] 张玉清，吴建平，李星. 模型检测技术和密码协议分析. 计算机科学. 2001：28（8）

[77] 杜慧敏，杨红丽，高得远.一种基于时态逻辑的有限状态系统验证方法.西北工业大学学报，2000，18(1)

[78] Bérard B，Bidoit M，Finkel A. System and Software Verification: Model Checking Techniques and Tools， Springer–Verlag， 2001.

[79] I. 2nd DIS 11770-3. Key management-part3: Mechanisms using asymmetric techniques， 1997

[80] Meadows C. Open issues in formal methods for cryptographic protocol analysis. In：Proceedings of the DARPA Information Survivability Conference an d Exposition. Los Alamitos：IEEE Computer Society Press，2000. 237～250

相关推荐