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

1、 . . . 1 / 43题目：基于公开密钥认证协议安全性题目：基于公开密钥认证协议安全性的分析与研究的分析与研究 . . . 1 / 43毕业设计（论文）原创性声明和使用授权说明毕业设计（论文）原创性声明和使用授权说明原创性声明原创性声明本人重承诺：所呈交的毕业设计（论文） ，是我个人在指导教师的指导下进行的研究工作与取得的成果。尽我所知，除文中特别加以标注和致的地方外，不包含其他人或组织已经发表或公布过的研究成果，也不包含我为获得与其它教育机构的学位或学历而使用过的材料。对本研究提供过帮助和做出过贡献的个人或集体，均已在文中作了明确的说明并表示了意。作 者 签 名：日 期：指导教师签名：

2、日期：使用授权说明使用授权说明本人完全了解大学关于收集、保存、使用毕业设计（论文）的规定，即：按照学校要求提交毕业设计（论文）的印刷本和电子版本；学校有权保存毕业设计（论文）的印刷本和电子版，并提供目录检索与阅览服务；学校可以采用影印、缩印、数字化或其它复制手段保存论文；在不以赢利为目的前提下，学校可以公布论文的部分或全部容。作者签名： 日 期：学位论文原创性声明学位论文原创性声明本人重声明：所呈交的论文是本人在导师的指导下独立进行研究所取得的研究成果。除了文中特别加以标注引用的容外，本论文不包含任何其他个人或集体已经发表或撰写的成果作品。对本文的研究做出重要贡献的个人和集体，均已在文中以明确

3、方式标明。本人完全意识到本声 . . . 2 / 43明的法律后果由本人承担。作者签名： 日期： 年 月 日学位论文使用授权书学位论文使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本人授权大学可以将本学位论文的全部或部分容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。涉密论文按学校规定处理。作者签名：日期： 年 月 日导师签名： 日期： 年 月 日注意事项1.设计（论文）的容包括：1）封面（按教务处制定的标准封面格式制作）2）原创性声明3）中文摘要（300 字

4、左右） 、关键词4）外文摘要、关键词5）目次页（附件不统一编入）6）论文主体部分：引言（或绪论） 、正文、结论7）参考文献8）致9）附录（对论文支持必要时）2.论文字数要求：理工类设计（论文）正文字数不少于 1 万字（不包括图纸、程序清单等） ，文科类论文正文字数不少于 1.2 万字。3.附件包括：任务书、开题报告、外文译文、译文原文（复印件） 。4.文字、图表要求： . . . 3 / 431）文字通顺，语言流畅，书写字迹工整，打印字体与大小符合要求，无错别字，不准请他人代写2）工程设计类题目的图纸，要求部分用尺规绘制，部分用计算机绘制，所有图纸应符合国家技术标准规。图表整洁，布局合理，文字

5、注释必须使用工程字书写，不准用徒手画3）毕业论文须用 A4 单面打印，论文 50 页以上的双面打印4）图表应绘制于无格子的页面上5）软件工程类课题应有程序清单，并提供电子文档5.装订顺序1）设计（论文）2）附件：按照任务书、开题报告、外文译文、译文原文（复印件）次序装订3）其它基于公开密钥认证协议安全性的分析与研究基于公开密钥认证协议安全性的分析与研究摘摘 要要公开密钥认证协议安全性分析与研究对于促进我国信息化建设以与网络安全和信息安全研究具有非常重要的意义。本文主要研究运用模型检测技术和基于模型检测技术的运行模式分析法，并研究了公开密钥认证协议的理论与技术。在此基础上，对公开密钥认证协议进行

6、了运行模式的手工分析。研究成果如下：系统介绍了公开密钥认证协议的基本概念与安全性分析的重要意义、研究进展和现状。研究了模型检测技术以与公开密钥认证协议运行模式分析法。给出了运用模型检测工具 SMV 分析公开密钥认证协议的方法。研究了公开密钥认证协议，运用运行模式分析法分析公开密钥认证协议的安全性，成功地发现了该协议的安全漏洞。并在学习了 SMV 模型检测工具的基础上，研究了公开密钥认证协议的 SMV 检测程序的框架和数据结构。关键词：关键词：公开密钥认证协议，模型检测协议分析，形式方法，运行模式分析法， SMV . . . 4 / 43AbstractAbstractAnalysis of s

7、ecurity 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

8、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 proto

9、col, 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:Keywords: Cryp

10、tographic protocolModel, checkingprotocol analysis, Formal methods，Running-mode, analysis approach， SMV . . . 5 / 43目录目录中文摘要英文摘要.1 绪论11.1 本课题的开发背景以与开发意义.11.2 国外研究现状.11.3 本课题研究的主要容22 公开密钥认证协议11.1 公开密钥认证协议的基本概念.11.2 公开密钥认证协议分类.21.3 公开密钥认证协议的安全性与其设计规.21.3.1 公开密钥认证协议的安全性分析与攻击 31.3.2 安全协议设计规 41.4 公开密钥认证协

