（计算机应用技术专业论文）可证明安全的认证及密钥交换协议设计与分析.pdf

摘要随着信息技术和网络技术的飞速发展，信息网络的广泛应用已成为社会进步和发展的重要标志之一。计算机网络在给人们带来巨大便利的同时，也对网络上信息的安全保护提出了巨大的挑战。如果不能切实有效地解决计算机网络的安全问题，必将影响到它的应用和发展。采用密码技术的安全协议是构建安全网络环境的基石，安全协议的目标不仅仅是为了实现信息的加密传输，更重要的是为了解决网络中的安全问题，它的正确性和安全性对于网络安全极其关键。本文对可证明安全的认证及密钥交换协议设计与分析进行了比较深入的研究，研究内容包括：可证明安全的认证及密钥交换协议设计与分析理论的研究；i n t e r n e t 密钥交换协议的分析与设计；w l a n 中接入、切换及漫游认证协议的分析与设计和群组密钥交换协议的分析与设计。主要研究成果有：1 根据无线网络认证协议的特点，对c a n e t t i k r a w c z y k ( c k ) 模型进行了扩展，引入了第三个协议参与方，并且定义了其行为和攻击者的能力。对b r e s s o n c h c v a s s u t - p o i n t c h e v a l ( b c p ) 模型和群组安全协议的安全属性之间的关系进行了分析，并且给出了新的安全定义。在通用可组合安全( u n i v e r s a l l y c o m p o s a b l es e c u r i t y ,u cs e c u r i t y ) 框架下提出了基于秘密共享体制的群组密钥交换协议的通用设计方法。2 对i n t c r n e t 密钥交换协议i k e v 2 进行了安全分析，并针对其存在的认证失败和发起者主动身份保护问题提出了改进方案：新的方案通过对通信对方的身份进行签名来实现有效的身份认证，同时还能够保证通信双方对交互消息内容的不可否认性，实现对协议发起者的主动身份保护。3 对国标w a p i x g i 进行了分析，指出其不能保证前向保密性、易遭受字典攻击的问题，然后提出了一种新的接入认证协议和一种支持快速切换的安全关联建立协议。针对i e e e8 0 2 1 l s 规范所定义的w l a nm e s h 不能解决m p 移动性的问题，提出了一种新的接入认证协议3 p a k e ，实现了申请者s 、认证者a 和认证服务器a s 三者之间的相互认证。在此基础上，分别提出了快速切换和漫游接入认证协议，并且为移动用户提供身份保护。4 分析了几个著名的群组密钥交换协议，指出其不能实现一致性的安全目标；然后提出了基于身份的常数轮的群组密钥交换协议；最后根据前面提出的u c安全的群组密钥交换协议设计方法，给出了u c 安全的群组密钥交换协议实例。关键词：可证明安全认证密钥交换安全协议a b s t r a c tw i t ht h er a p i dg r o w t ho fi n f o r m a t i o na n dn e t w o r kt e e h n o l o 百，i n f o r m a t i o nn e t w o r kh a v e8 e c naw i d ea p p l i c a t i o ni nm o r d o ns o c i e t y h o w e v e r , i n f o r m a t i o nn e t w o r k sf a c eg r e a tc h a l l e n g ei ns e c u r i t y a st h eb u i l d i n gb l o c ko fn e t w o r ks e c u r i t y ,c r y p t o g r a p h yp r o t o c o l sc a l lb eu s e dn o to n l yt op r o v i d ei n f o r m a t i o nc o n f i d e n t i a l i 劬b u ta l s ot or e s o l v em o s to ft h es e c u r i t yp r o b l e m si ni n f o r m a t i o nn e t w o r k s s ot h ec o r r e c t n e s sa n ds e c u r i t yo ft h e s ek i n d so fp r o t o c o l sa l ev e r yi m p o r t a n t t 1 1 i sw o r km a k e sac o m p a r a t i v ed e e pr e s e a r c hf o rt h ep r o v a b l ys 。c u r ea u t h e n t i c a t i o na n dk e ye x c h a n g e , w h i c hi n c l u d e s ：t h es t u d yo fp r o v a b l ys e c 眦t h e o r i e sf o ra u t h e n t i c a t i o na n dk e ye x c h a n g e , t h ea n a l y s i sa n dd e s i g no ft w o p a r t ya u t h e n t i c a t i o np r o t o c o l si ni n t e r n e t h ea n a l y s i sa n dd e s i g no fa u t h e n t i c a t i o np r o t o c o l sf o ra e 髓s s ，f a s th a n d o f fa n dr o a m i n gi nw l a na n dt h ea n a l y s i sa n dd e s i g no fm u l t i p a r t ya u t h e n t i c a t i o na n dk e ye x c h a n g ep r o t o c o l s 1 hm a i nr e s u l t sa r ea sf o l l o w i n g ：1 a c c o r d i n gt ot h ec h a r a c t e r i s t i e so f t h ea u t h e n t i c a t i o ni nw i r e l e s sn e t w o r k s ，w ee x t e n dt h ec a n e t t i k r a w c z y k ( c k ) m o d e lb yi n t r o d u c i n gat r u s t e dt h i r dp a r t ya n da d d i t i o n a la d v e r s a r i a lc a p a b i l i t i e s t h e nt h er e l a t i o n s h i pb e t w e e nt h es e c u r i t yd e f i n i t i o no fb r e s s o n c h e v a s s u t - p o i n t c h e v a l ( b c p ) m o d e la n dt h es e c u r i t yp r o p e r t i e so fg r o u pk e ye x c h a n g e ( g k e ) p r o t o c o l sa r ea n a l y z e da n dn e ws e c u r i t yd e f i n i t i o n sa r ep r o p o s e d f i n a l l y , am e t h o do fd e s i g n i n gc o n s t a n tr o u n dg k ep r o t o c o l si nu n i v e r s a l l yc o m p o s a b l es e c u r i t y ( u cs e c u r i t y )f r a m e w o r ki sp r e s e n t e d 2 t h es e c u r i t yo ft h en e _ t vi n t e r n e tk e ye x c h a n g ep r o t o c o li k e v 2i sa n a l y z e d t h e nt h ei m p r o v e m e n to f ( e v 2f o rt h ep r o b l e m so fa u t h e n t i c a t i o nf a i l u r ea n dt h ei n i t i a t o r sa c t i v ei d e n t i t yp r o t e c t i o ni sp r e s e n t e d 3 t h es t u d yo fs e c u r i t ys t a n d a r d so fw l a n f i r s t , b a s e do nt h ea n a l y s i so fw a p i x g l ，i t sv u l n e r a b i l i t i e sa r ei d e n t i f i e da n di m p r o v e m e n ti sp r e s e n t e d t h ei m p r o v e do n en o to n l ys o l v e st h es e c u r i t yp r o b l e m si nw a p i x g l ，b u ta l s op r o v i d e st h ef a s th a n d o f ff o rm o b i l et e r m i n a l s w l a nm e s hi san e wn e t w o r k i n gt e c h n o l o g i e s ，b u tt h eh a n d o f fa n dr o a m i n go fm e s hp o i n t s ( m p s )c a l ln o tb es u p p o r t e db yt h ec u r r e n ts t a n d a r do fw l a nm e s h s oac o m p l e t es e e u i r i t ys o l u t i o no f w l a nm e s hi sp r o p o s e d ，w h i c hc o n s i s t so f at h r e e - p a r t ya u t h e n t i c a t i o np r o t o c o lf o rt h ea c c e s so fam pt ot h ew i r e l e s sn e t w o r k , a na u t h e n t i c a t i o np r o t o c o lf o rt h ef a s th a n d o f fo fam pa n dat h r e e - p a r t ya u t h e n t i c a t i o np r o t o c o lf o rt h er o a m i n go f am ea d d i t i o n a l l y , t h ep r o t e c t i o no fm o b i l eu s e r s i d e n t i t i e si sr e a l i z e d 4 t h es t u d yo ft h eg k ep r o t o c o l s f i r s t ，s o m ef a m o u sg k ep r o t o c o l sa l ea n a l y z e d ，a n dt h er e s u l t ss h o wt h a tt h e s ep r o t o c o l se a r ln o tp r o v i d et h ec o n s i s t e n c y t h e nan e wi d e n t i t y - b a s e da n dau cs e c u r eg k ep r o t o c 0 1a l ep r e s e n t e dr e s p e c t i v e l y k e yw o r d s ：p r o v a b l es e c u r i t ya u t h e n t i c a t i o nk e ye x c h a n g ec r y p t o g r a p h yp r o t o c o l独创性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了本文中特别加以标注和致谢中所罗列的内容外，论文中不包含其他人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。本人签名：日期：关于论文使用授权的说明本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内容；可以允许采用影印、缩印或其它复制手段保存论文( 保密的论文在解密后遵守此规定)本人签名：导师签名：e l 期：日期：第一章绪论随着信息技术和网络技术的飞速发展，信息网络的广泛应用已成为社会进步和发展的重要标志之一。计算机网络在给人们带来巨大便利的同时，也对网络上信息的安全保护提出了巨大的挑战。如果不能切实有效地解决计算机网络的安全问题，必将影响到它的应用和发展。采用密码技术的安全协议是构建安全网络环境的基石，安全协议的目标不仅仅是为了实现信息的加密传输，更重要的是为了解决网络中的安全问题，它的正确性和安全性对于网络安全极其关键。由于诸多原因，安全协议的设计极易出错，即便对于最基本的交互认证协议。长期以来由于缺乏严格的设计和验证方法，安全协议的正确性和安全性始终无法得到有效保障。2 0 世纪9 0 年代初以来，各种形式化方法理论和支持工具的出现和应用，特别是可证明安全理论的出现，使得这一情况大为改观。可证明安全理论对于安全协议的设计以及验证有着巨大的推动作用。借助于可证明安全理论，不仅可以有效地验证协议安全性，还可以对协议设计起到重要的指导作用，对于保障协议安全性和正确性有着重大意义。1 1 安全协议概述开放系统中的主体数量非常庞大，一个主体要维护它和系统中所有其他主体的通信状态是极其困难的，这就要求参与主体采用“交互遗忘”的通信模式。如果两个互不相识的主体希望进行安全通信，他们应该首先建立一个安全信道，而该信道是由密钥支撑的。因此，希望建立安全信道的两个主体应该运行某种认证协议，这种认证协议具有建立密钥的任务。这样的协议称为认证及密钥建立密钥交换协议。在完成由认证密钥支撑的安全通信会话之后，通信双方应该立即删除所建立的信道，即参与主体把支撑安全信道的密钥遗忘，并且永不重用该密钥。因此，我们通常把一个认证的密钥交换协议产生的安全信道称为会话信道，而把支撑该信道的密钥称为会话密钥。1 1 1 基本概念下面我们对安全协议中的几个基本概念进行简单的介绍，详细信息可参考 1 ，2 】。定义1 - 1 ( 隐式) 密钥认证：若参与者确信可能与他共享一个密钥的其他参与者的身份时，其他的参与者无须采取任何行动。定义1 - 2 密钥确认：一个参与者确信其他的可能未经识别的参与者确实具有某个特定密钥。定义1 3 显式密钥认证：已经被识别的参与者具有给定的密钥。具有隐式密钥认证和密钥确认双重特征。密钥认证主要是对其他参与者身份的识别，而不是对密钥值的识别。密钥确认恰恰相反，是对密钥值的认证。此外，隐式密钥认证可以通过之后的加密应用来对密钥进行确认，而显式密钥认证则是在协议执行过程中进行密钥确认。因此，前者的效率相对后者来说要高一些。定义l - 4 基于身份( i d e n t i t y b a s e d ) 的密钥交换协议：协议中参与者的身份信息( 如名字、地址等) 用做该参与者的公钥。定义1 5 可信第三方：在很多的安全协议中包含一个中心化的或可信的参与方，用于初始化系统设置和在线的( 实时) 参与协议执行。这种可信第三方有多种名称：可信第三方、可信服务器、认证服务器、密钥牛成分发中心和证书认证中心( c a ) 等。1 1 2 安全协议分类在网络通信中最常用的、基本的密码协议按照其完成的功能可以分成以下三类【l 】：一认证协议：提供给一个参与方关于其通信对方身份的一定确信度。认证协议中包括实体认证( 身份认证) 协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。一密钥交换协议：在参与协议的两个或者多个实体之间建立共享的秘密，特别是这些秘密可以作为对称密钥，用于随后的加密、消息认证以及实体认证等多种密码学用途。协议可以采用对称密码体制，也可以采用非对称密码体制，例如d i f i l e h e l l m a n ( d h ) 密钥交换协议。一认证及密钥交换协议；为身份已经被确认的参与方建立一个共享秘密。这类协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。本文以认证及密钥交换协议作为主要对象开展研究。1 1 3 安全协议威胁模型在开放的无线网络环境中，必须考虑到攻击者的存在，他们可能实施各种攻击，不仪仪是被动地窃听，而且会主动地改变( 可能用某些未知的运算或方法) 、伪造、复制、删除或插入消息。插入的消息可能是恶意的并会对接收端造成破坏性的影响。一般假定攻击者的能力很强，其行为是不规范的，实施攻击的技术也是难以预料的。而且，攻击者有时不仅是一个实体，还可能是一个相瓦勾结的团伙。因此。在脆弱的网络环境中不能低估攻击者的能力。1 9 8 3 年，d o l e v 和y a o 提出了一个威胁模型【3 】，是用于安全协议验证研究并且使用最为广泛的一个安全协议攻击者模型，它界定了安全协议攻击者的行为能力。该模型将安全协议本身与安全协议具体所采用的密码系统分开，在假定密码系统是“完善的”( 即只有掌握密钥的主体才能理解密文消息) 基础上讨论安全协议本身的正确性、安全性和冗余性等问题。同时指出，在这个模型中，攻击者的知识和能力不可低估，假设攻击者可以控制整个通信网，并具有如下特征：( 1 ) 可以窃听所有经过网络的消息；( 2 ) 可以阻止和截获所有经过网络的消息；( 3 ) 可以存储所获得或自身创造的消息；( 4 可以根据存储的消息伪造并发送消息；( 5 ) 可以作为合法的主体参与协议的运行。因此，在d o l e v y a o 威胁模型中，发送到网中的任何消息都可看成是发送给攻击者处理的( 根据他的计算能力) 。因而从网络接收到的任何消息都可以看成是经过攻击者处理过的。换句话说，可以认为攻击者已经完全控制了整个网络。当然攻击者也不是全能的，也有一些攻击者所不能做的事情，具体包括：( 1 )攻击者不能猜到从足够大的空间中选出的随机数；( 2 ) 没有正确的密钥，攻击者不能由给定的密文恢复出明文；( 3 ) 对于完善的加密算法，攻击者也不能从给定的明文构造出正确的密文；( 4 ) 攻击者不能求出私有部分，比如，与给定的公钥相匹配的私钥；( 5 ) 攻击者虽然能控制计算和通信环境的大量公共部分，但一般不能控制计算环境中的许多私有区域，如访问离线主体的存储器等。此外，在分析密钥交换协议时，应该考虑到各种类型密钥材料的泄露，特别应当考虑下列情况：长期密钥泄露和过去会话密钥的泄露。定义1 - 6 完善的前向保密性( p f s ) ：长期密钥的泄露不会威胁以前会话密钥的安全性。p f s 的思想是指以前的通信不会因长期密钥的泄露而受到威胁，这种属性可以通过d h 协商建立会话密钥来保证。定义1 7 已知密钥安全：以前会话密钥的泄露不会威胁将来会话密钥的安全，也不会被攻击者用来假冒其他协议参与者。目前，绝大大部分关于协议分析与设计的工作都基于d o l e v y a o 攻击模型，“永远不能低估攻击者的能力”，这是设计安全协议时应当时刻牢记的一条重要原则。在本文的研究中，所有协议分析与设计都是基于d o l e v y a o 威胁模型的。1 1 4 对协议的一般攻击方法安全协议建立在密码学的基础上，其目的在于证明所声称的某种属性。认证协议的攻击者包括未经授权而企图获益的攻击者或共谋者。他们发动的攻击可能会造成严重的后果，例如，攻击者获得机密信息或者密钥，或者攻击者成功地欺骗某个参与者使其对宣称的某个属性做出错误判断，从而造成重大损失。通常，如果某个主体断定自己和对方正常运行了协议，而对方却有不同的结论，那么就认为该协议存在着缺陷。必须指出，对于认证协议的攻击主要是指那些不涉及破解底层密码算法的攻击。通常，认证协议不安全不是因为该协议所用的底层密码算法不安全，而是因为协议设计上的缺陷使得攻击者能够在不需要破解底层密码算法的条件下达到破坏认证的目的。因此，在分析认证协议时，通常假设底层的密码算法是“完善的”，不考虑其中可能存在的弱点。这些弱点通常在密码学的其它研究领域中予以研究解决。对认证协议的典型攻击主要有【4 ，5 j ：消息重放攻击、中间人攻击、平行会话攻击( p a r a l l e ls e s s i o n a t t a c k ) ( 在攻击者的特意安排下，一个协议的两个或更多的运行并发执行。并发的多个运行使得攻击者能够从一个运行中得到解决另外某个运行中的网难问题的答案) 、反射攻击( r e f l e c t i o na t t a c k ) 、交错攻击( i n t e r l e a v i n ga t t a c k ) 、归因于类型缺陷的攻击( a t t a c kd u et ot y p ef l a w ) 、归因于姓名遗漏的攻击、滥用密码服务攻击( m i s u s eo f c r y p t o g r a p h i cs e r v i c e s ) 等等。事实上，攻击方法难以穷尽，还有其他的分类方法 1 ，2 1 。因此，对认证协议的分析和设计不能特定针对某一种或几种已知类型的攻击，而是需要综合考虑所有可能的安全威胁，研究安全协议的设计与分析的理论，通过形式化的方法进行协议的安全性和正确性的分析和证明。1 1 5 协议设计原则在协议设计过程中，我们通常要求协议具有足够的复杂性以抵御交织攻击。另一方面，我们还要尽量使协议保持足够的经济性和简单性，以便可应用于低层网络环境。因此，协议的设计要遵循以下设计原则【2 j ：( 1 ) 采用一次性随机数来替代时戳，即用异步认证方式来替代同步认证方式。( 2 ) 具有抵御常见攻击的能力。( 3 ) 适用于任何网络结构的任何协议层( 消息要尽可能地短) 。所设计的协议不仅能够适用于低层网络机制，而且还必须能用于应用层的认证。这就意味着协议中包含的密码消息尽可能短。如果协议采用了分组密码算法，那么我们期望次密码消息的长度等同于一组密文的长度。( 4 ) 适用于任何数据处理能力( 消息尽可能地简单) ，所设计的协议不但能够在智能卡上使用，而且也能够在仅有很小处理能力和无专用密码处理芯片的低级网络终端和工作站上( 如p c 机) 使用。这要求协议必须具有尽可能少的密码运算。( 5 ) 可采用任何密码算法( 必须采用任何己知的和具有代表性的密码算法) 。( 6 ) 不受出口的限制。( 7 ) 便于进行功能扩充，特别是在方案上应该能够支持多用户( 多于两个) 之间的密钥共享。另一个明显的扩展是它应该允许在消息中加载额外的域，进而可以将其作为协议的一部分加以认证。( 8 ) 最少的安全假设，在进行协议设计时，常常首先对网络环境进行风险分析，做出适当的初始安全假设。例如，各通信实体应该相信各自产生的密钥是最好的，或者网络中心的认证服务器是可信赖的，或者安全管理是可信赖的，等等。但是初始假设越多，协议的安全性就越差。因此我们尽可能减少初始安全假设的数目。以上设计规范并非是一成不变的，可以根据实际情况做出相应的补充或调整，其他相关的设计准则可参考 1 ，6 】。1 2 可证明安全理论及研究现状密钥交换协议是一个基本的安全组件，通过它两个或者多个参与方可以得到一个共享的密钥来进行后继的安全通信【”。根据会话密钥产生的特点，可以广义地把密钥建立体制分成两类：密钥协商体制和密钥分发体制。前者的会话密钥是由所有的参与方共同产生，后者的会话密钥仅仅由其中一个参与方产生【l 一。目前，密钥交换协议主要是在下面三种安全原语的基础上设计的，它们分别是：d i f f i e - h e l l m a n ( d h ) 密钥交换1 7 、r s a 算法以及最近的基于椭圆曲线的双线性对( i d c o t i t y - b a s e d ) 。第一个采用公钥技术实现的密钥交换协议是d i m e h e l l m a n 于1 9 7 6年提出的r 玎。尽管之后m e r k e l 提出的协议“m e r k l e sp u z z l e s ”f 8 l 也实现了密钥分配的目标，但是相比较而言，d i 佑e 和h e l l m a n 的协议在效率和安全性的平衡上做的更好【9 】。尽管密钥交换协议已成为各种安全的电子商务应用所必需的关键技术，但是安全协议的分析与设计仍然是一项极其复杂的工作。对于任何一个新的安全协议，要对其安全性有足够的信任都是非常困难的。另外，实际中有很多协议在它们提出不久就被攻破，经验表明非形式化的协议设计方法经常导致错误【1 0 - 2 4 。目前对于认证及密钥交换协议的形式化设计与分析演化出两个方向：计算机安全方法( t h ec o m p u t e rs e c u d t ya p p r o a c h ) 与计算复杂性方法( t h ec o m p u t a t i o n a lc o m p l e x i t ya p p r o a c h ) ，如图1 1 所示：图1 1 安全协议分析技术1 2 1 计算机安全方法计算机安全方法又称基于符号理论的方法，该方法强调的是自动化的机器描述与分析( 例如，模型检测和定理证明) 。1 9 8 3 年，d o l e v 和y a o 发表的论文 3 1 开辟了安全协议的形式化研究领域，其中一个丰要贡献是将安全协议本身与安全协议所具体采用的密码系统分开，在假定密码系统是“完善”的基础上讨论安全协议本身的正确性、安全性、冗余性等课题。这样，学者们可以专心研究安全协议的内在安全性质了。因此，问题很清楚地被划分为两个不同的层次：首先研究安全协议本身的安全性质，然后讨论实现层次的具体细节，包括所采用的具体密码算法等等。密码操作采用黑盒子的方式，从而忽略不同的密码属性，但是这有可能会导致部分信息的丢失。这类自动化方法中存在的一个主要问题就是不可预测性和复杂性。因为攻击者具有指数规模的可能操作集( 例如，某些数据域可能的值的数量有无穷多) ，这会导致状态爆炸的问题1 2 5 1 。因此，这种方式下证明安全的协议往往是有缺陷的，甚至可能得到一个错误的结论。从实用性角度来讲，用这种方法的理想化模型对协议进行安全性证明而得到的结论，其可信度高低是值得商榷的。但是，计算机安全方法对于协议不安全的论证却是可信的，它可以发现协议中已知和未知安全的缺陷1 1 4 一, 2 6 - 2 9 。计算机安全理论主要包括以下几类方法3 0 】：基于模态逻辑的方法。模态逻辑由一些命题和推理规则组成。命题表示主体对消息的知识或者信仰，运用推理规则可以从已知的知识和信仰推导出新的知识和信仰。最著名的是b a n 3 1 ，3 2 1 及b a n 类逻辑。其次是用于分析电子商务协议可追究性的k a i l a r 逻辑 3 3 1 。1 9 8 9 年，b u r r o w s ，a b a d i h e 和n e e d h a m 提出了基于信仰的b a n 逻辑，是安全协议分析的个里程碑。b a n 逻辑的基本思想是通过对认证协议运行过程中消息的接收和发送来从最初的信仰逐渐发展到协议运行所要达到的目的一主体的最终信仰。b a n 逻辑只能分析安全协议的认证属性不能分析保密属性，并且其最大问题是不够完备，即b a n 逻辑不能查出协议的所有问题，因此使其面临这样的尴尬局面：如果b a n 证明一个协议是有问题的，那么那个协议一定存在问题；如果b a n 逻辑证明一个协议是安全的，却不能令人信服。许多研究人员对b a n 逻辑进行了大量的扩展和改进，包括g n y 逻辑3 4 1 、a t 逻辑【3 卯、v o 逻辑【3 6 】、s v o 逻辑”】等，这些统称为b a n 类逻辑。其中s v o 逻辑为b a n 类逻辑的集大成者。模型检测的方法。模型检测法也叫状态空间搜索法，它是一种验证有限状态系统的自动化技术。其基本思想是使用规范语言( 一般采用有限状态自动机) 对系统进行建模，使用逻辑语言( 一般采用时态逻辑) 对系统需要满足的性质进行描述，使用状态的搜索算法来确定系统的模型是否满足期望的性质。常用的模型检测工具有i n t e r r o g a t o r l 3 引、n r l 3 9 1 、f d r 2 “、m u rmi 删、s m v | 【 1 1 等。模型检测的优点是自动化程度高，若协议有缺陷能自动产生反例。但是其不足之处是容易产生状态空间爆炸问题，需要限定协议参与主体的数目。但是随着基于b d d ( b i n a r yd e c i s i o nd i a g r a m s ) 的符号方法的引入，模型检测技术已由原来只能对几千个状态进行有效处理增到能对1 0 1 2 0 个状态进行搜索。定理证明方法。定理证明是对形式化后的协议模型和规约，运用证明的技术来证明规约是否在协议模型中满足。该方法是证明公式在所有的模型都成立。其目的是证明协议满足安全属性，而不是去寻找协议的攻击，所以定理证明方法针对的是安全协议的正面，而模型检测方法针对的是安全协议的反面。定理证明的方法主要有p a u i s o n 归纳法【4 2 】、串空间模型【4 3 4 4 、阶函别4 5 1 、s p i 一演算删等。定理证明的实施需要定理证明器的支持。现有的定理证明器包括：用户导引自动推演工具、证明检验器和复合证明器。定理证明的方法不同于模型检测，其优点是通过状态的简化可以处理无限状态空间问题，不足之处是该方法难以完全自动化。近来也出现了一些其它的形式化方法。比较典型的是p e t r i 网【4 7 】。1 2 2 计算复杂性方法计算复杂性方法又称为可证明安全方法，该方法采用了归纳推理过程( 从一个已知的前提得出结论的逻辑过程) ，其主要思想是把攻破协议的问题规约到求解某个困难问题上。1 9 8 4 年，g o l d w a s s c r 和m i c a l i 为“可证明安全性”做出了奠基性的工作，将概率引入了密码学【4 剐。1 9 8 7 年，f i a t 和s h a m i r 提出了“随机预言机模型”( r a n d o mo r a c l em o d e l ，r o 模型) 【4 9 】。在随机预言机模型中，h a s h 函数( 散列函数) 被假设为理想函数。h a s h 函数被形式化为一个预言机，生成真随机值。可证明安全性的核心理论是提供模型和定义，安全性也最终简化为原子原语的安全性。b e l l a r e 和r o g a w a y ( b r 9 3 ) 将这种思想应用于密钥交换协议，建立了攻击者能力模型及相关的安全定义，并且对两方的实体认证和密钥交换协议进行了安全性证明【矧。此后，出现了很多b r 9 3 模型的扩展，如b e l l a r e 和r o g a w a y 于1 9 9 5年提出的密钥建立模型b r 9 5 【5 ”、b e l l a r e ，p o i n t c h e v a l 和r o g a w a y ( b p r ) 于2 0 0 0年提出的基于口令的相互认证和密钥建立模型垆“、b r e s s o n ，c h e v a s s u t 和p o i n t c h e v a l( b c p ) 于2 0 0 1 年提出的群组认证的密钥交换安全模型 5 3 5 5 】以及最近a b d a l l a ，f o u q u e 和p o i n t c h e v a l ( a f p ) 提出的基于口令的认证的密钥交换模型【5 。b e l l a r e ，c a n e t t i 和k r a w c z y k ( b c k ) 【57 】在1 9 9 8 年引入了模块化的思想，通过提供可重用的模块来构造新的可证安全的协议。在此基础上，s h o u p 提出了s h o u p 密钥交换模型l s s ，c a n e t t i 和k r a w c z y k 提出了c a n e t t i k r a w c z y k ( c k ) 模块化的协议分析与设计模型【5 9 】，而c a n e t t i 则提出了通用可组合( u n i v e r s a l l yc o m p a s s a b l e ，u c ) 模型【6 0 ，6 1 】。其中应用比较广泛的是c k 模型、b c p 模型以及u c 模型。c k 模型：c k 模型的主要目标是通过模块化的方法来分析和设计密钥交换协议。该模型采用了不可区分性方法来定义安全，即如果在允许的攻击能力下，攻击者不能够区分协议产生的密钥和一个独立的随机数，那么我们就可以说该密钥交换协议是安全的。用c k 模型证明所得到的安全保证是有实际意义的，因为这些安全保证反映了现实通信系统中的安全要求。但是c k 模型是一个两方密钥交换协议的设计和分析模型，不能用于三方密钥交换协议的分析与设计，特别是无线网络中基于可信第三方的密钥交换协议。b c p 模型：群组密钥交换协议的形式化设计和分析一直落后于两方的协议设计与分析。b c p 模型在群组密钥交换协议的安全性分析领域迈出了非常重要的一步，并且使设计者在协议设计中受益匪浅。对于群组密钥交换协议的安全模型，最关键的问题是如何把所有的攻击手段都囊括进来，进而给出合理的安全定义。但是b c p 模型作为一个安全模型是如何来描述各种基本安全目标的，以及在b c p模型下证明安全的协议能否满足相应的安全目标? 这些问题目前还不得而知。u c 模型：通用可组合是现实网络环境中的实际情况。在孤立模型中证明安全的协议在并发组合情况下不一定是安全的。所以，在孤立模型中证明一个协议安全还是不够的。而“通用可组合的安全”理论就是用来描述和分析并发组合情况下密码协议的安全性的。它能够确保许多的协议实例在并发执行时，以及同任意的协议组合时的安全，该理论中的安全定义最重要的性质是它能够确保协议在任意的和不可预测的多方环境( 如：i n t e r n e t ) 中运行时的安全。这对于密码协议来说是非常有实际意义的。通用可组合的安全定义要比其他的安全定义要更严格些。该模型最优秀的性质就是模块组合思想：可以单独设计子协议，只要协议满足u c 安全，则可以进行组合构造新的u c 安全协议，并保证协议组合及并发的安全性。但是目前对于群组密钥交换协议的u c 理论与方法上的研究还很少，因此如何利用u c 理论来进行群组密钥交换协议的设计与分析也是当前一个热点。可证明安全理论试图从数学的角度来处理协议的安全性。当然如果对协议的安全性有一个完整的数学证明，则完全可以相信协议会按照我们的意愿去运行。但是，从协议证明的发展历程来看，以往对协议的安全性证明往往存在很多错误之处【6 2 1 。而且这些安全证明设计复杂、拖沓冗长，使读者望而却步【6 3 】。尽管存在各种各样的缺点，可证明安全在协议安全性论证上的价值仍然是无法估量的，并且也是我们得到正确的、安全的协议过程中一个非常重要的工具【i ”。而且对于实际应用中的协议，这应该是目前所能达到的最好的安全级别了。1 2 3 形式化方法的国内研究现状国内对基于符号化理论方法开展了大量的研究工作。如上海交通大学刘东喜1 6 4 提出了基于串空间模型的自动化检测工具a a ，在l i n u x 下实现了该工具，并且用于i k e 和s e t 协议的分析。华东理工大学张爱新嘟】对b s w 逻辑进行了扩展，并在此基础上实现了自动化的协议分析器和设计器，并且采用c c r r tx 5 0 9 和n e e d h a m s c l a r o e d c r 公钥协议对其工具进行了验证。中国科技大学任侠【6 6 】对串空间模型进行了改进，但没有实现其原型工具。解放军信息工程大学范红【6 ”对形式化理论进行了分析与研究，在分析模型检测技术和逻辑推理技术的优点和不足的基础上提出了一种混合的安全协议形式化分析方法，但没有给出该方法的具体实现。武汉大学李莉瞄】将串空间理论和项节点图模型结合，并利用定理证明和模型检测技术，实现了安全协议的自动分析器，并利用该工具对n e e d h a m s c h r o e d e r 协议进行了分析。国防科技大学李梦君【6 9 】在h o m 逻辑和a c u n 理论的基础上，采用o b j e c t i v ec a r o l 设计并实现了一个安全协议自动验证工具原型s p v t ，但没有对具体的安全协议采用其工具进行验证。山东大学赵华伟【7 0 j 针对b a n 逻辑的不足，提出了一种新的逻辑一m b l 逻辑，并采用p r o l o g 语言实现了该工具。同时对符号理论和可证明安全理论之间的融合进行了研究，给出了一种调和两种理论的分析方法。对于可证明安全理论国内也开展了一些研究工作。如西安电子科技大学李兴华、张帆1 7 2 】对无线网络中安全协议的可证明安全设计与分析进行了研究，前者对c k 模型和协议安全属性之间的关系进行了分析，并且在i d b a s e d 密码系统中给出了一个重要的扩展；而后者则利用通用可组合模型定义并实现了一种适用于无线网络的匿名h a s h 认证理想函数。信息产业部电信科学技术研究院于德雷f _ ”】对加密体制的可证明安全性进行了研究。西安电子科技大学陈原【j m 】主要对公钥加密与混合加密的可证明安全性进行了研究。中国科学院电子学研究所陈伟东 7 5 j 主要对门限密码体制、基于口令的安全协议以及密钥托管协议的可证明安全性进行了研究。上海交通大学雷飞字【7 6 】在u c 安全框架下研究了安全多方计算，提出了一些新的u c 安全的门限密码体制和电子拍卖方案。! ! 。堕窒皇兰垒丝叁兰堕鎏塞i 里丝塑窒全笪坠堡星童塑窑丝垫堡鎏堇：窒坌堡1 3 本文的主要工作及结构安排本文主要针对无线网络安全方法和技术的核心问题一认证及密钥交换协议的分析与设计进行了研究，并给出了相关的研究结果。1 3 1 主要工作与主要贡献本文受国家8 6 3 高技术项目“宽带无线i p 网络系统安全技术”( 编号为2 0 0 2 a a l 4 3 0 2 1 ) 、国家自然基金“可信移动互联网络关键理论与应用研究”( 编号为6 0 6 3 3 0 2 0 ) 、“可证安全的多方安全协议的分析与设计”( 编号为6 0 5 7 3 0 3 6 ) 、华为基金、韩国围立庆北大学移动网络安全技术研究中心项目的资助，对可证明安全的协议分析与设计进行了深入的研究，取得了如下成果：1 对安全协议的可证明安全理论进行了研究。根据无线网络认证协议的特点，对c k 模型进行了扩展，引入了第三个协议参与方，并且定义了其行为和攻击者的能力。对b c p 模型和群组安全协议的安全属性之间的关系进行了分析，并且给出了新的安全定义。在u c 安全框架下提出了基于秘密共享体制的群组密钥交换协议的通用设计方法。2 对i n t e r n e t 密钥交换协议i k e v 2 进行了安全分析，并针对其存在的认证失败和发起者主动身份保护问题提出了改进方案：新的方案通过对通信对方的身份进行签名来实现有效的身份认证，同时还能够保证通信双方对交互消息内容的不可否认性，实现对协议发起者的主动身份保护。3 对w l a n 中的安全解决方案进行了研究。首先对国标w a p i x g i 进行了分析，指出其不能保证前向保密性、易遭受字典攻击的问题，然后提出了一种新的接入认证协议和一种支持快速切换的安全关联建立协议。针对i e e e8 0 1 l s 规范所定义的w l a nm e s h 不能解决m p 的移动性问题，首先提出了一种新的接入认证协议3 p a k e ，实现了申请者s 、认证者a 和认证服务器a s - - - 者之间的相互认证。在此基础上，分别提出了快速切换和漫游接入认证协议，并且为移动用户提供身份保护。4 对群组密钥交换协议中的一致性、扩展性以及通用可组合安全性等几个关键问题进行了研究。首先分析了几个著名的群组密钥交换协议，指出其不能实现一致性的安全目标；然后提出了基于身份的常数轮的群组密钥交换协议；最后根据前面提出的u c 安全的群组密钥交换协议设计方法，给出t u c 安全的群组密钥交换协议。1 3 2 本文结构安排本文第二章主要对安全协议的可证明安全理论进行了研究。主要内容包括：c k 模型、b c p 模型和u c 模型的介绍；对c k 模型在无线网络认证模型下进行的扩展；对b c p 模型和群组安全协议的安全属性之间的关系的分析及对b c p 的改进和u c 安全框架下基于秘密共享体制的群组密钥交换协议的通用设计方法的研究。第三章对i p s e e 、i k e v l 以及i l v 2 进行了介绍；然后对i k e v 2 进行了安全分析，并针对其存在的安全问题提出了改进方案。第四章主要对w l a n 接入、切换及漫游问题进行了研究。主要内容包括：对i e e e8 0 2 1 l i 、w a p i x g l 和i e e e8 0 2 1 l s的简单介绍；可用于i e e e8 0 2 1 l i 的无证书认证协议的设计：对国标w a p i x g l进行了分析，并且提出了一种新的接入认证协议和一种支持快速切换的安全关联建立协议；最后提出了一种新的w l a nm e s