文献综述报告.docx

文献综述报告 论文文献综述 论文题目：中学教学数学审美实力的培育 班级： 数学102班 姓名： 黄强 学号：1020221211 目 录 1 前言 2 数学美学探讨现状 2.1近十年来数学美学探讨分成两个时期 2.2探讨简况 2.3主要探讨成果 3、数学美学的探讨发展方向 3.1对数学美本质的进一步探究 3.2数学美学科学体系的建立和形成 3.3数学美学思想史的探讨 3.4对数学美追求的方法论意义的探讨 4 小结 5 参考文献 1.前言 信息技术的飞速发展和网络技术的全面应用，将世界带入了一个计算机和网络深化千家万户的信息时代。随着网络应用的快速发展，信息平安的问题日益重要。信息平安不但关系国家的政治平安、经济平安、军事平安、社会稳定，也关系到社会中每一个人的数字化生存的质量。由于系统的设计缺陷、网络协议的脆弱性，以及人为因素造成的各种漏洞，都可能被攻击者加以利用进行网络攻击。信息平安问题已经成为全球性问题，没有信息平安，就没有真正的政治经济的平安。信息革命是否得以保障确定了信息革命给人类带来的高效率和高效益是否真正实现。西方发达国家非常重视信息平安，美国多年来始终将信息平安技术列为国防重点项目，并已形成浩大的信息平安产业。欧洲、日本、加拿大、澳大利亚和以色列等国也在信息平安领域投入巨资，拥有相当规模的信息平安产业。信息平安涵盖了许多的方面，比如操作系统平安，数据库平安，网络平安等等。 当前， 以Internet 为代表的国际互联网的热潮正在向社会的每一个角落渗，因此网络平安成为目前人们关注的一个热点。网络平安主要有两个方面的内容：密码算法和密码协议。密码协议又称为平安协议。它们构成了网络平安体系的两个层次：密码算法为网络上传递的消息供应高强度的加密解密操作和其他协助算法，而密码协议则在这些算法的基础上为各种网络平安性方面的需求供应实现方案。平安协议是基于密码算法的更高一层的算法，它为有平安需求的各方供应了一个步骤序列，以使它们能够平安地完成实体之间的认证、在实体之间平安地安排密钥或其他各种隐私、确认发送和接收的消息的非否认性等。网络平安不能单纯依靠平安的密码算法。平安协议是网络平安的一个重要组成部分。近年来，平安协议越来越多地用于爱护因特网上传送的各种交易。网络协议的平安性分析和验证是当今计算机平安领域的热点和重大课题。 阅历告知我们，设计和分析一个正确的平安协议是一项非常困难的任务。即使我们只探讨平安协议中最基本的认证协议，其中参与协议的主体只有两三个，交换的消息只有35条，设计一个正确的、符合认证目标的、没有冗余的认证协议也很不简单12¨ 。很多平安协议在提出之初被认为是足够平安的，然而在一段时间内被证明有漏洞。如：Needham-Schroeder3协议是最为闻名的早期的认证协议，该协议可分为对称密码体制和非对称密码体制下的两种版本，分别简称为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年，Boyd9通过实例指出，假如应用序列密码，则在NSSK 协议中，密文消息4与5之间的差别只有1个比特，协议极易受到攻击。 4、1993年，Van Oorschot10给出了关于认证协议的6种不同形式的认证目标：Ping认证、实体认证、平安密钥建立、密钥确认、密钥簇新性、相互信任共享密钥。 5、1996年，Gollmann11正式提出探讨认证协议的目标 6、1997年，Clark和Jacob12对平安协议进行了概括和总结，列举了一系列有探讨意义和好用价值的平安协议。他们将平安协议进行如下分类： (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-Sacco16协议、Woo-Lam 协议等。 (4)对称密钥重复认证协议。属于这一类的典型协议有Kerberos协议版本 5、Neuman-Stubblebine协议17、Kao-Chow重复认证协议18等。 (5)无可信第三方的公开密钥协议。属于这一类的典型协议包括以下ISO系列协议16：ISO公开密钥一遍单边认证协议、ISO 公开密钥二遍单边认证协议、ISO 公开密钥二遍相互认证协议、ISO 公开密钥三遍相互认证协议、ISO公开密钥二遍并行相互认证协议、Diffie-Hellman17协议等。 (6)具有可信第三方的公开密钥协议属于这一类的典型协议有NSPK协议3等。 7、1996年，Lowe21先采纳CSP(通信依次进程)方法和模型校验技术对平安协议进行形式化分析。他应用CSP模型和CSP模型校验工具FDR分析NSPK协议，并令人惊异地发觉了一个近l7年来未知的攻击。 8、Lowe的论文发表不久，Roscoe22对CSP和FDR的组合作了进一步的探讨。他们认为，CSP+FDR是形式化分析平安协议的一条新途径。模型校验技术是验证有限状态系统的自动化分析技术，是一种平安协议的自动验证工具。Lowe等学者应用CSP方法的胜利，促进了这一领域的发展。Schneider发表了一系列关于CSP方法应用的论文，应用CSP方法探讨平安协议的平安性质、匿名等问题；分析了各种平安协议，例如NSPK协议、非否认协议等。 9、美国卡内基.梅隆高校以Clarke教授为首的探讨小组，长期从事定理证明和自动校验的探讨。他们提出了一种通用的模型校验器，构造了一种新型的模型及其代数理论，并证明白该模型的有效性。Marrero，Clarke和Jha23应用该方法对NSPK协议进行分析。得到了与Lowe相同的结论21。Mitchell24的方法是通过状态计数工具Murphi分析平安协议，从平安协议可能到达的状态，分析平安协议是否平安。他应用Murphi分析了一系列闻名的平安协议，胜利地发觉了全部己知的攻击。 10、Thayer，Herzog和Guttman25-27提出了串空间(strand space)模型，这是一种结合定理证明和协议迹的混合方法。事实证明，串空间模型是分析平安协议的一种好用、直观和严格的形式化方法。 11、Perrig和Song28等人对串空间模型进行了重要的扩展，将其增加和优化，并将串空间模型推广到分析三方平安协议。Song应用串空间模型，研制出平安协议自动检验工具 A曲ena。Athena结合定理证明和模型校验技术，证明从一些初始状态起先，进行回退搜寻。初始状态是满意某种平安属性的。 2.2 平安协议形式化分析的历史与现状 网络环境被视为是担心全的，网络中的攻击者可以获得、修改和删除网上信息，并可限制网上用户，因此网络协议是易受攻击的。而协议形式化分析长期以来被视为分析协议平安性的有效工具。最早提出对平安协议进行形式化分析思想的是Needham和Schroeder3，他们提出了为进行共享和公钥认证的认证服务器系统的实现建立平安协议，这些平安协议引发了平安协议领域的很多重要问题的探讨。1981年Denning & Sacco在文献16中指出了NS私钥协议的一个错误，使得人们起先关注平安协议分析这一领域的探讨。真正在这一领域首先 3 做出工作的是Dolev和Yao8，紧随其后，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 Procees)，Lowe和Roscoe分别发展了不同的理论和方法把大系统中的协议平安性值得探讨约化为小系统中的协议平安性质的探讨；Millen开发的CAPSL(Common Authentication Protocol Specification Language)为协议形式化分析工具供应通用说明语言，标记着不同形式化分析技术的日趋成熟与集成；Bolignano运用Coq来分析大协议取得实效。第三种思想是推广和（或）完善协议模型，依据该模型提出有效地分析理论。顺应此趋势，Thayer和Herzog给出了Dolev-yao模型的深度理论说明，在文献25中提出了融合协议形式化分析中的多种思想和技术的Strand Space的概念，Paulson的归纳方法也是有力的。 3.形式化方法的概述 平安协议的分析设计方法也许可分为形式化和非形式化两种方法。非形式化的方法我们 在前面已经分析了他的缺陷，形式化的方法是当前对平安协议验证的主要方法和手段。形式化方法293031323334353637383940原则上就是采纳数学与逻辑的方法描述和验证系统。其描述主要包括三方面：一是系统行为的描述，也称建模(modeling)。即通过构造系统的模型来描述系统及其行为模式；二是系统性质的描述，也称规范或规约(specification)。即表示系统满意的一些性质如平安性、活性等。它们可以用一种或多种(规范)语言来描述。这些语言包括命题逻辑、一阶逻辑、高阶逻辑、时序逻辑、自动机、(并发)状态机、代效、进程代数、丌一演算、演算，特别的程序语言。以及程序语言的子集等。三是系统的验证(verification)。形式化验证主要包括两类方法。一类是以逻辑推理为基础的演绎验证(deductive verification)。另一类是以穷尽搜寻为基础的模型检测(model-checking)。用形式化的方法对平安认证协议41424344454647进行分析和验证要从以下几个方面着手。 3.1 模型检测及相关技术 模型检测484950515253运用状态空间搜寻的方法来全自动地检验一个有穷状态系统是否满意其设计规范。这类方法的优点在于它有全自动化的检测过程且验证速度快、效率高，并且假如一特性质不满意能给出这特性质不满意的理由，并指导对协议描述的进行改进。该方法自提出以来发展特别快速，其理论与技术得到了工业界和学术界的广泛关注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模型检测。 性质模型检测技术模型MTrue 或给出counterexample 图 一 由于模型检测基于状态搜寻的基本思想，搜寻的可穷尽性要求系统模型状态数有穷。故不能干脆对无穷状态系统进行验证。因此对于一般系统来说，首先须要有一个从随意状态到有限状态的建模过程。即使对于有穷状态系统，模型检测也会面临“状态空间爆炸(state space explosion)”的严峻问题。CTL或LTL模型检测方法一般采纳列表或表格等方式显式表示状态空间，这些状态空间图的大小与系统模型的状态数成正比，而模型的状态数与并发系统的大小成指数关系。因此随着所要检测的系统的规模增大，所要搜寻的状态空间呈指数增大，算法验证所需的时间空间困难度将超过实际所能承受的程度。 如何有效缓解“状态爆炸”是模型检测能被广泛运用的一个重要前提，在这方面已有一些重要的方法被相继提出，主要包括符号(模型检测)方法、抽象技术、偏序归约，分解与组合以及对称、归纳、On-the-fly方法等56。 目前，模型检测与其它方法的结合也取得了一些显著的成果。如模型检测与定理证明方法相结合；模型检测与测试方法相结合；模型检测与概率论方法相结合。 3.2 模型检测工具Spin 常用模型检测工具有：SPIN、SMV、CWB、DESIGNCPN，UPPAAL，KRONOS，HYTECH等，这些工具的选用与所验证的系统以及系统性质的表示有很大的关系，其中SPIN 5758596061626364是一种闻名的分析验证并发系统（特殊是数据通讯协议）逻辑一样性的工具，其目标是对软件而不是硬件高效验证。 G.J.Holzmann因开发SPIN的杰出贡献， 2002年荣获ACM Software System Award。 SPIN的开发探讨始于上世纪八十年头初，1980年Bell 试验室推出第一个验证系统Pan65（Protocol analyzer），它严格限制于对平安性验证；1983 年，Pan被更名为Trace，意味着验证方法从基于进程代数转变为基于自动机理论；1989年推出SPIN的第一个版本，作为一个小型的实例验证系统用来对协议进行验证66；1994 年SPIN提出了基于Partial-order reduction的静态归约技术STREM67（Static Reduction Method），次年利用内嵌算法68 扩充了由LTL公式到自动机自动转换的功能；1997 年提出对软件验证的Minimized Automata69思想，在某些状况下，能指数级地削减对内存的需求；1999 年在SPIN 3.3中，提出了Statement Merging技术，能大大地削减对内存的需求及缩短SPIN的验证时间；2000 年在自动模型抽取中引入Property-base Slicing技术，2001年SPIN 4.0 中通过一个模型抽取器的运用，能干脆支持对嵌入的C语言代码的检测。目前，最高版本为SPIN 4.2.0。 待验证的系统用Promela（PROce MEta LAnguage）建模后，进行语法检查，SPIN能通过随机或交互方式模拟此系统的执行，SPIN也可从系统的高级规约中生成一个优化的on-the-fly验证程序（C程序），此验证程序选择优化算法进行编译、运行得到验证结果。若在检测过程中，发觉了相背correctne claim的反例，那返回到交互模拟执行状态再接着细致诊断，确定产生反例的缘由。生成的相应C程序，可以穷尽系统状态空间验证。SPIN不仅可以作为LTL模型检测系统，对全部用LTL描述的系统性质进行验证，还可on-the-fly高效地验证许多勿需用LTL刻画的safety properties和 livene properties，同时还能验证invariants（aertions）正确性、是否存在死锁（deadlock）。SPIN模拟与验证流程见图二（其中XSPIN是用Tcl/Tk书写的驱动执行SPIN的图形前端界面）： 3.3 Promela 建模 Promela是模型检测工具spin供应的一种直观的设计规约语言，用于明确地描述（规约）系统设计选择要求，而不考虑详细实现细微环节，它是一种系统的描述语言。Promela供应对并发系统进行抽象的机制，而不考虑与进程交互无关的细微环节，相关进程行为用Promela建模。随着对Promela所建模型的逐步精化，相应地整个并发系统要经过一系列的验证步骤。 20一旦某个模型的正确性被SPIN所验证，那么此结论就可用于随后精化模型的构建和验证。 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为原子命题）： 若pÎAP， 则p是一个状态公式； 若f， g 是状态公式，则Øf， fg， fg是状态公式； 若f是一个路径公式，则Ef， Af是状态公式。 对应路径公式的语法规则如下： 若f是状态公式，则f 也是路径公式； 若f， g 是路径公式，则Øf， fg， fg， Xf， Ff， Gf， fUg， fRg是路径公式。 （2）CTL*的语义 Kripke结构M用三元组 表示，路径pi表示无穷状态序列p= s0 s1 s2 。中从s i 起先的后缀。 设f是一个状态公式，则M，sf表示在M中状态s满意f， 设g是一个路径公式，则M， pg表示在 M中路径p满意g。“”的递归定义如下(设f 1、f2为状态公式，g 1、g2为路径公式)： M，spÛpÎL(s) M，sØf1 Û M，s f1 M，sf1f2Û M，sf1 或M，sf2 M，sf1f2Û M，sf1 且 M，sf2 M，sE g1Û $p，ps s1 s2 。，M， pg1 。M，sA g1Û"p，ps s1 s2 。，M， pg1 。M， pf1Û$s，ps s1 s2 。 且 M，sf1 M， M， M， M， M， M， M， M， pØg1Û M， p g1 pg1g2Û M， pg1 或 M， pg2 pg1g2Û M， pg1 且M， pg2 pX g1Û M， p1g1 pF g1Û $ k，k0，M， pkg1 pG g1Û " i，i0，M， pig1 p g1 U g2 Û$k ，k0，M， pkg2 且"j ，0j g1 则 M， pjg2 简单看出只运用操作算子、Ø、X、U、E足以表达其它CTL*公式： fgºØ(ØfØg) f R gºØ(Øf U Øg) F fºTrue U f G fºØF Øf A(f) ºØE( Øf) 3.4.2 CTL和LTL CTL和LTL7071727374757677是二种模型检测工具中常用的时态逻辑， 模型检测工具SMV78、SPIN79中性质描述分别运用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的语法规则为： 若pÎAP， 则p是一个路径公式； 若f， g 是路径公式，则Øf， fg， fg， Xf， Ff， Gf， fUg， fRg是路径公式1（文献中LTL 的时态算子X、F、G分别用、表示）。 LTL模型检测的常用方法是将所要检测的性质即LTL公式的补转换成Büchi自动机，然后求其与表示系统的自动机的交，假如交为空，则说明系统满意所要检测的性质；否则生成对应反例(counterexample)，说明不满意的缘由。 4.小结 平安协议探讨的进展非常可喜，取得了丰富的探讨成果。特殊是2O世纪9O年头以来，探讨取得突破性进展，对平安协议若干本质性的问题有了更为深刻的相识。但是，这一领域还有很多问题有待解决。Meadows80提出了平安协议领域的若干公开问题。我们当前探讨的协议大多数是认证协议，而电子商务协议、非否认协议、公允交换等是另一个重要的协议及形式化分析领域。 模型检测技术分析密码协议，开启了模型检测技术新的应用领域，并且取得了公认的胜利，并使密码协议的形式分析跨越了BAN类逻辑所存在的缺陷，向前进了一大步。 但模型检测技术分析密码协议仍旧存在着不少问题。如在协议及其环境条件下，假如小系统是平安的，如何使得大系统也是平安的。尽管Gavin Lowe26提出一种将大系统中协议平安性质的探讨，化为小系统中协议平安性质探讨的方法，这是目前这一领域的最新理论探讨成果，但是 仍旧有待于我们去探讨；另一个为解决的问题就是状态爆炸问题。模型检测基于对系统状态空间的穷举搜寻，对于并发系统，其状态数目往往随并发重量的增加成指数增长，当一个系统的并发重量较多时，干脆对其状态空间进行搜寻是不行行的。这一点也是我们须要接着去探讨的。 将来的探讨趋势是如何扩充模型检测技术从而扩大可分析密码协议的种类，并和定理证明技术相结台，进而解决密码协议平安性分析问题。 5.参考文献 1 Qing SH.Cryptography and Computer Network Security.Bering: Tsinghua University Pre， 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)：198208 9 Boyd C.Hidden aumptions 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 Pre.1993.233243.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 Pre.1996.4654.12 Clark J，Jacob J.A survey of authentication protocol literature：Version 1.0.1997.http：/wwwusers.cs.york.ac.ukjacunder the linkSecurity Protocols Review.13 ISOIEC.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 ISOIEC.Information technology-security techniques-entity authentication mechanisms part 4：Entity authentication using cryptographic check functions.1993. 10 16 Denning D，Sacco G.Timestamps in key distribution protocols.Communications of the ACM，1981，24(8)：533536.17 Nenman BC，Stubblebine SG.A note on the u