（计算机系统结构专业论文）通用可复合密码协议理论及其应用研究.pdf

摘要密码协议是为了获得某种特定的安全目标而执行的一个两方或者多方分布算法，这个算法是一个确定的动作序列，动作序列发送和接收的关键消息是基于某些密码学操作而构造的，例如加密、签名、散列函数等。一直以来，研究者更多地专注于使用形式化方法对现有的密码协议进行分析与验证，更为审慎和成熟的研究思路是设计和建立专用的方法和执行工具，用以指导安全协议的初始设计。在协议设计的过程中，密码协议的可复合性是一个重要属性。当对某个密码学任务进行协议化设计时，我们希望能够将一个任务分解成几个子任务，子任务通常相对简单，最后使用复合技术将已经设计的子任务作为安全子程序复合为给定的密码学任务。在任意协议并行的情况下，通用可复合( u n i v e r s a l l yc o m p o s a b l e ，u c ) 安全模型实现了密码协议的可复合安全性，本文基于u c 安全模型主要研究了以下三个内容：第一，基于u c 安全模型的身份相交复合操作理论的研究。u c 安全模型主要包括密码协议的u c 安全定义和相关的复合操作理论。在参与方唯一身份的假设下，现有的复合操作方法和理论包括子程序替换通用复合操作和多实例相交状态通用复合操作两类。基于协议仿真安全定义，首次提出了协议参与方实体多身份相交情况的复合操作方法和理论。针对参与方实体新身份与旧身份同时出现在单一的协议实例中，身份相交复合操作理论试图说明在一个协议实例中参与方实体安全的实现多身份鉴别自证明问题，身份相交复合操作理论解决了某些实际应用需求的可证明安全问题，例如组播密钥管理g d o i 协议。第二路由协议u c 安全模型的研究。路由协议是一类特殊的密码协议，可证明安全的路由协议设计和分析一直是网络安全领域的开放问题。本文将u c 安全模型引入路由协议可证明安全的研究，对该领域新的概念、技术和方法进行了有益的探索，首次提出了路由协议的u c 安全模型。提出了节点不相交多路径源路由协议的形式化安全定义，设计和实现了可证明安全的多路径路由协议。第三，基于u c 安全模型的应用研究。根据u c 安全模型对密码协议设计和分析的三步方法论，即密码协议的u c 安全定义、基于计算复杂性的困难问题假设、基于“理想函数”的协议实现和“协议仿真”的可证明安全分析，本文应用研究的内容除了组播密钥管理协议和多路径路由协议，主要包括两类情况，一方面针对构造安全多方计算协议的两个基础工具( 不经意传输，可否认认证) ，基于新的复杂性理论安全原语，设计和实现了高效可证明安全的不经意传输协议和可否认认证协议，另一方面针对特殊的无线网络( 例如，无线传感器网络，移动卫星通信网络) 安全需求，设计和实现了可证明安全的密钥分配和建立协议。关键词：密码协议通用可复合安全复合操作理论多方安全计算无线网络安全a b s t r a c tac r y p t o g r a p h i cp r o t o c o li sad i s t r i b u t e da l g o r i t h mt h a tp e r f o r m sas e c m - i t y - r e l a t e df u n c t i o na n da p p l i e sc r y p t o g r a p h i cm e t h o d s ( s u c ha sp u b l i ck e ye n c r y p t i o n ，d i g i t a ls i g n a t u r e s ，h a s hf u n c t i o n ) ，d e f i n e db yas e q u e n c eo fs t e p sp r e c i s e l ys p e c i f y i n gt h ea c t i o n sr e q u i r e do ft w oo rm o r ep a r t i e si no r d e rt oa c h i e v eas p e c i f i e do b j e c t i v e t h ef o r m a la n a l y s i so fc r y p t o g r a p h i cp r o t o c o l sh a st u r n e do u tt op r o v i d eau s e f u lw a yt of i n de r r o l si ns e c u r i t yp r o t o c o l st h a th a da l r e a d yb e e nd e s i g n e da n dd e p l o y e d ，o rt ov a l i d a t et h e m i np r i n c i p l e ，i ti so fc o u r s em u c hp r e f e r a b l et oc a t c ha n dy g 五i i o v cp r o b l e m se a r l yi nt h ed e s i g np h a s e ，a n db e f o r ed e p l o y m e n t w cn e e dm o d e l sa n dt o o l st h a te n a b l et h ed e v e l o p m e n ta n da n a l y s i so fn e w ，i m p r o v e ds o l u t i o n sa sw e l la st h ea n a l y s i so fe x i s t i n gp r o t o c o l s ak e yf e a t u r et h a ti sn e e d e dt os u p p o r tt h ei n t e g r a t i o no fm e t h o d si n t oc r y p t o g r a p h i cp r o t o c o ld e s i g ni sc o m p o s a b i l i t y , m o s to ft h ed e s i g no faw o r k i n ge r y p t o g r a p h i cp r o t o c o li si n c r e m e n t a li nn a t u r e o n es t a r t sw i t has i m p l ep a t t e r nt h a tg i v e st h eb a s i cs k e l e t o no ft h ep r o t o c 0 1 i fs o m eo ft h ea d d e df e a t u r e sr e q u i r ei n t e r a c t i o nb e t w e e nt h ep r i n c i p a l s ，i tm a yb en e c e s s a r yt oc o m p o s et h ep r o t o c o l 谢也s o m eo t h e rp r o t o c o lo rp r o t o c o l s ad e s i r a b l eg o a lf o rc r y p t o g r a p h i cp r o t o c o l si st og u a r a n t e es e c u r i t yw h e nt h ep r o t o c o li sc o m p o s e d 谢mo t h e rp r o t o c o li n s t a n c e s s u c hag e n e r a ln o t i o no fs e c u r i t yi sp r o v i d e db yt h eu n i v e r s a l l yc o m p o s a b l e c ) s e c u r i t yf i - a m e w o r k ,w h i c hp r o v i d e sav e r yg e n e r a lc o m p o s a b i l i t yp r o p e r t y ：au c - s e g m r ep r o t o c o lm a i n t a i n si t ss e c u r i t yp r o p e r t i e se v e nw h e nc o m p o s e dc o n c u r r e n t l y 衍t ha l lu n b o u n d e dn u m b e ro fi n s t a n c e so fa r b i t r a r yp r o t o c o l s i nt h i st h e s i s ，w es t u d ys o m ec r y p t o g r a p h i cp r o t o c o l sw i t h i nt h eu n i v e r s a l l yc o m p o s a b l e c ) s e c u r i t yf i a m c w o r k t h em a i nr e s u l t sp r e s e n t e da r ea sf o l l o w s ：1 w es t u d yt h ef e a s i b i l i t yo fo b t a i n i n gu n i v e r s a l l yc o m p o s a b l ew i t hi d e n t i t yj o i n ts t a t e t h ed e f i n i t i o no fs e c u r i t yf o rc r y p t o g r a p h i cp r o t o c o l ，a n dt h ec o m p o s i t i o no p e r a t i o na n dt h e o r e ma r ep r o v i d e db yt h eu n i v e r s a l l yc o m p o s a b l e ( u c ) s e c u r i t yf r a m e w o r k w es h o wt h et w ot y p eo fc o m p o s i t i o no p e r a t i o no ft h e s u b r o u t i n es u b s t i t u t i o n a n dt h e j o i n ti n t e r n a ls t a t eo fm u l t i i n s t a n c ei n t e r a c t i o n b ye a c hp a r t yw h oi si d e n t i f i e dv i aau n i q u ep a r t yi d e n t i f i e rp i d a si nt h ec a s eo fp r o t o c o le m u l a t i o n , w ep r e s e n tal l e wc o m p o s i t i o no p e r a t i o na n dt h e o r e m ，w h i c hi sc a l l e dt h eu n i v e r s a l l yc o m p o s a b l e 、) i r i 也i d e n t i t yj o i n ts t a t e ( i d j u c ) ，i nt h es e t t i n gw h e r eas i n g l ei n s t a n c eh a ss o m ea m o u n to fi d e n t i t yj o i n ts t a t e ，a n dd e m o n s t r a t es u f f i c i e n t2 3 c o n d i t i o nf o rw h e nt h en e wo p e r a t i o n p r e s e r v e ss e c u r i t y t h ec a s eo fc o m p o s i n gi d e a lp r o t o c o l sf o l l o w sa sas p e c i a lc a s e ，s p e c i f i e di na l la p p l i c a t i o nt os e c u r em u l t i c a s to ft h eg r o u pd o m m no fi n t e r p r e t a t i o n ( g d o i ) p r o t o c o li st h a tt h ei d e n t i t y , a l l o w i n gm u l t i p l ei d e n t i t i e sc a l lb eu s e f u lf o rs e c u r i t ya s s o c i a t i o n s w ed e m o n s t r a t et h eu s eo fo u ri d j u co p e r a t i o na n dt h e o r e mb yp r o v i n gt h a tg d o ip r o t o c o li ss c c u i ei no u rm o d e l r o u t i n gp r o t o c o l si so n eo ft h em o s tb a s i cn e t w o r k i n gf u n c t i o n si nn e t w o r k s h o w e v e r ，t h es e c u r i t yo fr o u t i n gp r o t o c o l sh a sm a i n l yb e e na n a l y z e db yi n f o r m a lm e a n so n l y w er e p o r to naf e we x c e p t i o n s ，w h e r es o m ea t t e m p t sa l em a d et ou s ef o r m a lm e t h o d sf o rt h ev e r i f i c a t i o na n dt h ed e v d o p m e n to fr o u t i n gp r o t o c o l s w ea d v o c a t eam o r es y s t e m a t i cw a yo fa n a l y s i s w ep r o p o s eaf r a m e w o r kb a s e do nu cs e c u r i t yi nw h i c hs e c u r i t yc a nb ep r e c i s e l yd e f i n e da n dr o u t i n gp r o t o c o l sc a l lb ep r o v e dt ob es e c u r ei nar i g o r o u sm a n n e r t ot h eb e s to fo u rk n o w l e d g e ，i th a sn o tb e e na p p l i e di nt h ec o n t e x to f r o u t i n gp r o t o c o l ss of a r w ea l s op r o p o s ean e ws o u r c er o u t i n gp r o t o c o l ，c a l l e ds e c u r em u l 印l en o d e d i s j o i n tp a t h ss o u r c er o u t i n gp r o t o c o l ，a n dw ed e m o n s t r a t et h eu s eo fo u rf r a m e w o r kb yp r o v i n gt h a ti ti ss e c u r ei no u rm o d e l w ed e f i n e da n dr e a l i z e ds p e c i f i cp r i m i t i v e sw i t h i nt h eu cf r a m e w o r k t h r e ep r o c e s so ft h ed e v d o p m e n ta n da n a l y s i so fu cs e c u r i t ye r y p t o g r a p h i cv o t o c o la r es e c u r i t yd e f i n i t i o n s ，c o m p l e x i t yt h e o r e t i cp r i m i t i v e s ，a n dd e f i n i n ga n dr e a l i z i n gt h ei d e a lf u n c t i o n a l i t yo ft h ee r y p t o g r a p h i cp r o t o c o l sa n dt h e i rp r o o f so fs e c u r i t y w ef o r m u l a t e dan u m b e ro fi d e a lf u n c t i o n a l i t yt h a tc a p t u r e st h es e c u r i t yr e q u i r e m e n t sf r o mag d o ip r o t o c o l ，s o u r c er o u t i n gp r o t o c o l s ，d e n i a b l ea u t h e n t i c a t i o n ，k e ye s t a b l i s h m e n tf o rw i r e l e s ss e r l s o rn e t w o r k sa n dm o b i l es a t e l l i t ec o m m u n i c a t i o ns y s t e m s ，a n dw ep r o p o s e da n da n a l y z ean u m b e ro fp r o t o c o l ss u c ha so b l i v i o u st r a n s f e ra n dp r o t o c o l sm e n t i o n e da b o v ei nu n i v e r s a l l yc o m p o s a b l em o d e l k e yw o r d s ：c r y p t o g r a p h i cp r o t o c o l ，u n i v e r s a l l ye o m p o s a b l es e c u r i t y ，c o m p o s i t i o no p e r a t i o na n dt h e o r e m ，m u t i n gp r o t o c o l s ，m u l t i - p a r t yc o m p u t a t i o n , w i r e l e s sn e t w o r ks e c u r i t y独创性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了本文中特别加以标注和致谢中所罗列的内容外，论文中不包含其他人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。本人签名：关于论文使用授权的说明本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内容；可以允许采用影印、缩印或其它复制手段保存论文。( 保密的论文在解密后遵守此规定)本人签名：刃佑日期：川，, 12导师签名：日期：p 嵋1 -第一章绪论u c 安全模型利用“交互式图灵机系统”描述密码协议的计算模型，“理想函数描述密码协议的安全需求，“协议仿真”概念定义密码协议的安全性，以及“协议复合操作理论”实现密码协议的通用可复合安全属性。u c 安全模型解决了多参与方( 具有唯一身份的多含协议实体) 、多协议( 不同协议共同完成某个密码学任务) 、多实例( 同一协议的不同副本) 网络环境情况下的密码协议复合安全问题。基于u c 安全模型，本文讨论了单一协议实例中单一参与方实体的多身份鉴别问题，首次提出了的参与方实体身份相交复合操作理论，解决了多身份情况下的密码协议复合安全问题，并将该理论应用于组播密钥管理协议；其次针对路由协议的可证明安全问题，借鉴u c 安全模型理论的研究成果，通过多路径路由协议的设计和分析，研究了路由协议可证明安全方法和关键技术问题；基于新的安全原语乖u c 安全模型，研究了两个典型的两方密码学任务：不经意传输和可否i x i x 汪；最后，针对特殊无线网络的实际应用场景，提出了u c 安全的无线传感器网络和移动卫星网络的认证密钥建立协议。1 1 密码协议密码学有着悠久的历史，在2 0 世纪4 0 年代以前，密码学还只是为军事和政治服务。1 9 4 9 年，s h a n n o n 发表了一篇具有划时代意义的论文“c o m m u n i c a t i o nt h e o r yo f s e c r e c ys y s t e m s ，首次用概率统计的观点对明文、密文、密钥、信息的传送进行了数学描述和定量分析，标志着密码学的研究走上了科学的轨道。1 9 7 6 年，d i f f i e 和h e l l m a n 发表的论文 n e wd i r e c t i o n si nc r y p t o g r a p h y 【2 】宣告了现代密码学时代的来临。公钥密码体系和数据加密标准( d e s ) 【3 】的诞生引发了密码学研究的重大变革。以公钥密码体系为基础的数字签名、认证加密以及数字证书等技术在信息安全领域有着广泛的应用。密码学是网络安全的基础。采用密码技术的密码协议是构建安全网络环境的基石，它的正确性和安全性对于网络安全极其关键，因此也被称为安全协议。密码协议涉及两个或两个以上的参与方，参与方分别利用自己的局部输入数据通过交互过程完成某个计算任务，同时，面对各种不同类型的攻击行为，密码协议借助密码学原语来保证某些“安全属性”。在实际系统中，需要通过密码协议进行实体之间的认证、在实体之间安全地分配密钥或其他各种秘密、确认发送和接收的消息的不可否认性等。为了清楚的理解本文密码协议问题的范围和涉及的概念，我们将密码协议任务分为三类：基本的密码协议、典型的两方密码学任务和安全多方计算密码学任务。1 1 1 基本的密码协议面对一个完全控制整个通信网络的攻击者，保证不同参与者之间的安全通信是一个最基本的目标。如果两个互不相识的主体希望进行安全通信，他们应该首先建立一个安全信道，而该信道是由密钥支撑的。建立安全信道的两个主体希望运行某种认证协议，这种认证协议具有建立密钥的任务。安全通信的实现通常需要借助公钥加密机制、数字签名等密码学原语，以及认证密钥交换协议完成。在网络通信中最常用的、基本的密码协议按照其完成的功能可以分成以下三类【4 5 】：认证协议：提供给一个参与方关于其通信对方身份的一定确信度。认证协议中包括实体认证( 身份认证) 协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。密钥交换协议：在参与协议的两个或者多个实体之间建立共享的秘密，特别是这些秘密可以作为对称密钥，用于随后的加密、消息认证以及实体认证等多种密码学用途。认证及密钥交换协议：为身份已经被确认的参与方建立一个共享秘密。这类协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。针对特殊无线网络的实际应用场景和密码协议的可复合安全属性，本文研究了无线传感器网络和移动卫星网络的认证密钥协议。更详细的内容见本文第六章的内容。1 1 2 两方密码学任务以基本的密码协议为前提，我们进一步理解通用的两方密码学任务。通用的两方密码学任务涉及两个参与方，他们之间相互不信任，但是又希望共同完成一个计算任务同。典型的两方密码学任务协议是零知识( z e r o k n o w l e d g e ) 协议【刀、承诺( c o m m i t m e n t ) 协议【8 1 、掷币( c o i n t o s s i n g ) 协议【9 】和不经意传输( o b l i v i o u st r a n s f e r ) 协议【l o 】、可否认认证协议【l l 】。零知识协议：是指一个参与方希望另一个参与方相信某种声称的正确性，同时不泄露任何额外的信息。即示证者( p r o v e r ) 向验证者( v e r i f i e r ) 证明他知道一个秘密，但是验证者在验证后并不知道秘密是什么。承诺协议：是产生保密的承诺和公开秘密( 解诺) 的安全协议。承诺协议是一个两阶段协议：提交阶段，承诺的接受者获得某些信息，信息是未知的承诺值，一旦提交，不可改变。展示阶段，接受者获得开启承诺的某些值，验证承诺是否有效。掷币协议：是指两个参与方试图协商一位或多位比特信息，即使某个参与方试图使输出趋近于某一个值时，该比特信息仍然能够来自于一个均匀分布。不经意传输：是指某个参与方传送两个消息，另一个参与方提供一个比特信息，协议结束后消息的提供者不知道接受者获得了哪个消息，消息的接受者不知道另一个消息的内容。可否认认证：能够使接收者鉴别消息的来源，但是，接收者不能向第三方证明消息来源，接收者通过“仿真”发送者和接收者之间的消息实现可否认认证。签名认证机制不具有可否认性。假设通信信道是安全的，攻击者行为通常发生在两个参与方之间，两方密码学任务涉及的两个主要概念是正确性和保密性。正确性：指能够通过一个本地输入的函数来保证密码学任务的有效性。保密性：指尽可能保护本地数据的秘密性。不经意传输协议可用于完成o b l i v i o u sc i r c u i te v a l u a t i o n ( o c e ) 、m e n t a lg a m e s 以及安全多方计算等密码学任务。本文提出了新的可复合安全的不经意传输协议方案。更详细的内容见第四章的内容。可否认认证协议在电子选举、电子拍卖、电子交易等安全多方计算应用场景中有着重要的作用。本文提出了解决并行可否认认证问题的新方法和新的研究思路。更详细的内容见第五章的内容。1 1 3 多方密码学任务安全多方计算任务，即两个以上的参与方利用他们私有的局部信息去完成某个共同的计算任务1 2 1 。从广义上讲，所有的密码学协议都是安全多方计算的一个特例。安全多方计算任务典型的应用有电子选举、电子商务、数据库交叉查询等。除了正确性和私密性之外他们还有基于某种特殊要求的安全属性。电子选举要根据各种上下文来综合考虑协议的正确性、公正性，私密性和可否认性。电子商务应用，比如在线拍卖、股票交易、购物、赌博，这些都需要解决传输过程中的公平性以及某种可接受的方式来处理争议，另外还包括结果的公平发布。数据库交叉查询是指多个数据库可以联合起来进行数据查询。除了查询的结果之外，数据库中的其它数据将保持私有状态。即保护各个独立主体的私密性时同时要保护统计学的信息，要隐藏获取数据的数据库，在处理过程不泄露额外信息的情况下能够对查询做出响应。安全多方计算协议牵涉到众多的底层密码理论和协议，一些新的方向正在逐渐获得越来越多的关注，如参与者匿名多身份问题( 别名系统或称匿名信任系统)【1 3 1 。本文借鉴别名系统的性质，研究了多身份鉴别问题的可复合问题，更详细的内容见第二章的内容。路由协议的安全定义和路由协议可证明安全的相关方法和技术问题一直是网络安全领域的困难问题。本文认为安全路由协议是一类特殊的安全多方计算协议，本文将可复合安全密码协议的研究成果引入路由协议可证明安全的研究，对该领域新的概念、新的技术和方法进行了有益的探索。更详细的内容见第三章的内容。1 2 协议形式化设计和分析方法一直以来，研究者更多地专注于使用形式化方法对现有的密码协议进行分析与验证，更为审慎和成熟的研究思路是设计和建立专用的方法和执行工具，用以指导安全协议的初始设计。目前对于密码协议的形式化设计与分析演化出两个方向：符号操作方法和计算复杂性方法【1 4 , 1 5 】。符号操作方法强调的是自动化的机器描述与分析，用简单的形式化语言和符号方法进行协议设计和推理分析计算复杂性方法采用归纳推理过程( 从一个已知的前提得出结论的逻辑过程) ，其主要思想是把攻破协议的问题归约到求解某个困难问题上。基于计算复杂性方法，本文开展了相关的研究工作。1 2 1 符号操作方法符号操作方法主要包括以下几类方法【1 6 j ：基于模态逻辑的方法。模态逻辑由一些命题和推理规则组成。命题表示主体对消息的知识或者信仰，运用推理规则可以从已知的知识和信仰推导出新的知识和信仰。最著名的是b a n 1 7 】及b a n 类逻辑1 8 之1 1 ，例如g n y 逻辑、a t 逻辑、v o 逻辑、s v o 逻辑等。其次是用于分析电子商务协议可追究性的k a i l a r 逻辑瞄】。模态逻辑只能分析安全协议的认证属性不能分析保密属性，并且其最大问题是不够完备，即模态逻辑不能查出协议的所有问题，因此使其面临这样的尴尬局面：如果模态逻辑证明一个协议是有问题的，那么协议一定存在问题；如果模态逻辑证明一个协议是安全的，却不能令人信服。模型检测的方法。模型检测法也叫状态空间搜索法，它是一种验证有限状态系统的自动化技术。其基本思想是使用规范语言( 一般采用有限状态自动机) 对系统进行建模，使用逻辑语言( 一般采用时态逻辑) 对系统需要满足的性质进行描述，使用状态的搜索算法来确定系统的模型是否满足期望的性质。常用的模型检测工具有l n t c r r o g a t o r 、n r l 、f d r 、m u f f 、s m v 掣2 3 - 2 6 1 。模型检测的优点是自动化程度高，若协议有缺陷能自动产生反例。但是其不足之处是容易产生状态空间爆炸问题，需要限定协议参与主体的数目。定理证明方法。定理证明是对形式化后的协议模型和规约运用证明的技术来证明规约是否在协议模型中满足。定理证明的方法主要有p a u l s o n 归纳法、串空间模型、阶函数、s p i 演算等【2 7 。3 。其目的是证明协议满足安全属性，而不是去寻找协议的攻击，所以定理证明方法针对的是安全协议的正面，而模型检测方法针对的是安全协议的反面。定理证明的方法不同于模型检测，其优点是通过状态的简化可以处理无限状态空间问题，不足之处是该方法难以完全自动化。符号操作方法提供了如下优点：( 1 ) 提供了分析分布式系统的系统方法学。( 2 )明确定义了协议的通信方向和协议的信息流。( 3 ) 提供模块化设计和分析的工具( 4 ) 提供了协议分析的机械化和自动化。但是，符号操作方法不具有表示协议攻击者计算能力的机制，也不能表达协议执行过程的随机性。密码协议的安全与攻击者计算能力和随机性有密切关系。1 2 2 计算复杂性方法1 9 8 4 年，g o l d w a s s e r 乘i m i e a l i 为计算复杂性方法做出了奠基性的工作，将概率论引入了密码掣1 4 1 。基于计算困难假设，g o l d w a s s e r 和m i c a l i 给出了第一个加密方案的精确定义，提出了一个具体的结构来满足可证明的安全定义。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模型) 【3 2 】。在随机预言机模型中，h a s h 函数( 散列函数) 被假设为理想函数。h a s h函数被形式化为一个预言机，生成真随机值。1 9 9 3 年，b e l l a r e 和r o g a w a y 渠j ：随机预言机模型这种思想应用于密钥交换协议，建立了攻击者能力模型及相关的安全定义，并且对两方的实体认证和密钥交换协议进行了安全性证吲3 3 】。可证明安全性的核心理论是提供协议计算描述模型、安全需求模型和协议安全定义，安全性也最终简化为基于计算困难假设的密码学原语安全性。此后，出现了很多b r 9 3 模型的扩展【弘3 羽。1 9 9 1 年，g o l d w a s s e ra n dl e v i n 借助计算复杂性理论，把理想状态下的协议用一簇二元随机变量描述出来? 再把实际状态下的协议用另一簇二元随机变量描述出来建立了基于两簇随机变量的不可区分性( i n d i s t i n g u i s h a b i l i t y ) 的安全定义，并且对多方计算进行了安全性证吲3 9 1 。此后，出现了基于不可区分性模型的扩展【4 0 - 5 0 】。其中将基于不可区分性模型这种思想应用于密码协议安全分析和设计并应用比较广泛的是c k 模型以及u c 模型。c a n e t t i 和k r a w c z y k 提出了基于认证器的协议分析与设计的c k 模型【4 7 】。c k 模型的主要目标是通过认证器的方法来分析和设计密钥交换协议。如果在允许的攻击能力下，攻击者不能够区分基于认证的密码协议产生的密钥和一个独立的随机数，那么我们就可以说该密钥交换协议是安全的。用c k 模型证明所得到的安全保垒垦鍪堑塾塑些堡墅蜜墼堑鱼墅垄墅塑壁垒塑丝墅堕二证是有实际意义的，因为这些安全保证反映了现实通信系统中的安全要求。在此基础上，s h o u p 提出了s h o u p 密钥交换模型【4 剐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 ) 模型【5 0 1 。通用可复合是现实网络环境中的实际情况。在孤立模型( s t a n d 。a l o n e ) 中证明安全的协议在并发复合情况下不一定是安全的。所以，在孤立模型中证明一个协议安全还是不够的。而“u c 安全”理论就是用来描述和分析并发复合情况下密码协议的安全性的。它能够确保许多的协议实例在并发执行时，以及同任意的协议复合时的安全，该理论中的安全定义最重要的性质是它能够确保协议在任意的和不可预测的多方环境( 如：i n t e r n e t ) 中运行时的安全。这对于密码协议来说是非常有实际意义的。在u c 框架中，基于“交互式图灵机( i n t e r a c t i v et u r i n gm a c h i n e s ) 计算模型描述密码协议系统，利用“理想函数”描述密码协议的安全需求，“协议仿真”概念定义密码协议的安全性，以及“协议复合操作理论”实现密码协议的通用可复合安全属性。称在该框架中的安全定义和满足安全定义的协议为u c 安全的协议。本文的工作都是在u c 框架中讨论的。计算复杂性方法试图从数学的角度来处理协议的安全性。当然如果对协议的安全性有一个完整的数学证明，则完全可以相信协议会按照我们的意愿去运行。但是，从协议证明的发展历程来看，以往对协议的安全性证明往往存在很多错误之处【5 1 1 。而且这些安全证明设计复杂、拖沓冗长，使读者望而却步【5 2 1 。尽管存在各种各样的缺点，可证明安全在协议安全性论证上的价值仍然是无法估量州5 3 】。而且对于实际应用中的协议，这应该是目前所能达到的最好的安全级别了。1 2 3 国内研究现状国内对基于符号化理论方法开展了大量的研究工作。如上海交通大学刘东喜【5 4 1提出了基于串空间模型的自动化检测工具a a ，在l i n u x 下实现了该工具，并且用于i k e 和s e t 协议的分析。华东理工大学张爱新p 5 j 对b s w 逻辑进行了扩展，并在此基础上实现了自动化的协议分析器和设计器，并且采用c c i t tx 5 0 9 和n e e d h a l n s c h r o e d e l 公钥协议对其工具进行了验证。中国科技大学任侠【5 6 】对串空间模型进行了改进，但没有实现其原型工具。解放军信息工程大学范红【5 1 7 】对形式化理论进行了分析与研究，在分析模型检测技术和逻辑推理技术的优点和不足的基础上提出了一种混合的安全协议形式化分析方法，但没有给出该方法的具体实现。武汉大学李莉【5 8 】年将串空间理论和项节点图模型结合，并利用定理证明和模型检测技术，实现了安全协议的自动分析器，利用该工具对n e e d h a m s c h r o e d e r 协议进行了分析。国防科技大学李梦君 3 9 1 在h o r n 逻辑和a c u n 理论的基础上，采用o b j e c t i v ec a m l 设计并实现了一个安全协议自动验证工具原型s p v t ，但没有对具体的安全协议采用其工具进行验证。山东大学赵华伟唧 针对b a n 逻辑的不足，提出了一种新的逻辑一l 逻辑，并采用p r o l o g 语言实现了该工具。同时对符号理论和可证明安全理论之间的融合进行了研究，给出了一种调和两种理论的分析方法。北京航空航天大学怀进鹏【6 l 】提出了密码协议代数模型，试图解决无限状态空间问题及协议的顺序复合问题。中国科学院软件研究所的季庆光【6 2 1 、冯登国【6 3 和卿斯汉哗】对当前的基于符号化理论方法的安全协议研究作了归纳，根据建模基础的不同，对协议形式模型进行了分类和分析。对于计算复杂性方法理论国内也开展了一些研究工作。信息产业部电信科学技术研究院于德雷【6 5 】对加密体制的可证明安全性进行了研究。西安电子科技大学陈原嘲】主要对公钥加密与混合加密的可证明安全性进行了研究。中国科学院电子学研究所陈伟东【6 7 】主要对门限密码体制、基于口令的安全协议以及密钥托管协议的可证明安全性进行了研究。西安电子科技大学李兴华【6 8 】对无线网络中安全协议的可证明安全设计与分析进行了研究，对c k 模型和协议安全属性之间的关系进行了分析，并且在i d - b a s e d 密码系统中给出了一个重要的扩展。西安电子科技大学曹春杰【6 9 】对群组安全协议的安全属性之间的关系进行了分析，并且给出了新的安全定义。张帆【1 7 0 】基于c k 模型分析了w a p i 的安全性，并得出w a p i 协议是c k安全的。中国科学院软件研究所的冯登国f 5 3 】对当前的基于计算复杂性方法安全协议研究作了归纳，根据安全定义基础的不同，对协议可证明安全方法进行了分类和分析。1 3 协议复合为了简化密码协议的设计和分析，传统的密码协议任务通常假设某个确定协议运行在一个独立的计算环境中，即s t a n d a l o n e 模型，典型的是d o l c v y a o 模型【1 5 1 。s t a n d a l o n e 模型假设密码协议具有固定的参与方集合、协议运行通过一个交互实例描述，协议参与方的身份是唯一的。但是，在实际的网络环境中由于密码协议的运行是消息驱动的，协议参与方的行为是异步并发，可能出现多种情况，例如多个参与方分别运行某个确定的两方或多方计算协议( 多用户) ，多个不同的密码协议同时运行( 多协议) ，某个密码协议的多个协议实例同时运行( 多实例) 、某个协议实例参与方可能需要以别名的形式参与协议交互( 多身份) ，即密码协议的运行呈现出多用户、多协议、多实例、多身份的情景。可复合性问题是目前安全协议分析研究的一个热点问题。主要原因是，协议的应用范围不断扩大，它们所承载的任务越来越庞大，因而协议的构成也越来越复杂这就给设计和验证工作带来了极大的问题目前看来，现有的协议验证工具和技术难以适应大型协议的评估工作人们期望利用小型的、可以验证安全的协议，通过某种复合技术构建大型的协议。以满足多用户、多协议、多实例、多身份实际需要!西安鱼王科技大学博十论文：通用可复合的密码协议理论及其应用研究由此，协议的可复合安全性就成为一个自然需要解决的问题安全复合需要保证某个协议在独立计算情况下是安全的，在网络环境中这个协议运行的多个实例仍然是安全的，这个协议作为其他协议的组件，通过复合操作构成大型的协议仍然是安全的。1 3 1 协议复合类型在现有的研究文献中，协议复合是指多参与方集合涉及的多个协议执行，并将协议复合归纳为协议自复合和协议通用复合两个主要的类型【7 l 】。本文仍然沿用上述分类方法，但是扩展了协议自复合的内容，提出了单一实体多身份鉴别复合概念。协议用户集合主要考虑在协议所有执行过程中参与主体是否是相同的。( 1 )单用户集合。在协议多个实例的执行中，参与者具有相同的协议角色。( 2 ) 多用户集合。参与者具有不同的协议角色，运行任意的协议执行过程。自复合如果同一个协议运行多个协议实例，协议仍然是安全的，该协议称为自复合。协议自复合通常指多实例复合，多实例复合强调每一个协议实例的运行与其他协议实例的运行是不同的，并且是独立的，即在自复合里，参与方集合运行了相同协议的不同协议副本。自复合包括协议实例状态不相交和相交两种情况，文献【5 0 7 2 1 分别研究了“不相交状态混合模型和通用复合理论”和相交状态通用可复合理论( u n i v e r s a lc o m p o s i t i o nw i t hj o i n ts t a t e ，j u c ) ”，并且假定参与方具有唯一的身份。但是在实际的密码学系统中，一个协议实例中某个参与方实体可能存在多个身份，呈现出身份相交、身份隐藏认证的状态，依靠现有的复合理论无法解决此类问题。通用复合如果多个协议运行多个协议实例，协议仍然是安全的，该协议称为通用复合。通用复合与自复合的区别有两点。在网络中，有多个不同的参与方在交互，第二点参与方在运行任意多个协议，该协议彼此之间独立。u c 安全框架利用“子程序替换( s u b r o u z i n es u b s t i t u t i o n