（计算机系统结构专业论文）密码协议工程与基于新鲜性的协议安全研究.pdf

密码协议工程与基于新鲜性的协议安全研究摘要密码协议的安全性研究是网络安全研究的主要热点。本论文主要研究了如何应用系统工程思想和形式化方法来分析和设计密码协议，取得的主要研究结果如下：1 将系统工程思想引入密码协议设计，结合前人的研究成果，提出了1 0 条密码协议工程原则：5 条安全需求分析原则，4 条详细设计原则以及l 条安全性证明原则。将密码协议设计看作密码协议工程，从协议设计的不同阶段给出原则，是帮助研究人员按系统工程思想进行密码协议设计的有益尝试。实例分析表明，这些原则不仅较为完备，而且可操作性强，能帮助研究人员明确协议设计背后的隐含假设，发现和避免协议设计中的漏洞，简化协议设计。2 首次提出基于信任的新鲜性标识符分析密码协议的安全性，给出了新鲜性原则：对每个通信参与主体而言，密码协议的安全性取决于发送或者接收的、包含自身已相信新鲜的新鲜性标识符的单向变换。该原则找到了条快捷、有效的密码协议安全性分析方法，论文示例了2 0 多个经典密码协议的分析结果，分析出的针对协议的攻击或者安全隐患有1 2 个是以往没有指出过的。新鲜性原则的特点是：能有效区分消息是否新鲜，安全性的分析独立于并发运行环境的具体形式化描述，也独立于攻击者能力的具体形式化描述；基于该原则得到的分析结果能够证明正确协议的安全性，也能够分析出不安全协议存在的安全属性缺失，以及由该缺失直接构造攻击的结构。3 基于新鲜性原则，提出了基于逻辑推理的信任多集形式化分析方法。以n e e d h a m - s c h r o e d e r 公钥认证协议为例，说明了该分析方法的有效性、严谨性和自动化实现的可能。另外，针对无线网络的开放性和数据包易失的特点，扩展了信任多集方法，能有效用于无线密码协议分析。4 证明了保证认证协议安全的充分必要条件，这些条件在计算模型下分别满足基于匹配对话和不可区分性的4 个可证安全定义。5 提出了信任多集自动分析工具的总体框架，通过在2 种不同开发环境下信任多集自动分析工具初步实现的比较，给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。6 基于新鲜性原则和因果一致性的分布式逻辑时间，建立了信任多集形式化设计方法。构造了一个公钥认证协议，并证明了该协议达到了消息数和轮数的下限。关键词：密码协议，协议分析，协议设计，非形式化方法，形式化方法，自动化实现a b s t r a c tt h es e c u r i t yr e s e a r c ho fc r y p t o g r a p h i cp r o t o c o l si sb e c o m i n go n eo ft h eh o t t e s tr e a s e a r c hs p o t si nn e t w o r ks e c u r i t yf i e l d t h i sd i s s e r t a t i o nm a i n l yd i s c u s s e sh o wt oa n a l y z ea n dd e s i g nc r y p t o g r a p h i cp r o t o c o l sb a s e do nt h ei d e ao fs y s t e me n g i n e e r i n ga n df o r m a lm e t h o d s t h em a i nr e s u l t st h a tt h ea u t h o ro b t a i n t e da r ea sf o l l o w s ：1 b a s e do nt h ei d e ao fs y s t e me n g i n e e r i n ga n dt h ep r e v i o u sp r e s e n t e dp r i n c i p l e s , w ep r e s e n ta n di l l u s t r a t e10c r y p t o g r a p h i cp r o t o c o le n g i n e e r i n gp r i n c i p l e si nt h r e eg r o u p s ：5c r y p t o g r a p h i cp r o t o c o ls e c u r i t yr e q u i r e m e n ta n a l y s i sp r i n c i p l e s ，4d e t a i l e dp r o t o c o ld e s i g np r i n c i p l e sa n d1p r o v a b l es e c u r i t yp r i n c i p l e c r y p t o g r a p h i cp r o t o c o le n g i n e e r i n gi san e wn o t i o ni n t r o d u c e di nt h i st h e s i sf o rc r y p t o g r a p h i cp r o t o c o ld e s i g n ，w h i c hi sd e r i v e df r o ms o f t w a r ee n g i n e e r i n gi d e a t h ei d e ai su s e f u li nt h a ti tc a ni n d i c a t ei m p l i c i ta s s u m p t i o n sb e h i n dc r y p t o g r a p h i cp r o t o c o ld e s i g n ，a n dp r e s e n to p e r a t i o n a lp r i n c i p l e so nu n c o v e r i n gt h e s es u b t l e t i e s 2 an o v e lf r e s h n e s sp r i n c i p l eb a s e do nt r u s t e df r e s h n e s sc o m p o n e n ti sp r e s e n t e d ：f o re a c hp a r t i c i p a n to fac r y p t o g r a p h i cp r o t o c o l ，t h es e c u r i t yo ft h ep r o t o c o ld e p e n d so n l yo nt h es e n to rr e c e i v e do n e w a yt r a n s f o r m a t i o no fam e s s a g e ，w h i c hi n c l u d e sc e r t a i nt r u s t e df r e s h n e s sc o m p o n e n t t h ef r e s h n e s sp r i n c i p l ei n d i c a t e sa ne f f i c i e n ta n de a s ym e t h o dt oa n a l y z et h es e c u r i t yo fc r y p t o g r a p h i cp r o t o c o l sa n dt h ea n a l y s i sr e s u l t so f2 0c l a s s i c a lc r y p t o g r a p h i cp r o t o c o l sa l ei l l u s t r a t e dw h i l e12p o s s i b l ea t t a c k so rf l a w sa r en e w t h ef r e s h n e s sp r i n c i p l eh a sf o l l o w i n gc h a r a c t e r i s t i c ：i tc o u l de f f i c i e n t l yd i s t i n g u i s ht h ef r e s h n e s so ft h em e s s a g e st oa v o i dr e p l a ya t t a c k sa n di n t e r l e a v i n ga t t a c k se t c ，a n dt h ea n a l y s i sp r o c e d u r ei si n d e p e n d e n to ft h ec o n c r e t ef o r m a l i z a t i o no ft h ep r o t o c o lc o n c u r r e n tr u n sa n dt h ea d v e r s a r y s p o s s i b l eb e h a v i o r s t h es e c u r i t ya n a l y s i sr e s u l t sb a s e do nt h ef r e s h n e s sp r i n c i p l ec a ne i t h e re s t a b l i s ht h ec o r r e c t n e s so ft h ep r o t o c o lw h e ni t i si nf a c tc o r r e c t , o ri d e n t i f yt h ea b s e n c eo ft h es e c u r i t yp r o p e r t i e sa n dt h es t r u c t u r et oc o n s t r u c ta t t a c k sb a s e do nt h ea b s e n c e 3 b a s e do nt h ef r e s h n e s sp r i n c i p l e ，ab e l i e fm u l t i s e t sf o r m a l i s mi sp r e s e n t e d w eh a v es h o w nt h ee f f i c i e n c y ，r i g o r o u s n e s s ，a u t o m a t i o np o s s i b i l i t yo ft h eb e l i e fm u l t i s e t sf o r m a l i s mb yi l l u s t r a t i n gi tv i at h en e e d h a m - s c h r o e d e rp u b l i ck e yp r o t o c 0 1 w i t ht h eo p e nm e d i u mt r a n s m i s s i o na n dp a c k al o s sc o n s i d e r a t i o n si nm i n d ，w ep r e s e n ta ne x t e n s i b l eb e l i e f m u l t i s e t sf o r m a l i s mi n c l u d i n gd o s t o l e r a n tp r o p e r t ya n dc o n s i s t e n c yl ip r o p e r t ya n a l y s i st h a ti ss u i t a b l ef o rw i r e l e s sp r o t o c o la n a l y s i s s e c u r i t yg o a l sa r ep r e s e n t e da c c u r a t e l y ，w h i c ha r ep r o v e dn o to n l yn e c e s s a r yb u ta l s os u b s t a n t i a lt og u a r a n t e et h es e c u r i t ya d e q u a c yo ft h ec r y p t o g r a p h i cp r o t o c o l st o4s e c u r i t yd e f i n i t i o n su n d e rt h ec o m p u t a t i o n a lm o d e l t h e s e4d e f i n i i t o n sa r ep r e s e n t e db a s e do nm a t c h i n gc o n v e r s a t i o nd e f i n i t i o na n di n d i s t i n g u i s h a b i l i t ys e c u r i t yd e f i n i t i o n ag e n e r a lm o d e lf o ra u t o m a t i o no ft h eb e l i e fm u l t i s e t sf o m a l i s mi sp r e s e n t e d v i at h ec o m p a r i s o no fo u rt w op a r t i a li m p l e m e n t a t i o n so ft h ea u t o m a t i o no ft h eb e l i e fm u l t i s e t sf o m a l i s mu n d e rt h ed i f f e r e n td e v e l o p m e n te n v i r o n m e n t s ，ad e t a i li m p l e m e n t a t i o na p p r o a c hi sd e t e r m i n e d t h ed e v e l o p i n ga u t o m a t i o no ft h eb e l i e fm u l t i s e t sf o m a l i s mh a ss u c c e s s f u l l ya n a l y z e ds e v e r a ic r y p t o g r a p h i cp r o t o c o l s b a s e do nt h ef r e s h n e s sp r i n c i p l ea n dt h et r e a t m e n to ft h ed i s t r i b u t e dl o g i ct i m ec a u s a lc o n s i s t e n c y ，am o d e lf o rd e s i g n i n gc r y p t o g r a p h i cp r o t o c o l si sa l s op r o p o s e d w ee x e m p l i f yt h eu s a b i l i t yo ft h em o d e lv i ar e d e s i g n i n gt h en e e d h a m s c h r o e d e rp u b l i c k e yp r o t o c o l ，a n dp r o v et h a tt h er e c o n s t r u c t e dc h a l l e n g e r e s p o n s ek e ye x c h a n g ep r o t o c o la c h i e v e st h el o w e rb o u n d so ft h r e em e s s a g e sa n dt h r e er o u n d s 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 ，p r o t o c o la n a l y s i s ，p r o t o c o ld e s i g n ，i n f o r m a lm e t h o d s ，f o r m a l i s m ，a u t o m a t i o n 1 n -毛i&学位论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：孰日期：三嗯年，口月彤日学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。保密口，在年解密后适用本授权书。本学位论文属于不保密口。( 请在以上方框内打“、”)学位论文作者签名：指导教师签名：他叫1 7日期：工吣年，a 月1 6e 1日期：勘好，o 月lb 日第一章绪论随着信息化在政府、军事以及电子商务应用中的不断深入，信息安全已成为全社会的共同需求。在计算机通信网或分布式系统中，常常通过密码协议( c r y p t o g r a p h i cp r o t o c 0 1 ) 实现安全共享网络资源的目标。密码协议，也称为安全协议( s e c u r i t yp r o t o c 0 1 ) ，是建立在密码体s t 4 ( c r y p t o g r a p h i cm e c h 卸i s m ) 基础上的一种交互通信协议【1 1 ，指两个或多个协议参与者采取约定的规程方式交换消息，并采用某种密码算法( c r y p t o g r a p h i ca l g o r i t h m ) j j l ：l 密交换的消息或消息中的某些部分，以保证实现预定的安全目标( s e c u r i t yo b j e c t i v e ) t 2 ”。1 1 密码协议的安全目标安全目标是指密码协议运行完成时需要满足的一些安全性质，安全目标的集合构成密码协议的安全属性( s e c u r i t yp r o p e r t y ) 。这些安全性质包括1 2 - 4 1 ：( 1 ) 保密性( s e c r e c y )保密性( 机密性) ，指密码协议的两个或多个协议参与者交换的是对重要信息由明文形式加密得到的密文，不会泄露给非授权拥有该机密信息的其它参与者。( 2 ) 认证性( a u t h e n t i c i t y )认证性( 真实性) ，指密码协议的两个或多个协议参与者通过协议运行实现参与主体身份的确认、或者消息来源的确认，即身份认证和消息认证( 数据源认证) 身份认证是信息安全的第一道防线，是最基本的安全服务，在安全系统中的地位极其重要。( 3 ) 完整性( i n t e g r i t y )完整性，指密码协议运行中交换的消息不会被非法删除、改变和替代。在某种意义上，完整性是协议正确运行的前提，即每一步正常协议动作的执行都隐含着消息的完整性。( 4 ) 不可否认性( n o n r e p u d i a t i o n )不可否认性( 抗抵赖性) ，指密码协议的两个或多个协议参与者能够向第三方提供对方参与协议运行的证据。不可否认性是电子商务协议的一条重要安全性质。( 5 ) 公平性( f a i r n e s s )公平性，指在密码协议运行完成后，协议的任何一方都有充分的证据以解决今后可能出现的纠纷，且在协议运行的任何阶段，参与协议运行的任何诚实参与者都不处于劣势。它包括执行的公平性、获得的公平性和追述的公平性【5 j 。其中，保密性和认证性是其它安全属性的基础。第一章绪论1 2 密码协议的分类按照安全目标的不同，网络通信中常用的密码协议大致可以分为以下四类：认证协议、认证的密钥建立协议、电子商务协议以及安全多方计算协议2 。4 ，1 6 , 8 引。( 1 ) 认证协议( a u t h e n t i c a t i o np r o t o c 0 1 )认证协议是以认证为目标的密码协议。认证的目的往往是为了在参与者之间安全地分配密钥或者协商密钥，以及共享各种秘密。常见的认证协议如w o o - l a m 协议 6 1 、基于零知衫 的身份识别协议【7 1 和o k a m o t o 协议【8 1 等。( 2 ) 认证的密钥建立协议( a u t h e n t i c a t e dk e y e s t a b l i s h m e n tp r o t o c 0 1 )认证的密钥建立协议，也称为认证密钥协议，为参与协议运行的两个或多个参与者完成身份认证并建立一个新的会话密钥，它是网络通信中应用最普遍的一种密码协议。新的会话密钥用于建立安全通道，实现后继的应用层上的数据安全通信。常见的认证密钥协议包括n e e d h a m s c h r o e d e r 公钥认证协议【9 】、i k e ( i n t e m e tk e ye x c h a n g e )协议【1 0 1 、k e r b o r o s 认证协议1 、x 5 0 9 协议坦1 、分布式认证安全服务( d a s s ，d i s t r i b u t e da u t h e n t i c a t i o ns e c u r i t ys e r v i c e ) 协议州等。( 3 ) 电子商务协议电子商务协议为参与协议运行的两个或多个参与者实现网上交易的功能。电子商务协议关注的是公平性和不可否认性。常见的电子商务协议有s e t ( s e c u r ee l e c t r o n i ct r a n s a c t i o n ) 协议【1 4 】和i k p ( i n t e m e tk e y e dp a y m e n t s ) 协议等。( 4 ) 安全多方计算协议安全多方计算协议用于保证分布式环境中各参与方以安全的方式来共同执行分布式计算的任务【1 6 1 。常见的安全多方计算协议有组密钥协商协议、分布式环境下的多方身份认证协议、网上选举、电子投标、电子现金等。本文的主要研究对象是认证和认证的密钥建立协议的安全性。1 3 课题研究背景密码协议的设计非常微妙，许多密码协议在公布甚至实际应用多年之后才被发现存在漏洞【l - 2 ，1 7 之1 。例如，一个最为著名的早期密码协议一一1 9 7 8 年公布的n e e d h a m s c h r o e d e r 认证协议【9 j ，在它发布的1 7 年后被发现存在漏洲1 。7 1 。经验告诉我们，设计和分析一个正确的密码协议是一项十分困难的任纠。2 ，协2 2 1 ，密码协议设计和分析在基础理论和工程技术两个层面向科技工作者提出了大量的挑战性研究课题。1 、密码协议非形式化方法的研究通过对大量有代表性密码协议的共同特性进行分析，可以提取一些有益而直观的上海交通人学博士学位论文密码协议非形式化设计准则【协川。坚持这些准则不仅能尽量避免协议漏洞，而且能简化协议设计。最有代表性的设计准则是a b a d i 等提出的密码协议谨慎工程原则1 2 叭。但现有的密码协议设计和分析方法类似早期的软件开发和测试，还没有引入系统工程的思想，形成密码协议工程的方法。借鉴软件工程的思想，改进著名的a b a d i 密码协议谨慎工程原则中的不足，寻找密码协议设计的协议工程原则是本文的研究内容之一。2 、密码协议安全验证机理及形式化验证的研究形式化描述比用自然语言的定义要精细得多。人们常常借助形式化方法对密码协议进行设计和分析【2 引。最早提出密码协议形式化分析思想的是n e e d h a m 和s c h r o e d e r ，但真正在这一领域做出开创性工作的是d o l e v 和y a o ，他们提出了多协议并行执行环境的d o l e v y a o 形式化模型2 6 】。此后的协议形式化分析模型大多基于该模型或其变体。目前，研究比较深入和广泛的形式化方法主要有以下几种1 2 j ：基于逻辑推理的分析方法1 2 7 - 3 2 、基于计算模型的分析方法【3 3 - 3 6 1 、基于模型检验的分析方法【3 7 删和基于定理证明的分析方法降弱j 。基于逻辑推理的分析方法以b a n 逻蚓2 7 】为代表，常常用于推理密码协议的认证性。b a n 逻辑简单实片j ，自推出后取得了巨大的成功。但是，由于b a n 逻辑抽象程度过高，缺乏必要的语义基础，因此，b a n 逻辑有时不能提供令人信服的安全性证明【8 8 1 。如，b a n 逻辑证明n e e d h a m s c h r o e d e r 公钥认证协议是安全的，但l o w 却发现了针对该协议的攻击。计算模型下可证明安全的思想，源自g o l d w a s s e r 和m i c a l i的开创性研究【3 3 1 ，b e l l a r e 和r o g a w a y 最先使用计算模型方法证明认证和认证的密钥建立协议的安全性【弘3 5 】。用数学方法分析协议，在某种程度上要求协议设计者和分析者采取正确的或者更精确的密码学技- 术【1 2 ，弭3 5 】。基于模型检验的分析方法是基于状态搜索的方法【3 7 - 4 3 1 ，与攻击者能力的具体描述密切相关。基于模型检验的分析方法常常用于推证密码协议的不安全性，而不是用于密码协议的安全性证明。基于定理证明的分析方法最著名的是s t r a n ds p a c e 的方法【4 5 郑】和认证测试的方法1 4 9 1 。基于定理证明的分析方法要解决密码协议的可验证性问题，并建立验证密码协议系统多个安全属性的统一分析模型。最为重要的是，由于安全验证机理的不同，已有的形式化方法有的在判断消息是否新鲜时存在缺陷，如b a n 逻辑的消息含义规则，无法防止类似重放和混淆的攻击1 8 8 1 ；有的形式化方法的分析过程是多协议运行环境、攻击者能力的具体形式化描述相关的，而多协议运行环境下攻击者能力是一个不断发展的可变量。对密码协议的安全验证机理进行研究，基于提出的安全验证机理给出密码协议分析和设计的形式化模型，安全性证明以及自动化实现，是本文的研究重点。第一章绪论该课题属密码协议设计和验证领域的基础性研究，本论文的研究受国家8 6 3 计划项目2 0 0 6 a a 01z 4 2 2 、博士点专项科研基金项目2 0 0 5 0 2 4 8 0 4 3 以及现代通信国家重点实验室基金514 3 6 0 4 0 4 0 5 j w 0 3 0 4 的资助。1 4 论文组织论文共分八章，主要涉及五个研究部分：密码协议非形式化分析部分；密码协议安全验证机理；密码协议的形式化分析；形式化分析方法的自动实现；密码协议的形式化设计。具体组织如下：第一章绪论介绍了论文的研究背景、研究内容以及总体框架。第二章密码协议工程原则与非形式化分析介绍了密码协议安全性分析所涉及的一些基础密码理论；指出了a b a d i 的密码协议谨慎工程原则的局限性；借鉴软件工程的思想，结合前人的研究成果，给出了安全协议设计的1 0 条密码协议工程原则。第三章密码协议安全验证机理介绍了计算模型下认证性和保密性的可证明安全定义，给出了该模型下的4 个可证安全定义以满足不同的安全需求；提出了基于信任的新鲜性标识符分析密码协议的安全性，给出了新鲜性原则；应用新鲜性原则分析了1 5 个经典密码协议的安全性，明确指出了不安全密码协议存在的安全隐患以及由安全属性缺失构造攻击的结构。第四章基于信任多集的形式化分析方法比较了已有形式化分析方法的特点，着重介绍了b a n 逻辑的验证机理：提出了基于新鲜性思想的信任多集形式化分析方法，以n e e d h a m s c h r o e d e r 公钥认证协议为例，说明了信任多集方法的有效性；证明了保证认证协议安全的充分必要条件，这些条件在计算模型下分别满足基于匹配对话和不可区分性的4 个可证安全定义。第五章基于信任多集的自动化分析比较了已有自动化分析方法的特点，提出了信任多集自动分析工具的总体框架，通过在2 种不同开发环境下信任多集自动分析工具初步实现的比较，给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。第六章基于信任多集的形式化设计方法比较了已有形式化设计方法的特点；基于新鲜性原则和冈果一致性的分布式逻辑上海交通大学博士学位论文时间，建立了信任多集形式化设计方法；以构造n e e d h a m s c h r o e d e r 公钥认证协议为例，说明了该设计方法；介绍了评价认证密钥协议效率的2 个指标，并证明了构造的协议达到了消息数和轮数的下限。第七章信任多集方法在无线通信环境的应用扩展了信任多集形式化分析方法，应用扩展的方法对i e e e8 0 2 1 1 i 的4 次握手协议和组密钥握手协议、传感器网络环境下一个基于k e r b e r o s 的对密钥管理方案等无线网络安全协议进行了分析。第八章总结与展望总结本文的工作，并对今后的研究方向做了简要的介绍。第二章密码协议工程原则与非形式化分析密码协议的安全性不仅取决于所选定的密码算法，还取决于协议的设计、应用环境等因素。即使设计者在头脑中对要使用的密码算法有清楚的认识，但由于对密码算法的不同使用方式，所能达到的安全强度就完全不同。由于通信的异步特性，一个简单的只有几条消息的通信过程，却可能在协议设计中引入了许多隐含的假设抛。隐含假设可以包括密码协议的强度需求，应用环境需求，上下文是否隐含主体信息等，这些都可能导致系统漏洞的产生。通过对大量有代表性协议的共同特性进行分析，对已有的攻击实例进行研究，密码协议的非形式化分析方法常常提取一些有益而直观的密码协议设计准则【1 9 - 2 4 】，帮助研究人员查找协议漏洞，简化协议设计。非形式化分析方法的优势在于，能够抓住协议的语义，快速发现协议中的缺点，有助于人们对协议的理解，同时也是形式化方法的基础。但是，现有的非形式化分析方法类似早期的软件开发和测试，没有引入系统- t 程的思想。借鉴软件工程的思想，结合前人的研究成果，将密码协议设计看作一个系统工程，本文给出了l o 条密码协议工程原则。2 1 基础理论2 1 1 基础知识2 1 1 1 常用的密码体制对称钥体制：加密和解密密钥相同，加解密效率高，适于对大量数据进行加解密操作。但存在数据交换之前的密钥交换问题。非对称钥体制：又叫公钥体制，每一用户有一对密钥即公钥和私钥，但加解密的效率低。公钥是公开的，多个用户使用公钥加密的消息只能由该用户用私钥解密，但用户用私钥加密的消息可被多个用户解读，因而能实现对用户身份的认证。数字签名：用来确保数据真实性和完整性，是实现网络应用中身份认证、数据完整性保护和不可否认性的基础。哈希函数：是确定的算法，能将任意长度的输入数据映射成某种固定长度输出数据( 哈希值) 的函数。哈希函数的单向性指从哈希值不能反向推导出消息本身。在共享密钥情况下，密钥哈希函数将密钥作为输入的一部分，另一部分为需要认证的消息。哈希函数的混合变换性质：对于任意的输入，输出的哈希值在函数输出空间上是均匀分布的，这点在计算上是不可区分的。上海交通大学博士学位论文随机预言机：对于任意的输入，输出的哈希值在函数输出空间上是均匀分布的。消息认证码m a c ( m e s s a g ea u t h e n t i c a t i o nc o d e ) ：由对称技术生成的消息检测码m d c ( m a n i p u l a t i o nd e t e c t i o nc o d e ) 。实现m a c 常用密钥哈希甬数技术，也可以使用分组密码加密算法。h m a c = h ( 纠m l k ) ，密钥七要认证消息的前缀和后缀，可以阻止攻击者利用某些哈希函数的轮函数迭代结构来修改消息。2 1 1 2 基本概念主体：通信的合法参与者，是概率多项式时间机器。攻击者也可以是系统的合法用户，拥有自己的加密密钥和解密密钥。攻击者：企图通过协议运行获得不该知道的秘密的参与者。消息：通信过程中在网络卜传输的数据。通信协议：两个或多个主体通过一系列规定的步骤来完成某项通信任务。消息驱动通信协议：某一方触发一次消息请求来执行协议的一个副本，随后两方或互相协作的多方按照约定处理接收的消息，生成并返回消息给另一方，等待新消息的到来，或者拒绝执行协议甚至结束协议。消息驱动协议具有异步的特钳5 1 l 。会话：主体中运行的某个协议副本，由主体标识符、通信对方标识符和一个会话标识符唯一确定。一个主体可以同时运行多个协议或一个协议的多个实例。新鲜性标识符：为协议的某次运行产生的一个唯一的标识符，可以是随机数( n o n c e ) 、时间戳( t i m e s t a m p ) 、新会话密钥、或生成新会话密钥的组成部分。我们平常所说的随机数是通过确定的密码算法产生的，是伪随机数，但产生的数列能通过各种随机性检验，具有随机性和不可预测性。时问戳需要各认证实体之间严格保持一个同步时钟，但对于分布式网络环境是十分网难的。密码协议的安全性：如果攻击者不能从密码协议的运行中获得比协议自身所体现的更多的有用信息，则称该协议是安全的【2 1 。协议的安全性分析：研究密码协议是否能达到预定的安全目标。对于密码学系统，计算模型下的可证明安全性是对一个系统抗攻击能力的一种肯定量度，度量的内容包括成功概率和计算代价。2 1 1 3 密码协议的其他分类方法按密钥的产生方式1 2 】：( 1 ) 密钥传输协议：协议输出的会话密钥来自于参与协议的某一个主体。( 2 ) 密钥协商协议：协议输出的会话密钥是某个函数的输出，且该函数的输入是协议所有参与者的随机输入。按消息的新鲜性方式来分i z j ：第二章密码协议工程原则与非形式化分析( 1 ) 随机数机制的密码协议：又称询问一应答机$ l j ( c h a l l e n g e r e s p o n s em e c h a n i s m )协议。协议某一方主体发出一个包含了随机数( c h a l l e n g e ) l 拘消息，该合成消息涉及了响应者所对应的密码操作，发起者根据响应( r e s p o n s e ) q b 所含的随机数来断定消息的新鲜性。( 2 ) 时间戮机制的密码协议：密码协议中消息的新鲜性f n 时间戳来保证，时间戳机制的密码协议要求认证主体之问保持同步时钟。密码协议还有其他的分类方式。比如，按认证方式的不同来分：单方认证协议和双方认证协议；按采用的密码体制来分：公钥体制方法和对称钥体制方法：按是否有可信第三方：含可信第三方的密码协议和不含可信第三方的密码协议。2 1 2 计算模型下的安全性定义被动攻击：攻击者对协议的消息流进行观察、收集，并进行密码分析。被动攻击不影响协议的执行，但这种攻击难以检测，如网络线路的窃听。主动攻击：攻击者通过改变协议以获得额外的利益或破坏协议的执行。主动攻击者可以在协议执行中引入新的消息、删除消息、替换消息、重发消息、干扰信道、改变协议的执行流程或修改计算机中存储的数据，甚至假胃合法的参与者。计算模型下的安伞性定义如下所裂2 】：1 完全或无的安全性完全或无( a l l - o r n o t h i n g ) 的安全性：攻击者要么完全( a 1 1 ) 得到想要的秘密，要么什么也得不到( n o t h i n g ) 。这个概念不考虑攻击者的主动攻击，也不考虑攻击者能否通过极低的概率或者极高计算代价获得一些有关明文的有用信息。2 不可区分性选择明文攻击的安全性选择明文攻击c p a ( c h o s e np l a i n t e x ta t t a c k s ) ：攻击者选择明文消息并得到加密服务，产生相应的密文。攻击者试图利用得到的明一密文对来降低密码体制的安全性。在c p a 下，攻击者选择两条不同的消息所口、朋，发给攻击游戏中的预言机，预言机对攻击者选择的明文进行加密，得到 m o k 、 m l k 并发送给攻击者。不可区分性选择明文攻击的安全性i n d c p a l 3 3 1 ( i n d i s t i n g u i s h a b l ec h o s e np l a i n t e x ta t t a c k s ) ：又称语义安全性，密文不会向任何计算能力多项式有界的攻击者泄漏有关相应明文的任何信息。i n d c p a 下的安全性是指攻击者区分密文 m o n 掰， i 的概率只能是l 2 加一个关于k 的可忽略量。3 不可区分性选择密文攻击的安全性选择密文攻击c c a ( c h o s e nc i p h e r t e x ta t t a c k s ) ：攻击者除了在c p a 游戏中可获得的加密帮助外，进一步允许攻击者可在有限时间内访问解密机。攻击者选择密文消息，预言机把解密结果返回给攻击者，这被认为是为攻击者提供的分析训练课程。在上海交通人学博士学位论文解密服务停止后( 即在得到解密目标密文后，解密服务立即停止) ，如果攻击者能够从目标密文中得到保密明文的信息，则说攻击是成功的。不可区分选择密文攻击的安全性i n d - c c a p 副( i n d i s t i n g u i s h a b l ec h o s e nc i p h e n e x ta t t a c k s ) ：攻击者和预言机进行c p a 中的游戏，在c c a 下获得攻击者满意的分析训练课程后，攻击者区分密文 m o ) i 、 m l t 的概率只能是l 2 加一个关于k 的可忽略量。4 不可区分适应性选择密文攻击的安全性适应性选择密文攻击c c a 2 | 3 3 ( a d a p t i v ec h o s e nc i p h e r t e x ta t t a c k s ) ：攻击者除了在c c a 游戏中获得的加、解密帮助外，还能根据解密预言机返回的解密信息来适应性的构造下一个密文( 解密目标密文除外) ，并再提交解密预言机进行解密。即除了对目标密文解密外，攻击者永远能够得到解密服务。不可区分适应性选择密文攻击的安全性i n d c c a 2 t 玎1 ( a d a p t i v ei n d i s t i n g u i s h a b l ec h o s e nc i p h e r t e x ta t t a c k s ) ：攻击者和预言机进行c p a 中的游戏，在c c a 2 下获得攻击者满意的分析训练课程后，攻击者区分密文 所o h 、 掰， t 的概率只能是l 2 加一个关于k 的可忽略量。如今，i n d c c a 2 已经成为公钥密码体制的标准，所有普通用途的新公钥加密方案必须具备i n d c c a 2 的安全性，才是实用的公钥密码体制。基于不可区分性的安全性定义是一种判定性的安全性定义，而不可展的安全性从计算的方面加强了密码体制的安全性定义。不可展密码学【6 引( n o n m a l l e a b l ec r y p t o g r a p h y ) 的安全性要求使得攻击者很难通过修改密文达到对明文的有效修改。但是，由于不可展问题的计算本质，对它们进行形式化处理非常困难o 因此，设计一个密码体制并证实它具有不可展安全性也非常用难。值得欣慰的是，研究人员建立了许多不可展安全性和不可区分性安全性之间的重要关系【2 1 ：假设a t k 表示c p a 、c c a 、c c a 2 ，如果一个公钥密码体制是n m a t k 安全的，那么它也一定是i n d a t k 安全的；公钥密码体制是n m c c a 2 安全的当且仅当它是i n d c c a 2 安全的。因为人们已经很好地建立了对i n d c c a 2 的形式化处理，所以，研究人员可以通过证明i n d - c c a 2 下的安全性获得在n m c c a 2 模式下的安全性证呼2 1 。这使得协议设计者可以基于不可区分性对密码协议进行研究，而获得强的不可展的安全性。2 1 3 协议分析的前提假设l 、关于密码体制的假设现代密码学基于计算复杂性理论建立。如果算法的执行时间是多项式时间，则称该算法是多项式时间算法或有效算法，而把找不到有效算法的问题称为难解问题。许多密码学算法就是基于大整数分解、离散对数等难解问题建立的1 2 j 。密码学算法是基于计算复杂性理论中的难解问题建立的，为网络上传递的消息提第二二章密码协议工程原则与非形式化分析供高强度的加解密操作和其他辅助算法( 如哈希函数等) 。本文的研究对象是在不考虑密码算法安全性被攻破的情况下，分析密码协议逻辑设计上的安全性。假设密码协议中所采用的特定密码学算法在特定的安全性定义( 完全或无安全的、或者i n d c p a 安全的、或者i n d c c a 安全的，或者i n d c c a 2 安全的) 下是强健和不可攻破的，这也是目前几乎所有的密码协议分析理论和方法都遵从的密码协议建模和分析原则。2 、对接收消息的假设通信参与者接收到的信息只应理解为_ 个比特串，该比特串是甭为消息，还需作进一步的判别。假设每个主体可分辨出消息的语句结构，有对基本消息的辨别能力。3 、对参与者的假设合法参与者严格按照协议规定参与协议运行。4 、对攻击者的假设d o l e v y a o 攻击者是一个概率多项式时间机器，运行在多协议并行执行环境d o l e v y a o 模型t 2 6 r f _ l ，攻击者对通信链路具有完全的控制能力。除此之外，我们允许攻击者使用加密或解密分析训练课程提升攻击能力，出于简洁的考虑，本文仍将具有上述攻击能力的所有攻击者简称为在d o l e v y a o 模型下的攻击者，。5 、对加解密操作的假设消息语句中含有的加、解密运算符可以互相抵消，即消息语句满足重写规则。6 、关于公钥及对称钥体制中长期密钥的获取在公钥体制下，假设密码协议参与者的公钥和私钥已经通过认证通道或者传统的方式分发完成即所有主体包括攻击者拥有自己的私钥和全部参与者的公钥。在对称钥体制下，假设密码协议参与者的长期共