（计算机应用技术专业论文）安全协议中的互模拟等价性验证.pdf

安全协议中的互模拟等价性验证 摘要 随着信息服务和商业活动等越来越多地出现在开放的通讯网络上，用以保证 上述服务的网络安全协议的可靠性成为备受人们关注的焦点。然而，由于外部面 临恶劣的网络环境和内部缺乏系统化设计验证方法，网络安全协议变得非常脆弱 和容易出错。 形式化的方法为验证和分析安全协议提供了有效的途径。它用形式化的语言 抽象出复杂的密文通讯协议，并借助于高级的推理或证明系统实现协议的分析验 证。建立在进程演算基础之上的互模拟等价性验证的方法，由于具有能确切地刻 画协议运行的代数语义模型( s p i 演算) 和十分有效的等价性验证方法而成为近年 来研究的热点。然后，s p i 演算模型中还存在某些不足，更重要的是基于原有的 互模拟关系的方法仅限于人工完成，不能实现自动验证。 我们的工作是针对上述不足之处展开的，目标是扩充s p i 演算语言，在此基 础上建立新型的互模拟等价关系，并实现该关系的自动证明，从而设计出安全协 议互模拟等价性自动验证工具。主要研究内容和创新之处在于以下三点： 1 ) 扩充s p i 演算语言，为密文通讯协议建立了新型s p i 演算模型。扩充s p i 演 算语法，建立了公钥密码操作原语，使之能表示所有密钥体制的安全协议； 修改了s p i 演算中并发语义，限制了原先通道可以传递的机制，使之能描述 协议中通讯主体跟其环境直接交互，从而可以更确切地刻画现实中的安全协 议： 2 ) 在新s p i 演算里设计了符号操作语义和符号互模拟。我们的符号操作语义使 输入进程仅接收环境中有意义的带符号的消息项，这样就很好地解决了输入 进程可能产生的无穷分支问题。定义的符号r e e f e d 互模拟确保了两个进程 只需要执行有限次的迁移动作，就可以判断出它们是否互模拟； 3 ) 建立并证明了符号r e d e d 互模拟与原具体互模拟之间的可靠性关系，从而 可以设计安全协议的互模拟等价性验证工具。 基于这项工作，可以实现安全协议的互模拟等价关系的自动验证，我们相信 这对于应用在软件和集成电路中的自动检测也有很大的启发作用。本文最后做出 了全文总结，并对本领域未来的研究提出了新的展望。 关键字：安全协议、s p i 演算、互模拟等价、自动验证。 b i s i m u l a t i o ne q u i v a l e n c ev e r i f i c a t i o ni n s e c u r i t yp r o t o c o l s a b s t r a c t w i t hm o r ea n dm o r ei n f o r m a t i o ns e r v i c ea n dc o m m e r c i a la c t i v i t i e sp r o v i d e do nt h eo p e n n e t w o r k ，t h es o u n d n e s so fn e t w o r ks o c u r i t yp r o t o c o l s ，w h i c ha r cu t i l i z e dt og u a r a n t e et h ea b o v e s e r v i c e ，a t t r a c tm a n yp e o p l e sa t t e n t i o n h o w e v e r , s u f f e r i n gf r o ms e v e r ea t t a c k sa n dl a c ko f s y s t e m a t i cd e s i g na n dv e r i f i c a t i o nm e t h o d ，n e t w o r ks e c u r i t yp r o t o c o l sb e c o m ev e r y 触酉l ea n d e r r o r - p r o n e f o r m a lm e t h o dp r o v i d e sa ne r i e c t i v ew a yf o ra n a l y z i n gs o c u r i t yp r o t o c o l s i tm a k e su s eo f f o r m a ll a n g u a g et om o d e l i z ct h e s ec o m p l e xp r o t o c o l sa n dv e r i f i e st h e i rc o h c c t t l e s so rt r a c e so u t t h ed e f i c i e n c i e s b ya d v a n c e dd e d u c t i o no rp r o o fs y s t e m b i s i m a l a t i o ne q u i v a l e n c ev e r i f i c a t i o n m e t h o di sa m o n gt h e s e b yt h ev i r t u eo f a c t u a t ea l g e b r a i cs e m a n t i cm o d e l s p ic a l c u l u s ，a sw e l la s v e r ye f f e c t i v eb i s i m u l a t i o ne q u i v a l e n c em e t h o d , i ta p p e a l sm a n yr e s e a r c h e r si nt h er e c e n ty e a r h o w e v e r , t h e r e r es o m ed e f i c i e n c i e si nt h i sm o d e la n dw h a t sm o r et h eb i s i m u l a t i o nr e l a t i o nn o w c a no n l yb ep r o v e db yh a n d s ，n o tb yc o m p u t e r w ei n t e n dt oe n r i c hs p il a n g u a g e ，a n db u i l dn e wb i s i m u l a t i o ne q u i v a l e n c eo ni t , w h o s ep r o o f c a nb ea u t o m i z e d ，t h e r e f o r ed e s i g na u t o m a t i cv e r i f i c a t i o nt o o l sf o rs e c u r i t yp r o t o c o l so nt h i s r e l a t i o n i ns m n m a r y , t h ec o n t r i b u t i o n so f o u rw o r kl i ei nt h ef o l l o w i n gt h r e ea s p e c t s ： 1 ) e n r i c ht h el a n g u a g eo f s p ic a l c u l u s ，b u i l tar l e ws p im o d e lf o rc r y p t o g r a p h i c c o m m u n i c a t i o np r o t o c o l s w eb u i l ts o m eo p e r a t i o np r i m i t i v e sf o rp u b l i ce n c r y p t i o ns y s t e m s oa st od e s c r i b i n gf u l le n c r y p t i o ns y s t e mi ns e c u r i t yp r o t o c o l s w em o d i f i e dc o n c ts e m a n t i c s o f s p ic a l c u l u s t o m o d e l t h e d i r e c t i n t e r a c t i o n b e t w e e n c o m m u n i c a t i o n p r i n c i p l e s e n d t h e o p e n e n v i r o n m e n t ，w h i c hm o r ea c t u a l l yd e p i c t sr e a lr u n n i n go f s e c u r i t yp r o t o c o l s 2 ) d e s i g ns y m b o l i co p e r a t i o n a ls e m a n t i c sa n ds y m b o l i cb i s i m u l a t i o n o u r s y m b o l i cs e m a n t i c sr e q u i r e st h em p u tp r o c e s so n l ya c c e p ts y m b o l i cm e s s a g et e r m sd e d u c t i v ef r o m i t se n v i r o n m e n t , b yw h i c ht h ei n f i n i t eb r a n c h e so f i n p u tp r o c e s sc a nb es u c c e s s f u l l ys o l v e d o u r s y m b o l i cr e e f e db i s i m u l a t i o ni n s u r e st w op r o c e s s e sm e x e c u t e di nf i n i t et r a c s i t i o n si nt h e b i s i m u l a t i o ng a m e s 3 ) b l l i l da n dp r o v et h es o u n d n e s sr e l a t i o nb e t w e e ns y m b o l i cr e e f e db i s i m u l a t i o n a n dp r e v i o u sc o n c r e t eb i s i m u l a t i o n , a n df u r t h e r m o r et h ea u t o m a t i cv e r i f i c a t i o nt o o l s o nb i s i m u l a t i o ne q u i v a l e n c ec a nb ed e v e l o p e d i nt h ee n do ft h i st h e s i s ，w em a d eas i m m l a r ya n dd i s c u s s e df o u rp r o s p e c t i v ev i e w si nt h e f u r t h e rw o r k k e y w o r d s ：s e c u r i t yp r o t o c o l s ，s p ic a l c u l u s ，b i s i m u l a t i o ne q u i v a l e n c e ，a u t o m a t i c v e r i f i c a t i o n 第一章0 1 苦 第一章引言 随着计算机网络应用普及和规模不断的扩大，许多个人信息服务、商业活动和政府服务 等已越来越多地出现在开放的通讯网络上，提供各种安全、可靠的网络服务成为备受人们关 注的焦点。与通常友好的计算机网络通讯环境相比，提供安全服务的密文网络通讯环境却充 满了敌意。已有的安全协议除了普通通讯协议中可能的失败以外，还要面l 临着各种新、旧攻 击手段的威胁。复杂的网络环境使得攻击者可以利用安全协议自身的缺陷来精心设计和实施 各种各样的攻击，从而达到破坏网络安全的目的。因此，密文通讯协议的安全可靠性成为网 络安全的关键。 由于网络安全协议的重要性，近二十年来，世界各国学者对其设计和分析进行了广泛而 深入的研究。但早期的科研人员主要是根据应用需求设计出大量的安全协议，并基于经验和 单纯软件测试来分析其安全性；大都安全协议的设计方法是通过已有协议安全有效性，结合 具体应用需求来设计出新的安全协议。然而，缺乏系统的设计方法，以及根据人工经验和软 件测试的方法使得设计出的安全协议非常的脆弱和危险，远不能满足新的安全应用需求。因 此，迫切需要研究设计出有效的系统化方法来帮助安全协议的设计和分析。 一般认为对网络安全的研究主要集中在两个方面：一是设计各种健壮的加密函数、哈希 函数及算法( 如d e s 对称加密算法、r s a 公钥算法、如5 ( s l i a ) 签名函数) ：二是在健壮的密码 基础之上设计出安全可靠的网络通信协议( 如n s 公钥分配协议、w o o l a i n 认证协议、k e r b e r o s 密钥分配认证协议) 。安全协议的形式化研究侧重于用各种形式化的方法来分析验证网络协 议是否满足所具有的性质，也即是否存在安全漏洞，从而从根本上保证网络协议的安全性， 同时也为设计合理可靠的安全协议提供强有效的支持。 1 1 安全协议 网络安全协议是密文通信协议的通俗说法。首先来认识什么是通讯协议。所谓通讯协议 就是两个或两个以上的参与者采取一系列步骤以完成某项特定的任务。这个定义包含三层含 义： l 、协议至少需要两个参与方； 2 、参与方交替地处理和传递信息； 3 、通过执行协议完成共同任务。 由此可见，通讯协议与算法的概念是不尽相同的。算法应用于协议的消息处理环节，而 对算法的具体化则可以定义不同类型的通讯协议。 安全协议( 密文通讯协议) 是带加密、解密算法的通讯协议，它不但要保证通讯过程的 顺利进行，而且还要在公开的网络中利用现代密码技术来保护或隐藏必要的信息。密码技术 中一个基本要素就是单向函数，其最大的特点是在无参数( 如解密密钥) 的情况下求其逆函 数( 解密密文) 是一个异常困难的难解性问题。理论上，单项函数的存在性保证了通讯过程 中信息的安全性。 由此可见，安全协议中的密码算法和通讯协议处于网络安全体系的不同层次，是网络信 息安全的两个主要内容。具体而言，密码算法为网络上传递的消息提供高强度的加密或哈希 操作，而通讯协议则是在这些密码算法的基础上为各种网络安全性方面的需求提供实现方 案。 第一章引苦 i i 1 安全协议的分类 在网络通讯中常见的安全协议按照其目的有如。f ) l 类： 1 认证协议 认证协议是一个实体向另一个实体证明某种声称的属性，包含数据源认证( 消息新鲜 性) 、数据完整性认证( 消息非篡改) 和实体认证( 实体间真实通讯) 。这类协议包括d e n n i n g 协议、w o o - t a m 协议、n e e d h a m 口令认证协议等。 2 认证和密钥交换协议 这类协议先对通讯实体的身份进行认证，在成功的基础上建立和分配回话密钥。与密钥 来自某一主体不同，密钥交换得到的密钥是通过协议中的所有参与者随机输入某个函数而产 生的共享密钥，因此各参与方对输出密钥的质量都比较有信- t l , 。这类协议包括著名的 n s f ( s ) k 协议、s t s 协议( 工作站一工作站) 、e k e 协议、i k e ( 因特网密钥交换) 协议、 l 沁r b c r o s 认证协议等。 3 公钥认证协议 在公开密钥密码系统中，为了传递用公钥加密的秘密消息，公钥的使用者需要验证公钥 确实属于所声明的主体。这里有两种不同的方法：公钥证书基础设施( p i ( i ) 和基于身份的 公钥密码学。p k i 是通过可信任的第三方证书机构( c a ) 发放公钥证书来证实用户公 钥数据的，如x 5 0 9 公钥证书框架( 含c i v i f ( 证书管理协议) 、o c s f ( 在线证书状态协议) 等协议) 。基于身份的签名方案保证了公钥主体已被c a 认证，公钥使用者可以用主体的d 来验证签名的真实性。 4 其他应用类型协议 消息和身份的认证可以保护通讯双方不受第三方的攻击，但它们不能处理通讯双方内部 可能发生的攻击，如通讯一方伪造消息并声称来自另一方，或否认来自另一方的消息。这就 需要安全协议提供公平性和不可否认性的性质。此外，有些网络服务还要求提供匿名的功能 等。这类协议有s e t ( 安全电子交易) 协议和信用卡交易协议。 1 1 2 安全协议的安全属性 安全协议的主要目的使在于通过协议消息的传递来达成通讯主体身份的识别与认证，并 在此基础上为下一步的秘密通讯分配所使用的会话密钥。因此，对通讯主体双方身份的认证 是基础，而在认证的过程中，对关键信息的秘密性及完整性的要求也是十分必要的。另外， 作为在电子商务、在线支付等交易协议中，由于有其自身特点，也有一些特殊安全属性的要 求【l 】。 1 认证性 认证性是最重要的安全性质之一，几乎所以其他安全性质的实现都依赖于此性质的实 现。认证性是分布式系统中的主体进行身份识别的过程。主体与认证服务器共享一个秘密， 通过对拥有的此秘密的证明，主体可建立对其的信任。认证可以对抗假冒攻击的危险，认证 可以用来确保身份，并可用于获取对某人或某事的信任。在协议的实体认证中可以是单向的， 也可以是双向的。具体有一下几种方法： 1 ) 声称者使用仅被研验证者知道的密钥封装消息，如果验证者能成果解密消息， 则声称者的身份得到证明： 2 ) 声称者使用其私钥对消息签名，验证者使用声称者的公钥进行验证，如通过验 证则声称者的身份得到证实： 2 第一章哼i 苦 3 ) 声称者通过可信第三方来证明自己的身份。 上述几种方法往往被综合使用以建立可靠的认证系统。 2 保密性 保密性的目的是保护协议消息不被泄漏给未授权的人，即使是攻击者观测到该消息，它 也是无法从中得到有意义的内容。保证协议消息秘密性的最好的方法就是对消息加密。加密 使得消息由明文变成密文，并且任何人在不拥有密钥的情况下是不能解密消息的。加密体制 分为公钥密码系统和对称密码系统，前者密钥管理更为简单，后者加密效率更高。在安全协 议中，一般不考虑具体的密码算法执行细节，但在实际应用中往往可能造成安全协议保密性 的缺陷。 3 完整性 完整性的目的是保护协议消息在传输过程中不被非法篡改、删除和替代。最常用的方法 是封装和签名，即用加密的方法或h a s h 函数产生一个摘要附在传送的消息上，作为验证消 息完整性的依据。一个关键性的问题是，通讯双方必须事先达成有关算法选择等诸项共识。 如果被保护的消息拥有一定的冗余，加密消息的冗余能保证消息完整性的效果。因为，如果 一个攻击者不知道加密密钥而修改了密文的另一部分，则会导致在解密过程中产生不正确的 结果。 4 不可否认性 不可否认性是防止通讯主体内部可能发生的攻击否认接收或发送了消息。不可否认 性主体的目的在于收集证据，以便事后能够向可信的仲裁机构举证对方确实发送或接收了消 息。证据一般是以签名消息方式出现的，从而将消息与消息的发送者进行了绑定。 在认证和密钥分配协议中，主体通讯双方的目标是一致的，如共享一个良好的会话密钥。 而在不可否认协议中，主体双方的目标各不相同，因而此类协议不用考虑诚实主体通讯之间 可能存在的恶意攻击。要达到不可否认性这一目标，协议必须具有以下两个特点：证据的正 确性和交易的公平性。在不可否认性之中还可以引申出电子商务中其他相关性质，如交易的 可追究性、货币和商品的原子性，匿名性等。 1 2 安全协议中的缺陷 “确保密文协议正确是很困难的”是一个众所周知的事实。设计一个正确的协议要求 安全协议设计者投入无限的精力。许多新提出的协议是为了修补已发现的现有协议的安全缺 陷。安全协议中的安全隐患总是可以用一个攻击脚本来描述，在其中协议所提供的一些安全 服务能够被一个或一些相互勾结的攻击者蓄意破坏。在安全协议领域，似乎永远存在着协议 设计者和攻击者之间的较量：提出一个协议，发现一种攻击：跟着进行修补，继而又发现一 种攻击：再一次修补【2 卜 本节所给出的是一个简单的认证和密钥交换协议。两个陌生的通讯主体a l i c e ( a ) 和 b o b ( b ) 起初彼此互不认识，但都认识可信的第三方t r e n d ( t ) 并且和t r e n d 共享了长期 密钥。a l i c e 和b o b 想通过一个协议达成相互认识，并用一个仅双方知道的会话密钥进行通 讯。 首先，a l i c e 把自己和b o b 的身份告诉t r e n t ，想借此共享一个秘密通道实现两者之间的 通讯。t r e n d 接收到a l i c e 的请求后，即产生一个随机的密钥置，并用与a 和b 共享的密 钥加密密钥眉返回给a 。a 收到后解密出置并发给b 密文 田k b t 。b 解密出k 后，发送 一条消息告诉a 已收到，自此a 跟b 之间建立了秘密的会话通道。具体协议见图i 一1 。 3 第一章引言 在完善加密假设下，一个被动的窃听者在截获到加密的信息后，由于这些密文仅能由合 法的接受者用各自的密钥解密后方能阅读，在没有共享解密密钥坼) 。盯 k ) 。的情况下， 无法得到会话密钥足的任何信息。 遗憾的是，该协议是有缺陷的。m a l i c e ( 攻击者) 在网上截获了传递的消息后，可以冒 充某一主体发送给另外一个主体，从而使得两个主体间共享的密钥是m a l i c e 所知道的密钥， 图1 2 给出了这种攻击的过程。 我们注意到，上述攻击结果是m a l i c e 通过改变b o b 的身份造成的，又由于b o b 的身份 是用明文发送的，这就暗示着我们可以通过隐藏b o b 的身份来弥补协议中的缺陷。 种修补在理解了上述m a l i c e 改变b o b 身份的攻击后，我们可以对协议第一条消息中 b o b 的身份处理成用a l i c e 和t r e n d 之间共享密钥加密的密文形式，也就是修改为： 1 a l i c e 发送给t r e n d ：a l i c e ， b o b ji c a t ； 注意，这里a l i c e 的身份保持明文是必要的，以便t r e n d 能知道他应用哪个密钥对密文 部分进行解密。 另一种攻击然而上述修改方法并没有为提供一种彻底修补。例如，不难看出， m a l i c e 可以发起如下攻击： 1 m a l i c e ( l i c e ) 发送给n d ：a l i c e ， m a l i c e ( ? 。； 4 第一章引占 其余部分与第一种攻击相同。注意，在这个攻击中我们假设m a l i c e 有密文肋，f c 曰，。 这可能是因为m a l i c e 已经从a l i c e 和m a l i c e 先前的一个正确的协议运行中记录下来的。 图1 2 对“简单的密钥交换协议”的攻击 假定：除原来假定外，m a l i c e 和t r e n d 共享密钥而 。 攻击结果：a 认为在和b 共享的会话密钥冒，事实上是在和m 共享。 固 再一种攻击事实上。对协议的还有另一种攻击方法，它并不依赖改变任何主体的身份。 而是，m a l i c e 将讯n d 发给a l i c e 的消息改为 m a l i c e ( t r e n d ) 向a l i c e 发送： k ) n r ，f 这里k 是再以前协议运行中a l i c e 和b o b 之间的会话密钥，这样m a l i c e 已经记下了密 文组 k ) 白，。这个攻击的其余部分和最初攻击相同，m a l i c e 截获由a l i c e 发给b o b 的随后 消息，最后伪装成b o b 向a l i c e 发送确认消息。 1 9 7 8 年，著名的密码学家n e e d l m m 和s c h r o e d e r 设计了一个基于公钥密码系统的认证 协议n s p k 公钥认证协议【5 】。这个协议可简化如下： 爿口； 。，爿) 岛； 2 占- 、嘣j m ，m ) “， 3 a _ b ：心0 k a ； 第一章= ；| 爵 这里，如，岛表示通讯主体a 和b 的公钥，口，坼表示a 和b 产生的随机数。a 和b 通过互相交换随机数来实现双方的认证，并且经过哈希后可产生两者之间的会话密钥。 该认证协议随后被许多商用协议采用作为实现未受信双方相互认证的重要基础。 然而，十七年后的1 9 9 5 年英国的l o w e 发现了其中一个重要的攻击 6 卜一中间人攻击。 攻击者m a l i c e 在不强行解密密文的前提下，通过在a l i c e 和b 0 b 之间发起两次会话可成功 获得的a 、b 之间用于认证和通讯的随机数。图l 一3 给出了该攻击的全过程。 在这种攻击中，m a l i c e 成功的关键步骤是a l i c e 无意地为他解密了b o b 的随机数坼。 当一个主体无意地为攻击者执行一个密码运算时，该主体就被称为提供了预言机服务 ( o r a c l es e r v i c e ) 。密码算法和协议要求即使用户为攻击者提供预言机服务也是安全的。 一种修补如果在b o b 返回给a l i c e 的消息中加入应答者的身份，即 b o b ，。，6 ) 。， 则可以防止这种攻击。然而，m a c ) 指出如此修改的协议仍然存在设计上的问题( 称为“解 密一检验消息认证”运行模式) ，并在文献 2 】中给出了新的修改方案。 尽管协议设计者尽可能地在协议设计种避免可能出现的人为错误，但复杂的系统仍可能 包含各种设计上的缺陷。而且，与提供安全服务的系统不同，其他复杂系统中的用户和环境 一般不是敌对的，甚至是友好的。例如，为了避免有问题软件系统的崩溃，细心的使用者可 能会学会如何避免使用某些方法。然而，对于一个信息安全系统，它的环境和一些用户总是 敌对的：它们的存在就是为了尽一切可能寻找到设计漏洞攻入系统。 s c - t i m a l i s 和d s p i n e t l i s 根据安全协议缺陷产生的原因将缺陷分成以下六类：a 、基本协 议缺陷；b 、密钥猜测缺陷；c 、陈旧消息缺陷；d 、并行会话缺陷；e 、内部协议缺陷；f 、 密码系统缺陷。 m a c ) 在其文献【2 】中也给出了对认证协议的8 类典型攻击：a 、消息重放攻击；b 、中间 人攻击；c 、平行会话攻击：d 、反射攻击；e 、交错攻击；f 、归因于类型缺陷攻击；g 、归 因于姓名遗漏攻击；h 、密码服务滥用攻击。 1 3 安全协议形式化分析初步 在上一节，我们注意到如下事实：安全协议是非常脆弱和容易出错的。怎样设计出安全、 可靠的认证协议，是具有各种背景的研究者正在从事的一个严峻课题。这些研究者包括密码 学家、数学家以及理论计算机科学家。他们一致地认为在安全协议分析中应该由人工经验或 工程测试的方法而转向采用形式化的方法。 形式化方法是对非形式化方法的自然扩展。形式化方法通常支持用符号或描述语言表示 的一个系统，这种描述语言模型化并详细说明系统的行为，并借助于逻辑推理和数学证明的 6 第一章弓i 苦 图1 - - 3l o w e 的关于n s 公钥认证协议的攻击 假定：a l i c e 、b o b 和m a l i c e 的公钥为k j 、k 口和k m 。 攻击结果：b o b 认为他i e l ia l i c e 共享秘密4 ，但实际上是在和m a l i c e 共享。 医习 。 区习臣a l 一 j 2 r r 3 4 j 1 1 5 l6 l 1 、a l i c e 南m 曲c e 发话髓视数砘：铺。，毯【。： 2 、m a l i c e 伪装成a l i c ei 句b o b 将该消息转发绘b o b ：磷，。毯k l ； 3 、b o b 躺密毛，生成黼规数，和n t 一起发给a k e ：氆。，n x 。； 4 、m a l i c e 截获该条消息，揪a l i c e ：磷4 ，n 矗x ； 5 、a l i c e 辑密褥虱随机数，i t j m a l i c e 确认收虱：氆矗k 。； 6 、m a l i c e 瓣密褥虱随机数n b 数 3 j b o b 确认收瓢：磷击k i ： 方法进一步推断系统的行为性质。形式化方法普遍的特征是在解决问题时采用系统的方法， 有时使用穷举的方法。因此，对于分析像安全协议这样的复杂系统尤其适用。 安全协议的形式化研究侧重于用各种形式化的方法来分析验证网络协议是否满足所具 有的性质，也即是否存在安全漏洞，从而从根本上保证网络协议的安全性，同时也为设计合 理可靠的安全协议提供强有效的支持。 目前为止，在采用逻辑推理和模型检测等形式化方法分析安全协议方面已取得了一系列 的成果，如b u r r o w ，a b a d i 和n e e d h a m 用他们设计的b a n 逻辑成功地找到n s ，k e r b e r o s 等 协议中已知和未知的漏洞。上节中隐藏在n s p k 协议中1 7 年之久的著名的中间人攻击漏洞就 是l o w e 借助于进程演算模型c s p 和模型检测工具f d r 发现的。 作为全文的技术引论，本节将给出在形式化研究安全协议领域常见的重要概念、定义和 约定，涵盖密码学基础知识、网络攻击模型和形式化分析常用方法。 7 第一章t j 【苦 1 3 1 密码学基本概念 对称密码体制 对称加密，也称传统加密和单钥加密，是采用替换和置换等技术实现加密。如从古老的 恺撒密码、p l a y f a i r 密码、转轮机密码，到最近著名的d e s ( 数据加密标准) ，是目前使用 最为广泛的一种。对称加密方案有s 个基本成分 3 】： 明文：原始的消息或数据，作为加密算法的输入； 加密算法：对明文进行各种代换和变换，使之变成不可理解的密文； 密钥：独立于明文的输入，加密算法将根据特定的密钥而产生不同的输出； 密文：经加密后产生的随机的数据流，依赖于明文和密钥； 解密算法：是加密算法的逆运算，输入密文和密钥可以还原出明文。 公钥密码体制 公钥密码，也称为非对称密码，是d i f f i e 和h e l l m a n 于1 9 7 6 年为了解决密钥分配和数 字签名而提出的一种与传统密码截然不同的密码体制。它有两个不同的密钥，用于异地的加 密和解密操作。其中只能为通讯主体所知道的密钥称为私钥，公开给他用户的密钥称为公钥。 著名的公钥密码算法有r s a 、椭圆曲线、d i f f i e - - h e l l m a n 和d s s 算法等【3 】。 一般地，公钥密码体制的应用可分为三类： 加密，解密：发送方用接受方的公钥对消息加密，只有拥有私钥的接受方才能对密 文解密； 数字签名：发送方用私钥加密消息。实现对该消息的“签名”。接受方可以利用发 送方的公钥来对签名的消息进行验证； 密钥交换：通讯双方交换产生会话密钥。如1 2 2 节中的n s p k 密钥交换协议。 完善加密假设 本文中消息m 的密文习惯上记为 m ) k ，这里k 可以是公钥或者私钥并且，所谓的 密文总是指在下述意义上的“完善”密码算法加密所得到的。 性质1 1 密文 膨) r 是完善加密的，当 1 ) 不用密钥k ( 私钥体制中) ，或者不用与k 匹配的私钥( 公钥体制中) ，密文f m ) f 是不能被解密的； 2 ) 已知密文，并提供了关于明文的一些消息，不能求解出密钥k ( 私钥体制中) ，或 者不用与k 匹配的私钥( 公钥体制中) 。 完善加密假设是对现实世界中存在的加密算法的理想化，这个理想化能便于我们将协议 设计与分析同协议所使用的密码算法的设计与分析的职责相分离。这种分离使协议的设计与 分析变得容易，但如我们所见到的，完善的密码加密并不能保证协议不含有安全缺陷。事实 上，很多已知的攻击，都不是因为密码加密算法的不完善，而是因为协议设计中的缺陷造成 的。 8 第一章q i 苦 1 3 2 攻击模型和常用分析方法 由计算机、设备和资源构成的大型网络( 如因特网) 是典型的开放系统，这就意味着一 个主体( p r i n c i p l e ) ( 或实体、代理、用户) 能够加入这样的网络，并通过该网络来发送和 接收消息，而不需要“超级”主体授权，这里的主体可以是一台计算机，一个设备，一些资 源、服务的提供者，一个人或组织等。在这样的开发性环境中，我们必须想到会有坏人( 攻 击者、窃听者、冒名顶替者等) ，他们会做各种坏事，不仅仅是被动地窃听，而且会主动地 篡改、伪造、复制、删除、注入消息，甚至改变路由在密码学中，这些坏人叫做主动攻 i 捐 - - m a l i c e 。m a l i c e 可以是单个人，也可以是相互勾结的团伙，一个特例是，它可以是协 议中的合法主体，也就是内部人员。 一般假定m a l i c e 在操纵开发性网络通讯方面是相当聪明的。由于他们的行为是不规范 的，其操纵技术也是很难预料的。而且，由于m a l i c e 可以表示一个相互勾结的团伙，他们 可以同时控制地域上相距很远的网络节点。 d o l e v 和y a o 在1 9 8 3 年首次针对开放网络上攻击者的能力提出了一个攻击模型 7 】，这 个模型被广泛地采纳为安全协议中的标准威胁模型- d o i e v y a o 模型。在这个模型中， m a l i c e 具有以下能力： 他能获得网络上传输的任何信息： 他能发起与任何其他主体的对话； 他能成为任何发送信息主体的接受者； 他能冒充任何主体给任意其他主体发送信息。 因此，在d o l e v - - y a o 攻击模型中，发送到网上的任何消息都可以看成是发送给m a l i c e 的，从网络上接收到的任何消息都可以看成是经过m a l i c e 处理过的。也就是，m a l i c e 完全 控制着整个网络。 但是，除非明确声明，在d o l e v - - y a o 模型里m a l i c e 并非是全能的。下面列举出它不能 做的事情： m a l i c e 不能从足够大的空间里猜到随机数； 没有正确的密钥( 或私钥) ，m a l i c e 不能从密文中恢复出明文，也不能从给定的明 文里构造出正确的密文； m a l i c e 不能从给定的公钥求出相应的私钥： m a l i c e 不能控制网络和计算机环境中的私有领域，如离线的存储器等。 本文将采用d o l e v - - y a o 模型作为网络协议分析时的攻击者模型。 形式化方法通常支持用符号或描述语言表示的一个系统，这种描述语言模型化并详细说 明系统的行为，并借助于逻辑推理和数学证明的方法进一步推断系统的行为性质。 安全协议的形式化分析是采用一种正规、标准的方法对协议进行分析，以检查协议是否 满足其安全目标。它有助于更准确地定义协议行为和属性。说明协议运行所需满足的条件。 常用的形式化分析方法主要有以下三种： 1 、基于定理证明的方法 该方法首先用代数或逻辑公式集为协议行为建立命题。并假定必要的公理集( 代数或逻 辑) 。然后将期望的安全性质描述成待证定理集，并利用前提、公理定理来证明定理集。 属于该类的具体方法有b a n 、国w 、a t 、s o v 和k a i l a r 逻辑；p a u l s o n 归纳法；s c h n e i d e r 秩函数和g u t 乜r m n 的线空间等。 2 、基于模型检测的方法 在该类方法中，协议首先被模型化为一个有限状态系统，协议的安全性质通过状态满足 9 第一章引占 关系来验证。 具体方法有被广泛研究的模型检测( m o d e lc h e c k i n g ) ，m e a d o w s 的n r l 协议分析机， 和h o a r e 的c s p 方法。 3 、基于互模拟等价性验证的方法 在这类方法中，设计好的安全协议被抽象成现实模型，与之对应地建立一个具有完美安 全性质的理想模型，然后判断现实模型和理想模型是否等价。 属于该类的方法主要是进程演算( s p i 和c c s 演算) 中的测试等价( t e s te q u i v a l e n c e ) 、 互模拟等价( b i s i m u l a t i o n ) 等方法。 这三种方法详细的介绍将在第二章部分给出。 1 4 主要研究内容和成果 本文主要集中于互模拟等价性验证方法在形式化分析安全协议中的研究，互模拟等价是 借助于用进程演算模型化安全协议来实现验证的。进程演算，如最初的c c s 、c s p ，到后来 的p i 演算、c h i 演算、a m b i e n t 演算等，是研究并发系统的理论模型。进程演算中具有通讯 功能的形式语言对于协议的描述几乎接近协议的本身含义，可以精确地刻画其运行的过程。 在进程演算中，协议的每一个通讯主体都被建模为一个单独的进程，这些子进程并发运行， 并使用进程之间的共享通道进行同步通信，这样得到的并发系统将作为安全协议的基本模 型。 1 9 9 7 年a b a d i 和g o r d o n 在p i 演算里增加了加密解密操作原语从而为安全协议提出 了专门的进程演算模型s p i 演算【8 】。在s p i 演算里，安全协议的安全性质，如保密性和 认证性等，被用原有的测试等价关系很好地定义。为了实现该等价关系的验证，他们引入了 f r a m e d 互模拟【9 】来近似证明测试等价关系。然而，在实际的验证中，他们指出存在两点不 足： l 、f r a m e d 互模拟中输入进程的无穷分支导致该关系无法实现自动验证问题； 2 、f r a m e d 互模拟对测试等价关系不完备。 本文研究的主要内容是试图解决上述第一个问题，即为s p i 演算建立新型的互模拟等价 关系，并实现该关系的自动证明，从而设计出安全协议等价性检测工具。 在此基础上，本文主要做出了以下5 点贡献： 1 在s p i 演算里形式化分析并验证了k e a g b e l o s 协议的认证性和保密性，并指出了在 保密性上的脆弱性； 2 为密文通讯协议建立了新型s p i 演算模型。扩充s p i 演算语法，建立了公钥密码 加密和解密原语；修改了s p i 演算中并发语义，使之能描述协议中通讯主体跟其 环境直接交互，从而可以更确切地刻画现实中的安全协议： 3 在新s p i 演算中引入了符号化技术，定义了符号操作语义和符号互模拟； 4 建立并证明了符号操作语义和原具体操作语义之间的结构等价关系； 5 建立并证明了符号互模拟与原具体互模拟关系之间的可靠性关系。 1 5 本文结构 本文共分为四章，除作为引言的第一章外，其他各章安排如下： 第二章综述性地介绍了在形式化分析安全协议中所采用的三种形式化方法基于定 理证明的方法、基于模型检测的方法和基于互模拟等价性验证的方法，以及这些方法的具体 1 0 第一章0 i 高 代表技术和利用这些技术来进行的实例分析； 第三章介绍了本文所使用的s 口i 演算的代数模型，以及在s p i 演算里形式化分析并验证 了k e r b e r o s 协议的认证性和保密性，并指出了在保密性上的脆弱性。 第四章重点讨论了我们为解决互模拟关系白动验证难题而提出的符号操作语义和符号 互模拟，以及相关的等价性和可靠性证明。 第五章总结了本文的主要 作，并对互模拟等价性验证和安全协议形式化研究未来的。l 作做出了初略的探讨和展望。 第二章形式化研究的主要方法 第二章形式化研究的主要方法 形式化方法内涵丰富，包括各种概念，譬如系统的方法、机械的方法、由规则和或工 具支持的方法，是其对非形式化方法的自然扩展。形式化方法通常支持用符号或形式语言表 示的一个系统，这种描述语言模型化并详细说明系统的行为，并借助于逻辑推理和数学证明 的方法进一步推断系统的行为性质。形式化方法普遍的特征是在解决问题时采用系统的方 法，有时使用穷举的方法。因此，对于分析像安全协议这样的复杂系统尤其适用。 安全协议的形式化研究侧重于用各种形式化的方法来分析验证网络协议是否满足所具 有的性质，也即是否存在缺陷或漏洞，从而从根本上保证网络协议的安全性，同时也为设计 合理可靠的安全协议提供强有效的支持。 在形式化分析安全协议的领域内，我们可以分为三种不同的方法：1 、基于定理证明的方 法；2 、基于模型检测的方法；3 、基于互模拟等价性验证的方法。下节将详细介绍这三种 方法。 2 1 定理证明的方法 定理证明的方法可以描述如下： - 定义一个代数和逻辑公式集，用来描述系统的行为或建立命题，这些命题可以是前提( 已 知的公式) 或者结论( 要推导的公式) ； 假设必要的公理集，从而允许用代数或逻辑方法由已知公式推导出新公式： - 将要分析的期望系统具有的行为或特性描述成一个待证定理集； _利用前提、公理或已证明的定理来证明一个定理以达到希望的结果。 有时，如果运用公理或定理的某些特定规则，定理证明方法中的证明过程就可以机械化。 应用项重写规则将一个公式重写成范式就是机械化证明的一个标准范例。但是，大多数情况 下，机械定理证明冗长乏味，而且机械证明的长度是关于要推导公式大小的非多项式有界量。 基于代数的定理证明方法中，一个必要性质是公理系统必须保持同余性质 ( c o n g r u e n c e ) 。代数结构上的一种二元关系r 称为同余，如果对该结构上的任何二元运算。 只要就有r ( x ，甜) 且上( y ，v ) 就有r ( x o y ，甜o v ) 。同余性也称为可代换性。当系统具有同余 性时，一个系统元素就可以换成具有相关行为的另一个元素，而系统的行为保持不变性。如 果一个系统不具有可代换性，这个系统就不能视为一个健全的系统。因此，同余性又称为定 理证明系统的正确性。无正确性的定理证明是没有用的