本科毕业论文---基于公开密钥认证协议安全性的分析与研究.doc

题目：基于公开密钥认证协议安全性的分析与研究 基于公开密钥认证协议安全性的分析与研究摘 要 公开密钥认证协议安全性分析与研究对于促进我国信息化建设以及网络安全和信息安全研究具有非常重要的意义。本文主要研究运用模型检测技术和基于模型检测技术的运行模式分析法，并研究了公开密钥认证协议的理论与技术。在此基础上，对公开密钥认证协议进行了运行模式的手工分析。研究成果如下： 系统介绍了公开密钥认证协议的基本概念及安全性分析的重要意义、研究进展和现状。 研究了模型检测技术以及公开密钥认证协议运行模式分析法。 给出了运用模型检测工具SMV分析公开密钥认证协议的方法。 研究了公开密钥认证协议，运用运行模式分析法分析公开密钥认证协议的安全性，成功地发现了该协议的安全漏洞。并在学习了SMV模型检测工具的基础上，研究了公开密钥认证协议的SMV检测程序的框架和数据结构。 关键词：公开密钥认证协议，模型检测协议分析，形式方法，运行模式分析法， SMVAbstractAnalysis of security protocols has a significance to promote the information construction and the research of the network and the information security in our country. This dissertation focuses on the theory and the technique of the model checking of the security protocols. Following are the main results of this thesis: Introduce the basic conception, the significance, the evolvement and the state of the cryptographic protocols analysis. Study the methods of model checking and running modes. Give the method of model checking by using the sofeware of Symbolic Model Verifier to analysis protocol. Design the protocol, Use the running-mode analysis approach based on the two-party cryptographic protocols to analyze the protocol, and design a SMV program to check the TW protocol. In the basis of the SMV program of protocol, Design the general program of SMV to check the two-party protocol.Keywords: Cryptographic protocolModel, checkingprotocol analysis, Formal methods，Running-mode, analysis approach， SMV目录中文摘要英文摘要.1 绪论11.1本课题的开发背景以及开发意义.11.2国内外研究现状.1 1.3本课题研究的主要内容22 公开密钥认证协议11.1公开密钥认证协议的基本概念.11.2公开密钥认证协议分类.21.3公开密钥认证协议的安全性及其设计规范.21.3.1公开密钥认证协议的安全性分析及攻击31.3.2安全协议设计规范41.4公开密钥认证协议模型检测分析技术的研究与进展.61.5论文安排与研究成果.71.5.1论文安排81.5.2主要研究成果83 模型检测技术及运行模式分析法研究93.1引言.93.2模型检测技术分析公开密钥认证协议的基本理论.93.2.1模型检测技术分析公开密钥认证协议的理论研究93.2.2模型检测技术的现状及存在的问题.123.3两方公开密钥认证协议运行模式分析法.133.3.1两方公开密钥认证协议运行模式分析法简介.133.3.2对两方公开密钥认证协议运行模式的研究.153.4小结.16 4 模型检测工具SMV174.1 引言.174.2 SMV语言语法及CTL表达式.184.2.1 SMV语言语法184.2.2时态逻辑CTL204.3 SMV实例.215 运行模式及SMV分析公开密钥认证协议实例研究245.1 引言.245.2 公开密钥认证协议.245.3运用模式法分析公开密钥认证协议.255.4 公开密钥认证协议安全性检测的SMV程序分析.295.4.1公开密钥认证协议的消息的定义295.4.2 公开密钥认证协议的有限状态305.4.3 公开密钥认证协议的SMV程序的数据结构315.4.4 公开密钥认证协议的主模块框架和有限状态属性335.4.5 公开密钥认证协议的安全性分析355.5小结.36 6总 结37参考文献38致谢39毕业设计（论文）知识产权声明40毕业设计（论文）独立性声明41英文翻译41译文原文481 绪 论本章主要系统地介绍了公开密钥认证协议的基本概念和公开密钥认证协议的分类，讨论了公开密钥认证协议的安全性及其设计规范，概述了公开密钥认证协议模型检测技术分析公开密钥认证协议安全性方法的重要意义、研究进展和现状。最后列举了本文的主要研究工作，给出了本文的内容安排。1.1本课题研究的背景、目的及意义现代社会计算机和互联网技术正在不断的改变着人类社会的面貌，随着计算机和网络技术的不断发展，与之伴随而来的是信息和网络的安全问题。网络作为现代信息传递的一个重要载体，其安全性是整个信息基础架构的安全基础，而网络的安全性离不开安全的网络协议。所以，网络协议本身是否存在安全隐患是信息安全的一个重要因素。因此，作为信息安全的一项重要研究内容，公开密钥认证协议的安全性分析与研究。对于促进信息化建设以及网络安全和信息安全研究具有非常重要的意义。此次毕业设计主要运用模型检测技术分析公开密钥认证协议的理论与技术。1.2.国内外研究现状自从1976年公钥密码的思想提出以来，国际上已经提出了许多种公钥密码体制，但比较流行的主要有两类：一类是基于大整数因子分解问题的，其中最典型的代表是RSA；另一类是基于离散对数问题的，比如ElGamal公钥密码和影响比较大的椭圆曲线公钥密码。由于分解大整数的能力日益增强，所以对RSA的安全带来了一定的威胁。目前768比特模长的RSA已不安全。一般建议使用1024比特模长，预计要保证20年的安全就要选择1280比特的模长，增大模长带来了实现上的难度。而基于离散对数问题的公钥密码在目前技术下512比特模长就能够保证其安全性。特别是椭圆曲线上的离散对数的计算要比有限域上的离散对数的计算更困难，目前技术下只需要160比特模长即可，适合于智能卡的实现，因而受到国内外学者的广泛关注。国际上制定了椭圆曲线公钥密码标准IEEEP1363，RSA等一些公司声称他们已开发出了符合该标准的椭圆曲线公钥密码。我国学者也提出了一些公钥密码，另外在公钥密码的快速实现方面也做了一定的工作，比如在RSA的快速实现和椭圆曲线公钥密码的快速实现方面都有所突破。公钥密码的快速实现是当前公钥密码研究中的一个热点，包括算法优化和程序优化。另一个人们所关注的问题是椭圆曲线公钥密码的安全性论证问题1.3主要研究内容：（1） 了解安全协议的基本概念和密码协议的安全性分析。（2） 研究运用公开密钥协议运行模式分析法，用此方法对公开密钥协议进行分析。（3） 尝试运用模型检测工具SMV系统对公开密钥协议的安全性进行分析和研究。2 公开密钥认证协议2.1公开密钥认证协议的基本概念通过网络来建立计算机系统之间的安全通信并证明此通信是安全的，不仅是一个日益受到关注的学术研究领域，而且也对社会生活具有非常重要的意义。在现实生活中，人们对协议并不陌生，人们都在自觉或不自觉地使用着各种协议。例如，在处理国际事物时，国家政府之间通常要遵守某种协议；在法律上，当事人之间常常要按照规定的法律程序去处理纠纷；在打扑克、电话订货、投票或到银行存款或取款时，都要遵守特定的协议。由于人们能够熟练地使用这些协议来有效地完成所要做的事情，所以很少有人去深入地考虑它们。所谓协议（Protocol），就是两个或两个以上的参与者为完成某项特定的任务而采取的一系列步骤。这个定义包含三层含义：第一、协议自始至终是有序的过程，每一步骤必须依此执行。在前一步没有执行完之前，后面的步骤不可能执行。第二、 协议至少需要两个参与者。一个人可以通过执行一系列的步骤来完成某项任务，但它不构成协议。第三、 通过执行协议必须能够完成某项任务。即使某些东西看似协议，但没有完成任何任务，也不能成为协议，只不过是浪费时间的空操作。我们把为了完成某种安全任务的协议称为安全协议。安全协议为了保证安全性，在设计时必须采用密码技术。因此，我们也将安全协议称作公开密钥认证协议。所以，我们可给公开密钥认证协议再下一个定义：公开密钥认证协议是建立在密码体制基础上的一种交互通信的协议，它运行在计算机通信网或分布式系统中，借助于密码算法来达到密钥分配、身份认证等目的。1.2公开密钥认证协议分类到目前为止，还未有人对公开密钥认证协议进行过详细的分类。因为将公开密钥认证协议进行严格分类是很难的事情，从不同的角度出发，就有不同的分类方法。例如，根据公开密钥认证协议的功能，可以将其分为认证协议、密钥建立（交换、分配）协议、认证的密钥建立（交换、分配）协议等；根据ISO的七层参考模型，又可以将其分成高层协议和低层协议；按照协议中所采用的密码算法的种类，又可以分成双钥（或公钥）协议、单钥协议或混合协议等；根据参与协议的主体个数可分为两方协议、三方协议和多方协议等。一般认为比较合理的分类方法是应该按照公开密钥认证协议的功能来分类，而不管协议具体采用何种密码技术。固把公开密钥认证协议分成以下几类：（1）密钥建立协议（Key Establishment Protocol），用于完成建立公开密钥。（2）认证建立协议（Authentication Protocol），向一个实体提供对他想要进行通信的另一个实体的身份的某种程度的确信。（3）认证的密钥建立协议（Authenticated Key Establishment Protocol），与另一身份已被证实或可被证实的实体之间建立共享秘密。 1.3公开密钥认证协议的安全性及其设计规范公开密钥认证协议是许多分布系统安全的基础。确保这些协议能够安全地运行是极为重要的。虽然公开密钥认证协议中仅仅进行很少的几组消息传输，但是其中的每一消息的组成都是经过巧妙设计的，而且这些消息之间有着复杂的相互作用和制约。在设计公开密钥认证协议时，人们通常采用不同的密码体制。而且所设计的协议也常常应用于许多不同的通信环境。但是，现有的许多协议在设计上普遍存在着某些安全缺陷。造成认证协议存在安全漏洞的原因有很多，我们通过对协议的安全性进行分析，可以发现协议的设计漏洞，反过来可以进一步指导协议的设计。1.3.1公开密钥认证协议的安全性分析及攻击在分析协议的安全性时，常用的方法是对协议施加各种可能的攻击来测试协议的安全程度。公开密钥认证协议攻击的目标通常有三个：第一个是协议中所采用的密码算法；第二个是算法和协议中所采用的密码技术；第三个是协议本身。由于我们本课题只讨论公开密钥认证协议本身的安全性，因此我们将只考虑对协议自身的攻击，而假设协议中所采用的密码算法和密码技术均是安全的。一般对协议自身的攻击可以分为被动攻击和主动攻击。被动攻击是指协议外部的实体对协议执行的部分或整个过程实施窃听。攻击者对协议的窃听并不影响协议的执行，他所做的是对协议的消息进行观察，并试图从中获得协议中涉及的各方的某些信息。他们收集协议各方之间传递的消息，并对其进行密码分析。这种攻击实际上属于一种惟密文攻击。被动攻击的特点是很难检测，因此我们在设计协议时应该尽量防止被动攻击，使公开密钥认证协议对于被动攻击是安全的，而不是试图检测它们。主动攻击对公开密钥认证协议来说具有更大的危险性。在这种攻击中，攻击者试图改变协议执行中的某些消息以达到获取信息、破坏系统或获得对资源的非授权的访问。他们可能在协议中加入新的消息、删除消息、替换消息、重发旧消息、干扰信道或修改计算机中存储的消息。在网络环境下，当通信各方彼此互不信赖时，这种攻击对协议的威胁显得更为严重。协议的攻击者不一定是局外人，他可能就是一个合法用户，可能是一个系统管理者，可能是几个人联手对协议发起攻击，也可能就是协议中的一方。若主动攻击者是协议涉及的一方，我们称其为骗子（Cheater）。他可能在协议执行中撒谎，或者根本不遵守协议。骗子也可以分为主动骗子和被动骗子。被动骗子遵守协议，但试图获得协议之外更多的信息；主动骗子则不遵守协议，对正在执行的协议进行干扰，试图冒充它方或欺骗对方，以达到各种非法目的。如果运行协议的参与者中大多数都是主动骗子，那么就很难保证协议的安全性。但是，在一些情况下，合法用户可以检测到主动欺骗的存在并采取一定的防范措施。在实际应用中，对协议的攻击方法是多种多样的。对不同类型的公开密钥认证协议，存在着不同的攻击方法。我们很难将所有攻击方法一一列出，这里仅仅对几个常用的攻击方法进行简单介绍。（1）重放攻击重放攻击主要指攻击者利用其消息再生能力生成诚实用户所期望的消息格式并重放，从而达到破坏协议安全性质的目的。防止重放攻击的关键是保证消息的新鲜性。（2）业务流分析攻击业务流分析的目标是通过检查数据包中未加密的字段和未保护的包的属性来发现受保护会话的机密信息。例如，通过检查未加密的IP源和目的地址（甚至TCP端口）或检查网络流量，业务流分析者就能确定哪些通信方在进行交互、使用什么类型的服务、有时甚至能发现有关商家或个人用户的信息。（3）中间人攻击当攻击者能够中途截获发送端的消息，读出它们并将它们发送给接收端(反之亦然)时，“中间人”攻击就可能发生。为实施“中间人”攻击，攻击者将必须破解密钥，而这是一项比针对加密算法的攻击还难的工作。（4）“剪一贴”攻击此攻击的大致过程是：首先，从一些包含敏感数据的包中切下一段密文；然后，再把这段密文拼接到另外一段密文中，被拼接的这段密文是经过仔细选择的，使得接收端非常有可能泄漏出经过解密后的明文。（5）截获攻击入侵者通过截获协议中传输的消息进行攻击。（6）伪造攻击入侵者通过伪造一条假协议消息进行攻击。1.3.2安全协议设计规范在协议的设计过程中，我们通常要求协议具有足够的复杂性以抵御交织攻击。另一方面，我们还要尽量使协议保持足够的经济性和简单性，以便可应用于低层网络环境。如何设计公开密钥认证协议才能满足安全性、有效性、完整性和公平性的要求呢？这就需要对我们的设计空间规定一些边界条件。归纳起来，常见的安全协议的设计规范如下：(1)采用一次随机数来替代时戳在已有的许多安全协议设计中，人们多采用同步认证方式，即需要各认证实体之间严格保持一个同步时钟。在某些网络环境下，保持这样的同步时钟不难，但对于某些网络环境却十分困难。因此，建议在设计公开密钥认证协议时，应尽量地采用一次随机数来取代时戳，即采用异步认证方式。(2)具有抵御常见攻击的能力对于所设计的协议，我们必须能够证明它们对于一些常见的攻击方法，如已知或选择明文攻击、交织攻击等是安全的。换言之，攻击者永远不能从任何“回答”消息中，或修改过去的某个消息，而推出有用的密码消息。(3)适用于任何网络结构的任何协议层所设计的协议不但必须能够适用于低层网络机制，而且还必须能用于应用层的认证。这就意味着协议中包含的密码消息必须要尽可能的短。如果协议采用了分组加密算法，那么我们期望此密码消息的长度等同于一组密文的长度。(4)适用于任何数据处理能力所设计的协议不但能够在智能卡上使用，而且也能够在仅有很小处理能力和无专用密码处理芯片的低级网络终端和工作站上（如PC机）上使用。这意味着协议必须具有尽可能少的密码运算。(5)可采用任何密码算法协议必须能够采用任何已知的和具有代表性的密码算法。这些算法可以是对称加密算法（如DES，IDEA），也可以是非对称加密算法（如RSA）。(6)不受出口的限制目前，各国政府对密码产品的进出口都进行了严格的控制。在设计公开密钥认证协议时，应该尽量做到使其不受任何地理上的限制。现在，大多数规定是针对分组加密/解密算法的进出口加以限制的。然而，对于那些仅仅用于数据完整性保护和认证功能的技术的进出口往往要容易得多。因此，对于某种技术，如果它仅依赖于数据完整性和认证技术而非数据加密函数，它取得进出口许可证的可能性就较大。例如，如果协议仅提供消息认证码功能，而不需要对大量的数据进行加密和解密，那么就容易获得进出口权。这就要求我们在设计协议时，尽量避免采用加密和解密函数。(7)便于进行功能扩充协议对各种不同的通信环境具有很高的灵活性，允许对其进行可能的功能扩展，起码对一些比较显然应具有的功能加以扩展。特别是，协议在方案上应该能够支持多用户（多于两个）之间的密钥共享。另一个明显的扩展是它应该允许在消息中加载额外的域，进而可以将其作为协议的一部分加以认证。(8)最少的安全假设在进行协议设计时，我们常常要首先对网络环境进行风险分析，作出适当的初始安全假设。例如，各通信实体应该相信它们各自产生的密钥是好的，或者网络中心的认证服务器是可信赖的，或者安全管理员是可信赖的，等等。但是，初始假设越多，协议的安全性就越差。因此，我们应尽可能地减少初始安全假设的数目。以上八条协议设计规范并不是一成不变的，我们可以根据实际情况作出相应的补充或调整。但是，遵循上面提出的八条规范是设计一个好协议的基础。1.4公开密钥认证协议模型检测分析技术的研究与进展协议安全性分析是揭示公开密钥认证协议中存在漏洞的重要途径。目前，对公开密钥认证协议进行安全性分析的方法主要有两种：一种是攻击检验方法；另一种是采用形式化分析的方法。攻击检验方法也称非形式化分析方法，是公开密钥认证协议早期的主要分析方法。这种方法对协议进行分析一般是根据已知的各种攻击方法对协议进行攻击，以攻击是否有效来检验公开密钥认证协议是否安全。因为实际应用中，存在着许多未知的攻击方法，这种对公开密钥认证协议的非形式化分析方法只能发现协议中是否存在着已知的缺陷，而不能全面客观地来分析公开密钥认证协议，可能导致不安全的协议经分析是安全的这样错误的结论。八十年代以后，随着对公开密钥认证协议安全性分析的进一步探索研究，公开密钥认证协议的形式化分析成为研究热点。安全协议的形式化分析是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。这种方法的出发点是希望将公开密钥认证协议形式化，然后借助于人工推导，甚至计算机的辅助分析，来判别公开密钥认证协议是否安全可靠。形式化分析方法和攻击检验方式相比，它能全面、深刻地检测到公开密钥认证协议中细微的漏洞。形式化分析方法不仅能发现现有的攻击方法对协议构成的威胁，而且还可能通过对公开密钥认证协议的安全性分析，发现协议中细微的漏洞，从而发现对公开密钥认证协议新的攻击方法。模型检测技术（Model Checking Technology）是属于一般目的的公开密钥认证协议的形式化分析方法，它是验证有限状态系统的自动化分析工具，常用于硬件电路设计和通信协议。目前模型检测技术也是一种十分有效的协议形式化分析工具。模型检测技术最早是用于分析和模拟硬件工作过程的形式化方法，随着形式化方法的日益进步和应用领域的推广，现已应用于软件分析和通信协议模拟等多个领域，但用于安全协议的分析还是近几年新的应用。关于模型检测的研究越来越受到人们的关注，因为它对协议的自动验证和协议的工程化设计具有指导意义。 在1996年，英国学者Gavin Lowe首先使用CSP和模型检测技术对公开密钥认证协议进行分析13，在这篇文章中，Gavin Lowe首次采用CSP模型和CSP模型检测工具FDR(故障偏差精炼检测器，Failures Divergences Refinement Checker)来分析Needhan-Schroeder公钥协议，并成功地找到一个BAN类逻辑等分析方法以前未发现的攻击。 模型检测技术应用于网络安全协议分析的成功，使学者们相继投入到这个领域。自97年起，计算机科学家及密码学家开始陆续应用模型检测这种新的形式方法来分析网络安全协议的安全性，对多个网络安全协议进行了分析，成功地发现了许多攻击。 在文献17中Steve Schneider用CSP研究了公开密钥认证协议的安全性质，在文献18中A.W.Roscoe和M.H.Goldsmith基于对CSP和FDR研究，认为它们是公开密钥认证协议完美的检测工具。 在文献19中W.Marrero等提出了一种通用的模型检测器，构造了他们的模型及代数理论，并证明该模型的有效性。文中并对Needhan-Schroeder公钥协议进行了分析，也成功地发现了文献20所找到的攻击。 在文献21中J.C.Mitchell等设计了一种通用的状态计数工具Mur，并用它来分析公开密钥认证协议可能达到的状态，进一步得出公开密钥认证协议是否安全的结论。文中分析了Needham-Schroeder协议、Kerberos协议和TMN协议，并找到了这些协议所有已知的攻击。在文献22中Zhe Dang等用ASTRAL这种实时系统形式化描述语言构造了模型检测器，文中并对Needham-Schroeder公钥协议和TMN协议进行了分析，也成功地发现了Gavin Lowe所找到的所有攻击。英国学者Gavin Lowe在模型检测上做出了非凡的创造性成果，相应的结论可参见2013。其中文献22是一篇关于模型检测大全性的文章，文中试图为模型检测技术提供一个完整地解决方案。目前对于协议分析来讲，模型检测已经证明是一条非常成功的途径，这种方法发现了协议的许多以前未发现的新的攻击，极大地促进了网络安全协议分析与设计的研究工作。但模型检测仍然存在着许多需要进一步研究的问题，最主要的问题在于：模型检测适用于有限状态系统地分析工具，如何将公开密钥认证协议说明成有限状态系统，而又没有增加或减少公开密钥认证协议的安全性。这是一个需要继续深入研究和探索的核心问题。1.5论文安排与研究成果本论文是在结合国家自然科学基金项目“公开密钥认证协议的模型检测分析”的基础上，围绕着公开密钥认证协议的模型检测技术进行了深入的研究，本论文的工作成果如下：1.5.1论文安排第二章：指出模型检测技术分析公开密钥认证协议的现状；研究模型检测技术分析公开密钥认证协议的基本理论；介绍两方公开密钥认证协议运行模式分析法并对其进行研究。第三章：介绍模型检测工具SMV。第四章介绍公开密钥认证协议；运用运行模式分析法分析公开密钥认证协议安全性；尝试使用SMV检测两方公开密钥认证协议的模型检测。1.5.2主要研究成果以下是我们取得的一些成果：(1) 系统的介绍了公开密钥认证协议的一些基本概念和公开密钥认证协议安全性分析的重要意义、研究进展和现状。(2)研究了模型检测技术和公开密钥认证协议运行模式分析法。(3)给出了运用模型检测工具SMV分析公开密钥认证协议的方法。(4)运用运行模式分析法分析了公开密钥认证协议，并尝试使用SMV研究了公开密钥认证协议的安全性检测。- 25- 2 模型检测技术及运行模式分析法研究本章首先介绍了模型检测技术和模型检测技术在公开密钥认证协议分析领域取得的研究成果；随后引出了以此技术为理论依据的公开密钥认证协议运行模式分析法，并对其运行模式作了进一步的研究。2.1引言模型检测技术原是用于分析和模拟硬件工作过程的形式化方法，随着形式化方法的推广和应用，模型检测技术现已用于软件分析和通信协议模拟等多个领域，但用于公开密钥认证协议的分析还是近几年比较新的应用。在1996年，英国学者Gavin Lowe首先使用CSP和模型检测技术对公开密钥认证协议进行分析20。并首次采用CSP模型和CSP模型检测工具FDR(故障偏差精炼检测器，Failures Divergences Refinement Checker)，来分析Needham-Schroeder公钥协议。在这个模型中，协议参与者被说明成CSP中的进程(process)，消息说明成事件（event），进而将协议说明成一个通信顺序进程的集合，这些进程并行运行而且和他们的环境交互作用，其对公开密钥认证协议的验证是从协议说明中抽取一个模型（通常是一个有限状态转换系统），然后用FDR检测，从而证明协议的安全性。此方法成功地找到Needham-Schroeder协议的一个以前从未发现的攻击。模型检测的成功，使研究者们相继投入到这个领域。实践证明对于公开密钥认证协议安全性分析来讲，模型检测是一条非常成功的途径。2.2模型检测技术分析公开密钥认证协议的基本理论2.2.1模型检测技术分析公开密钥认证协议的理论研究 模型检测技术可以抽象地描述为：给定一个模型M和逻辑描述的性质P，检查模型M中性质P是否成立。模型检测技术对协议进行验证与分析，是通过检查在恶意攻击者存在的情况下，协议运行的所有可能的路径，来判断协议是否实现了其安全保证；如果没有，将给出攻击者的攻击路径。模型检测用于有限状态系统的分析，要用模型检测技术分析公开密钥认证协议，就要研究如何为公开密钥认证协议构造有限状态系统。目前，模型检测技术分析公开密钥认证协议的基本方法主要采用英国学者Gavin Lowe研究成果，即：生成一个协议运行的小系统模型（通常是一个有限状态转换系统），以及一个可与协议互操作的攻击者模型，并用状态探测工具检测系统是否进入一个不安全状态，即是否存在对协议的攻击。并且基于代数理论证明：如果小系统是安全的，那么协议是安全的。这种方法提出了将大系统中协议安全的性质研究约化为小系统中协议安全性质的研究，这是目前这一领域的最新理论研究成果。使用该方法发现了公开密钥认证协议许多以前未发现的新的攻击，极大地促进了公开密钥认证协议分析与设计的研究工作。（1）模型检测对被分析协议的基本假设：任何一个系统都有其赖以存在的假设条件，用以避免结论的不当使用以及对一些限制的理解，同样，用模型检测技术分析公开密钥认证协议，对协议是有一定要求的，因为只有能用有限状态描述且满足一定条件的协议才能模型检测，并不是所有的公开密钥认证协议都能用模型检测技术来分析。在文献26中给出了能被模型检测技术所分析的公开密钥认证协议的基本假设，具体描述如下：1)加密部分从文字形式上是可以区分的公开密钥认证协议中所用到的加密项从文字上就可以区分。这意味着一个主体接收到一个加密项就知道这个加密项属于哪个消息，是消息的哪一部分。这个假设可以防止入侵者重置协议中的消息，也能防止入侵者用另一条消息对原消息进行替换。这个条件很容易满足，例如只要在每个加密项中放入项的编号即可。2)身份的可确定性参与协议运行的所有主体的身份是可以通过协议运行中的加密项推导出来的。这样一个主体当他接收了一个加密项后，他就可以确定这个加密项是否为他而发。更进一步，如果这个加密项起源于一个诚实的主体，接收者可以判断出谁是加密项的产生者，谁是这个加密项的接收者。假设1和假设2容易满足，只要在每个加密项中明显包含每个主体的身份即可：更进一步说，如果消息是来自诚实主体，那么接收方就能确定谁是消息的发送方和谁是消息的接收方。这两个假设条件可避免许多攻击，并且也使公开密钥认证协议的分析更容易。3)协议运行时不用协议运行期间建立的任何临时秘密如果一个特别的数据项不是那种要保持为秘密的数据项，那么一个监视通信的第三者就能够从有该数据项参与的运行中获知此数据项的值（或者这个值是公共信息，第三者早已知道它）；更进一步，如果一个特别的密钥不是那种要保持为秘密的密钥，那么一个监视通信的第三者就能够通过持有该密钥的逆参与的运行中获知此密钥的数值（或者明显得到，或者通过加密某些数据项）。（2）模型检测对基于模型的假设：1)完善加密假设协议采用的密码系统是完美的，不考虑密码系统被攻破的情况等。2)入侵者的知识和能力可窃听及中途拦截系统中传送的任何消息；可解密用他自己加密密钥（公钥或单钥）加密的消息；在系统中可插入新的消息；即使不知道加密部分的内容，也可重放他所看到的任何消息（其中可改变明文部分）；可运用他知道的所有知识（如临时值等），并可产生新的临时值等。（3）模型检测的结论 运用模型检测技术分析公开密钥认证协议，就要构造小系统模型，关于小系统的定义和安全性质的定义和结论如下：1)小系统的定义：所谓小系统是指参与协议运行的各主体都是唯一的（例如，一个初始者，一个响应者），作用也是唯一的。这些主体也都是诚实的：他们严格按照协议规定和遵循自己的身份参与协议运行，并不与入侵者运行协议。2)安全性破坏定义：定义1（强安全性破坏）：一个诚实的主体相信在协议运行中用到的一个值是仅他和另外诚实主体之间的共享秘密，但入侵者知道这个值。定义2（一般安全性破坏）：一个诚实的主体相信在一个完整协议运行中用到的一个值是仅他和另外诚实主体之间的共享秘密，但入侵者知道这个值。小系统理论旨在解决：在协议及其环境条件下，如果小系统是安全的，那么大系统也是安全的。文献19中用大量篇幅，创建了一套基于代数方法的理论，并证明了如下结论：如果在某一特定的小系统中不存在对协议强安全性破坏的攻击，那么对任意系统也不存在强安全性破坏的攻击，当然也就不存在攻击导致一般安全性破坏的攻击，即如果小系统是安全的，那么协议是安全的。小系统理论理论大大减少了安全协议分析的工作量，并从理论上增强了协议分析结果的可信任度。这个理论结果极大地促进了模型检测技术在安全协议分析领域的广泛应用，使安全协议形式化分析的主流从逻辑方法转向了模型检测，进而使安全协议的形式化分析更上一层楼。2.2.2模型检测技术的现状及存在的问题用模型检测技术分析网络安全协议，只要对被分析的协议在小系统上进行强安全性破坏分析，就可以保证协议在任意系统上的安全性。这一理论大大减少了公开密钥认证协议分析的工作量，并从理论上保证了人们对协议分析结果的信心。所以对于协议安全性分析来讲，模型检测技术已经证明是一条非常成功的途径。这种方法发现了协议的许多以前未发现的新的攻击。但模型检测技术仍然存在着一些问题：（1） 现有方法是否作到了理论上所要求的强安全型破坏分析？（2） 如何评价和衡量不同的检测方法和检测工具？（3） 这种分析方法对协议的种类有所限制，对具有满足以下情况的协议不能进行分析指导：1)黑匣协议。2)采用非标准的加密方式的协议。3)消息中包含长期秘密项的协议，如主体的私钥等这类协议，目前模型检测无法分析。我们将用于若干次协议运行的数据项，如主体的公开密钥、秘密密钥等定义为长期项。而将主体在一次协议运行中引入的短期数据项，如临时值，短期密钥等定义为短期项。长期项和短期项是不同类型的数据项。因此，模型检测分析公开密钥认证协议仍然存在着不少问题需要解决，其关键在于模型检测只能分析有限状态系统，这必然对公开密钥认证协议有所要求，因为协议要能用有限状态系统来描述。并且模型检测技术本身也存在着诸如可以生成现实的攻击路径，但很难辨别攻击造成的原因等问题。未来的研究趋势是如何扩大模型检测分析公开密钥认证协议的种类并采用混合分析技术。2.3两方公开密钥认证协议运行模式分析法2.3.1两方公开密钥认证协议运行模式分析法简介运行模式分析法由模型检测技术分析公开密钥认证协议若干结论推导而来。模型检测技术分析公开密钥认证协议的基本方法是构造一个运行协议的小系统模型（通常是一个有限状态系统），同时结合一个通常意义下的入侵者模型，他能与协议交互作用，利用状态探测工具来发现系统是否进入一个不安全状态，也就是说是否对协议存在一个攻击。这种方法发现了公开密钥认证协议许多以前未发现的新的攻击，极大地促进了公开密钥认证协议分析与设计的研究工作。在文献19中基于代数方法证明了对于一个构造的小系统，若协议在小系统中是安全的，则可以不用考虑任意系统。因为一个公开密钥认证协议如果在任意一个系统上有攻击的话，那么它一定有攻击在小系统上。这样只要对被分析的协议在小系统上进行安全分析，就可以保证协议在任意系统上的安全性。这大大减少了公开密钥认证协议分析的工作量，并从理论上保证了人们对协议分析结果的