11、议模型检测分析技术的研究与进展.61.5 论文安排与研究成果.71.5.1 论文安排 81.5.2 主要研究成果 83 模型检测技术与运行模式分析法研究93.1 引言.93.2 模型检测技术分析公开密钥认证协议的基本理论.93.2.1 模型检测技术分析公开密钥认证协议的理论研究 93.2.2 模型检测技术的现状与存在的问题.12 . . . 6 / 433.3 两方公开密钥认证协议运行模式分析法.133.3.1 两方公开密钥认证协议运行模式分析法简介.133.3.2 对两方公开密钥认证协议运行模式的研究.153.4 小结.164 模型检测工具 SMV174.1 引言.174.2SMV 语言语法

12、与 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 小结.366

13、 总结37参考文献 38致 39毕业设计（论文）知识产权声明 40毕业设计（论文）独立性声明 41英文翻译 41译文原文 48 . . . 7 / 431 绪 论本章主要系统地介绍了公开密钥认证协议的基本概念和公开密钥认证协议的分类，讨论了公开密钥认证协议的安全性与其设计规，概述了公开密钥认证协议模型检测技术分析公开密钥认证协议安全性方法的重要意义、研究进展和现状。最后列举了本文的主要研究工作，给出了本文的容安排。1.11.1 本课题本课题研究的背景、目的与意义研究的背景、目的与意义现代社会计算机和互联网技术正在不断的改变着人类社会的面貌，随着计算机和网络技术的不断发展，与之伴随而来的是信息和

14、网络的安全问题。网络作为现代信息传递的一个重要载体，其安全性是整个信息基础架构的安全基础，而网络的安全性离不开安全的网络协议。所以，网络协议本身是否存在安全隐患是信息安全的一个重要因素。因此，作为信息安全的一项重要研究容，公开密钥认证协议的安全性分析与研究。对于促进信息化建设以与网络安全和信息安全研究具有非常重要的意义。此次毕业设计主要运用模型检测技术分析公开密钥认证协议的理论与技术。1.2.1.2.国外研究现状国外研究现状自从 1976 年公钥密码的思想提出以来，国际上已经提出了许多种公钥密码体制，但比较流行的主要有两类：一类是基于大整数因子分解问题的，其中最典型的代表是 RSA；另一类是基

15、于离散对数问题的，比如 ElGamal 公钥密码和影响比较大的椭圆曲线公钥密码。由于分解大整数的能力日益增强，所以对 RSA 的安全带来了一定的威胁。目前 768 比特模长的 RSA 已不安全。一般建议使用 1024 比特模长，预计要保证 20 年的安全就要选择 1280 比特的模长，增大模长带来了实现上的难度。而基于离散对数问题的公钥密码在目前技术下 512 比特模长就能够保证其安全性。特别是椭圆曲线上的离散对数的计算要比有限域上的离散对数的计算更困难，目前技术下只需要 160 比特模长即可，适合于智能卡的实现，因而受到国外学者的广泛关注。国际上制定了椭圆曲线公钥密码标准 IEEEP1363

16、，RSA 等一些公司声称他们已开发出了符合该标准的椭圆曲线公钥密码。我国学者也提出了一些公钥密码，另外在公钥密码的快速实现方面也做了一定的工作，比如在 RSA 的快速实现和椭圆曲线公钥密码的快速实现方面都有所突破。公钥密码的快速实现是当前公钥密码研究中的一个 . . . 8 / 43热点，包括算法优化和程序优化。另一个人们所关注的问题是椭圆曲线公钥密码的安全性论证问题1.31.3 主要研究容：主要研究容：（1） 了解安全协议的基本概念和密码协议的安全性分析。（2） 研究运用公开密钥协议运行模式分析法，用此方法对公开密钥协议进行分析。（3） 尝试运用模型检测工具 SMV 系统对公开密钥协议的安全

17、性进行分析和研究。2 公开密钥认证协议2.1 公开密钥认证协议的基本概念通过网络来建立计算机系统之间的安全通信并证明此通信是安全的，不仅是一个日益受到关注的学术研究领域，而且也对社会生活具有非常重要的意义。在现实生活中，人们对协议并不陌生，人们都在自觉或不自觉地使用着各种协议。例如，在处理国际事物时，国家政府之间通常要遵守某种协议；在法律上，当事人之间常常要按照规定的法律程序去处理纠纷；在打扑克、订货、投票或到银行存款或取款时，都要遵守特定的协议。由于人们能够熟练地使用这些协议来有效地完成所要做的事情，所以很少有人去深入地考虑它们。所谓协议（Protocol） ，就是两个或两个以上的参与者为完

18、成某项特定的任务而采取的一系列步骤。这个定义包含三层含义：第一、协议自始至终是有序的过程，每一步骤必须依此执行。在前一步没有执行完之前，后面的步骤不可能执行。第二、协议至少需要两个参与者。一个人可以通过执行一系列的步骤来完成某项任务，但它不构成协议。第三、通过执行协议必须能够完成某项任务。即使某些东西看似协议，但没有完成任何任务，也不能成为协议，只不过是浪费时间的空操作。我们把为了完成某种安全任务的协议称为安全协议。安全协议为了保证安全性，在设计时必须采用密码技术。因此，我们也将安全协议称作公开密钥认证协议。所以，我们可给公开密钥认证协议再下一个定义：公开密钥认证协议公开密钥认证协议是建立在密

