1、 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公
2、开密钥认证协议模型检测分析技术的研究与进展. 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 模型检测工具SMV 174.1 引言.174.2 SMV语言语法及CTL表达式.184.
3、2.1 SMV语言语法 184.2.2时态逻辑CTL 204.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毕业设计（论
4、文）知识产权声明 40毕业设计（论文）独立性声明 41英文翻译 41译文原文 481 绪 论本章主要系统地介绍了公开密钥认证协议的基本概念和公开密钥认证协议的分类，讨论了公开密钥认证协议的安全性及其设计规范，概述了公开密钥认证协议模型检测技术分析公开密钥认证协议安全性方法的重要意义、研究进展和现状。最后列举了本文的主要研究工作，给出了本文的内容安排。1.1本课题研究的背景、目的及意义现代社会计算机和互联网技术正在不断的改变着人类社会的面貌，随着计算机和网络技术的不断发展，与之伴随而来的是信息和网络的安全问题。网络作为现代信息传递的一个重要载体，其安全性是整个信息基础架构的安全基础，而网络的安全
5、性离不开安全的网络协议。所以，网络协议本身是否存在安全隐患是信息安全的一个重要因素。因此，作为信息安全的一项重要研究内容，公开密钥认证协议的安全性分析与研究。对于促进信息化建设以及网络安全和信息安全研究具有非常重要的意义。此次毕业设计主要运用模型检测技术分析公开密钥认证协议的理论与技术。1.2.国内外研究现状自从1976年公钥密码的思想提出以来，国际上已经提出了许多种公钥密码体制，但比较流行的主要有两类：一类是基于大整数因子分解问题的，其中最典型的代表是RSA；另一类是基于离散对数问题的，比如ElGamal公钥密码和影响比较大的椭圆曲线公钥密码。由于分解大整数的能力日益增强，所以对RSA的安全
6、带来了一定的威胁。目前768比特模长的RSA已不安全。一般建议使用1024比特模长，预计要保证20年的安全就要选择1280比特的模长，增大模长带来了实现上的难度。而基于离散对数问题的公钥密码在目前技术下512比特模长就能够保证其安全性。特别是椭圆曲线上的离散对数的计算要比有限域上的离散对数的计算更困难，目前技术下只需要160比特模长即可，适合于智能卡的实现，因而受到国内外学者的广泛关注。国际上制定了椭圆曲线公钥密码标准IEEEP1363，RSA等一些公司声称他们已开发出了符合该标准的椭圆曲线公钥密码。我国学者也提出了一些公钥密码，另外在公钥密码的快速实现方面也做了一定的工作，比如在RSA的快速
7、实现和椭圆曲线公钥密码的快速实现方面都有所突破。公钥密码的快速实现是当前公钥密码研究中的一个热点，包括算法优化和程序优化。另一个人们所关注的问题是椭圆曲线公钥密码的安全性论证问题1.3主要研究内容：（1） 了解安全协议的基本概念和密码协议的安全性分析。（2） 研究运用公开密钥协议运行模式分析法，用此方法对公开密钥协议进行分析。（3） 尝试运用模型检测工具SMV系统对公开密钥协议的安全性进行分析和研究。2 公开密钥认证协议2.1公开密钥认证协议的基本概念通过网络来建立计算机系统之间的安全通信并证明此通信是安全的，不仅是一个日益受到关注的学术研究领域，而且也对社会生活具有非常重要的意义。在现实生活
8、中，人们对协议并不陌生，人们都在自觉或不自觉地使用着各种协议。例如，在处理国际事物时，国家政府之间通常要遵守某种协议；在法律上，当事人之间常常要按照规定的法律程序去处理纠纷；在打扑克、电话订货、投票或到银行存款或取款时，都要遵守特定的协议。由于人们能够熟练地使用这些协议来有效地完成所要做的事情，所以很少有人去深入地考虑它们。所谓协议（Protocol），就是两个或两个以上的参与者为完成某项特定的任务而采取的一系列步骤。这个定义包含三层含义：第一、协议自始至终是有序的过程，每一步骤必须依此执行。在前一步没有执行完之前，后面的步骤不可能执行。第二、 协议至少需要两个参与者。一个人可以通过执行一系列
9、的步骤来完成某项任务，但它不构成协议。第三、 通过执行协议必须能够完成某项任务。即使某些东西看似协议，但没有完成任何任务，也不能成为协议，只不过是浪费时间的空操作。我们把为了完成某种安全任务的协议称为安全协议。安全协议为了保证安全性，在设计时必须采用密码技术。因此，我们也将安全协议称作公开密钥认证协议。所以，我们可给公开密钥认证协议再下一个定义：公开密钥认证协议是建立在密码体制基础上的一种交互通信的协议，它运行在计算机通信网或分布式系统中，借助于密码算法来达到密钥分配、身份认证等目的。1.2公开密钥认证协议分类到目前为止，还未有人对公开密钥认证协议进行过详细的分类。因为将公开密钥认证协议进行严
10、格分类是很难的事情，从不同的角度出发，就有不同的分类方法。例如，根据公开密钥认证协议的功能，可以将其分为认证协议、密钥建立（交换、分配）协议、认证的密钥建立（交换、分配）协议等；根据ISO的七层参考模型，又可以将其分成高层协议和低层协议；按照协议中所采用的密码算法的种类，又可以分成双钥（或公钥）协议、单钥协议或混合协议等；根据参与协议的主体个数可分为两方协议、三方协议和多方协议等。一般认为比较合理的分类方法是应该按照公开密钥认证协议的功能来分类，而不管协议具体采用何种密码技术。固把公开密钥认证协议分成以下几类：（1）密钥建立协议（Key Establishment Protocol），用于完成
11、建立公开密钥。（2）认证建立协议（Authentication Protocol），向一个实体提供对他想要进行通信的另一个实体的身份的某种程度的确信。（3）认证的密钥建立协议（Authenticated Key Establishment Protocol），与另一身份已被证实或可被证实的实体之间建立共享秘密。1.3公开密钥认证协议的安全性及其设计规范公开密钥认证协议是许多分布系统安全的基础。确保这些协议能够安全地运行是极为重要的。虽然公开密钥认证协议中仅仅进行很少的几组消息传输，但是其中的每一消息的组成都是经过巧妙设计的，而且这些消息之间有着复杂的相互作用和制约。在设计公开密钥认证协议时，人
12、们通常采用不同的密码体制。而且所设计的协议也常常应用于许多不同的通信环境。但是，现有的许多协议在设计上普遍存在着某些安全缺陷。造成认证协议存在安全漏洞的原因有很多，我们通过对协议的安全性进行分析，可以发现协议的设计漏洞，反过来可以进一步指导协议的设计。1.3.1公开密钥认证协议的安全性分析及攻击在分析协议的安全性时，常用的方法是对协议施加各种可能的攻击来测试协议的安全程度。公开密钥认证协议攻击的目标通常有三个：第一个是协议中所采用的密码算法；第二个是算法和协议中所采用的密码技术；第三个是协议本身。由于我们本课题只讨论公开密钥认证协议本身的安全性，因此我们将只考虑对协议自身的攻击，而假设协议中所
13、采用的密码算法和密码技术均是安全的。一般对协议自身的攻击可以分为被动攻击和主动攻击。被动攻击是指协议外部的实体对协议执行的部分或整个过程实施窃听。攻击者对协议的窃听并不影响协议的执行，他所做的是对协议的消息进行观察，并试图从中获得协议中涉及的各方的某些信息。他们收集协议各方之间传递的消息，并对其进行密码分析。这种攻击实际上属于一种惟密文攻击。被动攻击的特点是很难检测，因此我们在设计协议时应该尽量防止被动攻击，使公开密钥认证协议对于被动攻击是安全的，而不是试图检测它们。主动攻击对公开密钥认证协议来说具有更大的危险性。在这种攻击中，攻击者试图改变协议执行中的某些消息以达到获取信息、破坏系统或获得对
14、资源的非授权的访问。他们可能在协议中加入新的消息、删除消息、替换消息、重发旧消息、干扰信道或修改计算机中存储的消息。在网络环境下，当通信各方彼此互不信赖时，这种攻击对协议的威胁显得更为严重。协议的攻击者不一定是局外人，他可能就是一个合法用户，可能是一个系统管理者，可能是几个人联手对协议发起攻击，也可能就是协议中的一方。若主动攻击者是协议涉及的一方，我们称其为骗子（Cheater）。他可能在协议执行中撒谎，或者根本不遵守协议。骗子也可以分为主动骗子和被动骗子。被动骗子遵守协议，但试图获得协议之外更多的信息；主动骗子则不遵守协议，对正在执行的协议进行干扰，试图冒充它方或欺骗对方，以达到各种非法目的
15、。如果运行协议的参与者中大多数都是主动骗子，那么就很难保证协议的安全性。但是，在一些情况下，合法用户可以检测到主动欺骗的存在并采取一定的防范措施。在实际应用中，对协议的攻击方法是多种多样的。对不同类型的公开密钥认证协议，存在着不同的攻击方法。我们很难将所有攻击方法一一列出，这里仅仅对几个常用的攻击方法进行简单介绍。（1）重放攻击重放攻击主要指攻击者利用其消息再生能力生成诚实用户所期望的消息格式并重放，从而达到破坏协议安全性质的目的。防止重放攻击的关键是保证消息的新鲜性。（2）业务流分析攻击业务流分析的目标是通过检查数据包中未加密的字段和未保护的包的属性来发现受保护会话的机密信息。例如，通过检查
16、未加密的IP源和目的地址（甚至TCP端口）或检查网络流量，业务流分析者就能确定哪些通信方在进行交互、使用什么类型的服务、有时甚至能发现有关商家或个人用户的信息。（3）中间人攻击当攻击者能够中途截获发送端的消息，读出它们并将它们发送给接收端（反之亦然）时，“中间人”攻击就可能发生。为实施“中间人”攻击，攻击者将必须破解密钥，而这是一项比针对加密算法的攻击还难的工作。（4）“剪一贴”攻击此攻击的大致过程是：首先，从一些包含敏感数据的包中切下一段密文；然后，再把这段密文拼接到另外一段密文中，被拼接的这段密文是经过仔细选择的，使得接收端非常有可能泄漏出经过解密后的明文。（5）截获攻击入侵者通过截获协议
17、中传输的消息进行攻击。（6）伪造攻击入侵者通过伪造一条假协议消息进行攻击。1.3.2安全协议设计规范在协议的设计过程中，我们通常要求协议具有足够的复杂性以抵御交织攻击。另一方面，我们还要尽量使协议保持足够的经济性和简单性，以便可应用于低层网络环境。如何设计公开密钥认证协议才能满足安全性、有效性、完整性和公平性的要求呢？这就需要对我们的设计空间规定一些边界条件。归纳起来，常见的安全协议的设计规范如下：（1）采用一次随机数来替代时戳在已有的许多安全协议设计中，人们多采用同步认证方式，即需要各认证实体之间严格保持一个同步时钟。在某些网络环境下，保持这样的同步时钟不难，但对于某些网络环境却十分困难。因
18、此，建议在设计公开密钥认证协议时，应尽量地采用一次随机数来取代时戳，即采用异步认证方式。（2）具有抵御常见攻击的能力对于所设计的协议，我们必须能够证明它们对于一些常见的攻击方法，如已知或选择明文攻击、交织攻击等是安全的。换言之，攻击者永远不能从任何“回答”消息中，或修改过去的某个消息，而推出有用的密码消息。（3）适用于任何网络结构的任何协议层所设计的协议不但必须能够适用于低层网络机制，而且还必须能用于应用层的认证。这就意味着协议中包含的密码消息必须要尽可能的短。如果协议采用了分组加密算法，那么我们期望此密码消息的长度等同于一组密文的长度。（4）适用于任何数据处理能力所设计的协议不但能够在智能卡
19、上使用，而且也能够在仅有很小处理能力和无专用密码处理芯片的低级网络终端和工作站上（如PC机）上使用。这意味着协议必须具有尽可能少的密码运算。（5）可采用任何密码算法协议必须能够采用任何已知的和具有代表性的密码算法。这些算法可以是对称加密算法（如DES，IDEA），也可以是非对称加密算法（如RSA）。（6）不受出口的限制目前，各国政府对密码产品的进出口都进行了严格的控制。在设计公开密钥认证协议时，应该尽量做到使其不受任何地理上的限制。现在，大多数规定是针对分组加密/解密算法的进出口加以限制的。然而，对于那些仅仅用于数据完整性保护和认证功能的技术的进出口往往要容易得多。因此，对于某种技术，如果它仅
20、依赖于数据完整性和认证技术而非数据加密函数，它取得进出口许可证的可能性就较大。例如，如果协议仅提供消息认证码功能，而不需要对大量的数据进行加密和解密，那么就容易获得进出口权。这就要求我们在设计协议时，尽量避免采用加密和解密函数。（7）便于进行功能扩充协议对各种不同的通信环境具有很高的灵活性，允许对其进行可能的功能扩展，起码对一些比较显然应具有的功能加以扩展。特别是，协议在方案上应该能够支持多用户（多于两个）之间的密钥共享。另一个明显的扩展是它应该允许在消息中加载额外的域，进而可以将其作为协议的一部分加以认证。（8）最少的安全假设在进行协议设计时，我们常常要首先对网络环境进行风险分析，作出适当的
21、初始安全假设。例如，各通信实体应该相信它们各自产生的密钥是好的，或者网络中心的认证服务器是可信赖的，或者安全管理员是可信赖的，等等。但是，初始假设越多，协议的安全性就越差。因此，我们应尽可能地减少初始安全假设的数目。以上八条协议设计规范并不是一成不变的，我们可以根据实际情况作出相应的补充或调整。但是，遵循上面提出的八条规范是设计一个好协议的基础。1.4公开密钥认证协议模型检测分析技术的研究与进展协议安全性分析是揭示公开密钥认证协议中存在漏洞的重要途径。目前，对公开密钥认证协议进行安全性分析的方法主要有两种：一种是攻击检验方法；另一种是采用形式化分析的方法。攻击检验方法也称非形式化分析方法，是公
22、开密钥认证协议早期的主要分析方法。这种方法对协议进行分析一般是根据已知的各种攻击方法对协议进行攻击，以攻击是否有效来检验公开密钥认证协议是否安全。因为实际应用中，存在着许多未知的攻击方法，这种对公开密钥认证协议的非形式化分析方法只能发现协议中是否存在着已知的缺陷，而不能全面客观地来分析公开密钥认证协议，可能导致不安全的协议经分析是安全的这样错误的结论。八十年代以后，随着对公开密钥认证协议安全性分析的进一步探索研究，公开密钥认证协议的形式化分析成为研究热点。安全协议的形式化分析是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。这种方法的出发点是希望将公开密钥认证协议形式化
23、，然后借助于人工推导，甚至计算机的辅助分析，来判别公开密钥认证协议是否安全可靠。形式化分析方法和攻击检验方式相比，它能全面、深刻地检测到公开密钥认证协议中细微的漏洞。形式化分析方法不仅能发现现有的攻击方法对协议构成的威胁，而且还可能通过对公开密钥认证协议的安全性分析，发现协议中细微的漏洞，从而发现对公开密钥认证协议新的攻击方法。模型检测技术（Model Checking Technology）是属于一般目的的公开密钥认证协议的形式化分析方法，它是验证有限状态系统的自动化分析工具，常用于硬件电路设计和通信协议。目前模型检测技术也是一种十分有效的协议形式化分析工具。模型检测技术最早是用于分析和模拟
24、硬件工作过程的形式化方法，随着形式化方法的日益进步和应用领域的推广，现已应用于软件分析和通信协议模拟等多个领域，但用于安全协议的分析还是近几年新的应用。关于模型检测的研究越来越受到人们的关注，因为它对协议的自动验证和协议的工程化设计具有指导意义。 在1996年，英国学者Gavin Lowe首先使用CSP和模型检测技术对公开密钥认证协议进行分析13，在这篇文章中，Gavin Lowe首次采用CSP模型和CSP模型检测工具FDR（故障偏差精炼检测器，Failures Divergences Refinement Checker）来分析Needhan-Schroeder公钥协议，并成功地找到一个BA
25、N类逻辑等分析方法以前未发现的攻击。 模型检测技术应用于网络安全协议分析的成功，使学者们相继投入到这个领域。自97年起，计算机科学家及密码学家开始陆续应用模型检测这种新的形式方法来分析网络安全协议的安全性，对多个网络安全协议进行了分析，成功地发现了许多攻击。 在文献17中Steve Schneider用CSP研究了公开密钥认证协议的安全性质，在文献18中A.W.Roscoe和M.H.Goldsmith基于对CSP和FDR研究，认为它们是公开密钥认证协议完美的检测工具。 在文献19中W.Marrero等提出了一种通用的模型检测器，构造了他们的模型及代数理论，并证明该模型的有效性。文中并对Needhan-Schroeder公钥协议进行了分析，也成功地发现了文献20所找到的攻击。 在文献21中J.C.Mitch
