《文献综述报告-范文.docx》由会员分享，可在线阅读，更多相关《文献综述报告-范文.docx（15页珍藏版）》请在课桌文档上搜索。
1、论文文献综述论文题目：中学教学数学审美能力的培养班级：数学102班姓名：黄强学号：10201512111前言2数学美学研究现状2.1近十年来数学美学研究分成两个时期2.2研究简况2.3主要研究成果3、数学美学的研究开展方向3.1 对数学美本质的进一步探索3.2 数学美学科学体系的建立和形成3.3 数学美学思想史的研究3.4 对数学美追求的方法论意义的研究4小结5参考文献1.前言信息技术的飞速开展和网络技术的全面应用，将世界带入了一个计算机和网络深入千家万户的信息时代。随着网络应用的迅速开展，信息平安的问题日益重要。信息平安不但关系国家的政治平安、经济平安、军事平安、社会稳定，也关系到社会中每一
2、个人的数字化生存的质量。由于系统的设计缺陷、网络协议的脆弱性，以及人为因素造成的各种漏洞，都可能被攻击者加以利用进行网络攻击。信息平安问题已经成为全球性问题，没有信息平安，就没有真正的政治经济的平安。信息革命是否得以保障决定了信息革命给人类带来的高效率和高效益是否真正实现。西方兴旺国家十分重视信息平安，美国多年来一直将信息平安技术列为国防重点工程，并已形成庞大的信息平安产业。欧洲、日本、加拿大、澳大利亚和以色列等国也在信息平安领域投入巨资，拥有相当规模的信息平安产业。信息平安涵盖了很多的方面,比方操作系统平安，数据库平安，网络平安等等。当前，以Internet为代表的国际互联网的热潮正在向社会
3、的每一个角落渗，因此网络平安成为目前人们关注的一个热点。网络平安主要有两个方面的内容：密码算法和密码协议。密码协议又称为平安协议。它们构成了网络平安体系的两个层次：密码算法为网络上传递的消息提供高强度的加密解密操作和其他辅助算法，而密码协议那么在这些算法的根底上为各种网络平安性方面的需求提供实现方案。平安协议是基于密码算法的更高一层的算法，它为有平安需求的各方提供了一个步骤序列，以使它们能够平安地完成实体之间的认证、在实体之间平安地分配密钥或其他各种秘密、确认发送和接收的消息的非否认性等。网络平安不能单纯依靠平安的密码算法。平安协议是网络平安的一个重要组成局部。近年来,平安协议越来越多地用于保
4、护因特网上传送的各种交易。网络协议的平安性分析和验证是当今计算机平安领域的热点和重大课题。经验告诉我们，设计和分析一个正确的平安协议是一项十分困难的任务。即使我们只讨论平安协议中最根本的认证协议，其中参加协议的主体只有两三个，交换的消息只有35条，设计一个正确的、符合认证目标的、没有冗余的认证协议也很不容易12。许多平安协议在提出之初被认为是足够平安的，然而在一段时间内被证明有漏洞。如：Needham-Schroeder3协议是最为著名的早期的认证协议，该协议可分为对称密码体制和非对称密码体制下的两种版本，分别简称为NSSK协议和NSPK协议。从1978年NSPK协议问世以来，到LoWe于19
5、96年发现NSPK协议的平安缺陷，已经过去了大约17年之久。平安协议设计的困难性和平安协议分析的微妙性，由此可见一斑。这些漏洞严重的威胁了网络平安。目前越来越多的平安协议不断地涌现，伴随着相应协议的漏洞也会不断产生。因此对协议进行平安分析找出协议漏洞并修改相应协议成为当前的热点也是难点。平安协议的分析设计方法大概可分为形式化和非形式化两种方法。非形式化的方法根据的各种攻击方法来对协议进行攻击，以攻击是否有效来检验密码协议是否平安，是早期的密码协议平安分析所采用形式。长期以来，密码学专家一直依赖经验性的指导原那么来设计密码协议，但事实说明非形式化的设计方法很容易忽略掉-些微妙的直觉难以发现的漏洞
6、。这种方法只是停留于发现协议中是否存在的缺陷，而不能全面客观地分析密码协议。因此在密码协议的分析过程中引入形式化方法就成为必然。2 .平安协议及平安协议形式化分析领域研究现状2.1 平安协议开展的20年1、从1978年NeedhanI-Schroeder协议的诞生算起，平安协议的开展已经历经20余年了。除了NSSK协议和NSPK协议之外，早期著名的经典平安协议还有OtWay-Rees协议4、Yahalom协议5、大嘴青蛙协议5等，以及一些重要的实用协议，如KeberoS协议6、CCITTXo509协议7等。2、1983年，DoIeV和Yao发表了平安协议开展史上的一篇重要的论文8。该论文的主要
7、奉献有两点。第一点是将平安协议本身与平安协议所具体采用的密码系统分开，在假定密码系统是“完善”的根底上讨论平安协议本身的正确性、平安性、冗余性等课题。从此，学者们可以专心研究平安协议的内在平安性质了。亦即，问题很清楚地被划分为两个不同的层次：首先研究平安协议本身的平安性质，然后讨论实现层次的具体细节，包括所采用的具体密码算法等等。第2点奉献是，DoleV和Yao建立了攻击者模型。他们认为，攻击者的知识和能力不能够低估，攻击者可以控制整个通信网络。DoIeV和Yao认为攻击者具有如下能力：(1)可以窃听所有经过网络的消息；(2)可以阻止和截获所有经过网络的消息；(3)可以存储所获得或自身创造的消
8、息；(4)可以根据存储的消息伪造消息，并发送该消息；(5)可以作为合法的主体参与协议的运行。DoleV和Yao的工作具有深远的影响。迄今为止，大局部有关平安协议的研究工作都遵循DoIeV和YaO的根本思想。3、1990年，BOyd9通过实例指出，如果应用序列密码，那么在NSSK协议中，密文消息4与5之间的差异只有1个比特，协议极易受到攻击。4、1993年，VanoOrSChOt10给出了关于认证协议的6种不同形式的认证目标：Ping认证、实体认证、平安密钥建立、密钥确认、密钥新鲜性、互相信任共享密钥。5、1996年，GoIhnannn1正式提出讨论认证协议的目标6、1997年，Clark和Ja
9、Cob12对平安协议进行了概括和总结，列举了一系列有研究意义和实用价值的平安协议。他们将平安协议进行如下分类：(D无可信第三方的对称密钥协议。属于这一类的典型协议包括以下ISO系列协议13：ISO对称密钥一遍单边认证协议、ISO对称密钥二遍单边认证协议、ISO对称密钥二遍相互认证协议、ISO对称密钥三遍相互认证协议、AndreW平安RPC协议等14。(2)应用密码校验函数(CCF)的认证协议。属于这一类的典型协议包括以下ISO系列协议15：ISO应用CCF的一遍单边认证协议、ISO应用CCF的二遍单边认证协议、ISO应用CCF的二遍相互认证协议、ISO应用CCF的三遍相互认证协议。(3)具有可
10、信第三方的对称密钥协议3。属于这一类的典型协议包括NSSK协议、OtWay-Rees协议、Yahalom协议、大嘴青蛙协议、Denning-SaCCo16协议、Woo-Lam协议等。(4)对称密钥重复认证协议。属于这一类的典型协议有KerberOS协议版本5、NeUman-StUbbIebine协议17、Kao-Chow重第认证协议18等。(5)无可信第三方的公开密钥协议。属于这一类的典型协议包括以下ISo系列协议16：ISO公开密钥一遍单边认证协议、ISO公开密钥二遍单边认证协议、ISO公开密钥二遍相互认证协议、ISO公开密钥三遍相互认证协议、ISO公开密钥二遍并行相互认证协议、Diffie
11、Telhnan17协议等。(6)具有可信第三方的公开密钥协议属于这一类的典型协议有NSPK协议3等。7、1996年，LOWe21先采用CSP(通信顺序进程)方法和模型校验技术对平安协议进行形式化分析。他应用CSP模型和CSP模型校验工具FDR分析NSPK协议，并令人惊讶地发现了一个近17年来未知的攻击。8、LoWe的论文发表不久，RoSCOe22对CSP和FDR的组合作了进一步的研究。他们认为，CSP+FDR是形式化分析平安协议的一条新途径。模型校验技术是验证有限状态系统的自动化分析技术，是一种平安协议的自动验证工具。LoWe等学者应用CSP方法的成功，促进了这一领域的开展。SChneider
12、发表了一系列关于CSP方法应用的论文，应用CSP方法讨论平安协议的平安性质、匿名等问题；分析了各种平安协议,例如NSPK协议、非否认协议等。9、美国卡内基.梅隆大学以CIarke教授为首的研究小组，长期从事定理证明和自动校验的研究。他们提出了一种通用的模型校验器，构造了一种新型的模型及其代数理论，并证明了该模型的有效性。Marrero,Clarke和Jha23应用该方法对NSPK协议进行分析。得到了与Lowe相同的结论21。MiteheIl24的方法是通过状态计数工具MKPhi分析平安协议，从平安协议可能到达的状态，分析平安协议是否平安。他应用MUrPhi分析了一系列著名的平安协议，成功地发现
13、了所有己知的攻击。10、Thayer,HerZOg和GUttnIan25-27提出了串空间(StrandSPaCe)模型，这是种结合定理证明和协议迹的混合方法。事实证明，串空间模型是分析平安协议的一种实用、直观和严格的形式化方法。11、Perrig和Song28等人对串空间模型进行了重要的扩展，将其增强和优化，并将串空间模型推广到分析三方平安协议。Song应用串空间模型，研制出平安协议自动检验工具A曲ena。Athena结合定理证明和模型校验技术，证明从一些初始状态开始，进行回退搜索。初始状态是满足某种平安属性的。2.2 平安协议形式化分析的历史与现状网络环境被视为是不平安的，网络中的攻击者可
14、以获取、修改和删除网上信息，并可控制网上用户，因此网络协议是易受攻击的。而协议形式化分析长期以来被视为分析协议平安性的有效工具。最早提出对平安协议进行形式化分析思想的是Needham和SChrOeder3,他们提出了为进行共享和公钥认证的认证效劳器系统的实现建立平安协议，这些平安协议引发了平安协议领域的许多重要问题的研究。1981年Denning&SaCeO在文献16中指出了NS私钥协议的一个错误，使得人们开始关注平安协议分析这一领域的研究。真正在这一领域首先做出工作的是DOlev和Yao8,紧随其后，Dolev,EVen和KarP在20世纪七八十年代开发了一系列的多项式时间算法，用于对一些协
15、议的平安性进行分析。DOleV和YaO所作的工作是十分重要的。此后的协议形式化分析模型大多基于此或此模型的变体。如InterrOgato八NRL协议分析器和LOngIey-Rigby工具。在此根底上开展起来的大多数形式化分析工具都采用了状态探测技术，即定义一个状态空间，对其探测已确定是否存在一条路经对应于攻击者的一次成功的攻击。有些工具中用到了归纳定理推证技术，如在NRL协议分析其中运用此技术证明搜索的空间规模已经可以确保平安性。在形式化分析技术出现的早期阶段，它已成功地发现了协议中不为人工分析所发现的缺陷等。如NRL协议分析器发现了SimnIOnSSelectiveBrOadCaSt协议的缺
16、陷，Longley-Rigby工具发现了banking协议的缺陷等。尽管如此，直到1989年，BurrowsAbadi和Needham提出了BAN逻辑之后才打破了形式化分析技术这一领域的神秘感，并从此逐步引起人们广泛的关注。BAN逻辑采用了与状态探测技术完全不同的方法，它是关于主体拥有的知识与信仰以及用于从已有信仰推知新的信仰的推理规那么的逻辑。这种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接受消息从最初的信仰逐渐开展到协议运行最终要到达的目的一认证双方的最终信仰。BAN逻辑的规那么十分简洁和直观，因此易于使用。BAN逻辑成功地对Needham-SChroeder协议
17、、KerberoS协议等几个著名的协议进行了分析，找到了其中的和未知的漏洞。BAN逻辑的成功极大的激发了密码研究者对平安协议形式化分析的兴趣，并导致许多平安协议形式化方法的产生。但BAN逻辑还有许多缺乏，出现这样的为难局面：当逻辑发现协议中的错误时，每个人都相信那确实是有问题；但当逻辑证明一个协议是平安的时，却没人敢相信它的正确性。协议形式化分析技术目前主要有三类。第一类是以BAN逻辑为代表的基于推理结构性方法，第二类是基于攻击结构性方法，第三类是基于证明结构性方法。沿着第一个思路，BraCkin推广了GNY逻辑并给出了该逻辑的高阶逻辑(HOL)理论，之后利用HOL理论自动证明在该系统内与平安
18、相关的命题。第二种思路是近年来的研究焦点，大量一般目的的形式化方法被用于这一领域，并取得了大量成果。LoWe在文献21中证明了可用RUSCoe的模型检测程序FDR发现对NeedhanI-SChroeder公钥协议的一个中间人攻击行为，这引发了人们将协议形式化分析研究的热点集中于基于DoIeVTao模型的状态检测和定理推证技术上。MitCheIl和Stern使用Dill的MUr模型检测程序对Needham-SChrOeder公钥协议、TMN和KerberOS协议进行分析；基于进程代数CSP(ComnlUniCatingSeqUentialProcesses),LOWe和ROSCoe分别开展了不同
19、的理论和方法把大系统中的协议平安性值得研究约化为小系统中的协议平安性质的研究；MiIIen开发的CAPSL(COmmOnAuthenticationProtocolSpecificationLangUage)为协议形式化分析工具提供通用说明语言，标志着不同形式化分析技术的日趋成熟与集成；BoIignanO使用COq来分析大协议取得实效。第三种思想是推广和(或)完善协议模型，根据该模型提出有效地分析理论。顺应此趋势，Thayer和HerZog给出了Dolev-yao模型的深度理论说明，在文献25中提出了融合协议形式化分析中的多种思想和技术的StrandSPaCe的概念，Paulson的归纳方法也
20、是有力的。3 .形式化方法的概述平安协议的分析设计方法大概可分为形式化和非形式化两种方法。非形式化的方法我们在前面已经分析了他的缺陷，形式化的方法是当前对平安协议验证的主要方法和手段。形式化方法293031323334353637383940原那么上就是采用数学与逻辑的方法描述和验证系统。其描述主要包括三方面：一是系统行为的描述，也称建模Gnodeling)。即通过构造系统的模型来描述系统及其行为模式；二是系统性质的描述，也称标准或规约(SPeCifiCation)。即表示系统满足的一些性质如平安性、活性等。它们可以用一种或多种(标准)语言来描述。这些语言包括命题逻辑、一阶逻辑、高阶逻辑、时序
21、逻辑、自动机、(并发)状态机、代效、进程代数、TT一演算、演算，特殊的程序语言。以及程序语言的子集等。三是系统的验证(VerifiCatiOn)。形式化验证主要包括两类方法。一类是以逻辑推理为根底的演绎验证(deductiveverification)。另一类是以穷尽搜索为根底的模型检测(modeI-CheCking)。用形式化的方法对平安认证协议41424344454647进行分析和验证要从以下几个方面着手。3.1 模型检测及相关技术模型检测484950515253使用状态空间搜索的方法来全自动地检验一个有穷状态系统是否满足其设计标准。这类方法的优点在于它有全自动化的检测过程且验证速度快、效
22、率高，并且如果一个性质不满足能给出这个性质不满足的理由，并指导对协议描述的进行改良。该方法自提出以来开展非常迅速，其理论与技术得到了工业界和学术界的广泛关注54。目前许多世界著名大公司如AT&T、FujitsulnterIBM、Microsoft%LucentMotorolaSiemenS等纷纷在其产品设计和开发过程中使用模型检测技术，并在许多复杂的实例研究中发挥了重要的作用。模型检测是一种基于算法的性质验证方法。即对于一类给定的有穷状态并发程序(系统)和表示系统性质(或标准)的某种时序逻辑公式，能否找到一算法，判定系统类中的任一给定系统是否满足公式类中任意给定的一个时序逻辑式。如图1所示，模
23、型检测算法的输入包括二局部，分别是待验证系统的模型M和系统待检测性质的描述中，如模型M满足性质中。那么算法输出“true”；否那么给出反例说明M为何不满足中。系统建模、性质描述和算法验证是模型检测技术的三个主要步骤。最初的模型检测算法由E。M,Clarke.EoA,Emerson、Queille,SifakiS等人在20世纪80年代初期提出55,他们采用分支时序逻辑CTL来描述系统的性质，又称为CTL模型检测；稍后又出现了线性时序逻辑LTL模型检测。性质中I模型MATrUe或给出counterexample图一由于模型检测基于状态搜索的根本思想，搜索的可穷尽性要求系统模型状态数有穷。故不能直接
24、对无穷状态系统进行验证。因此对于一般系统来说，首先需要有一个从任意状态到有限状态的建模过程。即使对于有穷状态系统，模型检测也会面临“状态空间爆炸(Statespaceexplosion),的严重问题。CTL或LTL模型检测方法一般采用列表或表格等方式显式表示状态空间，这些状态空间图的大小与系统模型的状态数成正比，而模型的状态数与并发系统的大小成指数关系。因此随着所要检测的系统的规模增大，所要搜索的状态空间呈指数增大，算法验证所需的时间/空间复杂度将超过实际所能承受的程度。如何有效缓解“状态爆炸”是模型检测能被广泛使用的一个重要前提，在这方面已有一些重要的方法被相继提出，主要包括符号(模型检测)
25、方法、抽象技术、偏序归约，分解与组合以及对称、归纳、On-the-fIy方法等56。目前，模型检测与其它方法的结合也取得了一些显著的成果。如模型检测与定理证明方法相结合；模型检测与测试方法相结合；模型检测与概率论方法相结合。3.2 模型检测工具Spin常用模型检测工具有：SPIN、SMV.CWBDESIGN/CPN,UPPAAL,KRoNOS,HYTECH等，这些工具的选用与所验证的系统以及系统性质的表示有很大的关系，其中SPIN5758596061626364是一种著名的分析验证并发系统(特别是数据通讯协议)逻辑一致性的工具，其目标是对软件而不是硬件高效验证。G.J.Holzmann因开发S
26、PIN的杰出奉献，2002年荣获ACM“SoftwareSystemAward”。SPlN的开发研究始于上世纪八十年代初，1980年BeIl实验室推出第一个验证系统Pan65(Protocolanalyzer),它严格限制于对平安性验证；1983年，Pan被更名为TraCe,意味着验证方法从基于进程代数转变为基于自动机理论；1989年推出SPIN的第一个版本，作为一个小型的实例验证系统用来对协议进行验证66；1994年SPlN提出了基于PartiaI-Orderreduction的静态归约技术STREM67(StaticReductionMethod),次年利用内嵌算法68扩充了由LTL公式到
27、自动机自动转换的功能；1997年提出对软件验证的MinimiZedAUtOmata69思想，在某些情况下，能指数级地减少对内存的需求；1999年在SPlN3.3中，提出了StatementMerging技术，能大大地减少对内存的需求及缩短SPlN的验证时间；2000年在自动模型抽取中引入ProPerty-baseSIiCing技术，2001年SPIN4.0中通过一个模型抽取器的使用，能直接支持对嵌入的C语言代码的检测。目前，最高版本为SPIN4.2.0。待验证的系统用Promela(PROcessMEtaLAngUage)建模后，进行语法检查，SPlN能通过随机或交互方式模拟此系统的执行，SP
28、IN也可从系统的高级规约中生成一个优化的On-Ihe-fly验证程序IC程序)，此验证程序选择优化算法进行编译、运行得到验证结果。假设在检测过程中，发现了相背CorreCtneSSclaim的反例，那返回到交互模拟执行状态再继续仔细诊断，确定产生反例的原因。生成的相应C程序，可以穷尽系统状态空间验证。SPlN不仅可以作为LTL模型检测系统，对所有用LTL描述的系统性质进行验证，还可On-Ihe-fly高效地验证很多勿需用LTL刻画的SafetypropertiesIIivenessproperties,同时还能验证invariants(assertions)止确性、是否存在死锁(deadloc
29、k)SPIN模拟与验证流程见图二(其中XSPIN是J3acftvePromela model MSunUatcwTtSdataSyntax checkXSPtNVEIfietOeneratovSdng windowSmu!aon OPnoBWrficaon QphovzMSC Hmulefion windowxunp%checker用TclZTk书写的驱动执行SPIN的图形前端界面）：图2Spin的T件机理3.3 Promela建模ProInela是模型检测工具SPin提供的一种直观的设计规约语言，用于明确地描述（规约）系统设计选择要求，而不考虑具体实现细节，它是一种系统的描述语言。Prome
30、la提供对并发系统进行抽象的机制，而不考虑与进程交互无关的细节，相关进程行为用PrOmeIa建模。随着对PromeIa所建模型的逐步精化，相应地整个并发系统要经过一系列的验证步骤。一旦某个模型的正确性被SPIN所验证，那么此结论就可用于随后精化模型的构建和验证侬、Promela基于DijkSIra的非确定性卫式命令语言，语法类似于C语言，并借鉴HOare的CSP思想。它的建模方式是以进程为单位，进程异步组合，同步那么需要进行显式的声明。进程描述的根本要素包括赋值语句，条件语句，通讯语句，非确定性选择和循环语句。Promela程序由进程、信息通道和变量组成。进程是全局对象，而信息通道和变量相对于
31、一个进程可说明为全局的，也可说明为局部的。进程刻画系统的行为，通道和全局变量用来定义进程执行的环境。3.4 时态逻辑由于并发执行的程序在执行过程中各程序交替点的不确定性所引起对各程序的走停点及交替过程的不确定性、使得并发程序的描述与时间变化密切相关。在时态逻辑中，时间并不是显式地表述，相反,在公式中可能会描述某个指定状态最终（eventually）会到达，或者会描述某个错误状态从不（never）进入。性质eventually,never可以用时态算子说明，这些算子也可以和逻辑连接词（V）结合在一起或嵌套使用，构成更复杂的时态逻辑公式来描述并发系统的性质。3.4.1 计算树逻辑（CTL*）CTL
32、*公式由路径算子和时态算子组成。路径算子用来描述树中的分支结构，路径算子A（-A1,对于所有的路径）和E（Exist”，存在某条路径）分别表示从某个状态出发的所有路径或某些路径上具有某些性质（描述分枝情况）。时态算子描述经由树的某条路径的性质（描述状态的前后关系），时态算子具体有:X（“neXt）、F（Future）、GLGOba1”）、U（Until”）、R（Release），直观含义分别为（其中、甲为原子命题）：X对于某条路径为其，如果在该路径的当前状态的下一个状态为真；F中对于某条路径为真，如果在该路径的某个状态中为真；G中对于一条路径为真，如果在该路径的所有状态都为真；中U中对于某条路
33、径为真，如果中在该路径的某个状态为真，而中在这个状态以前的所有状态都为真（U为二元操作算子）；9RW对于某条路径为真，如果中在该路径的某个状态及以后所有状态为真，而在这个状态以前的所有状态都为假（R为二元操作算子）。CTL*中有二类公式：状态公式（其值在某个指定的状态上为真）和路径公式（其值沿着某指定的路径为真）。（1） CTL*语法CTL*是由下述规那么生成的状态公式集（设AP为原子命题集，P为原子命题）：假设pAP,那么p是一个状态公式；假设f,g是状态公式，那么f,fVg,fg是状态公式；假设f是一个路径公式，那么Ef,Af是状态公式。对应路径公式的语法规那么如下：假设f是状态公式，那么
34、f也是路径公式；假设f,g是路径公式，那么f,fVg,fg,Xf,Ff,Gf,fUg,fRg是路径公式。（2） CTL*的语义KriPke结构M用三元组S,R,L表示，路径；ri表示无穷状态序列乃二SOSlS2中从s,开始的后缀。设f是一个状态公式，那么M,s建表示在M中状态S满足3设g是一个路径公式，那么M,卜g表示在M中路径乃满足g。“卜”的递归定义如下（设0、f2为状态公式，gg2为路径公式）：M, s卜POPL（s）M,S卜一IflM,sfN, skfjVf2OM,sp,f或M,sHf2O, s11ff2M,sHfi且M,sFf2P, S卜EgIo3,乃=SSIS2.，M,冗FgiQ,
35、 SkAgI乃，乃=ssiS2.，M,pgR, -f3s,乃=SSlS2且M,s11fM,I-IgloM,gM,M,M,M,M,M,bg1Vg2M,hg或M,Hg2 X g M, , HgiFg1g2M,万卜gi且M,三g2HFg3k,k20,M,乃k-g1兀-GgDi,i20,M,乃,Fg1Fgi冗FgUg23k,k20,M,万lH2且Vj,0jk,M,M,HgRg2j0,假设Vi,ifU-Ig)Ff三TrueUfGf三-IF-fA(f)三一E(-f)3.4.2CTL和LTLCTL和LTL7071727374757677是二种模型检测工具中常用的时态逻辑,模型检测工具SMV78、SPIN79
36、中性质描述分别使用CTL、LTL,它们都是CTL*的子逻辑。二者的区别在于：分支时态逻辑CTL是在状态的计算树上解释的，对应于计算树上的每一个状态，要考虑它的一切可能的后继状态(确定沿于某一给定状态的所有可能路径)；线性时态逻辑LTL那么是在状态的线性序列上解释的，状态之间按照一个隐含的时间参数严格排序，对于每个状态都有唯一的后继状态。CTL中路径算子和时态算子成对出现，而且路径算子后面必须有一个时态算子。使用以下规那么对CTL*中的路径公式的语法加以限制即得CTL公式：假设f,g是状态公式，那么Xf,Ff,Gf,fUg,fRg是路径公式。对CTL公式存在线性时间的模型检测算法，即算法的最坏时
37、间复杂度与ISI*IFI成正比，这里ISI是状态迁移系统的大小，IFl是CTL逻辑公式的长度。形如Af为LTL公式，路径公式f中被允许的状态子公式只能是原子命题，构建f的语法规那么为:假设pAP,那么p是一个路径公式；假设f,g是路径公式，那么f,fVg,fg,Xf,Ff,Gf,fUg,fRg是路径公式(文献中LTL的时态算子X、F、G分别用O、口表示)。1.TL模型检测的常用方法是将所要检测的性质即LTL公式的补转换成Buchi自动机,然后求其与表示系统的自动机的交，如果交为空，那么说明系统满足所要检测的性质；否那么生成对应反例(counterexample),说明不满足的原因。4.小结平安
38、协议研究的进展十分可喜，取得了丰富的研究成果。特别是20世纪90年代以来，研究取得突破性进展，对平安协议假设干本质性的问题有了更为深刻的认识。但是，这一领域还有许多问题有待解决。MeadOWS80提出了平安协议领域的假设干公开问题。我们当前研究的协议大多数是认证协议，而电子商务协议、非否认协议、公平交换等是另一个重要的协议及形式化分析领域。模型检测技术分析密码协议，开启了模型检测技术新的应用领域，并且取得了公认的成功，并使密码协议的形式分析跨越了BAN类逻辑所存在的缺陷，向前进了一大步。但模型检测技术分析密码协议仍然存在着不少问题。如在协议及其环境条件下，如果小系统是平安的，如何使得大系统也是
39、平安的。尽管GaVinLoWe26提出一种将大系统中协议平安性质的研究，化为小系统中协议平安性质研究的方法，这是目前这一领域的最新理论研究成果，但是仍然有待于我们去研究；另一个为解决的问题就是状态爆炸问题。模型检测基于对系统状态空间的穷举搜索，对于并发系统，其状态数目往往随并发分量的增加成指数增长，当一个系统的并发分量较多时，直接对其状态空间进行搜索是不可行的。这一点也是我们需要继续去探讨的。未来的研究趋势是如何扩充模型检测技术从而扩大可分析密码协议的种类，并和定理证明技术相结台，进而解决密码协议平安性分析问题。5.参考文献1 QingSH.CryptographyandComputerNet
40、workSecurity.Bering:TsinghuaUniversityPress,2001,127-147(inChinese).2 QingSH.Formalanalysisofauthenticationprotocols.JournalofSoftware,19967(Supplement):107-114(inChinesewithEnglishabstract).3 NeedhamR,SchroederM.Usingencryptionforauthenticationinlargenetworksofcomputers.CommunicationsoftheACM,1978,
41、21(12)：993-999.4 OtwayD,ReesO.Efficientandtimelymutualauthentication.OperatingSystemsReview,1987,21(1)：8-10.5 BurrowsM,AbadiM，NeedhamR.Alogicofauthentication.In：ProceedingsoftheRoyalSocietyofLondonA,Vol426.1989.233-271.6 MillerSPNeumanCSchillerJI,SaltzerJH.Kerberosauthenticationandauthorizationsyste
42、m.ProjectAthenaTechnicalPlanSectionE.2.1,MIT,1987.7 CCITT.CCITTdraftrecommendationX.509.TheDirectory-AuthenticationFramework,Version7,1987.8 DolevD,YaoA.Onthesecurityofpublickeyprotocols.IEEETransactionsonInformationTheory,198329(2)：198-2089 BoydC.Hiddenassumptionsincryptographicprotocols.Proceeding
43、softheIEEE,1990,137(6)：433-436.1 vanOorschotPC.Extendingcryptographiclogicsofbelieftokeyagreementprotocols.In：Proceedingsofthe1stACMConferenceonComputerandCommunicationsSecurity.ACMPress.1993.233243.2 GollmmmD.Whatdowemeanbyentityauthentication?In：ProceedingsoftheIEEESymposiumonSecurityandPrivacy.Lo
44、sAlamitos：IEEEComputerSocietyPress.1996.46-54.12 ClarkJ,JacobJ.Asurveyofauthenticationprotocolliterature：Version1.0.1997.：/Zwwwusers.cs.york.ac.uk/jac/underthelinkSecurityProtocolsReview.13 ISO/IEC.Informationtechnologysecuritytechniquesentityauthenticationmechanismspart2：Entityauthenticationusingsy
45、mmetrictechniques.1993.14 SatyanarayananM.Integratingsecurityinalargedistributedsystem.TechnicalReport,CMU-CS,CMU,1987.87-179.15 ISO/IEC.Informationtechnology-securitytechniquesentityauthenticationmechanismspart4：Entityauthenticationusingcryptographiccheckfunctions.1993.16DenningD,SaccoG.Timestampsi
46、nkeydistributionprotocols.CommunicationsoftheACM,1981,24(8)：533536.17 NenmanBC,StubblebineSG.Anoteontheuseoftimestampsasnonces.OperatingSystemsReview,1993,27(2)：10-14.18 KaoIL,ChowR.Anefficientandsecureauthenticationprotocolusinguncertifiedkeys.OperatingSystemsReview,1995,29(3)：1421.19 ISO/IEC.Infor
47、mationtechnology-securitytechniquesentityauthenticationmechanismspart3：Entityauthenticationusingapublickeyalgorithm.1995.20 DifieW,HelhnanME.Newdirectionsincryptography.IEEETransactionsonInfonnatkmTheory,1976,IT-22(6):644-4554.21 1.oweG.BreakingandfixingtheNeedham-Schroederpublic-keyprotocolusingFDR-Software-ConceptsandTools,1996,17：93-102.222324252612728