19、码体制基础上的一种交互通信的协议，它运行在计算机通信网或分布式系统中，借助于密码算法来达到密钥分配、身份认证等目的。 . . . 9 / 431.2 公开密钥认证协议分类到目前为止，还未有人对公开密钥认证协议进行过详细的分类。因为将公开密钥认证协议进行严格分类是很难的事情，从不同的角度出发，就有不同的分类方法。例如，根据公开密钥认证协议的功能，可以将其分为认证协议、密钥建立（交换、分配）协议、认证的密钥建立（交换、分配）协议等；根据 ISO 的七层参考模型，又可以将其分成高层协议和低层协议；按照协议中所采用的密码算法的种类，又可以分成双钥（或公钥）协议、单钥协议或混合协议等；根据参与协议的主体

20、个数可分为两方协议、三方协议和多方协议等。一般认为比较合理的分类方法是应该按照公开密钥认证协议的功能来分类，而不管协议具体采用何种密码技术。固把公开密钥认证协议分成以下几类：（1）密钥建立协议（Key Establishment Protocol） ，用于完成建立公开密钥。（2）认证建立协议（Authentication Protocol） ，向一个实体提供对他想要进行通信的另一个实体的身份的某种程度的确信。（3）认证的密钥建立协议（Authenticated Key Establishment Protocol） ，与另一身份已被证实或可被证实的实体之间建立共享秘密。 1.3 公开密钥认证协

21、议的安全性与其设计规公开密钥认证协议是许多分布系统安全的基础。确保这些协议能够安全地运行是极为重要的。虽然公开密钥认证协议中仅仅进行很少的几组消息传输，但是其中的每一消息的组是经过巧妙设计的，而且这些消息之间有着复杂的相互作用和制约。在设计公开密钥认证协议时，人们通常采用不同的密码体制。而且所设计的协议也常常应用于许多不同的通信环境。但是，现有的许多协议在设计上普遍存在着某些安全缺陷。造成认证协议存在安全漏洞的原因有很多，我们通过对协议的安全性进行分析，可以发现协议的设计漏洞，反过来可以进一步指导协议的设计。1.3.1 公开密钥认证协议的安全性分析与攻击在分析协议的安全性时，常用的方法是对协议

22、施加各种可能的攻击来测试协议的安全程度。公开密钥认证协议攻击的目标通常有三个：第一个是协议中所采用的密码算法；第二个是算法和协议中所采用的密码技术；第三个是协议本身。由于我们本课题只讨论公开密钥认证协议本身的安全性，因此我们将只考虑对协议自身的攻击，而假设协议中所采用的密码算法和密码技术均是安全的。一般对协议自身的攻 . . . 10 / 43击可以分为被动攻击和主动攻击。被动攻击是指协议外部的实体对协议执行的部分或整个过程实施窃听。攻击者对协议的窃听并不影响协议的执行，他所做的是对协议的消息进行观察，并试图从中获得协议中涉与的各方的某些信息。他们收集协议各方之间传递的消息，并对其进行密码分析

23、。这种攻击实际上属于一种惟密文攻击。被动攻击的特点是很难检测，因此我们在设计协议时应该尽量防止被动攻击，使公开密钥认证协议对于被动攻击是安全的，而不是试图检测它们。主动攻击对公开密钥认证协议来说具有更大的危险性。在这种攻击中，攻击者试图改变协议执行中的某些消息以达到获取信息、破坏系统或获得对资源的非授权的访问。他们可能在协议中加入新的消息、删除消息、替换消息、重发旧消息、干扰信道或修改计算机中存储的消息。在网络环境下，当通信各方彼此互不信赖时，这种攻击对协议的威胁显得更为严重。协议的攻击者不一定是局外人，他可能就是一个合法用户，可能是一个系统管理者，可能是几个人联手对协议发起攻击，也可能就是协

24、议中的一方。若主动攻击者是协议涉与的一方，我们称其为骗子（Cheater） 。他可能在协议执行中撒谎，或者根本不遵守协议。骗子也可以分为主动骗子和被动骗子。被动骗子遵守协议，但试图获得协议之外更多的信息；主动骗子则不遵守协议，对正在执行的协议进行干扰，试图冒充它方或欺骗对方，以达到各种非法目的。如果运行协议的参与者多数都是主动骗子，那么就很难保证协议的安全性。但是，在一些情况下，合法用户可以检测到主动欺骗的存在并采取一定的防措施。在实际应用中，对协议的攻击方法是多种多样的。对不同类型的公开密钥认证协议，存在着不同的攻击方法。我们很难将所有攻击方法一一列出，这里仅仅对几个常用的攻击方法进行简单介

25、绍。（1）重放攻击重放攻击主要指攻击者利用其消息再生能力生成诚实用户所期望的消息格式并重放，从而达到破坏协议安全性质的目的。防止重放攻击的关键是保证消息的新鲜性。（2）业务流分析攻击业务流分析的目标是通过检查数据包中未加密的字段和未保护的包的属性来发现受保护会话的信息。例如，通过检查未加密的 IP 源和目的地址（甚至 TCP 端口）或检查网络流量，业务流分析者就能确定哪些通信方在进行交互、使用什么类型的服务、有时甚至能发现有关商家或个人用户的信息。（3）中间人攻击当攻击者能够中途截获发送端的消息，读出它们并将它们发送给接收端(反之亦然)时， “中间人”攻击就可能发生。为实施“中间人”攻击，攻击

