文献综述报告-范文论文文献综述 班级：数学 102 学号：1020151211 信息技术的飞速发展和网络技术的全面应用，将世界带入了一个计算机和网络深入千家万户的信息时代。随着网络应用的迅速发 展，信息安全的问题日益重要。信息安全不但关系国家的政治安全、 经济安全、军事安全、社会稳定，也关系到社会中每一个人的数字化 生存的质量。由于系统的设计缺陷、网络协议的脆弱性，以及人为因 素造成的各种漏洞，都可能被攻击者加以利用进行网络攻击。信息安 全问题已经成为全球性问题，没有信息安全，就没有真正的政治经济 的安全。信息革命是否得以保障决定了信息革命给人类带来的高效率 和高效益是否真正实现。西方发达国家十分重视信息安全，美国多年 来一直将信息安全技术列为国防重点项目，并已形成庞大的信息安全 产业。欧洲、日本、加拿大、澳大利亚和以色列等国也在信息安全领 域投入巨资，拥有相当规模的信息安全产业。信息安全涵盖了很多的 方面，比如操作系统安全，数据库安全，网络安全等等。 当前，以Internet 为代表的国际互联网的热潮正在向社会的每 一个角落渗，因此网络安全成为目前人们关注的一个热点。网络安全 主要有两个方面的内容：密码算法和密码协议。密码协议又称为安全 协议。它们构成了网络安全体系的两个层次：密码算法为网络上传递 的消息提供高强度的加密解密操作和其他辅助算法，而密码协议则在 这些算法的基础上为各种网络安全性方面的需求提供实现方案。安全 协议是基于密码算法的更高一层的算法，它为有安全需求的各方提供 了一个步骤序列，以使它们能够安全地完成实体之间的认证、在实体 之间安全地分配密钥或其他各种秘密、确认发送和接收的消息的非否 认性等。网络安全不能单纯依靠安全的密码算法。安全协议是网络安 全的一个重要组成部分。近年来，安全协议越来越多地用于保护因特 网上传送的各种交易。网络协议的安全性分析和验证是当今计算机安 全领域的热点和重大课题。 经验告诉我们，设计和分析一个正确的安全协议是一项十分困难的任务。即使我们只讨论安全协议中最基本的认证协议，其中参加 协议的主体只有两三个，交换的消息只有3～5 条，设计一个正确的、 符合认证目标的、没有冗余的认证协议也很不容易[1][2] 。许多安 全协议在提出之初被认为是足够安全的，然而在一段时间内被证明有 漏洞。如：Needham-Schroeder[3]协议是最为著名的早期的认证协议， 该协议可分为对称密码体制和非对称密码体制下的两种版本，分别简 称为NSSK 协议和NSPK 协议。从19xx 年NSPK 协议问世以来，到 Lowe 于19xx 年发现NSPK 协议的安全缺陷，已经过去了大约l7 之久。安全协议设计的困难性和安全协议分析的微妙性，由此可见一斑。这些漏洞严重的威胁了网络安全。 目前越来越多的安全协议不断地涌现，伴随着相应协议的漏洞也会不断产生。因此对 协议进行安全分析找出协议漏洞并修改相应协议成为当前的热点也是难点。安全协议的分析设计方法大概可分为形式化和非形式 化两种方法。非形式化的方法根据已知的各种攻击方法来对协议进行 攻击，以攻击是否有效来检验密码协议是否安全，是早期的密码协议 安全分析所采用形式。长期以来，密码学专家一直依赖经验性的指导 原则来设计密码协议，但事实表明非形式化的设计方法很容易忽略掉 一些微妙的直觉难以发现的漏洞。这种方法只是停留于发现协议中是 否存在已知的缺陷，而不能全面客观地分析密码协议。因此在密码协 议的分析过程中引入形式化方法就成为必然。 1、从19xx年Needham-Schroeder 协议的诞生算起，安全协议 的发展已经历经20 余年了。除了NSSK 协议和NSPK协议之外，早 期著名的经典安全协议还有Otway-Rees 协议[4]、Yahalom 协议[5]、 大嘴青蛙协议[5]等，以及一些重要的实用协议，如Keberos 协议[6]、 CCITTX。509 协议[7]等。 2、19xx年，Dolev Yao发表了安全协议发展史上的一篇重 要的论文[8]。该论文的主要贡献有两点。第一点是将安全协议本身 与安全协议所具体采用的密码系统分开，在假定密码系统是―完善‖ 的基础上讨论安全协议本身的正确性、安全性、冗余性等课题。从此， 学者们可以专心研究安全协议的内在安全性质了。亦即，问题很清楚 地被划分为两个不同的层次：首先研究安全协议本身的安全性质，然 后讨论实现层次的具体细节，包括所采用的具体密码算法等等。第2 点贡献是，Dolev 和Yao 建立了攻击者模型。他们认为，攻击者的知 识和能力不能够低估，攻击者可以控制整个通信网络。Dolev Yao认为攻击者具有如下能力：(1)可以窃听所有经过网络的消息；(2)可 以阻止和截获所有经过网络的消息；(3)可以存储所获得或自身创造 的消息；(4)可以根据存储的消息伪造消息，并发送该消息；(5)可以 作为合法的主体参与协议的运行。 Yao的工作具有深远的影响。迄今为止，大部分有关 安全协议的研究工作都遵循Dolev 和Yao 的基本思想。 3、19xx年，Boyd[9]通过实例指出，如果应用序列密码，则在 NSSK 协议中，密文消息4 之间的差别只有1个比特，协议极易 受到攻击。 4、19xx年，Van Oorschot[10]给出了关于认证协议的6 种不同 形式的认证目标：Ping 认证、实体认证、安全密钥建立、密钥确认、 密钥新鲜性、互相信任共享密钥。 5、19xx年，Gollmann[11]正式提出讨论认证协议的目标 6、19xx年，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、19xx年，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) 模型，这是一种结合定理证明和协议迹的混合方法。事实证明，串空 间模型是分析安全协议的一种实用、直观和严格的形式化方法。 Song[28]等人对串空间模型进行了重要的扩展，将其增强和优化，并将串空间模型推广到分析三方安全协议。Song 应用串空间模型，研制出安全协议自动检验工具— —A曲ena。Athena 结合定理证明和模型校验技术，证明从一些初始状态开始，进行回退 搜索。初始状态是满足某种安全属性的。 网络环境被视为是不安全的，网络中的攻击者可以获取、修改和删除网上信息，并可控制网上用户，因此网络协议是易受攻击的。 而协议形式化分析长期以来被视为分析协议安全性的有效工具。最早 提出对安全协议进行形式化分析思想的是Needham和Schroeder[3]， 他们提出了为进行共享和公钥认证的认证服务器系统的实现建立安 全协议，这些安全协议引发了安全协议领域的许多重要问题的研究。 19xx 年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 协议的缺陷等。 尽管如此，直到19xx年，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 的Mur?模型检测程序 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 的归纳方法也是有力的。 安全协议的分析设计方法大概可分为形式化和非形式化两种方法。非形式化的方法我们 [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]进行分析和验证要从以下几个方面着手。 模型检测[48][49][50][51][52][53]使用状态空间搜索的办法来全自动地检验一个有穷状态系统是否满足其设计规范。这类方法的优 点在于它有全自动化的检测过程且验证速度快、效率高，并且如果一 个性质不满足能给出这个性质不满足的理由，并指导对协议描述的进 行改进。该方法自提出以来发展非常迅速，其理论与技术得到了工业 界和学术界的广泛关注[54]。目前许多世界著名大公司如 AT&T、 Fujitsu、Inter、IBM、Microsoft、Lucent、Motorola、Siemens 等纷纷 在其产品设计和开发过程中使用模型检测技术，并在许多复杂的实例 研究中发挥了重要的作用。 模型检测是一种基于算法的性质验证方法。即对于一类给定的有穷状态并发程序(系统)和表示系统性质(或规范)的某种时序逻辑公 式，能否找到一算法，判定系统类中的任一给定系统是否满足公式类 中任意给定的一个时序逻辑式。如图1 所示，模型检测算法的输入包 括二部分，分别是待验证系统的模型M 和系统待检测性质的描述?， 如模型 何不满足?。系统建模、性质描述和算法验证是模型检测技术的三个 主要步骤。最初的模型检测算法由E。M，Clarke、E。A，Emerson、 Queille，Sifakis 等人在20 世纪80 年代初期提出[55]，他们采用分支 时序逻辑CTL 来描述系统的性质，又称为CTL 模型检测；稍后又出 现了线性时序逻辑LTL 模型检测。 由于模型检测基于状态搜索的基本思想，搜索的可穷尽性要求系统模型状态数有穷。故不能直接对无穷状态系统进行验证。因此对 于一般系统来说，首先需要有一个从任意状态到有限状态的建模过 程。即使对于有穷状态系统，模型检测也会面临―状态空间爆炸(state space explosion)‖的严重问题。CTL或LTL 模型检测方法一般采用列 表或表格等方式显式表示状态空间，这些状态空间图的大小与系统模 型的状态数成正比，而模型的状态数与并发系统的大小成指数关系。 因此随着所要检测的系统的规模增大，所要搜索的状态空间呈指数增 大，算法验证所需的时间／空间复杂度将超过实际所能承受的程度。 如何有效缓解―状态爆炸‖是模型检测能被广泛使用的一个重要前提，在这方面已有一些重要的方法被相继提出，主要包括符号(模 型检测)方法、抽象技术、偏序归约，分解与组合以及对称、归纳、 On-the-fly 方法等[56]。 目前，模型检测与其它方法的结合也取得了一些显著的成果。如模型检测与定理证明方法相结合；模型检测与测试方法相结合；模 型检测与概率论方法相结合。 常用模型检测工具有：SPIN、SMV、CWB、DESIGN／CPN，UPPAAL，KRONOS，HYTECH 等，这些工具的选用与所验证的系 统以及系统性质的表示有很大的关系，其中SPIN [57][58][59][60][61][62][63][64]是一种著名的分析验证并发系统（特别是数据通讯协议）逻辑一致性的工具，其目标是对软件而不 是硬件高效验证。 Holzmann 因开发SPIN 的杰出贡献， 20xx 获ACMSoftware System Award‖。 SPIN的开发研究始于上世纪八十年代初，19xx 年Bell 实验室 推出第一个验证系统Pan[65]（Protocol analyzer），它严格限制于对安 全性验证；1983 年，Pan 被更名为Trace，意味着验证方法从基于进 程代数转变为基于自动机理论；19xx 年推出SPIN 的第一个版本，作 为一个小型的实例验证系统用来对协议进行验证[66]；1994 SPIN提出了基于Partial-order reduction 的静态归约技术STREM[67] （Static Reduction Method），次年利用内嵌算法[68] 扩充了由LTL 公式到自 动机自动转换的功能；1997 年提出对软件验证的 Minimized Automata[69]思想，在某些情况下，能指数级地减少对内存的需求； 1999 年在SPIN 中，提出了Statement Merging 技术，能大大地减少 对内存的需求及缩短 SPIN 的验证时间；2000 年在自动模型抽取中 引入Property-base Slicing 技术，20xx 年SPIN 中通过一个模型抽取 器的使用，能直接支持对嵌入的 语言代码的检测。目前，最高版本为SPIN 待验证的系统用Promela（PROcessMEta LAnguage）建模后， 进行语法检查，SPIN 能通过随机或交互方式模拟此系统的执行，SPIN 也可从系统的高级规约中生成一个优化的 on-the-fly 验证程序（C 序），此验证程序选择优化算法进行编译、运行得到验证结果。若在检测过程中，发现了相背correctness claim 的反例，那返回到交互模 拟执行状态再继续仔细诊断，确定产生反例的原因。生成的相应 程序，可以穷尽系统状态空间验证。SPIN不仅可以作为LTL 模型检 测系统，对所有用LTL 描述的系统性质进行验证，还可on-the-fly 效地验证很多勿需用LTL 刻画的 safety properties livenessproperties，同时还能验证invariants（assertions）正确性、是否存在死 锁（deadlock）。SPIN 模拟与验证流程见图二（其中XSPIN 是用Tcl/Tk 书写的驱动执行SPIN 的图形前端界面）： Promela建模 Promela是模型检测工具spin提供的一种直观的设计规约语言，用于明确地描述（规约）系统设计选择要求，而不考虑具体实现细节， 它是一种系统的描述语言。Promela 提供对并发系统进行抽象的机制， 而不考虑与进程交互无关的细节，相关进程行为用Promela 建模。随 着对Promela 所建模型的逐步精化，相应地整个并发系统要经过一系 列的验证步骤。 [20]一旦某个模型的正确性被SPIN所验证，那么此结论就可用 于随后精化模型的构建和验证。 Promela基于Dijkstra 的非确定性卫式命令语言，语法类似于C 语言，并借鉴 Hoare CSP思想。它的建模方式是以进程为单位， 进程异步组合，同步则需要进行显式的声明。进程描述的基本要素包 括赋值语句，条件语句，通讯语句，非确定性选择和循环语句。Promela 程序由进程、信息通道和变量组成。进程是全局对象，而信息通道和 变量相对于一个进程可说明为全局的，也可说明为局部的。进程刻画 系统的行为，通道和全局变量用来定义进程执行的环境。 由于并发执行的程序在执行过程中各程序交替点的不确定性所引起对各程序的走停点及交替过程的不确定性、使得并发程序的描 述与时间变化密切相关。在时态逻辑中，时间并不是显式地表述，相 反，在公式中可能会描述某个指定状态最终（ eventually）会到达， 或者会描述某个错误状态从不（never）进入。性质eventually， never 可以用时态算子说明，这些算子也可以和逻辑连接词（、、?） 结合在一起或嵌套使用，构成更复杂的时态逻辑公式来描述并发系统 的性质。 CTL*公式由路径算子和时态算子组成。路径算子用来描述树中的分支结构，路径算子 A（All‖，对于所有的路径）和 E(Exist‖，存在某条路径)分别表示从某个状态出发的所有 路径或某些路径上具有某些性质（描述分枝情况）。时态算子描述经由树的某条路径的性质（描述状态的前后关系），时态算子具 体有：X（neXt‖）、 F(Future‖) 、G（Gobal‖）、U（Until‖）、 R（Release‖），直观含义分别为（其中Φ、为原子命题）： 对于某条路径为真，如果Φ在该路径的当前状态的下一 个状态为真； 对于某条路径为真，如果在该路径的某个状态为真， 而Φ在这个状态以前的所有状态都为真（U 为二元操作算子）； 在该路径的某个状态及以后所有状态为真，而Φ在这个状态以前的所有状态都为假（R 为二元 操作算子）。 CTL*中有二类公式：状态公式（其值在某个指定的状态上为真）和路径公式(其值沿着某指定的路径为真)。 CTL*是由下述规则生成的状态公式集（设AP为原子命题集， 是一个路径公式，则Ef，Af 是状态公式。 是状态公式，则f也是路径公式； Xf，Ff， Gf， fUg， fRg 是路径公式。 Kripke结构M用三元组 表示，路径?i 表示无穷状态序列?= s0 s1 s2 是一个状态公式，则M，sf表示在M中状态s 满足f， 表示在M中路径?满足g。 ―‖的递归定义如下(设f1、f2 为状态公式，g1、g2 为路径公式)： M，sf1f2?M，sf1 M，sf1f2?M，sf1 s1s2 g1?，?＝ss1 s2 ?f1?s，?＝ss1 s2 g1?g1g2? ?g2?g1 g2? CTL和LTL LTL[70][71][72][73][74][75][76][77]是二种模型检测工具中常用的时态逻辑， 模型检测工具SMV[78]、SPIN[79]中性质描述分别使用CTL、 LTL，它们都是CTL*的子逻 辑。二者的区别在于：分支时态逻辑CTL 是在状态的计算树 上解释的，对应于计算树上的每一个状态，要考虑它的一切可能的后 继状态（确定沿于某一给定状态的所有可能路径）；线性时态逻辑LTL 则是在状态的线性序列上解释的，状态之间按照一个隐含的时间参数 严格排序，对于每个状态都有唯一的后继状态。 CTL中路径算子和时态算子成对出现，而且路径算子后面必须有一个时态算子。使用下列规则对CTL*中的路径公式的语法加以限 制即得CTL公式： 是状态公式，则Xf， Ff， Gf， fUg， fRg 是路径 公式。 CTL公式存在线性时间的模型检测算法，即算法的最坏时 间复杂度与S*F成正比，这里S是状态迁移系统的大小，F 是CTL 逻辑公式的长度。 为LTL公式，路径公式f 中被允许的状态子公式只能 是原子命题，构建f 的语法规则为： Xf，Ff， Gf， fUg， fRg 是路径公式 [1]（文献中LTL的时态算子X、F、G 分别用〇、、表示）。 LTL模型检测的常用方法是将所要检测的性质即LTL公式的补转换成Bchi 自动机，然后求其与表示系统的自动机的交，如果交为 空，则说明系统满足所要检测的性质；否则生成对应反例 (counterexample)，说明不满足的原因。 2O世纪 9O 年代以来，研究取得突破性进展，对安全协议若干本 质性的问题有了更为深刻的认识。但是，这一领域还有许多问题有待 解决。Meadows[80]提出了安全协议领域的若干公开问题。我们当前 研究的协议大多数是认证协议，而电子商务协议、非否认协议、公平 交换等是另一个重要的协议及形式化分析领域。 模型检测技术分析密码协议，开启了模型检测技术新的应用领域，并且取得了公认的成功，并使密码协议的形式分析跨越了 BAN 类逻辑所存在的缺陷，向前进了一大步。 但模型检测技术分析密码 协议仍然存在着不少问题。如在协议及其环境条件下，如果小系统是 安全的，如何使得大系统也是安全的。尽管Gavin Lowe[26]提出一种 将大系统中协议安全性质的研究，化为小系统中协议安全性质研究的 方法，这是目前这一领域的最新理论研究成果，但是 仍然有待于我们去研究；另一个为解决的问题就是状态爆炸问题。模型检测基于对系统状态空间的穷举搜索，对于并发系统，其状 态数目往往随并发分量的增加成指数增长，当一个系统的并发分量较 多时，直接对其状态空间进行搜索是不可行的。这一点也是我们需要 继续去探讨的。 未来的研究趋势是如何扩充模型检测技术从而扩大可分析密码协议的种类，并和定理证明技术相结台，进而解决密码协议安全性 分析问题。 QingSH. Cryptography ComputerNetwork Security. Bering: Tsinghua University Press， 2001，127-147(in Chinese). QingSH. Formal analysis authenticationprotocols. Journal Software，1996， 7(Supplement)：107-114(inChinese Englishabstract). NeedhamR，Schroeder Usingencryption largenetworks OtwayD，Rees timelymutual authentication. Operating Systems Review，Proceedings LondonA，Vol MillerSP，Neuman C，Schiller JI，Saltzer JH. Kerberos authentication system.Project Athena Technical Plan Section draftrecommendation Directory-Authentication Framework， Version7，1987. DolevD，Yao publickey protocols. IEEE Transactions Hiddenassumptions cryptographicprotocols. Proceedings 137(6)：433-436. [10]van Oorschot PC. Extending cryptographic logics keyagreement protocols. 1stACM Conferenceon Computer CommunicationsSecurity. ACM —243. [11]Gollmmm Whatdo we mean entityauthentication? Privacy.Los Alamitos ：IEEE Computer Society ~54. [12]Clark J，Jacob survey authenticationprotocol literature： Version link＼mation technology--security techniques----entity authentication mechanisms part2：Entity authentication using symmetric [14]Satyanarayanan Integratingsecurity largedistributed Report， [15]ISO IEC.Information technology---security techniques----entity authentication mechanisms part4：Entity authentication using cryptographic check [16]Denning D，Sacco keydistribution protocols. Communications [17]Nenman BC，Stubblebine SG. nonces.Operating Systems [18]Kao IL，Chow secureauthentication protocol using uncertified keys. OperatingSystems Review，1995，29(3)：l4～21. [19]ISO IEC.Information technology~ security
