（应用数学专业论文）基于广义串空间模型的密码协议设计与分析的研究.pdf

信息f 稃人学硕十学位论文 摘要 本文主要研究了d o l e v y a o 模型中的攻击者模型、基于广义串空问模型的构造攻击以 及密码协议的设计，共三部分。第一部分，d o l e v y a o 模型的扩展及应用；第二步部分， 推广基于广义串空日j 模型的构造攻击；第三部分，应用推广的构造攻击方法指导密码协议 的设计。 第一部分取得的结果如下： 通过对串空日j 理论和模型进行扩展，使其充分表达较多的密码学原语，以满足分析复 杂密码协议的需要；对d o l e v y a o 模型中的攻击者串轨迹增加了主动签名、主动签名验证、 被动签名，钥控散列函数以及产生新鲜随机值等模型；重新定义了理想概念并对衍生出的 相关命题和定理进行了证明；以t l s 协议为例，利用扩展的串空间模型与理论分析，发现 了个攻击，为了避免此类攻击的发生，提出了设计密码协议时应注意的事项。 第二部分取得的结果如下： 以n e e d h a m s c h r o d e r 协议为例，说明了基于广义串空f 日j 模型的构造攻击的使用方法； 在使用这种构造攻击方法分析n e e d h a m s c h r o d e r 协议的过程中，虽然发现了众所周知的中 | 日j 人攻击，却不能发现隐藏的类型错误攻击；因此基于广义串空日j 模型的构造攻击是有缺 陷的，仔细分析了这种构造攻击，找到了它的弊端，给出了修讵措施；为了验证修币过的 基于广义串空日j 模型构造攻击的有效性，提出了一个类似于m i u e n 曾经设计的“堍g ”协议 “f 龟g 协议，它们具有共同的密码学性质( m i l l e n 曾使用p a u l s o n 的归纳法证明了“堍雪 协议是安全的) ；修正过的基于广义串空间模型的构造攻击在寻找密码协议的缺陷方面比 p a u l s o n 的归纳法更有效，事实上，修丁f 过的基于广义串空间模型的构造攻击证明了“f 埯矿” 协议是不安全的，存在着并行攻击缺陷，且易证明“f f g g 协议也是不安全的。 第三部分取得的结果如下： 总结了设计密码协议时应该遵循的基本原则。以n e e d h a m s c h r o e d e r - l o w e 协议为例， 说明了如何应用改进的基于广义串空日j 模型构造攻击来指导密码协议的设计；根掘这种方 法提出了设计密码协议时应该遵循的一般过程。 关键词：密码协议广义串空间模型构造攻击d o l e v - y a o 模型 第页 信息i 科人学硕十学何论文 a b s t r a c t n i sd i s s e r t a t i o nm a i n l ys t u d i e sa t t a c k e ro f d o l e v y a om o d e i 、c o n s t r u c t i n ga t t a c kb a s e do n g e n e r a l i z e ds t r a n ds p a c em o d e la n dd e s i g no fc r y p t o g r a p h i cp r o t o c o l s ，a n dt o g e t h e r , o u rr e s e a r c h f o c u s e so nt h r e ep a r t s t h ef i r s tp a r ti se x t e n s i o n st od o l e v - y a om o d e la n di t sa p p l i c a t i o n s ；t h e s e c o n dp a r ti sg e n e r a l i z a t i o nt oc o n s t r u c t i n ga t t a c kb a s e do ng e n e r a l i z e ds t r a n ds p a c em o d e l ；t h e t h i r dp a r ti st oa p p l yg e n e r a l i z e dc o n s t r u c t i n ga t t a c km e t h o dt og u i d ed e s i g no fc r y p t o g r a p h i c p r o t o c o l s r e s e a c hr e s u l t so f t h ef i r s tp a r ti sa sf o l l o w s ： i ti sv e r yn e c e s s a r yt oe x t e n do r i g i n a lt h e o r yo fs t r a n ds p a c e ss ot h a ti tc a nb ea p p l i e dt o a n a n l y z er e a lw o r l dp r o t o c o l s ；1 1 1 ep e n e t r a t o r 。ss t r a n d sa r ee x t e n d e dt h r o u g ha d d i n gi n i t i a t i v e s i g n a t u r e 、i n i t i a t i v es i g n a t u r ev e r f i c a t i o n 、h m a c ( k e y e d - h a s h i n gf o rm e s s a g ea u t h e n t i c a t i o n c o d e ) a n dg e n e r a t i n gf l e s hr a n d o mv a l u et r a c e st od o l e v y a om o d e l ；an e wn o t i o no fi d e a li s d e f i n e da n dt h er e l e v a n tp r o p o s i t i o n so rt h e o r e m sa r et h e r e f o r em o d i f i e da n dp r o v e d ；1 酞i n gt l s p r o t o c o lf o re x a m p l e ，s t r a n ds p a c em o d e la n dt h e o r ye x t e n d e da r eu s e dt of i n da na t t a c k i no r d e r t oa v o i dt h ek i n do fa t t a c k ，ap i e c eo fs t r a t e g yt ob ep a i da t t e n t i o nt oi sp u tf o r w a r dw h e n c r y p t o g r a p h i cp r o t o c o l sa r ed e s i g n e d r e s e a c hr e s u l t so f t h es e c o n dp a r ti sa sf o l l o w s ： t a k i n gn e e d h a m - s c h r o e d e rp r o t o c o lf o re x a m p l e ，u s a g eo fc o n s t r u c t i n g a t t a c ki s i l l u m i n a t e db a s e do ng e n e r a l i z e ds t r a n ds p a c em o d e l ；d u r i n ga n a n l y z i n gn e e d h a m s c h r o e d e r p r o t o c o lu s i n gt h i sm e t h o d ，t h o u g ht h ek n o w nm i d d l e - i n - m a na t t a c k i sf o u n d ，t h eh i d d e n t y p e f l a wa t t a c kc a nn o tb ef o u n d ；s o ，f l a w sl i ei nc o n s t r u c t i n ga t t a c kb a s e do ng e n e r a l i z e ds t r a n d s p a c em o d e l a f t e rt h i sm e t h o di sa n a n l y z e dc a r e f u l l y ，t h ef l a w sa r ef o u n do u t ，a n dc o r r e s p o n d i n g a r n e n d a t o r ym e a s u r e sa r eb r o u g h tf o r w a r d ；i no r d e rt ov e r i f ya m e n d a t o r yc o n s t r u c t i n ga t t a c k b a s e do ng e n e r a l i z e ds t r a n ds p a c em o d e ie f f e c t i v e a l la r t i f i c i a lp r o t o c o li sp u tf o r w a r d ，w h i c hi s s i m i l a rt o f f g g ”p r o t o c o lc o n s t r u c t e db ym i l l e n ，t h a ti st os a y ，t h et w op r o t o c o l sh a v e c r y p t o g r a p h i cp r o p e r t yi nc o m m o n ( a f t e r “堍g ”p r o t o c o li sa n a n l y z e db ym i l l e nu s i n gp u l s o n s i n d u c t i v ea p p r o a c h ，i ti ss e c u r e ) ；a m e n d a t o r yc o n s t r u c t i n ga t t a c ki sm o r ee f f e c t i v et h a np u l s o n si n d u c t i v ea p p r o a c hi nf i n d i n gf l a w so fc r y p t o g r a p h i cp r o t o c o l s i nf a c t ，i ti sn o ts e c u r e ，a f t e r f f g g ”p r o t o c o li sa n a l y z e db yu s i n gt h ea m e n d a t o r yc o n s t r u c t i n ga t t a c km e t h o db a s e do n g e n e r a l i z e ds t r a n ds p a c em o d e l ，a n dt h e r ei sap a r a l l e la t t a c ki n “魄g “p r o t o c 0 1 m o r e o v e r , i ti s e a s i l yp r o v e dt h a t “堍g p r o t o c o li sn o t8 e 4 ：u r eb yu s i n gh ea m e n d a t o r yc o n s t r u c t i n ga t t a c k m e t h o d r e s e a e hr e s u l t so f t h et h i r dp a r ti sa sf o l l o w s ： f u n d a m e n t a lp r i n c i p l ei ss u m m a r i z e dw h i e hi sf o l l o w e dw h e nw ed e s i g nc r y p t o g r a p h i c p r o t o c o l s t a k i n gn e e d h a m - s c h r o e d e r - l o w ef o re x a m p l e t h i sd i s s e r t a t i o ne x p l a i n st oh o wt o a p p l ya m e n d a t o r yc o n s t r u c t i n ga t t a c kb a s e do ng e n e r a l i z e ds t r a n ds p a c em o d e lt og u i d ed e s i g n o f c r y p t o g r a p h i cp r o t o c o l s ，a n dp u tf o r w a r dg e n e r a lc o u r s ew es h o u l df o l l o ww h e nc r y p t o g r a p h i c p r o t o c o l sa r ed e s i g n e da c c o r d i n gt ot h i sa m e n d a t o r ym e t h o d k e y w o r d s ：c r y p t o g r a p h i cp r o t o c o l g e n e r a l i z e ds t r a n ds p a c em o d e l c o n s t r u c t i n g a t t a c kd o l e v - y a om o d e i 第1 v 页 论文原创性声明和使用授权 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及 取得的研究成果。尽我所知，除了本文中特别加以标注和致谢中所罗列 的内容外，论文中不包含其它人已经发表或撰写过的研究成果；也不包 含为获得信息工程大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确 的说明并表示了谢意。 本人完全了解信息工程大学电子技术学院有关保留和使用学位论 文的规定，即：学院有权保留论文的复印件，允许查阅和借阅论文；可 以公布论文的全部或部分内容；可以采用影印、缩印或其它手段保存论 文。涉密论文按保密规定执行。本论文取得的研究成果归学院所有，学 院对该研究成果享有处置权。 枞签名：张氟 导师签名： 穸 铭 、d j 嘭 k 瓤 瓤 口九y， 信息￥人学硕+ 学位论文 第一章绪论 1 1 引言 随着互联网技术及应用的飞速发展，人们对网络通信的安全要求越束越高，这主要包 括通信各方的相互身份认证、消息源认证、访闯控制、信息保密、信息完整性、不可否认 性等各种安全要求。达到这些安全要求的一些传统手段已经不适应当的网络的环境，如： 早期的物理隔离的方法以及在一个控制台或是通过安全连接的环境中基于用户名n 令的 认证方式等。为了保证计算机网络通信的安全性，许多密码协议应运而生，通过运行这些 密码协议柬实现网络通信中通信各方的身份认证等安全要求。网络上的通信大都是从身份 认证的握手过程丌始的，所以身份认证是网络的第一道安全屏障，认证协议的目标实现与 否直接制约着网络的安全系数。按照b o y d 的观点，认证协议的目标分为内在目标( 身份认 证) 与外延目标( 建立会话密钥) i l l ，因此，认证协议的目的不仅仅单纯是一个身份认证的协 议，而且也是个建立会话密钥的协议，这根据用户的需求而定的。 密码协议是在不可靠或者敌意的通信环境下，保障一定安全特性的( 网络) 协议。在这 种环境中，敌手对于协议可以有各种各样的攻击手段，包括窃听、篡改、截断协议的通信， 甚至加入任何可能的消息，把协议的消息转向到其它接收者等等。因此，这些因素决定了 看似完美的协议，却存在着难以察觉的缺陷。 虽然密码协议的设计过程就那么几步，然而经过精心设计的协议往往存在一些微妙的 漏洞，这样检测协议的漏洞并加以改进就显得非常重要，从而引发了密码协议的安全设计 及安全性分析的浪潮。 1 2 密码协议的研究现状 1 2 1 密码协议的内涵1 2 i 在理解密码协议这一概念之静，首先要了解的是什么是协议。所谓协议，就是两个或 两个以上的参与者采取一系列步骤以完成某项特定的任务。这个定义包含三层意思： 协议至少需要两个参与者。一个人可以通过执行一系列的步骤来完成一项任务，但 它不构成协议： 在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤； 通过执行协议必须能够完成某项任务或达成某种共识。 第l 页 信息l 徉人学硕十学付论文 协议与算法的概念不尽相同。算法应用于协议中消息处理的环节。对不同的消息处理 方式则要求用不同的算法，而对算法的具体化则可定义出不同的协议类型。因此，可以简 单地说，密码协议就是在消息处理环节采用了若干密码算法的协议。具体而苦，密码算法 为传递的消息提供高强度的加解密操作和其它辅助算法( 如h a s h 函数) ，而密码协议是在这 些密码算法的基础上为各种安全性方面的需求提供实现方案。 密码协议的分析与普通协议的分析一个不同之处在于：普通的通信协议并不假设通信 系统之外有别的主体。因此，分析普通的通信协议主要着眼于协议的活性、保险性以及公 平性，这罩的公平性并非电子商务协议中要求的公平性，而是协议激活的公平性。而密码 协议则要针对一个额外的敌手，做出尽可能的防范。 密码协议是指建立在密码体制基础上的一种高互通协议，它运行在计算机网络或分布 式系统中，为安全需求的各方提供一系列步骤，借助于密码算法来达到密钥分配、身份认 证以及安全地完成电子交易等目的。 1 2 2 密码协议的形式模型 密码协议是使用密码算法且能够提供某种安全服务的协议，其协议模型就是如何形式 化地描述协议，根据文献【3 i ，可以将协议模型分为四类：基于知识演化系统的模型；基于 规则推理系统的模型：基于代数演算系统的模型；基于计算复杂性理论的模型。 基于知识演化系统的模型 这类模型把协议视为n 个主体组成的分布式系统的运行，系统本身已完全确定每个主 体所有可能的局部状态，而协议则规定了这些局部状态联合转移的所有方式。在迁移的过 程中，各个主体的知识集合不断发生演化。因此模型是通过协议对系统作用的结果来刎哂 协议的，也就是说，系统执行协议的行为的迹完全决定了协议。有代表性的是h a l p e m 模 型以及w o o l a m 模型。 基于规则推理系统的模型 这类模型的基本出发点是：构造一个证明系统，使协议的规则变成该系统的推理规则， 而协议要达到的目标被规范为该系统的推理决策问题或某些不变量。之后，借助于推理规 则证明这些不变量或决定决策问题是否有解。有代表性的是m i l l e n p a u l s o n 模型以及 d m t y 模型。 基于代数演算系统的模型 这类模型往往是根据协议先定义一个具有某些代数结构的系统，之后利用这些代数结 构及系统元素把协议描述为满足某些代数性质的代数对象。这类模型的一个共同点就是： 它们都独立地定义不关心运行环境的协议、攻击者利用环境进行攻击的能力及系统要达到 第2 页 信息i 拌人学硕十学何论文 的安全目标；在代数系统中精确定义协议的安全性，通常是把它定义为代数系统上的命题； 模型的任务之一就是通过代数运算把代表协议的代数对象与代表攻击者能力的代数对象 结合起来，形成代表在实际环境中运行的协议的代数对象。模型的另一个重要任务就是建 立一种推理机制利用代数性质证明代表在实际环境中的协议的代数对象满足描述安全目 标的命题。有代表性的是：d o l e v - y a o 模型与以d o l e v y a o 模型为基础的s t r a n ds p a c e 模型 以及c s p 模型。 计算复杂性理论的模型 这类模型一般都是借助计算复杂性理论，把理想状态下的协议用一簇二元随机变量描 述出来；再把实际状态下的协议用另一簇二元随机变量描述出来。之后，研究这两簇随机 变量的不可区分性。有代表性的是：c a n e t t i 模型。 1 2 3 密码协议的分类 根掘文献【2 】，常用的密码协议可以分为血类： ( 1 ) 密钥交换协议。该类协议用于完成会话密钥的建立。一般情况下是在参与协议的两 个或者多个实体之b j 建立共享的秘密，如用于一次通信中的会话密钥。协议中的密码算法 可采用对称密码体制，也可采用非对称密码体制。代表性的协议有：d i f f i e h e l l m a n 协议、 k e r b o r o s 协议等。 ( 2 ) 认证协议。该类协议包括实体认证( 身份认证) 协议、消息认证协议、数掘源认证协 议和数掘目的认证协议等，用来防止假冒、篡改、否认等攻击。 最令人瞩目的身份认证协议有两类：一类是1 9 8 4 年s h a m i r 提出的基于身份的身份认 证协议，另一类是1 9 8 6 年f i a t 等人提出的零知识身份认证协议。随后，人们在这两类方 案的基础上又提出了一系列实用的身份认证协议，如s c h n o r r 协议、o k a m o t o 协议、 g u i l l o u q u i s q u a t e r 协议、f c i g e f i a t - s h a m i r 协议等。 消息认证协议、数据源认证协议和数据目的认证协议可通过加密、数字签名等技术实 现，不过，也有很多相应的专用协议，如非否认协议。 ( 3 ) 认证密钥交换协议。 幺类协议将认证协议和密钥交换协议结合在一起，先对通信实 体的身份进行认证，在认证成功的基础上，为下一步安全通信分配所使用的会话密钥。 常见的认证密钥交换协议有互联网密钥交换( i k e ) 协议、分佰式认证安全服务( d a s s ) 协议、k e r b e r o s 认证协议、x 5 0 9 协议等。 ( 4 ) 电子商务协议。该类协议中主体往往代表交易的双方，其利益目标不一致。因此， 电子商务协议最为关注的是公平性，即协议应保证交易双方都不能通过损害对方利益而得 到它不应得的利益。常见的电子商务协议有s e t 协议、i k p 协议等。 第3 页 信息j 拌人学颂十学伊论文 ( 5 ) 安全多方计算协议。安全多方计算协议的目的是保证分稚式环境中各参与方以安全 的方式来共同执行分布式的计算任务。考虑到分御式的计算环境，在安全多方计算协议中， 总假定协议的执行过程中会受到一个外部的实体，甚至是束自内部的一组参与方的攻击。 这种假定很好地反映了网络环境下的安全需求。安全多方计算协议的两个最基本的安全要 求是保证协议的f 确性和各参与方私有输入的秘密性，即协议执行完之后每个参与方都应 该得到正确的输出，并且除此之外不能获知其它任何信息。安全多方计算协议的实例包括： c o i n - t o s s i n g 、广播、网上选举、电子投标和拍卖、电子现会，合同签署、匿名交易、保密 信息检索、保密数掘库访问、联合签名、联合解密等协议。 1 2 4 密码协议的安全性质1 2 f 简单地说，密码协议的目标就是保证某些安全性质在协议执行完毕时能够得以实现， 换言之，评估一个密码协议是否是安全的就是检查其所要达到的安全性质是否受到攻击者 的破坏。主要有认证性、机密性、完整性、非否认性和公平性等安全性质。 ( 1 ) 认证性。认证可以对抗假冒攻击的危险，认证可以用柬确保身份，并可用于获取对 某人或某事的信任。在协议中，当某一成员( 声称者) 提交一个主体身份并声称它是那个主 体时，需要运用认证以确认其身份是否如其声称所言。或者声称者需拿出证明其真实身份 的证据，这个过程称为认证的过程。在协议的实体认证中可以是单向的也可以是双向的。 ( 2 ) 机密性。机密性的目的是保护协议消息不被泄漏给非授权拥有此消息的人，即使是 攻击者观测到了消息的格式，它也无法从中得到消息的内容或提炼出有用的消息。保证协 议消息机密性的最直接的办法是对消息进行加密。加密使得消息由明文变为密文，并且任 何人在不拥有密钥的情况下是不能解密消息的。加密的体制分为公钥加密体制和私钥加密 体制，前者的密钥管理更为简单，后者的效率更高。 ( 3 ) 完整性。完整性的目的是保护协议消息不被非法改变、删除和替代。最常用的方法 是封装和签名，即用加密的方法或者h a s h 函数产生一个明文的摘要附在传送的消息上， 作为验证消息完整性的依掘，称为完整性校验值( i c 、，) 。一个关键性的问题是，通信双方必 须事先达成有关算法的选择等款项的共识。如果被保护的消息拥有一定的冗余，加密消息 的冗余能保证消息完整性的效果。因为如果一个攻击者不知道加密密钥而修改了密文的一 部分，则会导致在解密的过程中产生不正确的结果。 ( 4 ) 非否认性。非否认性是电子支付协议的一个重要性质。其目的是通过通信主体提供 对方参与协议交换的证掘以保证其合法利益不受侵害，即协议主体必须对自己的合法行为 负责，而不能也无法事后否认。非否认协议的主体的目的是收集证据，以便事后能够向可 信仲裁证明对方主体的确发送了或接收了消息。证据一般是以签名消息的形式出现的，从 第4 页 信息l ：稃人学硕十学臂论文 而将消息与消息的意定发送者进行了绑定。 ( 5 ) 公平性。公平性是电子支付协议的一个重要性质。其目的是保证参加协议的各方在 协议执行的任何阶段都处于同等地位，当协议执行完后或者各方得到各自所需的或者什么 也得不到。 1 2 5 密码协议的安全性分析 应用于计算机通信网的密码协议始于1 9 7 8 年r m n e e d h a m 和m d s c h r o e d e r 设计的 n e e d h a m s c h r o e d e r ( n s ) 认证协议1 4 】，这是第一个应用于计算机网络的密码协议。n s 认证协 议的提出，使计算机通信网络的安全性发生了巨大的变化，具有划时代的意义，以后许多 著名的协议如k e r b e r o s 协议就是以此为蓝本而发展起来的。 n s 认证协议提出之后不久，便遇到了密码协议发展史上的一个纠缠不休的问题，即 安全性。当时n e e d h a m 和s c h r o e d e r 提出的主要是两个用以建立交互通信的认证协议，其 中一个采用传统的对称密钥加密体制，另一个采用非对称密钥加密机制。对于前者， d d e n n i n g 和g s a c c o 5 1 于1 9 9 1 年发现其存在重放攻击缺陷，即当一个主动攻击者使用一个 旧的泄密的会话密钥冒充新的会话密钥时，攻击便成功了；对于后者，g a v i n l o w e 6 于1 9 9 5 年j 饯现其存在并行攻击缺陷，攻击者可以利用该缺陷冒充某个协议参与者与其它协议参 与者进行通信。之后，人们丌发了许多新的密码协议或者对已存在的密码协议进行了改进， 但这些协议往往在发布之后被陆续发现其中存在某些缺陷。j 下如n e e d h a m 和s e h r o e d e r 所 说 7 1 ，非常强烈地需要有某种技术来验证安全协议的安全性。但迄今为止，密码协议的安 全论证仍是一个难以根本解决的问题。 1 2 6 密码协议形式化方法的研究进展 在形式化方法出现胁，几乎没有一般可以遵循的密码协议分析的过程：即使在形式化 方法出现之后，许多密码协议也是依然通过观察的方式，直观地说明它们的安全性。所谓 形式化方法是指用数学方法描述和推理基于计算机的系统，直观地说，就是规范语言+ 形 式推理，在技术上通过精确的数学手段和强大的分析工具得到支持。其表现形式通常有逻 辑、离散数学、状念机等等；规范语言包括语法、语义以及满足关系等几部分。它主要用 于发现一个系统中的歧义性、不一致性与不完备性。因此，在密码协议的形式化分析过程 中，形式化方法主要用于研究协议的性质，这在很大程度上独立于协议所包含的密码算法 的性质，因此下文总是假设协议所使用的密码算法是不可破解的，形式化分析主要是针对 密码协议的自身结构。 根掘文献【8 】，密码协议的形式化分析方法按照不同的时期出现不同的思想体系为依据 第5 页 信息l 程人学硕十学位论文 可以划分为以下三类： 基于推理结构性方法 在基于推理结构性形式化方法中，最具有影响力的当属b a n 逻辑1 9 ，它是由b u r r o w s 、 a b a d i 和n e e d h a m 于1 9 8 9 年提出的。b a n 逻辑是关于主体拥有的知识与信仰的逻辑，它 通过定义基本的结构和假设来形式化地描述协议，并提供一系列规则对信仰进行推理。这 种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接收消 息从最初的信仰逐渐发展到协议运行最终要到达的目的认证双方的最终信任关系。 b a n 逻辑精细，规则简洁、直观，易于使用。b a n 逻辑也曾成功地发现了一些著名协议( 如， n e e d h a m - s c h r o e d e r ，c c i t t 的x 5 0 9 协议等) 中存在的缺陷】。然而，b a n 逻辑缺乏非 单调逻辑，缺乏精确定义的语义，无法检查出并行攻击等等，由于这些缺陷使得它的应用 范围比较窄。为了拓宽b a n 逻辑的应用范围，使之能够适用于公钥密码协议、不确定性推 理、非单调性逻辑等多种安全协议的分析，人们通过在b a n 逻辑中加入一些新的结构和谓 词扩展b a n 逻辑。扩展的b a n 逻辑( 如，g n y 逻辑f 1 2 1 、a t 逻辑【1 3 】、m b 逻辑【1 4 1 、v o 逻辑【1 5 l 、 s v o 逻辑【l6 】) 统称为b a n 类逻辑。b a n 类逻辑抽象性较高，它所捕获的一些协议缺陷有的并 未被人们所理解；而且，协议的理想化过程是非形式化的，无法验证理想化的币确性；一 旦b a n 类逻辑推出协议错误，仍需要采用其它协议分析工具来指出相应的攻击。 基于攻击结构性方法 基于攻击结构性方法对协议进行分析时一般要借助于自动工具，如一般目的的模型检 测工具f d r 和m u r o 以及特殊目的的n r l 分析器和i n t e r r o g a t o r 。这些方法都是从协议的 初始状念丌始，对合法主体和一个攻击者的所有可能的执行路径进行穷尽搜索以期找到协 议可能存在的错误。与基于推理结构性方法相比，基于攻击结构性方法一旦推出协议错误， 就可以直接指出相应的攻击。实验表明这些工具是有效的。如m e a d o w s 和s y v e r s o n 用n r l 协议分析器发现了s i m m o n ss e l e c t i v eb r o a d c a s t 协议的缺陷 1 7 j 8 1 ；1 9 9 6 年，英国学者g a v i n l o w c 首先启用模型检测工具f d r ，来分析并发现了n e e d h a m - s c h r o e d e r 公钥协议的一个以 前从未发现的漏洞；m i t c h e l l 和s t e m 使用模型检测工具m u r ( 通用状态计数工具) 对 n e 它d h a m s c h r o e d e r 公钥协议、t m n 和k e r b e r o s 等协议进行了分析“”。 但同时它们也存在着一些问题，突出表现在以下两个方面： i 主体数目的有限性。这些工具首先要做的是规定参与协议的主体的最大数目，这意 味着它们只能分析包括有限个主体的协议。即使是这些工具没有发现一个协议的错误，但 当协议的主体数目增加时仍可能存在错误。 i i 无法解决状态空问爆炸问题。 基于证明结构性方法 第6 页 信息l 。科人学硕十学位论文 由于基于推理结构性的形式化分析方法不能解决秘密性，而且缺乏清晰的语义，甚至 有时很难明确指出信仰逻辑在证明什么；另一方面，基于攻击结构性的形式化分析方法不 得不对随着协议的增大而呈指数增长的协议状念空日j 进行搜索，其所需的时日j 与空问往往 超过可用资源。为解决上述问题，p a u l s o n 独立地提出了一个基于协议消息和事件攻击结 构方法注记的结构性证明法，称为p a u l s o n 归纳法 2 0 1 。p a u l s o n 将协议归纳定义为所有可能 事件路径的集合，每条路径是一个包含多轮协议通信的事件序列，主体接收到一个路径， 可转发它或根掘协议规则进行扩展使消息的真讵发送者对此无从可知。这种方法可以摸拟 所有攻击和密钥丢失，部分过程可用i s a b e l l e 定理证明器通过对路径的归纳来自动证明性 质的成立；s c h n e i d e r 提出使用秩函数1 2 1 1 柬验证恶意环境下协议性质的成立。秩函数对系统 中所有可能的消息进行赋值，赋值的结果作为消息的可循环的不变式，并进而运用不变式 技术来对协议的安全性质进行证明，这样的目的在于一方面试图找到可能存在的攻击，另 一方面直接证明攻击是不可能发生的；t h a y e r , h e r z o g 和g u t t m a n 提出了串空1 日j 协议模型昭 2 3 。川，它是集n r l 协议分析器、s c h n e i d e r 的秩函数以及p a u l s o n 的归纳法思想之大成，是 一种新型有效的形式化分析方法。与i ； 两种形式化方法相比，具有如下优点： i 手工推理，从s t r a n ds p a c e 模型最重要的环节( 即组成协议内容的最基本的加密术语 成分) 入手寻找使协议失败的路径，避免了状态空间爆炸问题。 i i 证明协议t f 确性以及寻找协议攻击均以命题证明的形式出现，使得协议分析变成了 一个数学问题，理论性更强了。 基于证明结构性方法的代表类型还有如h u m a n r e a d a b l e 证明法，a t t a c k s 限定法， r e w r i t i n g 逼近法，m a u d e 分析法，i n v a r i a n t 技术等等。 1 2 7 密码协议形式化方法成立的前提 加密前提 i 密码系统是完善的假设。 1 9 8 3 年，d o l e v 和y a o 发表了安全协议发展史上一篇重要的论文2 5 1 。将密码协议本身 与密码协议所具体采用的密码系统分丌，在假定密码系统是“完善”的基础上讨论密码协 议本身的正确性、安全性，冗余性等课题。从此，学者们可以专心研究安全协议的内在安 全性质了。亦即，问题很清楚地被划分为两个不同的层次：首先研究安全协议本身的安全 性质，然后讨论实现层次的具体细节，包括所采用的具体密码算法等等。 i i 完美加密假设。 如果攻击者拥有此加密消息的解密密钥，他j 能获得此加密消息的明文内容。 i 自由加密假设。 第7 页 信息i 拌人学硕十学伊论文 自由加密假设保证一个密文只以一种方式存在，描述为：对于m ，m a 和七，k k ， 如果 肌l - - m 。，那么m = 脚 t = 七1 。 协议参与者及角色的假设 参与协议运行的主体分为诚实主体( 即合法主体) 和攻击者。他们均了解协议的执行步 骤、采用的密码算法和消息的格式。诚实主体将同意并严格按照协议舰定运行协议，攻击 者不受协议规定的约束。攻击者的角色具有多样性，他既可以是协议运行的合法主体。又 可以是协议运行的非法主体。 攻击者的知识和能力假设 d o l e v 和y a o 于1 9 8 3 年提出了密码协议模型【2 5 1 ，定义了攻击者模型，以后密码协议攻 击者模型的研究都是依此为基础的。攻击者模型描述了攻击者的知识和能力。具体如下： i d o l e v - y a o 模型中攻击者的知识： 熟悉现代密码学，知道加解密等运算操作； 知道参与协议运行的各实体名及其公钥； 拥有自己的加密密钥和解密密钥； 将窃听或收到的消息增加为自己的知识。 1 1 d o l e v y a o 模型中攻击者的能力： 可窃听、拦截系统中传送的任何消息； 可解密用他自己加密密钥加密的消息； 可在系统中插入新的消息； 即使不知道加密部分的内容，也可重放他所看到的任何消息； 可运用他知道的所有知识( 如临时值等) ，并可产生新的临时值。 1 3 论文的主要研究目的和结果 i 3 1 论文的主要研究目的 自从基于d o l e v y a o 模型的s t r a n ds p a c e 模型理论方法被提出来之后，国内外的许多 学者在这方面做了大量的工作_ 2 3 , 2 4 1 ，不过最终只是能证明密码协议的正确性，找到密码 协议中已经存在的攻击，对于未知的攻击却未从涉猎。中科院软件所信息安全重点实验室 季庆广、卿斯汉、冯登国尝试性地提出了基于广义串空间模型的构造攻击方法f 捌，以实体 认证协议1 1 为例，使这个构造攻击方法初露锋芒，试探性地找到了几个未知的攻击，说明 第8 页 信息i ：稃人学硕十学位论文 了构造攻击方法存在的价值与意义。因此，我们觉得这种方法值得研究与探讨，所以就提 出了基于广义串空日j 模型构造攻击的密码协议设计与分析的研究这个课题。 1 3 2 论文的主要研究结果 i 对d o l e v y a o 模型的攻击者模型进行了扩充，使之能反映更多的密码学原语；利用 扩充的攻击者模型，分析了t l s 2 1 协议，发现了一个攻击。 从理论上抽象出了基于广义串空b j 模型的构造攻击方法，给出了分析密码协议时切 实可行的步骤方案；指出基于广义串空问模型的构造攻击方法的缺陷，并给出了具体的修 正措施；提出一个类似于m i l l e n 曾经设计的“仃g g 协议1 2 7 1 的密码协议“f i g g ”协议，它们具 有共同的密码学性质( m i l l e n 曾用p a u l s o n 的归纳法证明了“f 埯g ”协议是安全的) ；用修证过 的基于广义串空日j 模型的构造攻击方法证明了“f 龟g 协议是不安全的，存在着并行攻击缺 陷，而且容易证明“f f g g ”协议也是不安全的，存在着同样的缺陷。 m 以n e e d h a m s c h r o e d e r - l o w 协议为例，分析了基于改进的串空间模型构造攻击方法 在密码协议设计中的应用，提出了设计密码协议时应该遵循的一般过程。 1 4 论文的结构和组织脉络 本文的章节和脉络是这样安排的： 第一章绪论。介绍了密码协议的研究现状；简述了论文的主要研究目的和结果；给出了 论文的组织脉络。 第二章串空间概述。概述了串空日j 基本模型；阐述了串空间的研究现状；指出了串空i 日j 的应用前景。 第三章d o l e v - y a o 模型的扩展及其应用。基于恶意攻击软件的工作原理扩充了d o l e v y a o 模型，分析了t l s 1 】协议。 第四章推广基于广义串空日j 模型构造攻击的研究。介绍了广义串空间模型，研究了基于 广义串空日j 模型的构造攻击的渊源、使用方法：以n e e d h a m - s c h r o e d e r 协议为例， 指出了这种构造攻击的缺陷，给出了修j 下措施；提出了修证的基于广义串空f h j 模型 构造攻击的具体应用。 第五章基于广义串空间模型密码协议的设计。总结了设计密码协议时应该遵循的一般原 则，说明了基于改进的广义串空间模型的构造攻击在密码协议设计中的应用，并提 出了一般设计过程。 结束语。总结了目i i f 的工作，提出了进一步研究的方向。 第9 页 信息i 聘人学硕十学位论文 第二章串空间概述 本章从串空问的基本模型、研究现状以及它的应用前景入手，详细介绍了串空阃。 2 1 基本模型 本节主要介绍串空日j 所包含的基本概念、丛与因果次序、消息空间以及攻击者模型。 2 1 1 基本概念 定义2 1 1 1 考虑一个集合a ，其元素为协议中主体问交换的可能的消息，记为术语。 例如t o c t i 表示t o 是t l 的一个子术语。 定义2 1 1 2 一个符号术语是一个二元对( o ，a ) ，其中a e a ，o 为符号+ 或一。例如 + t 或一t ，读作发送术语t 或接收术语t 。( a ) 是有限序列符号术语s 集合，其元素为 ( ( o l ，a 1 ) ，( o n ，a n ) ) 。 定义2 1 1 3a 上的一个串空问是一个集合和一个路径映射：t r ：一( a ) 。 定义2 1 1 4 对于a 上的一个串空日j ，下面是一些基本概念。 节点是一个二元对( s ，i ，其中s e e ，i 满足1 _ i _ l e n g t h ( t r ( s ) ) 。节点集合记为n 。( s ，i ) 属于串s 。 如果n = ( s ，i ) n ，那么i n d e x ( n ) = i 和s t r a n d ( n ) = s 记术语( n ) 为( t r ( s ) ) i ，也就是路径 s 的第i 个符号术语。 对于一些a a ，当且仅当t e r m ( n 1 ) ；+ a 和t e r m ( n 2 ) = - a ，则存在一条边n l n 2 。边表 示消息a 由节点1 1 l 发送，并由节点1 1 2 接收。 当i l l = ( s ，i ) ，n f ( s ，i + 1 ) 为n 的成员时，存在一条边n l n 2 ，表示n i 是s t r a n ds 中1 1 2 的直接父节点。n l j + n 2 表示在同一个s t r a n d 中，n i 在