26、者将必须破解密钥，而这是一项比针对加密算法的攻击还难的工作。（4） “剪一贴”攻击 . . . 11 / 43此攻击的大致过程是：首先，从一些包含敏感数据的包中切下一段密文；然后，再把这段密文拼接到另外一段密文中，被拼接的这段密文是经过仔细选择的，使得接收端非常有可能泄漏出经过解密后的明文。（5）截获攻击入侵者通过截获协议中传输的消息进行攻击。（6）伪造攻击入侵者通过伪造一条假协议消息进行攻击。1.3.2 安全协议设计规在协议的设计过程中，我们通常要求协议具有足够的复杂性以抵御交织攻击。另一方面，我们还要尽量使协议保持足够的经济性和简单性，以便可应用于低层网络环境。如何设计公开密钥认证协议才能

27、满足安全性、有效性、完整性和公平性的要求呢？这就需要对我们的设计空间规定一些边界条件。归纳起来，常见的安全协议的设计规如下：(1)采用一次随机数来替代时戳在已有的许多安全协议设计中，人们多采用同步认证方式，即需要各认证实体之间严格保持一个同步时钟。在某些网络环境下，保持这样的同步时钟不难，但对于某些网络环境却十分困难。因此，建议在设计公开密钥认证协议时，应尽量地采用一次随机数来取代时戳，即采用异步认证方式。(2)具有抵御常见攻击的能力对于所设计的协议，我们必须能够证明它们对于一些常见的攻击方法，如已知或选择明文攻击、交织攻击等是安全的。换言之，攻击者永远不能从任何“回答”消息中，或修改过去的某

28、个消息，而推出有用的密码消息。(3)适用于任何网络结构的任何协议层所设计的协议不但必须能够适用于低层网络机制，而且还必须能用于应用层的认证。这就意味着协议中包含的密码消息必须要尽可能的短。如果协议采用了分组加密算法，那么我们期望此密码消息的长度等同于一组密文的长度。(4)适用于任何数据处理能力所设计的协议不但能够在智能卡上使用，而且也能够在仅有很小处理能力和无专用密码处理芯片的低级网络终端和工作站上（如 PC 机）上使用。这意味着协议必须具有尽可能少的密码运算。(5)可采用任何密码算法协议必须能够采用任何已知的和具有代表性的密码算法。这些算法可以是对称加密算法（如 DES，IDEA） ，也可以

29、是非对称加密算法（如 RSA） 。(6)不受出口的限制目前，各国政府对密码产品的进出口都进行了严格的控制。在设计公开密钥认证协议时，应该尽量做到使其不受任何地理上的限制。现在，大多数规定是针对分 . . . 12 / 43组加密/解密算法的进出口加以限制的。然而，对于那些仅仅用于数据完整性保护和认证功能的技术的进出口往往要容易得多。因此，对于某种技术，如果它仅依赖于数据完整性和认证技术而非数据加密函数，它取得进出口许可证的可能性就较大。例如，如果协议仅提供消息认证码功能，而不需要对大量的数据进行加密和解密，那么就容易获得进出口权。这就要求我们在设计协议时，尽量避免采用加密和解密函数。(7)便于

30、进行功能扩充协议对各种不同的通信环境具有很高的灵活性，允许对其进行可能的功能扩展，起码对一些比较显然应具有的功能加以扩展。特别是，协议在方案上应该能够支持多用户（多于两个）之间的密钥共享。另一个明显的扩展是它应该允许在消息中加载额外的域，进而可以将其作为协议的一部分加以认证。(8)最少的安全假设在进行协议设计时，我们常常要首先对网络环境进行风险分析，作出适当的初始安全假设。例如，各通信实体应该相信它们各自产生的密钥是好的，或者网络中心的认证服务器是可信赖的，或者安全管理员是可信赖的，等等。但是，初始假设越多，协议的安全性就越差。因此，我们应尽可能地减少初始安全假设的数目。以上八条协议设计规并不

31、是一成不变的，我们可以根据实际情况作出相应的补充或调整。但是，遵循上面提出的八条规是设计一个好协议的基础。1.4 公开密钥认证协议模型检测分析技术的研究与进展协议安全性分析是揭示公开密钥认证协议中存在漏洞的重要途径。目前，对公开密钥认证协议进行安全性分析的方法主要有两种：一种是攻击检验方法；另一种是采用形式化分析的方法。攻击检验方法也称非形式化分析方法，是公开密钥认证协议早期的主要分析方法。这种方法对协议进行分析一般是根据已知的各种攻击方法对协议进行攻击，以攻击是否有效来检验公开密钥认证协议是否安全。因为实际应用中，存在着许多未知的攻击方法，这种对公开密钥认证协议的非形式化分析方法只能发现协议

32、中是否存在着已知的缺陷，而不能全面客观地来分析公开密钥认证协议，可能导致不安全的协议经分析是安全的这样错误的结论。八十年代以后，随着对公开密钥认证协议安全性分析的进一步探索研究，公开密钥认证协议的形式化分析成为研究热点。安全协议的形式化分析是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。这种方法的出发点是希望将公开密钥认证协议形式化，然后借助于人工推导，甚至计算机的辅助分析，来判别公开密钥认证协议是否安全可靠。形式化分析方法和攻击检验方式相比，它能全面、深刻地检测到公开密钥认证协议中细微的漏洞。形式化分析方法不仅能发现现有的攻击方法对协议构成的威胁，而且还可能通过对公

