（计算机软件与理论专业论文）安全协议形式化分析方法的比较和研究.pdf

郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 摘要 随着计算机网络的广泛应用，计算机网络的安全问题也日益引起人们的重 视。在网络安全中，各种安全服务都是基于安全协议的，这使得安全协议的安全 性变得尤为重要。在过去的二十多年中，为了满足各种各样的网络应用，提出了 大量安全协议，但是后来的研究证明这些安全协议大多数都含有这样或者那样的 安全漏洞，如何设计一个比较安全的安全协议以及如何验证一个已设计出来的安 全协议是否安全成为安全协议研究领域中最重要的两方面。 安全协议是一种通信协议，它的主要目的是利用密码技术实现网络通信中的 密钥分发和身份认证。然而，大量事实表明，有许多安全协议经过安全专家认真 仔细地分析、设计和实现后仍然存在着漏洞。本文首先介绍了以往的各种安全协 议，在此基础上总结出了五种典型的安全协议漏洞。 形式化方法能有效检验安全协议的安全性，b a n 逻辑的发展极大地促进了 这一领域的研究。本文重点阐述了形式化方法及其在安全协议验证中的应用。同 时，针对串空间模型这一新兴的形式化方法进行了深入地分析和研究，在此基础 上，应用串空间模型对a n d r e w r p c 安全协议进行了形式化分析和验证，指出了 该协议的安全缺陷。论文还比较了b a n 逻辑和串空间模型这两种形式化方法各 自的优缺点。然后，对串空间模型提出了扩展，使得它能更好地分析公平的不可 否认协议，并且以z g 协议为例，用扩展理论成功地对它进行了安全性分析和验 证。 关键词：安全协议，形式化方法，b a n 逻辑，串空间模型 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 a b s t r a c t w i t ht h ec o m p u t e rn e t w o r kb ew i d e l yu s e d , s e c u r i t yp r o b l e m so fc o m p u t e r n e t w o r kh a v eb e e ne x p o s e dm o r ea n dm o r e i nt h ea r e ao fn e t w o r ks e c u r i t y , b e c a u s e a nk i n d so fs e c u r i t ys e r v i c e sa r ea l lb a s e do ns e c u r i t yp r o t o c o l s , i ti sm o s ti m p o r t a n t t h a tt h es e c u r i t yp r o t o c o l sa g es e o t l r o i nt h ep a s t2 0y e a r s ，p e o p l ei n t r o d u c e dm a n y s e c u r i t yp r o t o c o l si no r d e rt of u l f i l la l ls o r t so fn e t w o r ka p p l i c a t i o n s h o w e v e r , l a t e r r e s e a r c hp r o v e dt h a tt h e r ew e r es e c u r i t yl e a k si nm o s ts c c l h i t yp r o t o c o l s h o wt o d e s i g ns e c u r es e c u r i t yp r o t o c o l sa n dh o wt ov e i l f y s e c u r i t yp r o t o c o l sb e c o m et h em o s t i m p o r t a n tt w oa r e a si nt h er e s e a r c ho ns e c t u i t yp r o t o c o l s s e c u r i t yp r o t o c o l sb e l o n gt oc o m m u n i c a t i o np r o t o c o l s t h em a i n a i mo fs e c u r i t y p r o t o c o l si st or e a l i z ek e ya g r e e m e n ta n da u t h e n t i c a t i o nu s i n gc r y p t o g r a p h y h o w e v e r , m a n yf a c t ss h o wt h a tt h e r ea r es t i l ls o m el e a k si nt h es e c u r i t yp r o t o c o l sw h i c hh a v e b e e nc a r e f u l l ya n a l y z e da n dd e s i g n e db ys e c u r i t ye x p e r t s f i r s t l y , t h i sp a p e ra n a l y z e s a l l k i n d so f s e c u r i t y p r o t o c o l s t h e n t h i s p a p e rs u m m a r i z e s5 k i n d s o f t y p i c a ls e c u r i t y p r o t o c o ll e a k s f o r m a lv e r i f i c a t i o ni si ne f f e c tt od e t e c ts e c u r i t yp r o t o c o l s t h ed e v e l o p m e n to f b a ni c l g i cp r o m o t e st h er e s e a r c ho ft h i sa r e a t h i sp a p e rd e s c r i b e st h ef o r m a l m e t h o d sa n dt h ea p p l i c a t i o no ff o r m a lm e t h o d so nv e r i f i c a t i o no fs e c i m t yp r o t o c o l s s i m u l t a n e o u s l yi nt h i sp a p e r , am o d e lo fs t r a n ds p a c e s ，ac u r r e n tl e a d i n gb r a n c ho f f o r m a lm e t h o d s ，i sr e s e a r c h e da n da n a l y z e di nd e t a i l a n dt h e nb yu s i n gs t r a n ds p a c e s t oa n a l y z et h ea n d r e ws e c t l r er p c p r o t o c o l ，s o m es e c u r i t yf l a w sa r ed i s c o v e r e d i n t h i sp a p e r , b a nl o g i ci sc o m p a r e dw i t hs t r a n ds p a c em o d e la n dl a s t l yg o o da n db a d p o i n t so ft h ea b o v ea p p r o a c h e sa r ei n d i c a t e d t h e ns e i n ee x t e n s i o no fs t r a n ds p a c e m o d e li sn e e d e dt oa n a l y s ef a i rn o n r c p u d i a t i o np r o t o c o l si ne f f e c t t h ee x t e n d e d s t r a n ds p a c em o d e li sa p p l i e di nt h ef o r m a ld e s e r i p t i o f z h o u - g o l h n a np r o t o c 0 1 k e y w o r d s ：s e c u r i t yp r o t o c o l s ，f o r m a lm e t h o d s ，b a nl o g i c ，s t r a n ds p a c e 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 第一章引言 近年来，伴随着i n t e r n e t 在全世界的飞速发展，网络数据和资源的共享、多 媒体通信、电子邮件和电子商务等网络应用逐渐建立和使用，用户对于信息安 全传输的要求越来越迫切。要保证信息的安全性，仅仅依赖于良好的加密算法 是不够的。在实际应用中，还需要建立可信的机制为各个独立的通信实体分发 密钥，并且在通信实体之间进行身份认证，这就迫使人们研究设计出了各种加 密协议，或者称作安全协谢1 1 这些协议主要完成密钥分发和身份认证任务。 1 1 安全协议简介 协议【l j 是在计算机网络和分布系统中两个或多个主体( p r i n c i p a l s ) 为相互交 换信息而规定的一组信息交换规则和约定。其中的主体，可以是用户、进程或 计算机( u s e r s ，p r o c e s s e s0 1 m a c h i n e s ) 。它设计的目的是要完成一项任务或者 几项任务。协议有如下的特点： 1 协议中的每个人都必须了解协议，并且预先知道要完成的所有步骤； 2 协议中的每个人都必须同意并遵守协议； 3 协议必须是清楚的，每一步必须明确定义，并且不会引起误解； 4 协议必须是完整的，对每种可能的情况必须规定具体的动作。 安全协议p 增时也称作密码协议，是在协议中应用加密解密的手段隐藏或 获取信息，以达到安全性的各种目的。运用安全协议人们可以解决一系列的安 全问题，例如：完成信息源和目标的认证；信息的完整性，防止窜改；密钥的 安全分发，保证通信的安全性；公证性和及时性，保证网络通讯的时效性与合 法性；不可抵赖性；授权，实现权限的有效传送等等。其中认证协议是其它安 全目标的基础，也是我们研究的重点。安全协议是通信和网络安全体系、分布 式系统和电子商务的关键组成部分，是安全系统的主要保障手段和工具。 1 2 课题的背景和意义 在网络安全中，各种安全服务都基于安全协议，因此，安全协议的安全性 郑州大学硕士学位论文 安全协议形式化分析方法的比较和研究 是十分重要的。正是由于安全协议在网络安全中扮演着如此重要的角色，对于 安全协议设计和安全性验证的研究是有非常重要的研究价值的。但是由于安全 协议存在着许多不安全的因素，甚至有些安全协议在提出来很多年以后才发现 有安全漏洞，这使得安全协议的研究也存在一定难度，需要不断探索和发展 对于安全协议的验证，发展到现在已经有很多种不同的方式，在安全协议 的形式化验证逻辑出现以前，安全协议的设计很容易出错，其中最重要的原因 是没有一个简单实用的逻辑来推导出安全协议是否正确。1 9 8 9 年，b u r r o w ，a b a d i 和n e e d h a m 共同提出了一种分析认证协议的逻辑，称之为b a n 逻辑【l 卅。随着 安全协议的不断发展，原有的逻辑也不断被扩展，如g n y 逻辑【4 】、v o 逻辑【5 1 、 a t 逻辑1 6 7 】、s v o 逻辑嘲等。同时，研究人员开始使用各种状态机对网络安全 协议进行漏洞测试，这一方法以斯坦福大学计算机研究所的j o h nc m i t c h e l l 、 m a r km i t c h e l l 和u l r i hs t e r n 等人于1 9 9 7 提出的m e 脚验证方法【9 】为代表，而验 证协议的状态机的搜索证明也由o x f o r d 大学完成的f d r ( f a l l u r e s - d i v e r g e n c e r e f i n e m e n t ) 系统提供支持，一时成为各个研究机构重点研究的方向，并且解决 了网络安全协议验证的一些问题。另一方面，应用推理归结的研究也有很多成 果。1 9 9 7 年，l a v e l 大学的d e b b a b i 教授就提出了一个用于验证安全协议的自 动的形式化算法1 1 0 1 。到了1 9 9 8 年，f a b r e g a ，h e r z o g 和g u t t m a n 建立了串空间 模型( s t r a n ds p a c e s ) 【l l 】，这一研究内容受到美国军方的资金支持。1 9 9 9 年c m u 的研究人员研制成功了基于这种模型的a t h e n a 1 2 系统，并且声称基本解决了网 络安全协议验证的问题，得到了许多科研机构的重视。此外，还有k a i l a r 逻辑 【3 ”、r u b i n 逻辑【3 1 】和c s p 方、法 3 ”等等，都不失为优秀的形式化方法。 近二十年来，为了应对这一挑战，人们设计了不同种类的形式化分析方法， 投入了大量的精力，同时也取得了可喜的成果。随着网络通信的不断发展，对 安全通信以及其他各种需求越来越大，对于安全协议设计和研究是非常有意义 的。 1 3 论文的主要内容 论文共分为七章，主要涉及两个研究部分：安全协议的设计和安全协议的 验证具体组织如下： 郑州大学硕士学位论文 安全协议形式化分析方法的比较和研究 第一章介绍课题研究的目的与意义、本文的研究内容和论文各部分的主要 内容。 第二章详细介绍了安全协议，本章在分析以往各种安全协议分类的基础上， 列举了一些典型的安全协议。然后，总结出了五种典型安全协议漏洞，以期引 起安全协议设计者足够的重视。 第三章阐述形式化方法及其在安全协议验证中的应用，详细介绍了一种十 分重要的安全协议形式化验证方法b a n 逻辑。 第四章主要介绍了一种新兴的安全协议形式化验证方法一串空间模型。 第五章主要以a n d r e wr p c 协议为例，用b a n 逻辑和串空间模型两种形式 化方法进行验证与分析，找出了a n d r e wr p c 协议的漏洞所在，并且对两种形 式化方法进行比较分析，说明了各自的优点和局限性。 第六章主要对串空间模型进行了扩展，并且以公平的不可否认协议z g 协 议为例，用扩展后的串空间理论进行了分析和验证。 第七章简单总结了本文的主要内容并对未来进行了展望。 最后是参考文献、致谢以及攻读硕士学位期间发表的学术论文。 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 第二章安全协议 安全协议提供安全服务，是保证网络安全的基础。近年来，安全协议越来 越多地用于保护因特网上传送的各种交易，保护针对计算机系统的访问。但是， 设计一个符合安全目标的安全协议是十分困难的。因此，我们必须借助形式化 方法，对安全协议进行设计和分析。自二十世纪七十年代末期以来，安全协议 的研究已经成为一个热点，有众多的形式化研究方法涌现出来。本章是对这一 重要研究领域发展二十年的简要概括和总结。 2 1 基本概念 在过去的二十年中，网络和分布式系统的大量使用，给网络的使用者提供 了巨大的网络资源，通过网络进行传递和共享的信息越来越多，在网络传输过 程中的安全问题也越来越得到更多的关注，尤其是近年来，随着电子商务的发 展，对于安全的要求更是迫切，而安全协议在其中起着至关重要的地位。 安全协议可以描述为：建立在密码体制基础上的一种高互通协议，它运行 在计算机通信网络或分布式系统中，为安全需求的各方提供一系列步骤，借助 于密码算法来达到密钥分配、身份认证、信息保密以及安全地完成电子交易等 目的。 安全协议是一种通信协议，它的主要目的是实现网络通信中的密钥分发和 身份认证。安全协议是网络通信安全系统的基础，是实现计算机网络安全的关 键。然而，大量事实表明，有许多安全协议经过安全专家认真仔细地分析、设 计和实现后仍然存在漏洞，有些甚至在使用许多年后才被发现有漏洞。 2 2 安全协议的分类 1 9 9 7 年，c l a r k 和j a c o b l l 3 1 对安全协议进行了概括和总结，列举了一系列有 研究意义和实用价值的安全协议。他们将安全协议进行如下分类： ( 1 ) 无可信第三方的对称密钥协议： 属于这一类的典型协议包括以下i s o 系列协议【1 4 1 ：i s o 对称密钥一遍单边 一4 一 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 认证协议、i s o 对称密钥二遍单边认证协议、i s o 对称密钥二遍相互认证协议、 i s o 对称密钥三遍相互认证协议、a n d r e w 安全r p c 协议f 1 5 】等。 ( 2 ) 使用密码检查函数( c r y p t o g r a p h i cc h e c kf u n c t i o n s ) 的协议 属于这一类的典型协议包括以下i s o 系列协议【1 4 】：i s o 应用c c f 的一遍单 边认证协议、i s o 应用c c f 的二遍单边认证协议、i s o 应用c c f 的二遍相互认 证协议、i s o 应用c c f 的三遍相互认证协议。 ( 3 ) 具有可信第三方的对称密钥协议 属于这一类的典型协议包括n s s k 协议【1 6 1 、o t w a y - r e e s 协谢堋、y a h a l o m 协议【1 3 1 、大嘴青蛙协谢嘲、d c n n i n g - s a c c o 协议【1 9 1 、w o o - l m n 协议f 2 0 珞。 ( 4 )对称密钥的重复认证协议 属于这一类的典型协议有k e r b e r o s 协议版本5 【2 1 2 2 1 、n e u m a n s t u b b l e b i n c 协议等。 ( 5 ) 没有可信第三方的公钥协议 属于这一类的典型协议包括以下i s o 系列协议【1 ：i s o 公钥一遍单边认证 协议、i s o 公钥二遍单边认证协议、i s o 公钥二遍相互认证协议、i s o 公钥三遍 相互认证协议、i s o 公钥二遍并行相互认证协议。及d i f f i e - h e l l m a n 2 4 1 协议等。 ( 6 )具有可信第三方的公钥协议 属于这一类的典型协议有n s p k 协谢1 6 1 等。 ( 7 )其它协议 例如e k e 协议【2 翻。 此外，还有基于应用目的的分类和基于所使用密码方法的分类的分类方法， 前者可以分为密钥交换协议、认证协议、认证及密钥交换协议、签名协议和电 子商务协议。后者分为基于对称密钥的安全协议、基于公钥的安全协议、基于 哈希函数的安全协议和混合协议及其它。 2 3 安全协议的漏洞 安全协议本身是用来完成秘密信息的安全传递的，因而安全协议是否安全 是至关重要的，这是安全之上的安全。 但是，目前的实际情况却表明：安全协议的正确性或者说安全性不容乐观。 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 即使我们不考虑与实现相关的协议缺陷和密码系统被成功破译的可能性，安全 协议本身也可能存在一些未知的漏洞，致使攻击者可以使用直观上难以发现的 攻击序列，冒充协议中的诚实的通信实体。目前已经发表甚至投入使用的安全 协议不少，但许多协议在发表甚至使用几年或十几年后，却被发现存在安全漏 洞。 安全协议的漏洞有很多种，就大的分类可以分为两类，一类是协议实现相 关漏洞，例如：密码算法的具体实现等等。这类漏洞和具体的实现相关，不是 本文研究的重点。另一类是非实现相关漏洞，这些漏洞和具体的实现无关，一 旦出现漏洞的话，就会产生严重的后果。 安全协议的攻击方式有很多，c l a r k 和j a c o b 对于安全协议的攻击提出了自 己的分类方式。本文在此基础上，列举出5 种最典型的攻击安全协议的方法， 这些攻击方式也是安全设计中最需要防范的。 2 3 i 新鲜性攻击 当攻击者使用前面协议轮或者前面协议步中的消息重放到当前协议步并且 能产生一个有效的协议步的时候，新鲜性攻击就发生了。新鲜性攻击产生的原 因就是协议的设计过程中没有充分考虑到协议的新鲜性。 设计新鲜性攻击的协议有很多，最典型的是n e e c l h a r a s c h r o e c l e r ( 埘t hs h a r e d k e y s ) 协议f 1 6 1 。该协议消息如下： ( 1 ) a - - - - h s ：彳，b ，圯 ( 2 ) s a ： 虬，丑，j 匕， 足，彳) k ) k ( 3 ) a b ： k ，彳) k ( 4 ) 曰一a ： 帆) k ( 5 ) 彳_ b ： 一1 k 对于这个协议的新鲜性攻击如下： ( 1 ) a 4 - s ：a ，b ，m ( 2 )s - - hd ： m ，b ，x 曲， k 曲，彳) k 置。 一融 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 ( 3 ) ，( 彳) - - hb ：t j 匕，4 ) k ( 4 ) b j ，( 彳) ： m ) 屹 ( 5 ) ，( 彳) 斗b ： m 一1 ) 珞 当攻击者i 获得了这个协议以前的某个会话密钥屹的时候，攻击者i 就可 以实施新鲜性攻击。在这个协议中，能够提供新鲜性攻击的原因就是在协议的 第3 步，b 不能判断收到的k 的新鲜性。 遭受新鲜性攻击的协议还有很多，这里就不一一罗列了。在b a n 逻辑出现 以前，新鲜性攻击是最常用的攻击方式之一，也是协议设计中很容易被忽视的。 b a n 逻辑的出现极大的改变了这种状况，用b a n 类逻辑来验证协议中的新鲜 性漏洞是很方便的。 2 4 2 并行会话攻击 当两个或者多个协议同时运行时，如果把一个协议轮的消息使用在另外一 个协议轮中，并行会话攻击就可能发生。在安全协议的设计中，协议的设计者 可能会注重一个协议轮运行的安全性，很容易忽视并行会话时的攻击。而且， 由于会话并行带来了极大的复杂性，所以协议设计的时候要防止这种攻击相对 于其他的一些攻击方法来说更加困难。这也使得这种攻击方式为协议设计者和 协议攻击者所关注。 一个简单的单方认证协议如下： ( 1 ) a b ： 虬) k ( 2 ) b 寸彳： n o 1 ) k 这个简单的单方认证常使用在一些著名的协议中，例如著名的n s s k 协议 【1 6 1 。 对于单独的这个认证协议，可以实施并行会话攻击如下： ( 1 ) a 寸f ( b ) ： m ) i - ( 2 ) ，( 曰) 寸a ： 虬，k 郑卅f 大学硕士学位论文 安全协议形式化分析方法的比较和研究 ( 3 ) a 斗，( 占) ： d + 1 ) k ( 4 ) j ( 口) 斗a ： m + 1 ) k 这样，攻击者i 就成功假冒b 和a 完成了这个协议。 2 4 3o r a c l e 攻击 安全协议能够被攻击者在特殊的条件下来预先获得他们想要获得的消息， o r a c l e 攻击就这样诞生了。 大嘴青蛙协议是由b u r r o w 、a b a d i 和n e e d h a m 共同提出的【2 6 j ，协议如下： ( 1 ) a s ：a ， r a ，b 屹) k ( 2 ) s 呻b ： r s ，a ，) k 对于这个协议攻击如下： ( 1 ) a - - ) s ：a ， r a ，b 瓦) k ( 2 ) s - - - ) b ： t s ，a ，k ) k ( 3 ) ，( 占) 斗s ：b ，f f a ，b 屹) k ( 4 ) s - - ) ，( 爿) ： r ，b ，k ) k ( 5 ) ，( 一) - - - ) s ：彳， 7 2 ，b j c 。b k ( 6 ) s ，( 曰) ： r 0 ，a ， k 这个协议被攻击是结合o r a c l e 攻击和并行会话攻击的结果。 2 4 4 对于类型漏洞的攻击 协议中的一条消息是几个组成部分组合起来的，每个部分都具有某种类型 ( 例如：参与者的名字、随机数、密钥等) 。当参与者接收到一条合法消息的 时候，如果消息的某个组成部分的实际类型不是接受者认可的类型时，针对类 型漏洞的攻击就可能发生。 下面以o t w a y - r e e s 1 7 】协议为例子介绍什么是对于类型漏洞的攻击。协议如 郑州大学硕士学位论文安全协议形式化分析方法的比较和盟 f ： ( 1 ) a 斗b ：m ，a ，b ， m ，肘，彳，研l ( 2 ) b 斗s ：m ，a ，b ， m ，m ，4 ，研k ， m ，m ，4 ，毋k ( 3 ) s b ：m ， 虬，如) k ， 以，c a x ( 4 ) b 专a ：m ， 虬，如) k o t w a y - r e e s 协议中m 是一个随机数，用于表示该协议的轮数a 这个协议经 受不住对于类型漏洞的攻击，其中一种攻击方式如下： ( 1 ) a 斗，( 雪) ：m ，a ，b ， m ，m ，4 ，毋k ( 2 ) b j s ：m ，a ，b ， m ，m ，一，b ) k ， 6 ，m ，a ，研 ( 3 ) s 专b ：m ， 虬，髟) k ， n b ，k a x ( 4 ) j ( 曰) _ a ：m ， 虬，足) k 第1 条消息，i 窃听了a 发给b 的消息，第4 条消息，i 冒充b 给a 发消 息，消息的内容是从l 窃听的第1 条消息来的。这样a 就认为s 产生的密钥是 ( m ，a ，b ) 。这样，如果( m a b ) 被a 认为是膏女的话，攻击者就获取了会话 密钥。 2 4 5 中间人攻击 最典型的中间人攻击莫过于针对d i m e _ h e l l l i l a n 【2 4 1 密钥交换协议的攻击，这 个协议如下： ( 1 )a b ：x = g 。m o d n 1 2 )b a ：y = g 7 m o d n 攻击方法如下： 1 1 ) a 。1 1 8 ) ：x = g 。m o d n ( 2 )，( 曰) 寸a ：z = g x m o d n 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 ( 3 ) ，( 彳) 斗b ：z = g r m o d n ( 4 ) 口号，( 彳) ：y = g 7 m o d nb a ：y = g 7 m o d n 2 4 6 安全协议漏洞总结 现有的一些对安全协议的攻击方式是与实现有关的，也就是有前提条件的， 当满足某种前提的时候，这种攻击方式就能攻击成功。如果从协议的安全角度 来看，这种安全协议的安全性是有前提的，如果协议实现的时候不能满足安全 的前提，这个协议的实现就是不安全的。如果协议的安全性是实现相关的话， 必须在设计协议的同时还要给出使用者的实现规范，只有按照规范来实现这个 协议才是安全的。很明显，要求协议实现者在实现协议的时候避免某些漏洞， 而不是协议设计者在设计的时候就已经避免了这些漏洞，这样做是不科学的。 同样，作为一个协议的设计者，不能把安全与否建立在协议的实现上。 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 第三章安全协议的形式化分析方法 对于安全协议有很多种分析方法。总的来说，可以分为两大类：非形式化 方法和形式化方法。非形式化方法的特点是：分析时不把协议用形式化方法表 示出来，而是采用直观的分析检验方法。但是这种方法是一种懒惰的、甚至是 冒险的方法。形式化方法兴起于七十年代末期，如今已广泛用于解决理论和实 际问题，计算机安全是它一个比较成功的应用领域。使用形式化方法来进行安 全协议的验证已经是硕果累累。 3 1 形式化方法简介 形式化的数学系统，是一个由符号以及使用这些符号的规则共同组成的系 统。规则可以是形成规则，证明规则，或者语义规则。对于很多应用领域，采 用形式化方法的代价极其昂贵。传统上，形式化方法把计算机安全视为一个应 用领域，在这一领域中，形式化方法的代价相对于软件错误造成的损失是较低 廉的。另一方面，计算机安全学界习惯把形式化方法看作是一种确证的来源， 它超越了通过测试可以得到的结果。 计算机安全关心各种各样的威胁。一般的威胁可以被良好配置的放火墙击 退，但即使是最佳管理的放火墙，也不免被高度发达的攻击者穿破。计算机安 全还关心具有各种复杂性的各种程序和设备的各种属性。传统上，计算机安全 学界感兴趣的属性有保密性、完整性和实用性。伴随着计算机网络的发展，身 份认证和不可否认性也成为主要关心的属性。一般来说，对属性理解得越好， 用于实现的程序或设备越小，应用形式化方法就越成功。 在计算机安全中应用形式化方法的一大困难是，如何形式化定义、描述这 些属性。实用的一种解决办法是采用近似方法描述属性。 尽管形式化方法和计算机安全的结合并非二帆风顺，但是它们的结合导致 了双方的极大发展。在过去的二十年中，形式化方法被应用于广泛的领域：安 全模型、流分析、安全协议分析、软件验证、硬件验证、体系结构分析、秘密 信道分析等等。 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 形式化方法在安全学界最大的成功是应用它分析安全协议。安全协议足够 小，易于完成形式化分析，而且这些分析发现了很多以前不为人所知的漏洞。 形式化方法和计算机安全共同成长，相互帮助对方前进。形式化方法使得 系统更安全，计算机安全则显示了运用形式化方法进行分析的有效方式。 形式化方法分析安全协议的发展历史在第一章第二节中已做了详细介绍， 在此不再赘述。 3 2b a n 逻辑 从1 9 7 8 年到1 9 8 9 年b a n 逻辑【l q l 诞生的十余年中，产生了大量的安全协 议，不幸的是，这些协议中，大多数身份认证协议都含有安全漏洞或者信息冗 余。身份认证协议的设计是十分困难的，很容易出错。有许多原因可能造成错 误，例如不熟悉攻击者的行为等，但是最重要的原因是：没有完善的协议正确 性的概念，以及没有方便的可用逻辑来推导出正确或错误的结论。 在这样的背景下，b u r r o w 、a b a d i 和n e e d h a m 共同提出了一种分析认证协 议的逻辑( 后人以他们名字的首字母命名为b a n 逻辑) ，他们的出发点是用这 种逻辑对认证协议进行形式化分析，来研究认证双方是否相信正是认证双方在 相互通信而不是和入侵者在进行通信。b a n 逻辑可以精确地描述各个主体所相 信的内容( 称为“信念”) ，并记录导致结果的推理过程。b a n 逻辑定义了这 种基于信念的逻辑，用于研究通过认证协议的运行，认证双方通过相互接收和 发送消息来从最初的信念逐渐发展到协议运行最终要达到的目的认证双方 的最终信念。其目的是为分析安全协议提供逻辑工具。b a n 逻辑对被分析的安 全协议确立了前提，即协议采用的密码算法是安全的，不考虑密码算法被攻破 的情况。这样就可以集中分析认证协议的运行所带来的信念结果，这种分析前 提成为以后安全协议形式化分析方法所遵循的共同基本准则。 b a n 逻辑的提出具有划时代意义，它是分析安全协议的一个里程碑。 3 2 1b a n 逻辑概念 b a n 逻辑建立在模态逻辑基础上，它区分几种对象： 主体( p r i n c i p a l s ) ，即协议参与者，通常用a 、b 、s 表示； 一1 2 - 郑：i l i 大学硕士学位论文安全协议形式化分析方法的比较和研究 密钥( e n c r y p t i o nk e y s ) ，通常用e 6 、量乙、置h 表示二个主体之间的共 享密钥，k 。、k b 、k z 表示各主体的公钥，e 一、k b 一、e 1 表示相应的私 钥； 公式( f o r m u l a s ) 或者叫做声明( s t a t e m e n t s ) ，例如用4 、m 和札表 示随机数。 p 、q 、r 表示表示一般意义上的主体，x 、y 表示一般意义上的公式，k 表示一般意义上的密钥。b a n 逻辑中用逗号表示各部分的连接，连接有类似集 合的性质，其元素的顺序可交换。表示符号如下： ( 1 ) p l - x 或pb e l i e v e s x ：p 相信x 。即p 做出行动时认为x 为真。这 种结构在b a n 逻辑中处于中心地位。主体p 所相信内容的集合简称为p 的信 条。 ( 2 ) p 司x 或ps e e s x ：p 看见了x 。有人向p 发送了包含x 的消息，并 且p 能够读取和重复x ( 有可能是在解密运算之后) 。 ( 3 ) p i 工或ps a i dx ：p 曾经说过x 。p 在某个时候发出过包含公式x 的消息，虽然不知道是多久以前发出的消息，但是可以肯定p 发出时p 相信x 。 ( 4 ) p b x 或pc o n t r o l sx ：p 有权限控制x 。即应该相信“p 对x 有控 制权”这个论断，例如通常相信一个服务器能可靠地生成会话密钥。 ( 5 ) 撑( x ) 或f r e s h ( x ) ：公式x 是新鲜的。除了当前这一轮协议的执行， 以前任何时候传送的消息都不包括x 。这对随机数( n o n c e ) 来说通常是正确的， 随机数一般包含一个时间戳( t i m e s t a m p ) 或者一个一次性使用的数字。 ( 6 ) p 山q ：p 和q 使用共享密钥k 通信。k 是安全的，除了p ，q 或 k 他们相信的主体之外，其它主体无法获得k 。 ( 7 ) 墨寸p 或l 苎一p ： k 是p 的公钥。相应的私钥置。1 绝不会被p 或 p 信任的主体k 之外的主体知道。 r ( 8 ) p 营q ：公式x 是仅仅只有p 和q 或者他们信任的主体知道的秘密。 只有p 和q 可以使用x 来证明他们的身份，例如x 可以是一个i = 1 令。 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 ( 9 ) ( 柳f ：表示公式x 用密钥k 加密。一般，( x ) 。是( z ) r l o m p 的简写。 可以这样简写的原因是假设每个主体能够识别并忽略他自己加密的消息。 ( 1 0 ) z ) ，：表示x 和公式y 连接；y 是秘密，用来证明发出x 的人的身 份，例如在实现时，x 简单地和口令y 连接在一起，y 证明了x 的来源。 3 2 2 推理规则 在研究认证协议时，需要关心的是“过去”和“现在”两个时间段的区别。 “现在”时间段起始于当前这一轮协议的开始执行，在这以前发送的所有消息 都被认为是“过去”，认证协议必须很小心地防止“过去”的消息被当作是“现 在”的消息而接收。所有“现在”的信条在整个协议执行阶段都是稳定的，然 而“过去”的信条不能直接带到“现在”。区分了“过去”和“现在”，逻辑 的易操作性大为提高。 还需假定加密算法能够保证每个加密部分不能被改变；如果一条消息包含 两个独立的加密部分，它们被视为位于不同的消息中；没有密钥的主体无法理 解加密的消息；密钥无法从已知密文推导出来；每一密文有足够的冗余使得主 体解密后可以验证它是否使用了正确的密钥。 以下是一些主要的规则： ( 一) 消息含义规则( m e s s a g e - m e a n i n gr u l e s ) ： m 1 ：p | - q 山p ，p 4 册i p l = q 卜z m 2 ：p 障- q ，p 司( z ) r - ii 一尸净q 卜r t m 3 ：p l = 尸q ，p q x ) ri p i - q 卜r 处理如何解释消息，从原始消息中提取可相信的内容，对于共享密钥：如 果主体p 相信他和主体q 共享密钥k ，并且看到了用k 加密的声明x ，则p 相 信q 曾经说过x 。成立的前提是要保证p 能够识别自己发过的消息。 ( 二)随机数验证规则( n o n c e - v e r i f i c a t i o nr u l e ) ： 随机数验证规则，表示经检验的消息是新鲜的，因此发送者仍然相信它： n i ：pj - - - # ( x ) ，p | _ q i x l - p i 兰q 障x 郑州大学硕士学位论文安全悱议形式化分析方法的比较和研究 p 相信x 仅可能是新近产生的，即x 属于“现在”，而q 现在或者过去曾 经说过x ，则p 相信q 相信x 。 ( 三) 管辖权规则( j u r i s d i c t i o nr u l e s ) ： 如果p 相信q 对x 有管辖权，则p 相信q 对x 的判断： j 1 ：p i - q 睁x ，p l - q 障x i p i = z ( 四)信念联合规则( b e l i e f - c o n c a t e n a t i o nr u l e s ) ； b 1 ：p | = x ，p i - y i p l 兰( x ，y ) b 2 ：p i 葺( ，y ) l - p | 主x b 3 ：p 睁q f - ( x ，d i p q 净x b 4 ：p 净q i ( x ，】，) l p | 暑q 卜工 ( 五)新鲜性联合规则( f r e s h n e s s - c o n c a t e n a t i o nr u l e s ) ： 如果公式的一部分是新鲜的，则整体也是新鲜的： f i ：p l * 样( x ) l p i ；群( x ，功 ( 六) 接收规则( r e c e i v i n gr u l o s ) ： r i ：p 司( 石，r ) 卜p 司x r 2 ：p 司( x ri p 日x r 3 ：p 睁p 苎二 g ，p q x ) 篁i p 司x r 4 ：p 障量哼p 尸司 x ) xi 廿司x r 5 ：p _ - - 与q ，p 司i x f 一f - p 司x 注意：如果p x 且p y ，并不能得出p ) ( y ，因为x ，y 不是同时产生 的。 ( 七)密钥与秘密规则 k 1 ：p 降r + 马r i p 1 r + 马月 k 2 ：尸l 兰q 净r 与r l 一尸净q i - - - r + 与r xx k 3 ：p | - r r l 一尸睁r 铮r 一1 5 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 jf k 4 ：p i - q | 兰r r i p 障q i _ r r 3 2 3 理想化的协议 在常见的协议中，每个协议步的一般写法是：p _ q ：m e s s a g e ，表示主体 p 发给主体q 消息，这种使用非形式化符号的表达通常是模糊的，不适合作为 形式化分析的基础。所以有必要把协议的每一步转化成一种理想的形式，例如 一个协议步骤：a 斗b ：即，j 匕 k 应该告诉b ( 它知道密钥k h ) 疋6 是它和a 进行通信的密钥，这一步应该理想化为：a - 4b ：臼+ _ 盐j 彤k 理想化后的协议比传统的描述具有更清楚和更完备的规范，因此在生成和 描述协议时应该使用理想化的形式。 为了研究已经存在的大量协议，必须先生成每个协议的理想化形式。为此， 需要列出一些简单的指导方针，这些简单的指导方针可以控制哪些转化是可能 的，哪些转化有助于获得协议中特定的每一步的理想化形式。粗略来说有，如 果任何时候接收者得到一个真实消息m 后都能推导出发送者必然相信x ，那么 m 能被解释成一个公式x ；现实中的随机数被转化为任意的新公式，假定在整 个过程中发送者都相信这些公式； ，表示把y 作为一个秘密使用，仅当该秘 密用作身份证明时有效；最重要的是，出于实用性目的，总是保证每个主体相 信它作为消息产生的公式。 3 2 4 协议的分析 为了分析理想化协议，需要把它用逻辑公式来注释，如同h o a r e 逻辑中的 证明一样，在每消息前后加入注释，得到合法注释的主要规则是： 如果在p q ：y 之前x 成立，则之后x 和q 司y 都成立。 如果根据推理规则，能从已知的x 推导出y ，则x 成立时，y 也必然成立。 如果能从x 得到y ，则x 成立的时候y 也成立。 协议的注释是在协议执行过程中，一系列关于各个主体的信条和所看到内 容的说明，特别地，发送第一条消息以前的公式表示各主体在协议开始时的信 郑州大学硕士学位论文安全协议形式化分析方法的比较和研究 条，称为初始假设或初始信条。然后根据推理规则进行推理，一步接一步，就 能够从初始假设演化出最终的信条，推导出结论。 初始假设通常包括：各主体间共享了哪些密钥，哪些主体能产生新鲜的随 机数，哪些主体在哪方面被信任等等大多数情况下，待分析协议的初始假设 是标准的、显然的。一旦给定所有初始假设，验证协议就等于证明某些公式是 否作为结论成立。 最终得到的结论描述认证协议的目标根据协议的不同使用用途是不一样 的，身份认证通常是用共享会话密钥保护的某些通信的先行步骤，因此应该将 能够使通信开始的状态作为身份认证的目标。例如，在以下状态，a 和b 都相 信自己正在使用共享密钥k 和对方通信，可以认为a 和b 之间的身份认证成功 结束： 彳障彳马曰b i - 爿+ 马曰 有些协议则能够得到的结论更强，例如： 4 l - b 睁彳+ 马曰曰i = a i - 彳+ 与b a 和b 不仅相信自己正在使用k 和对方通信，而且相信对方也正在使用k 和自己通信。一些协议只得到较弱的最终结论，例如：一l - b l = z ，对某些x 而言，这仅仅反映a 相信b 最近发送过的消息。 某些公钥协议的目的不是交换共享密钥，而是传输一部分数据，这时要求 的目标通常能从上下文中得到。 b a n 逻辑验证协议的四个步骤 理想化协议； 写出初始状态的