（信息与通信工程专业论文）关于密码协议的形式化分析方法的研究.pdf

l ，ll；，ill引， i，f 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均己在论文中作了明 确的说明并表示谢意。 签名：力 岔 日期：厶。年钼胃日 论文使用授权 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁 盘，允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名：丛导师签名： 日期：厶 ， 一 摘要 摘要 随着信息技术的快速发展和广泛应用，诸如电子商务这类需要高度安全性的 应用逐渐普及，建立安全信道的重要性可想而知。在网络这个特殊的大环境里， 两个互相不认识的主体如果想要达成某种通信目的，必须要在密码技术保障的前 提下进行。 虽然现阶段对密码协议的分析方法的研究已经有了很多观点，但是还没有一 种被广泛认同的可以作为工业标准的方法，所以对于密码协议的形式化分析方法 仍然是一个开放性的热点问题，而且具有重要的理论意义。 本文首先介绍了密码学领域的一些基本概念，密码协议的分类，以及在密码 协议中需要用到的一些重要的密码学技术：保密性，数据完整性，抗抵赖性以及 消息认证性。为了使得分析方法的设计更加具有针对性，本文假设所讨论的协议 都是在底层密码技术安全的前提下进行的；然后，本文通过分析密码协议形式化 方法的主流观点，总结出这些观点存在的缺陷。接着通过对一些经典的攻击方式 的分析，引出本文的主题，即对密码协议安全性分析的形式化方法，提出这套方 法的依据在于b e l l a r e 和r o g a w a y 对于密码协议安全的公式化定义，以及作者在 学习过程中总结出的一些密码协议的设计原则。这个形式化方法分为五个模块， 首先对协议进行前四个模块的检验，然后在第五个模块中对协议进行安全性证明。 本文通过对大量相关文献的研究，深深的体会到对于密码协议安全性证明的困难 性。所以本文所采用的证明方式基于不同于传统密码学证明的逻辑方式，并不是 将攻击者攻破协议的行为归约到攻破数学难题上，而是归约到对已知假设的否定 上，每个步骤在逻辑上都严密合理。接下来利用这套方法对一些工业协议例如s s h ， k e r b e r o s 以及s t s 协议进行分析；最后，对密码协议的研究做出总结和展望。 关键字：密码协议，密码学技术，形式化方法。 _ _ - 。 一 _ ， a b s t r a c t a b s t r a c t a l o n gw i t ht h er a p i dd e v e l o p m e n ta n d w i d ea p p l i c a t i o no fi n f o r m a t i o nt e c h n o l o g y , t h ea p p l i c a t i o n ，s u c ha se c o m m e r c e ，b e c o m e sm o r ea n dm o r ep o p u l a r s oy o uc a l l i m a g i n eh o wi m p o r t a n tt h ei n f o r m a t i o ns e c u r i t yi s i nt h en e t w o r k ，w h i c hi ss os p e c i a l a n do p e n i ft w op a r t i c i p a n t sw h od o n tk n o we a c ho t h e rw a n tt oh a v ec o m m u n i c a t i o n , t h ec o u r s em u s tb ep r o t e c t e db yc r y p t o g r a p h y t h e r eh a sb e e nm a n ys t a r t o i n to ft h ec r y p t o g r a p h yp r o t o c o l ss e c u r i t yb yn o w , b u t n o n eo ft h e mh a sb e c o m et h es t a n d a r do ft h ea n a l y s i sm e t h o d ，s ot h er e s e a r c ho ft h e f o r m a l i z e dm e t h o do ft h ec r y p t o g r a p h yp r o t o c o li sr e m a i nt h eh o tt o p i c f i r s t ，t h i st h e s i si n t r o d u c e ss o m eb a s i ck n o w l e d g ea b o u tc r y p t o g r a p h y , t h es o r to f t h ec r y p t o g r a p h yp r o t o c o l ，a n ds o m ei m p o r t a n tc r y p t o g r a p h yt e c h n i c s ：e n - d e c r y p t i o n ， d a t ai n t e 酣t y , d i g i t a ls i g n a t u r e ，a n dm e s s a g ea u t h e n t i c a t i o n f o rm a k i n gt h ea n a l y s i s m e t h o dm o r ee f f i c i e n t ，a l lt h ep r o t o c o l so ft h i st h e s i si sa n a l y s e du n d e rt h es u p p o s i n g t h a tt h el o wl a y e rc r y p t o g r a p h yt e c h n i c sa r es a f e ；t h e n ，t h r o u g ha n a l y z i n gt h em a i n s t a n d p o i n to f t h ep r o t o c o la n a l y s i s ，c o n c l u d es o m ed i s a d v a n t a g e so ft h e m a n dt h r o u g h a n a l y z i n gs o m ec l a s s i c a la t t a c kt ot h ep r o t o c o l s ，c o n c l u d et h es u b j e c to ft h i s t h e s i s m e f o r m a l i z em e t h o da b o u tc r y p t o g r a p h yp r o t o c o l s ，w h i c hd e p e n d s o nb e l l a r ea n d r o g a w a y sd e f i n i t i o no f t h ep r o t o c o l ss e c u r i t y , a n ds o m ed e s i g np r i n c i p l eb yt h ea u t h o r t h r o u g ht h es t u d yi n t h e s ey e a r s t h i sm e t h o dh a s5m o d u l e s ，f i r s t ，t h ep r o t o c o li s a n a l y s e db yt h ef i r s t4m o d u l e s ，a n dt h e ni t ss e c u r i t yw o u l db ep r o v e db yt h e l a s t m o d u l e t h r o u g ht h ea n a l y s i so fm a n yl i t e r a t u r e sa b o u tt h ep r o v a b i l i t yt e c h n i c , t h e a u t h o rf i n dt h a tt h ed i f f i c u l t yo ft h ep r o o fo fc r y p t o g r a p h yp r o t o c o l ss e c u r i t y t h e r e f o r e ， t h i st h e s i s ，sp r o o fi sb a s e do nal o g i c a li d e aw h i c hi sd i f f e r e n tf r o mt h ec l a s s i c a l c r y p t o g r a p h y sp r o o f e v e r ys t e po ft h ep r o o fi s a c c u r a t e t h e n ，u s et h ef o r m a l i z e m e t h o dt ot e s ts o m er e a lc o m m u n i c a t i o np r o t o c o l s ，s u c ha ss s h ，k e r b e r o s ，a n ds t s f i n a l l y , t h i st h e s i ss u m su pt h ec o n t e n ta n d m a k e p r o s p e c to f t h i sf i e l d k e y w o r d s ：c r y p t o g r a p h yp r o t o c o l ，c r y p t o g r a p h yt e c h n i c ，f o r m a l i z e dm e t h o d 1 1 一 ， 目录 目录 第一章绪论。1 1 1 密码协议相关的密码技术1 1 2 密码协议简介。2 1 2 1 密码协议的概念2 1 2 2 密码协议的历史2 1 2 3 对于密码协议的直观描述2 1 3国内外研究现状3 1 4 论文主要工作、创新点及组织结构4 1 4 1 论文主要工作和创新点4 1 4 2 论文组织结构4 第二章密码协议的常见缺陷以及相应的攻击。6 2 1 攻击者的模型6 2 2分析密码协议的主要困难7 2 3 对于密码协议的常见攻击7 2 3 1 重放攻击8 2 3 2 中间人攻击1 l 2 3 3 平行会话攻击1 3 2 3 4 类型攻击1 4 2 3 5 攻击方法难以穷尽1 5 2 4 本章小结15 第三章密码协议形式化分析方法16 3 1计算观点16 3 1 1 相互认证的目标：匹配对话1 6 3 1 2 相互认证成功的定义1 6 3 1 3m a p l 协议以及其安全性证明1 7 3 1 4 对计算观点的分析1 9 3 2 逻辑符号观点1 9 3 2 1b a n 逻辑1 9 i v 目录 3 2 2b a n 逻辑框架介绍2 0 3 2 3b a n 逻辑分析举例2 2 3 2 4b a n 逻辑的缺陷以及提出新的形式化方法的必要性2 5 3 3 状态探查观点2 6 3 4 对这三种观点的理解2 6 3 5本章小结2 7 第四章一种新的密码协议形式化分析方法2 8 4 1对密码协议的非形式化分析方法2 8 4 1 1 非形式化分析方法简介2 8 4 1 2 提出非形式化分析方法的原因3 0 4 1 3 非形式化分析方法的作用3 0 4 2 形式化分析方法的基本框架3 2 4 3系统各子模块的功能说明3 2 4 3 1 模块l ：对协议进行符号化3 2 4 3 2 模块2 ：对消息本身进行的源认证3 3 4 3 3 模块3 ：新鲜性标识符对于各个主体的关联验证3 5 4 3 4 模块4 ：进行w e n b om a o 规则检验3 7 4 3 5 模块5 ：对协议进行安全性证明3 9 4 4 本章小结4 8 第五章新形式化分析方法的实践应用4 9 5 1形式化分析方法的应用4 9 5 2 对s s h 协议的分析4 9 5 2 1s s h 协议简介4 9 5 2 2s s h 协议的整体架构4 9 5 2 3s s h 传输层协议5 0 5 2 4 对s s h 传输层协议的安全性进行安全性分析5 1 5 3对k c r b e r o s 协议的分析5 2 5 3 1k e r b c r o s 协议简介5 2 5 3 2k e r b c r o s 协议的总体结构5 2 5 3 3 认证服务交换5 3 5 3 4与t g s 运行协议5 3 5 3 5 与应用服务器运行协议5 4 v 、_ _ _ _ _ _ _ _ _ _ _ _ 一 ， 电子科技大学硕士学位论文 5 3 6 对k e r b e r o s 协议的安全性进行形式化分析5 4 5 4 对工作站工作站( s t s ) 协议的分析5 6 5 4 1s t s 协议简介5 6 5 4 2 对s t s 协议的安全性进行形式化分析5 8 5 5 本文提出的形式化方法的优缺点6 2 5 6 本章小结6 3 第六章总结和展望6 4 致谢6 5 参考文献6 6 v i ， 一 第一章绪论 第一章绪论 随着互联网技术的高速发展，人们的生活发生着革命性的变化，短短的几十 年时间，信息技术提供的便利已经深入人心，就在人人都为大量的资源共享，方 便快捷的服务感到幸福的时候，相应的安全隐患也随之而来。网络是个虚拟的世 界，虚拟就意味着不真实，这时候，密码协议就出现了。 1 1密码协议相关的密码技术 密码协议中用到了很多的基本的密码学技术n3 ，总结如下： 1 ) 保密性服务 协议中的消息在网络中传输的时候，发送者和接收者可能要求消息的内容保 密，也就是说其他主体不能理解加密了的消息的内容。现代密码学提供两种加密 算法，对称加密和非对称加密。其中对称加密算法效率比后者要高，故多用来加 密大量的数据；而非对称加密算法则由于其独特的性质可以用来协商会话密钥， 然而由于其算法的效率较对称加密技术低，所以多用来加密少量重要的数据，比 如密钥等。在密码协议中主要通过这两种密码算法来实现保密性。 2 ) 数据完整性服务 所谓数据完整性是指数据在传输过程中由密码技术来保证不被非授权用户修 改，也即是说如果数据在传输过程中被非授权的用户修改了，那么授权用户能够 通过验证消息发现这个行为。对称加密算法通过产生篡改检测码来实现： 篡改检测码的生成：m d c = f ( k | | m ) ( 其中f ( ) 是带密钥的杂凑函数，k 是 对称密码算法的密钥，m 是数据) 非对称加密算法则可以通过数字签名来实现数据的完整性服务。 3 ) 抗抵赖服务 抗抵赖服务是指某个主体对自己发出过的消息承担责任，通过非对称密码技 术的数字签名和一个仲裁方即可实现这个目的。 本文重点研究的是密码协议本身的安全性，所以以上提到的密码学技术假设 都是安全的，当然涉及到底层的密钥协商协议的时候，不可避免的要讨论细节的 安全性。 电子科技大学硕士学位论文 1 2 密码协议简介 1 2 1密码协议的概念 所谓协议乜1 ，就是指两个或者两个以上的参与者为完成某项特定的任务而采取 的一系列步骤。此定义包括三个含义：第一，协议自始至终是个有序的过程，每 一个步骤必须依次执行。在前一步没完成之前，后面的步骤不能执行。第二，协 议至少需要两个主体。一个人可以通过一系列步骤来完成某项任务，但它不能称 之为协议。第三，通过执行协议必须能够完成某项任务。某些东西看似协议，但 它却没有完成任何的任务，故不能称之为协议，只不过是浪费时间。 密码协议可以分为两类，即身份认证协议和密钥协商协议。而在进行密钥协 商之前通常都需要双方的身份认证，在这里将两者分开讨论可以使问题更加清晰。 1 2 2 密码协议的历史 实现密码协议的方法有很多，有基于口令的认证，基于生物特征的认证，基 于智能卡的认证等等。早期的保证安全的方法是利用物理隔离的方法，即对未被 授权的用户限制其物理连接。在计算机中，各个用户通过用户名和口令的方式来 认证各自的身份。这种方法对于所有用户在一个安全的信道中是可行的。但是， 在当今高度共享资源的网络环境中，这种物理隔离的方法已经不可行了，而且安 全信道需要一系列密码协议来建立。在这种情况下，对于安全性要求高的场所， 如电子商务等，仅用简单的用户名和口令的方式是不够的，因为它可能被攻击者 篡改和重放。因此，人们提出了基于密码体制的认证方式，具体是通过协议来实 现。为了这个目的，人们提出过很多的密码协议，通过这些协议来解决认证的问 题。但是由于密码协议的灵活性，逻辑的模糊性，很难设计出一套方法来对协议 进行安全性强度的分析。要知道，只依靠经验来设计如此重要的认证协议是多么 危险的事情，所以对于密码协议的形式化分析的研究一刻都没有停息过。 1 2 3 对于密码协议的直观描述 两个主体a 和b 之间的密码协议是可以这样描述的，如果两个主体a 和b 要 进行通信，比如说a 要把一个消息m 发送给不认识的b ，这个过程如果成功了， 2 第一章绪论 那么直观来讲，产生的结果就好像是a 和b 亲自见了一面，互相拿出彼此的身份 证后，a 手递手的把消息m 递给了b 。也即是说，这个协议运行成功了，如果： 1 ) a 能够确定b 是否已经收到了消息m ；( 收到消息后的验证) 2 ) b 能够确定消息m 是否来自于a ；( 消息源认证) 3 ) a 和b 能够确定整个过程中消息m 是否没有被除了a 的人修改；( 数据完整 性) 在这个密码协议中，如果双方要成功运行协议，则以上的描述还是不够的。 这个直观描述中没有涉及到一个非常重要的方面，即消息新鲜性，对于这一点， 在后面的分析讨论中会特别重视到。下面来谈谈密钥协商协议，密钥的建立通常 可以通过两种方式，第一种是由一个主体单独生成会话密钥，然后进行传递的方 式。这种方法如果采用对称加密方式来设计协议的话，则需要可信三方的加入， 如果采用的是非对称加密方式的话，则两方即可。这里需要说明一点，可信第三 方始终都是协议中的一个潜在的威胁，所以有很多文献 5 6 l 8 1 曾经对可信第三方 的去除方法做了研究。这种通过一方建立密钥，然后传递的方式又称为密钥建立： 第二种则是双方都输入一些生成会话密钥的参数，用基于d i f f i e h e l i m a n 协议阻1 的方法来进行密钥建立，这种方法又称为密钥协商。 1 3 国内外研究现状 在现阶段，对于密码协议的形式化分析的研究主要集中在三种观点上，即计 算观点、逻辑符号观点以及状态探查观点。下面分别对这三种观点进行一下简要 的介绍。 计算观点是最容易想到的分析协议的观点，因为它和研究加解密算法和数字 签名算法的方法有同样的思想，都是在计算模型下的可证明安全的思想们。它证 明协议安全的思想是将攻击者成功攻破密码体制的行为在多项式时间内归约到一 个计算复杂性理论中的数学难题上来，从而通过得出矛盾来证明协议的安全。本 文的安全性证明也借鉴了这种思想的一部分。 对于这种观点，b e l l a r e 和r o g a w a y 。1 2 3 是最早的也是最成功的研究者，他们 最先使用计算模型的方法证明认证和认证的密钥建立协议的安全性。他们的证明 是把对协议的所谓成功攻击转化为伪随机性的失败，即可以用一个多项式时间的 分辨器将伪随机函数的输出同真随机函数的输出分辨开来；换句话说，否定伪随 机函数的存在性。 电子科技大学硕士学位论文 逻辑符号观点的思想是将协议的安全特性表达成一些可操作的抽象符号的集 合，通过一些符号式的推导关系，最终得到定义为安全的符号式，从而证明协议 的安全。这种观点最著名的代表思想是由b u r r o w s 、a b a d i 和n e e d h a m 创造出的b a n 逻辑。它提供一个逻辑公式的集合来模型化协议参与者的行为。 b a n 逻辑的公理系统是在直观的基础上假定的，也就是以人广泛认同的形式定 义协议的安全。可以说b a n 逻辑开创了对于密码协议的形式化分析方法的先河。 状态探查观点的分析方法是将复杂的协议模型化为一个状态系统。状态系统 的性质可以通过一些状态满足关系来表示。对协议的分析涉及到对状态空间的探 查，来验证某些性质是否满足。 这种观点的代表作是c s p 方法，c s p 表示通信时序进程，是由h o a r e h 钔提出来 的。在c s p 中，行为是顺序发生事件的一个有限序列。例如一个0 长的序列，代 表什么都不做。所有可能时间的集合称为进程字母表。这些进程可以执行行动的 一个实例就是具有某种性质的一个比特串。 1 4 论文主要工作、创新点及组织结构 1 4 1 论文主要工作和创新点 本文的主要工作主要有两个方面，第一，通过对大量的密码协议的分析，对 密码协议的种类做了归纳，并且设计出一套新的密码协议形式化分析方法。首先 用统一的符号将协议公式化，然后通过一些设计原则对协议进行安全性的检测， 最后通过安全性证明作为这个系统的结尾，使得这一套方法更加的完整；第二， 通过使用这一套形式化分析方法对一些著名协议进行分析，对这套方法的实用性 进行了检验和评估。 1 4 2 论文组织结构 本文共分为六章，各章节内容安排如下： 第一章介绍了本文所研究的相关的密码协议的历史，以及所要用到的一些底 层的密码学技术的相关概念，并且介绍了国内外对于密码协议形式化分析方法的 研究现状。 第二章对目前出现过的典型的攻击方式进行了总结，并且分析了受到这种攻 4 目了然，更加清晰。 第五章也是本文的核心部分，主要是对本文所提出来的形式化方法的实用性 进行了检验，通过对三个著名协议：s s h 和k e r b e r o s 以及i k e 协议的核心部分s t s 协议的分析，来说明本文所提出的形式化方法能够应用到实际中，并且在最后总 结了这套形式化方法的优势以及缺陷。 第六章总结了全文的要点，并且对这个领域的前景进行了展望。 电子科技大学硕士学位论文 第二章密码协议的常见缺陷以及相应的攻击 在分析密码协议形式化方法之前， 以及相应的攻击方式进行简单的描述， 2 1 攻击者的模型 本章首先就目前密码协议存在的常见缺陷 为后续的密码协议的分析提供参考。 著名的d o l e v - y a o 威胁模型司是研究攻击者行为和能力的典型模式。 由于计算机、设备和资源所构成的大型网络是典型开放的，这就意味着一个 主体能够进入这样的网络，并通过该网络来发送和接收消息，这里的主体可以是 台计算机，一个设备，一些资源、服务的提供者，总之可以是网络中的任何节 点。在这样的开放环境中，我们必须想到会有入侵者，他们会做各种坏事，不仅 仅是被动的窃听，而且会主动的修改、伪造、复制、改变路由、截断或者注入消 息。注入的消息可能是恶意的并对接收端主体产生破坏性的影响。这些人被称为 主动攻击者。 在这样脆弱的环境中，攻击者有如下特征： 1 ) 他能获得经过网络的任何消息； 2 ) 他是网络的一个合法使用者，因而能够发起与任何其他用户的对话； 3 ) 他有机会成为任何主体发出信息的接收者： 4 ) 他能够冒充任何别的主体给任意主体发送消息。 因此，在d o l e v - y a o 模型中，发送到网络中的任何消息都可以看成是发送给 攻击者来处理的。因而从网络接收到的任何消息也都可以看成是由攻击者处理过 的。换句话说，可以认为攻击者已完全控制了整个网络。 但是，并不认为攻击者是全能的，也就是说还有一些攻击者所不能做的事情。 对于他不能做的事情，具体量化如下： 1 ) 攻击者不能猜到从足够大的空间中选出的随机数： 2 ) 没有正确的密钥，攻击者不能由给定的密文恢复出明文：对于完善加密的 算法，攻击者也不能从给定的明文构造出密文来； 3 ) 攻击者不能求出私有部分，比如与给定公钥绑定的私钥； 4 ) 攻击者虽然能够控制我们的计算和通信环境的大部分，但是一般情况下他 6 第二章密码协议的常见缺陷以及相应的攻击类型 不能控制计算环境中的许多私有区域，如访问离线设备等。 2 2 分析密码协议的主要困难 目前设计出的密码协议已经有很多了，但是许多协议刚一发表，便被发现有 安全漏洞。如n s 认证协议在1 9 8 1 年被d e n n i n g 和s a c c o n 6 3 发现存在安全隐患：当 一个攻击者用一个己被破译的旧会话密钥冒充新的时( 重放攻击) ，攻击成功。据 g a v i nl o w e ( 协议分析专家) n 7 1 估计，超过一半的公开协议事实上不能保证它们 的安全目标。 造成密码协议失败的原因主要有两点：第一点是人为因素，即密码协议的设 计者缺乏对协议的深度理解，往往设计出来的协议和预想的目标有很大的偏差。 有时候错误的利用密码学技术也会导致协议的安全性能的下降，比如滥用保密性 服务就会给攻击者以可乘之机( 后文会讨论) ；第二点是客观因素，密码协议的设 计不同于加密算法和签名算法的设计那样模式固定、目的鲜明，加密算法对于攻 击者的行为描述的很全面和透彻，这对于模拟攻击者的行为提供了很大的便利， 完全能够预料到攻击者可能采用的攻击手段，然后对症下药即可。签名算法也是 一样的。但是对于密码协议的攻击则以多样化，难以预料为主要特点，无法完全 预测，有时候只能靠经验来模拟攻击者的行为，这无疑是非常被动的防御。加之 密码协议的灵活性，步骤繁多，提供给攻击者的攻击点也就很多，这也就造成了 对于密码协议安全性分析的复杂性。 2 3 对于密码协议的常见攻击 在系统分析密码协议的安全性以前，有必要对于常见的攻击种类进行一下总 结。对密码协议的攻击目标主要有三点： 1 ) 协议中的密码算法： 2 ) 算法和协议中采用的密码技术： 3 ) 协议本身。 对于身份认证协议的安全性分析，前两点可以不考虑，假定是理想状况即可， 但是对于密钥协商协议，由于涉及到一些基本的单向函数，而且互相传递的消息 有很大的关联性，所以对其安全性的考虑会更加细化，而且需要进行严格的安全 性证明。 电子科技大学硕士学位论文 对协议本身的攻击可以分为被动攻击和主动攻击。 被动攻击是指协议外部的实体对协议进行窃听。攻击者只对协议窃听并不会 影响协议的执行，他所做的知识对协议的消息进行观察，并努力从中得到用的信 息，帮助其破解协议的安全性。他们收集协议各方之间传递的消息，并对其进行 密码分析和逻辑分析。这种攻击是一种唯密文攻击，被动攻击的特点是难以检测， 因此在设计协议时应该意识到所传递的消息都经过了攻击者的手，想要防止攻击 者窃听是不可能的。 主动攻击对于密码协议来说具有更大的危险性。在这种攻击中，攻击者试图 改变协议执行中的某些消息以达到获取信息、破坏系统或者获得对资源的非授权 访问等目的。他们可能会篡改消息、替换消息、重放旧消息等。在网络环境中， 通信双方和可能彼此不信任，这种攻击对协议的威胁就更加严重了。攻击者可能 并不是一个局外人，相反很可能是一个合法用户，他具有一定的合法权限，那么 他自然就可以冒充和欺骗对方了，这种攻击者对于协议安全性的危害是巨大的。 显然，安全的密码协议对于这样的攻击者应该是安全的。 实际上，对协议的攻击方法是多种多样的。大致来说可以分为如下几类：重 放攻击、中间人攻击、并行会话攻击等等。 2 3 1重放攻击 重放攻击是攻击者捕获以前协议运行时的消息，并加以分析，破译了相关的 内容，比如会话密钥等，而后在攻击过程中用已破译的密钥来加密自己需要的内 容来替换协议中的消息，从而达到自己的目的。 重放攻击是最常见的攻击方式之一，在前面介绍过的对于密码协议的直观描 述中都不能很好地对这种攻击进行描述，所以可见对这种攻击的免疫是涉及密码 协议的第一要务。 作为例子，我们来看一个密钥建立协议，这个密钥建立过程属于第一种方式， 即传递密钥的方式，而且采用了对称密码算法来设计，故而需要一个可信的第三 方，记为t a 。 协议2 - 1n e e d h a m s c h r o e d e r 协议u 羽，如图2 1 所示。 假定a 和t r e n d 共享会话密钥丸7 ；b 和t r e n d 共享会话密钥k 占7 ： 目标a 和b 希望建立一个新的共享会话密钥k 。 l a 随机生成 ，向t r e n d 发送：a ，b ，。； 第二章密码协议的常见缺陷以及相应的攻击类型 2 t r e i l d 随机生成k ，向a 发送： 圯，k ，且 墨4 嘞j 3 a 解密以，向b 发送：t r e n d ， k ，彳) 。，； 4 b 生成随机数n b ，向a 发送： 虬) 尼； 5 a 向b 发送： 虬- 1 x 。 图2 1n e e d h a m - s c h r o e d 盯单钥认证协议 在这个协议中，由于a 和b 以前并不认识，而且又没有使用非对称的密码算 法，故而只有借助可信的第三方t r e n d 来帮助完成协议。 显然在整个协议运行过程中已经加入了防止重放的一次性随机数，但是在第 三步中消息没有涉及到任何新鲜性标识符的内容，故而此就成为了突破口，产生 如下重放攻击：( m 为攻击者) ，如图2 2 所示 l 和2 与前面相同； 3 m 伪装成a ，向b 发送： f ，彳 。，： 4 b 上了当，向m ( a ) 发送： ) ； 5 m 伪装成a ，向b 发送： 虬一1 ) 。 在攻击的第三步中，m 拦截a 发给b 的消息，并用以前a 和b 运行协议时的 旧消息来进行重放，在这个时间点上，m 很可能已经破译了k ，所以产生的结果 是： a 在线上等待b 的回应，可能超时后会退出；而b 则认为自己已经和a 建立 了共享的会话密钥k 。这严重的偏离了认证的目的，攻击得手。 这个协议的毛病出在一次性随机数的运用上，协议中。的作用是使消息2 防 9 电子科技大学硕士学位论文 止被重放，而并没有新鲜性标识符用在a 给b 发送的消息中，但是在其中加入新 鲜性标识符是不现实的，因为协议中b 是被动一方，他是先接收消息，才回复的， 所以没有时间来发送自己的新鲜性标识符。 图2 - 2 对单钥n s 协议的重放攻击 所以利用时间戳来代替一次性随机数是个有效的解决方案： 1 a 发送给t r e n d ：a ，b ； 2 t r e n d 发送给a ： e e l 4 k 丁 f ； 3 a 发送给b - a ，k ，t ，； f 7 4 和5 同上 确实时间戳能够解决问题，由于时间戳本身的优越的性质：能够不通过交互 来保证消息的新鲜性。但是由于时间戳对硬件同步的要求较高，而网络环境对于 实现时钟同步又不是很现实，所以在设计协议时尽量不推荐使用时间戳。 重放攻击攻击是非常常见的典型攻击，在攻击者的攻击方式中占有很大的比 重，抵抗重放攻击的方式最主要就是一次性随机数和时间戳，但是有的时候，一 次性随机数和时间戳只能对一些用户保证消息的新鲜性，而不能保证这个消息对 所有用户是新鲜的，所以对抗重放攻击仍然存在不确定性，在下文中我会提到一 种分析方法，能够分析新鲜性标识符对于消息和主体的关联关系，这样就使得消 息的新鲜性与不同用户的关系，这对于分析协议的抗重放性有很大的意义。 1 0 第二章密码协议的常见缺陷以及相应的攻击类型 2 3 2 中间人攻击 中间人攻击适应于缺少双方认证的通信协议。这种攻击方式是非常典型的一 种攻击方式，文献n 钔专门系统的研究了这种攻击。在这种攻击中，攻击者能够利 用协议的结构利用一个主体回答另一个主体提出的困难问题，然后把得到的答案 交给提问者，从而获得认证。为了说明这种攻击方式，用一个实例来进行说明： 协议2 2n e e d h a m - s c h r o e d e r 公钥认证协议明，如图2 - 3 ， 第一步，a 向b 发送： 。，a ，； 第二步，b 向a 发送： 虬，虬 k ： 第三步，a 向b 发送： 。 ， 其中k 。是a 的公钥，k 。是b 的公钥。 这个协议是利用非对称密码体制来实现的双方认证的过程，一般来说公钥认 证协议不需要第三方的帮助。 图2 3 公钥n s 协议 l o w e 发现了对这个协议的一种中间人攻击晗们：如图2 4 l a m ： m ，彳) h ； 1 m ( 爿) _ b ： 以，彳) x 。； 2 口一m ( 彳) ： 以，虬) k ； 2 m a ： m ，虬) 石； 3 a m ： m ) h ； 3 m ( a ) 一b ： 以) “ 这个攻击中m 是作为一个合法用户的身份出现的，m 一方面用自己的真实身份 和a 通信，另一方面则利用a 的解密能力帮助自己欺骗b 。这个协议被攻击的关键 电子科技大学硕士学位论文 是a 充当了预言机的作用，而一个设计完好的协议应该有这样的性质：即使给攻 击者提供预言机服务，协议也是安全的。 a 被当做预言机的原因在于他所解密的消息中没有含有身份信息，所以一种很 容易想的到的修改方法是在第二步中b 发送给m 的消息中加入b 的身份，使得这 个消息有了消息源认证的特性，这个时候a 解密出消息后看到有b 的身份信息就 知道受骗了。 图2 4 对公钥n s 协议的中间人攻击 但是这种修改方法是一种消极的、被动的方法，所以在本文后一部分讨论的 形式化方法中，提出了一套协议设计的准则，按照这套准则就可以省去很多设计 协议中的缺陷，从而使得对协议的讨论更加有效率。 另一个中间人攻击的例子是对著名的公钥体制下的密钥协商协议 d i f f i e - h e l l m a n 协议的攻击。 协议2 - 3d i f f i e - h e l l m a n 密钥协商协议： 共同输入：( p ，g ) ：p 为大素数，g 为f ：中的一个元素。 协议运行的结果：a 和b 共享一个会话密钥k 。 1 a 选择a 气 1 ，p - 1 ) ；计算g 。= 9 4 ( m o dp ) ；然后发送给b ； 2 b 选择b ， 1 ，p - 1 ) ：计算9 6 = g b ( m o d p ) ；然后发送岛给a ； 3 a 计算k = 薛( m o dp ) ； 4 b 计算k = g ：( m o d p ) d i f f i e h e l l m a n 密钥协商协议是非对称密码体制下密钥协商协议的基础协议 后来专家们又在此基础上提出了很多的密钥协商协议。由于这种密钥协商协议涉 及到了比较底层的密码学技术，所以可以运用随机预言机模式来对其安全性和密 钥的认证性进行证明，本文最后就对一种公钥体制下的密钥协商协议进行了安全 1 2 第二章密码协议的常见缺陷以及相应的攻 性的证明。 对这个协议的攻击如下： 1 m 截获了步骤1 中a 准备发给b 的消息氍，然后选择某个m 【1 ，p 一1 ) ，计 算g 。= g ”( m o d p ) ，冒充a 发送给b ； 2 m 截获了步骤2 中b 准备发给a 的消息，然后冒充b 发送g 。给a ； 3 a 计算k l = g ：( m o dp ) ，m 也能计算k l ，所以m 和a 就共享了密钥k l ； 4 b 计算如= g b , 。( m o d p ) ，m 也能计算如，所以m 和b 就共享了密钥k 2 。 从而，这个攻击的结果是： a 认为自己和b 共享了密钥，事实上是a 与m 共享了密钥；b 认为自己和a 共 享了密钥，事实上是b 与m 共享了密钥。这个协议到此灾难性的失败。 虽然d i f f i e - h e l l m a n 密钥协商协议如此的脆弱，但是它的想法是具有革命性 的，这给公钥体制下的密钥交换提供了宝贵的基础条件，从而可以使得密钥协商 不用再依靠那可恶的第三方了( 谁都不想自己和别人共享的秘密被多一个人知道， 而且谁都不能保证可信第三方永远可信) 。由于这样的密钥协商协议具有重要的意 义，所以有必要以这个协议为基础设计公钥体制下的密钥协商协议。 2 3 3 平行会话攻击 当协议同时运行两次或者多次，而且某一次运行中的消息被用于形成另一个 运行中的消息时，并行会话攻击就产生了。举个简单的例子来说明： 协议2 - 4 一个单向认证的协议： 1 a 给b 发送消息： 口) r ； 2 b 给a 发送消息： n o - 1 k 假设在这个协议运行之前，a 和b 已经有了会话密钥k 。 这个协议运行成功后的结果是：b 向a 认证了他的身份。 给出攻击如下： 1 m 截获第一步中的消息 口) k ，然后发回给a ； 2 a 收到 口) 足后，发送 n o 一1 ) 髟给m ； 3 m 发送 口一1 ) r 给a ，获得认证 这个攻击之所以成功，是因为两点原因。第一，由于a 是不会检查自己发送 出去的消息和接收到的消息之间的关联的，所以对接收来的消息进行了预言服务； 第二，此协议设计中的两条消息格式几乎一模一样，这本来就会造成类型攻击， 电子科技大学硕士学位论文 而且消息中没有任何表示身份的信息，身份信息并不是必要的，但是有时候在消 息中添加入身份信息可以免掉很多种潜在的攻击。 2 3 4 类型攻击 如果协议的设计者使得协议中的消息部分的类型信息不明确，就可能使这个 消息的接收方产生误解。下面以n e u m a n 和s t u b b l e b i n e 晗提出的协议来说明这种 攻击。 协议2 5 ：如图2 5 图2 5 一种带有司信第三方的认证协议 1 彳一b ：a ，m ； 2 b - - t r e n d ：曰， 彳，m ，乃) 石。，m ； 3 t r e n d 寸a ： 召，n a ，k 彳口，易) 足。， 彳，k 占，乃) 石。，虬； 4 彳一b ： 彳，k 占，乃) k 。， 虬) 置船 这个协议的目的是在可信第三方t r e n d 的帮助下，a 和b 实现双方认证和认证