33、开密钥认证协议的安全性分析，发现协议中细微的漏洞，从而发现对公开密钥认证协议新的攻击方 . . . 13 / 43法。模型检测技术（Model Checking Technology）是属于一般目的的公开密钥认证协议的形式化分析方法，它是验证有限状态系统的自动化分析工具，常用于硬件电路设计和通信协议。目前模型检测技术也是一种十分有效的协议形式化分析工具。模型检测技术最早是用于分析和模拟硬件工作过程的形式化方法，随着形式化方法的日益进步和应用领域的推广，现已应用于软件分析和通信协议模拟等多个领域，但用于安全协议的分析还是近几年新的应用。关于模型检测的研究越来越受到人们的关注，因为它对协议的自动验

34、证和协议的工程化设计具有指导意义。 在 1996 年，英国学者 Gavin Lowe 首先使用 CSP 和模型检测技术对公开密钥认证协议进行分析13，在这篇文章中，Gavin Lowe 首次采用 CSP 模型和 CSP 模型检测工具 FDR(故障偏差精炼检测器，Failures Divergences Refinement Checker)来分析 Needhan-Schroeder 公钥协议，并成功地找到一个 BAN 类逻辑等分析方法以前未发现的攻击。 模型检测技术应用于网络安全协议分析的成功，使学者们相继投入到这个领域。自 97 年起，计算机科学家与密码学家开始陆续应用模型检测这种新的形式方

35、法来分析网络安全协议的安全性，对多个网络安全协议进行了分析，成功地发现了许多攻击。 在文献17中 Steve Schneider 用 CSP 研究了公开密钥认证协议的安全性质，在文献18中 A.W.Roscoe 和 M.H.Goldsmith 基于对 CSP 和 FDR 研究，认为它们是公开密钥认证协议完美的检测工具。 在文献19中 W.Marrero 等提出了一种通用的模型检测器，构造了他们的模型与代数理论，并证明该模型的有效性。文中并对 Needhan-Schroeder 公钥协议进行了分析，也成功地发现了文献20所找到的攻击。 在文献21中 J.C.Mitchell 等设计了一种通用的状

36、态计数工具 Mur，并用它来分析公开密钥认证协议可能达到的状态，进一步得出公开密钥认证协议是否安全的结论。文中分析了 Needham-Schroeder 协议、Kerberos 协议和 TMN 协议，并找到了这些协议所有已知的攻击。在文献22中 Zhe Dang 等用 ASTRAL 这种实时系统形式化描述语言构造了模型检测器，文中并对 Needham-Schroeder 公钥协议和 TMN 协议进行了分析，也成功地发现了 Gavin Lowe 所找到的所有攻击。英国学者 Gavin Lowe 在模型检测上做出了非凡的创造性成果，相应的结论可参见2013。其中文献22是一篇关于模型检测大全性的文

37、章，文中试图为模型检测技术提供一个完整地解决方案。目前对于协议分析来讲，模型检测已经证明是一条非常成功的途径，这种方法发现了协议的许多以前未发现的新的攻击，极促进了网络安全协议分析与设计的研究工作。但模型检测仍然存在着许多需要进一步研究的问题，最主要的问题在于：模型检测适用于有限状态系统地分析工具，如何将公开密钥认证协议说明成有限状态系统，而又没有增加或减少公开密钥认证协议的安全性。这是一个需要继续深入 . . . 14 / 43研究和探索的核心问题。1.5 论文安排与研究成果本论文是在结合国家自然科学基金项目“公开密钥认证协议的模型检测分析”的基础上，围绕着公开密钥认证协议的模型检测技术进行

38、了深入的研究，本论文的工作成果如下：1.5.1 论文安排第二章：指出模型检测技术分析公开密钥认证协议的现状；研究模型检测技术分析公开密钥认证协议的基本理论；介绍两方公开密钥认证协议运行模式分析法并对其进行研究。第三章：介绍模型检测工具 SMV。第四章介绍公开密钥认证协议；运用运行模式分析法分析公开密钥认证协议安全性；尝试使用 SMV 检测两方公开密钥认证协议的模型检测。1.5.2 主要研究成果以下是我们取得的一些成果：(1) 系统的介绍了公开密钥认证协议的一些基本概念和公开密钥认证协议安全性分析的重要意义、研究进展和现状。(2)研究了模型检测技术和公开密钥认证协议运行模式分析法。(3)给出了运

39、用模型检测工具 SMV 分析公开密钥认证协议的方法。(4)运用运行模式分析法分析了公开密钥认证协议，并尝试使用 SMV 研究了公开密钥认证协议的安全性检测。 . . . 15 / 432 模型检测技术与运行模式分析法研究本章首先介绍了模型检测技术和模型检测技术在公开密钥认证协议分析领域取得的研究成果；随后引出了以此技术为理论依据的公开密钥认证协议运行模式分析法，并对其运行模式作了进一步的研究。2.1 引言模型检测技术原是用于分析和模拟硬件工作过程的形式化方法，随着形式化方法的推广和应用，模型检测技术现已用于软件分析和通信协议模拟等多个领域，但用于公开密钥认证协议的分析还是近几年比较新的应用。在

40、 1996 年，英国学者 Gavin Lowe 首先使用 CSP 和模型检测技术对公开密钥认证协议进行分析20。并首次采用 CSP 模型和 CSP 模型检测工具 FDR(故障偏差精炼检测器，Failures Divergences Refinement Checker)，来分析 Needham-Schroeder公钥协议。在这个模型中，协议参与者被说明成 CSP 中的进程(process)，消息说明成事件（event） ，进而将协议说明成一个通信顺序进程的集合，这些进程并行运行而且和他们的环境交互作用，其对公开密钥认证协议的验证是从协议说明中抽取一个模型（通常是一个有限状态转换系统） ，然后用

41、 FDR 检测，从而证明协议的安全性。此方法成功地找到 Needham-Schroeder 协议的一个以前从未发现的攻击。模型检测的成功，使研究者们相继投入到这个领域。实践证明对于公开密钥认证协议安全性分析来讲，模型检测是一条非常成功的途径。2.2 模型检测技术分析公开密钥认证协议的基本理论2.2.1 模型检测技术分析公开密钥认证协议的理论研究模型检测技术可以抽象地描述为：给定一个模型 M 和逻辑描述的性质 P，检查模型M 中性质 P 是否成立。模型检测技术对协议进行验证与分析，是通过检查在恶意攻击者存在的情况下，协议运行的所有可能的路径，来判断协议是否实现了其安全保证；如果没有，将给出攻击者

42、的攻击路径。模型检测用于有限状态系统的分析，要用模型检测技术分析公开密钥认证协议，就要研究如何为公开密钥认证协议构造有限状态系统。目前，模型检测技术分析公开密钥认证协议的基本方法主要采用英国学者 Gavin Lowe 研究成果，即：生成一个协议运行的小系统模型（通常是一个有限状态转换系统） ，以与一个可与协议互操作的攻击者模型，并用状态探测工具检测系统是否进入一个不安全状态，即是否存在 . . . 16 / 43对协议的攻击。并且基于代数理论证明：如果小系统是安全的，那么协议是安全的。这种方法提出了将大系统中协议安全的性质研究约化为小系统中协议安全性质的研究，这是目前这一领域的最新理论研究成果

43、。使用该方法发现了公开密钥认证协议许多以前未发现的新的攻击，极促进了公开密钥认证协议分析与设计的研究工作。（1 1）模型检测对被分析协议的基本假设：）模型检测对被分析协议的基本假设：任何一个系统都有其赖以存在的假设条件，用以避免结论的不当使用以与对一些限制的理解，同样，用模型检测技术分析公开密钥认证协议，对协议是有一定要求的，因为只有能用有限状态描述且满足一定条件的协议才能模型检测，并不是所有的公开密钥认证协议都能用模型检测技术来分析。在文献26中给出了能被模型检测技术所分析的公开密钥认证协议的基本假设，具体描述如下：1)加密部分从文字形式上是可以区分的公开密钥认证协议中所用到的加密项从文字上

44、就可以区分。这意味着一个主体接收到一个加密项就知道这个加密项属于哪个消息，是消息的哪一部分。这个假设可以防止入侵者重置协议中的消息，也能防止入侵者用另一条消息对原消息进行替换。这个条件很容易满足，例如只要在每个加密项中放入项的编号即可。2)身份的可确定性参与协议运行的所有主体的身份是可以通过协议运行中的加密项推导出来的。这样一个主体当他接收了一个加密项后，他就可以确定这个加密项是否为他而发。更进一步，如果这个加密项起源于一个诚实的主体，接收者可以判断出谁是加密项的产生者，谁是这个加密项的接收者。假设 1 和假设 2 容易满足，只要在每个加密项中明显包含每个主体的身份即可：更进一步说，如果消息是

45、来自诚实主体，那么接收方就能确定谁是消息的发送方和谁是消息的接收方。这两个假设条件可避免许多攻击，并且也使公开密钥认证协议的分析更容易。3)协议运行时不用协议运行期间建立的任何临时秘密如果一个特别的数据项不是那种要保持为秘密的数据项，那么一个监视通信的第三者就能够从有该数据项参与的运行中获知此数据项的值（或者这个值是公共信息，第三者早已知道它） ；更进一步，如果一个特别的密钥不是那种要保持为秘密的密钥，那么一个监视通信的第三者就能够通过持有该密钥的逆参与的运行中获知此密钥的数值（或者明显得到，或者通过加密某些数据项） 。（2 2）模型检测对基于模型的假设：）模型检测对基于模型的假设：1)完善加

46、密假设协议采用的密码系统是完美的，不考虑密码系统被攻破的情况等。2)入侵者的知识和能力可窃听与中途拦截系统中传送的任何消息； . . . 17 / 43可解密用他自己加密密钥（公钥或单钥）加密的消息；在系统中可插入新的消息；即使不知道加密部分的容，也可重放他所看到的任何消息（其中可改变明文部分） ；可运用他知道的所有知识（如临时值等） ，并可产生新的临时值等。（3 3）模型检测的结论）模型检测的结论运用模型检测技术分析公开密钥认证协议，就要构造小系统模型，关于小系统的定义和安全性质的定义和结论如下：1)小系统的定义：所谓小系统是指参与协议运行的各主体都是唯一的（例如，一个初始者，一个响应者）

47、，作用也是唯一的。这些主体也都是诚实的：他们严格按照协议规定和遵循自己的身份参与协议运行，并不与入侵者运行协议。2)安全性破坏定义：定义 1（强安全性破坏）：一个诚实的主体相信在协议运行中用到的一个值是仅他和另外诚实主体之间的共享秘密，但入侵者知道这个值。定义 2（一般安全性破坏）：一个诚实的主体相信在一个完整协议运行中用到的一个值是仅他和另外诚实主体之间的共享秘密，但入侵者知道这个值。小系统理论旨在解决：在协议与其环境条件下，如果小系统是安全的，那么大系统也是安全的。文献19中用大量篇幅，创建了一套基于代数方法的理论，并证明了如下结论：如果在某一特定的小系统中不存在对协议强安全性破坏的攻击，

48、那么对任意系统也不存在强安全性破坏的攻击，当然也就不存在攻击导致一般安全性破坏的攻击，即如果小系统是安全的，那么协议是安全的。小系统理论理论大大减少了安全协议分析的工作量，并从理论上增强了协议分析结果的可信任度。这个理论结果极促进了模型检测技术在安全协议分析领域的广泛应用，使安全协议形式化分析的主流从逻辑方法转向了模型检测，进而使安全协议的形式化分析更上一层楼。2.2.2 模型检测技术的现状与存在的问题用模型检测技术分析网络安全协议，只要对被分析的协议在小系统上进行强安全性破坏分析，就可以保证协议在任意系统上的安全性。这一理论大大减少了公开密钥认证协议分析的工作量，并从理论上保证了人们对协议分

49、析结果的信心。所以对于协议安全性分析来讲，模型检测技术已经证明是一条非常成功的途径。这种方法发现了协议的许多以前未发现的新的攻击。但模型检测技术仍然存在着一些问题：（1） 现有方法是否作到了理论上所要求的强安全型破坏分析？ . . . 18 / 43（2） 如何评价和衡量不同的检测方法和检测工具？（3） 这种分析方法对协议的种类有所限制，对具有满足以下情况的协议不能进行分析指导：1)黑匣协议。2)采用非标准的加密方式的协议。3)消息中包含长期秘密项的协议，如主体的私钥等这类协议，目前模型检测无法分析。我们将用于若干次协议运行的数据项，如主体的公开密钥、秘密密钥等定义为长期项。而将主体在一次协议

50、运行中引入的短期数据项，如临时值，短期密钥等定义为短期项。长期项和短期项是不同类型的数据项。因此，模型检测分析公开密钥认证协议仍然存在着不少问题需要解决，其关键在于模型检测只能分析有限状态系统，这必然对公开密钥认证协议有所要求，因为协议要能用有限状态系统来描述。并且模型检测技术本身也存在着诸如可以生成现实的攻击路径，但很难辨别攻击造成的原因等问题。未来的研究趋势是如何扩大模型检测分析公开密钥认证协议的种类并采用混合分析技术。2.3 两方公开密钥认证协议运行模式分析法2.3.1 两方公开密钥认证协议运行模式分析法简介运行模式分析法由模型检测技术分析公开密钥认证协议若干结论推导而来。模型检测技术分

51、析公开密钥认证协议的基本方法是构造一个运行协议的小系统模型（通常是一个有限状态系统） ，同时结合一个通常意义下的入侵者模型，他能与协议交互作用，利用状态探测工具来发现系统是否进入一个不安全状态，也就是说是否对协议存在一个攻击。这种方法发现了公开密钥认证协议许多以前未发现的新的攻击，极促进了公开密钥认证协议分析与设计的研究工作。在文献19中基于代数方法证明了对于一个构造的小系统，若协议在小系统中是安全的，则可以不用考虑任意系统。因为一个公开密钥认证协议如果在任意一个系统上有攻击的话，那么它一定有攻击在小系统上。这样只要对被分析的协议在小系统上进行安全分析，就可以保证协议在任意系统上的安全性。这大

52、大减少了公开密钥认证协议分析的工作量，并从理论上保证了人们对协议分析结果的信心。对公开密钥认证协议构造小系统模型时，对于小系统的分析规模必须要进行恰当的指定。文献22中给出当对一个公开密钥认证协议执行有限状态模型检测时，有一些涉与分析对象和分析规模的参数必须在系统中说明，它们是：（1）参与协议运行的诚实主体的个数；（2）每个诚实主体的身份；（3）每个诚实主体所能运行协议的次数； . . . 19 / 43（4）入侵者的身份和能运行协议的次数。（5）入侵者的初始知识和获取信息的能力等。对于两方公开密钥认证协议（即参与协议运行的只有两个主体，初始者和响应者） ，文献18中定义了如下的小系统（有限状

53、态系统）：参与协议运行的主体集合：初始者 A，响应者 B，入侵者 I。其中 A 和 B 是诚实的主体，他们将严格按照初始者和响应者的身份参与协议运行，并且 A 和 B 只运行一次公开密钥认证协议，而入侵者 I 则不受此限制，他既可以以自己本来身份 I参与协议运行，也可以冒充 A 和 B 的身份以 I(A)和 I(B)方式参与协议运行，并可以多次运行公开密钥认证协议。在此小系统前提下，两方公开密钥认证协议所有可能的初始者集合和所有可能的响应者集合如下所示：初始者集合：A，I，I(A)；响应者集合：B，I，I(B)。模型检测试图检查协议运行的所有可能的路径，对于只有合法用户 A、B 与入侵者 I

54、的两方公开密钥认证协议，根据对 A、B、I 身份和运行次数的限制，可以得出对于两方公开密钥认证协议初始者和响应者所有可能的运行模式，共有十四种。下面是双方公开密钥认证协议运行模式的运用，其中 XY 表示一次两方协议运行，X是协议的初始者，Y 是协议的响应者。这十四种运行模式具体描述如下：（1） AB在这种运行模式中，A 和 B 运行一次协议，其中 A 作为初始者，B 作为响应者，这是协议正常运行情况。（2） AB II这种运行模式包含了两个并行运行的协议，A 和 I 运行一次协议，I 和 I 自己运行一次协议。（3） AI这种运行模式只有一次协议运行，即 A 和 I 运行一次协议。（4） AI

55、 IB这种运行模式包含了两个并行运行的协议，A 和 I 运行一次协议，I 和 B 运行一次协议。（5） AI I(A) B这种运行模式包含了两个并行运行的协议，A 和 I 运行一次协议，I 冒充 A 和 B运行一次协议。（6） AI II这种运行模式包含了两个并行运行的协议，A 和 I 运行一次协议，I 和 I 自己运行一次协议。（7） AI(B)在这种运行模式中，A 和冒充 B 的 I 运行协议。（8） AI(B) IB . . . 20 / 43这种运行模式包含了两个并行运行的协议，A 和冒充 B 的 I 运行协议，I 和 B 运行一次协议。（9） AI(B) I(A)B这种运行模式包含了

56、两个并行运行的协议，A 和冒充 B 的 I 运行协议，I 冒充 A和 B 运行一次协议。（10）AI(B) II这种运行模式包含了两个并行运行的协议，A 和冒充 B 的 I 运行协议，I 和 I 自己运行一次协议。（11）IB在这种运行模式中，I 和 B 运行一次协议。（12）IB II这种运行模式包含了两个并行运行的协议，I 和 B 运行一次协议，I 和 I 自己运行一次协议。（13）I(A) B在这种运行模式中，I 冒充 A 和 B 运行一次协议。（14）I(A) B II这种运行模式包含了两个并行运行的协议，I 冒充 A 和 B 运行一次协议，I 和 I自己运行一次协议。对于两方公开密钥

57、认证协议生成的小系统进行安全性分析，只要模型检测这 14种可能的运行模式，如果小系统不存在攻击的话，则协议是安全的。2.3.2 对两方公开密钥认证协议运行模式的研究通过研究两方公开密钥认证协议运行模式中的这十四种运行模式，我们可以发现有些运行模式是不需要进行分析的。例如对于两方公开密钥认证协议，II 这种情况对于入侵者 I 来讲是不能增加任何知识的，故此运行情况中有 II 的都可以不用分析，属于这种情况的有运行模式（2） 、模式（6） 、模式（10） 、模式（12） 、模式（14） 。对于运行模式（3） 、模式（11） ，协议只有一次运行，A 或 B 都清楚自己正和一个合法用户 I 运行协议，

58、同时入侵者 I 以自身身份参与运行可以知道这一次协议运行中的所有信息，没有可骗的第三方，因此也不必分析。这样对于两方公开密钥认证协议只要分析剩余的 7 种运行模式即可。也就是说如果对这 7 种运行模式进行分析，协议没有攻击的话，则整个协议就是安全的，但有一个前提：对被分析的两方公开密钥认证协议必须满足本章中所给出的对公开密钥认证协议的所有假设，否则无法从理论上保证分析结果的正确性。这 7 种运行模式列举如下：（1）AB（2）AI IB . . . 21 / 43（3）AI I(A) B（4）AI(B) IB（5）AI(B) I(A)B（6）AI(B)（7）I(A) B2.4 小结本章主要介绍了

59、模型检测技术和基于模型检测技术的两方公开密钥认证协议运行模式分析法，并对此方法所需分析的运行模式进行了研究。运用运行模式分析法分析公开密钥认证协议有如下好处：(1)使用运行模式法分析公开密钥认证协议时，可以独立于任何模型检测工具来分析符合要求的两方公开密钥认证协议，并且可以检测不同模型检测工具在分析两方公开密钥认证协议时是否完全覆盖了这些运行模式，从而保证分析的完整性和正确性。(2)使用运行模式法分析公开密钥认证协议时，可以脱离任何模型检测工具，手工分析符合要求的两方公开密钥认证协议。这对于分析简单的两方公开密钥认证协议更为方便。 . . . 22 / 433 模型检测工具 SMV3.1 引言

60、SMV 系统是一项为了要检测有限状态系统是否符合 CTL（Computation Tree Logic）逻辑所表达的系统属性的工具。SMV 的输入语言允许被设计成有限状态系统的描述，它的围包括从全同步到全异步，以与从具体到抽象。这种语言提供了模块分层描述，以与复用组成功能的定义。CTL 逻辑允许一种丰富的时态属性，它包括安全性、灵活性、直接性以与死锁的解除等等。SMV 使用 OBDD 基础的符号模型检测等算法来有效指定在 CTL 中的表达是否是满意的。模型检测工具通过在模型中建立一个包含所有状态的图的方式来验证系统性质。在 SMV 中，模型检测程序只检测那些从初始状态可以到达的状态的路径是否满