（计算机软件与理论专业论文）串空间模型及其认证测试方法的扩展与应用.pdfVIP

串空间模型及其认证测试方法的扩展与应用中文摘要 中文摘要 安全协议提供安全服务，是构建网络安全的基石。随着网络的迅速发展，越来越 多的密码技术被应用到安全协议中，保证了网络不同程度的安全性。然而各种针对协 议的攻击技术也不断出现，这对安全协议的分析提出了更高的要求。 形式化方法是一种非常有效的安全协议分析的方法。串空间模型及相关理论的出 现推动了安全协议的形式化分析研究。然而原始的串空间模型及其认证方法在分析一 些安全协议时还存在一些不足，因此本文针对基于丰富密码学的安全协议和基于猜测 攻击的安全协议，扩展了串空间模型和认证测试方法。 由于原始的串空间模型仅考虑了一些简单操作，无法描述和分析在安全协议中使 用越来越广泛的其他一些操作，如散列函数、签名运算和d h 计算等，因此需要扩展串 空间模型。由于认证测试方法以串空间模型为基础，因此串空间模型中存在的一些不 足在认证测试方法中同样存在，因此本文还提出了一种基于丰富密码学的扩展认证测 试方法。扩展后的模型和方法能够更精确地描述和分析安全协议的安全性，并能够应 用于更广泛的领域。 由于分析安全协议猜测攻击时需要考虑密码系统不完善所产生的问题，而原始的 认证测试方法对密码系统做了完善的假设，需要三个基本前提假设，难以发现安全协 议中存在的猜测攻击。本文提出了一种基于猜测攻击的扩展认证测试方法。首先定义 了猜测数据和验证项，并将其引入到串空间模型中；然后定义了验证项判断规则和验 证项判断算法，并将其引入到认证测试方法中。扩展后的模型和方法能够发现安全协 议中存在的猜测攻击。 为验证扩展串空间模型和认证测试方法的有效性，本文首先分析了s s l 3 0 和 t l s l 0 握手协议，验证了协议的认证性；然后分析了y a h a l o m b a n 和e x e 协议， 发现了协议中存在的猜测攻击。实例分析结果说明了扩展说明了扩展串空间模型和认 证测试方法的正确性和有效性。 关键字：串空间模型；认证测试方法；密码学；猜测攻击 作者：方燕萍 指导老师：张广泉 a bs t r a c t s e c u r i t yp r o t o c o lp r o v i d i n gs e c u r i t ys e r v i c e si st h ei n f r a s t r u c t u r eo fn e t w o r ks e c u r i t y w i t ht h er a p i dd e v e l o p m e n to fn e t w o r k ，m o r ea n dm o r ec r y p t o g r a p h i ct e c h n i q u e sa l e a p p l i e dt os e c u r i t yp r o t o c o l si no r d e rt og u a r a n t e ed i f f e r e n t l e v e l so fn e t w o r ks e c u r i t y h o w e v e r , d i f f e r e n tk i n d so fa t t a c k i n gt e c h n i q u e sa l s oa p p e a rc e a s e l e s s l y , w h i c hb r i n g f o r w a r dm u c hh i g h e rr e q u i r e m e n to ft h ea n a l y s i so fs e c u r i t yp r o t o c o l s f o r m a lm e t h o di sav e r ye f f e c t i v ei n s t r u m e n tt oa n a l y z es e c u r i t yp r o t o c o l s t h e a p p e a r a n c eo fs t r a n ds p a c em o d e la n dr e l a t e dt h e o r i e sp r o m o t et h er e s e a r c ho ff o r m a l a n a l y s i s o f s e c u r i t yp r o t o c o l s h o w e v e r , t h eo r i g i n a l s t r a n ds p a c em o d e la n di t s a u t h e n t i c a t i o nm e t h o dh a v es o m ed r a w b a c k sw h e na n a l y z i n gs o m es e c u r i t yp r o t o c o l s t h e r e f o r e ，t h i st h e s i se x t e n d st h i sm o d e la n di t sm e t h o da c c o r d i n gt ot h ec o m p l e xs e c u r i t y p r o t o c o l sb a s e do nr i c hc r y p t o g r a p h i cp r i m i t i v e sa n dt h es e c u r i t yp r o t o c o lb a s e do n g u e s s i n ga t t a c k s a st h eo r i g i n a ls t r a n ds p a c em o d e lo n l yc o n s i d e rp o o rc r y p t o g r a p h i cp r i m i t i v e s ，a n d t h u sc a n n o td e s c r i b ea n da n a l y z es o m ec r y p t o g r a p h i cp r i m i t i v e si ns e c u r i t yp r o t o c o l ss u c h a sh a s hf u n c t i o na n ds i g no p e r a t i o n , s oi ti sn e c e s s a r yt oe x t e n dt h es t r a n ds p a c em o d e l s i n c ea u t h e n t i c a t i o nt e s ti sb a s e do nt h es t r a n ds p a c em o d e l ，s o m ed e f i c i e n c i e si nt h e s t r a n ds p a c em o d e la l s oe x i s ti na u t h e n t i c a t i o nt e s t t h u s ，t h i st h e s i sp r e s e n t sa ne x t e n d e d a u t h e n t i c a t i o nt e s tm e t h o db a s e do nr i c hc r y p t o g r a p h i cp r i m i t i v e s t h ee x t e n d e dm o d e la n d m e t h o dc a nb e t t e rd e s c r i b ea n da n a l y z et h es e c u r i t yo fp r o t o c o l s ，a n da p p l i e di nm o r e e n t e n s i v ef i e l d s w h e na n a l y z i n gg u e s s i n ga t t a c k so fs e c u r i t yp r o t o c o l s ，i tn e e d st ot a k et h ep r o b l e mo f i m p e r f e c tc r y p t o g r a p h i cs y s t e mi n t oa c c o u n t h o w e v e r ，t h eo r i g i n a la u t h e n t i c a t i o n t e s t m e t h o da s s u m e st h a tt h ec r y p t o g r a p h i cs y s t e mi sp e r f e c ta n dr e l y so nt h r e eb a s i c h y p o t h e s e s ，s oi tc a nh a r d l yf i n dt h eg u e s s i n ga t t a c k se x i s t i n gi ns e c u r i t yp r o t o c o l s t h i s t h e s i sp r o p o s e sa ne x t e n d e da u t h e n t i c a t i o nt e s tm e t h o db a s e do ng u e s s i n ga t t a c k s f i r s t l y , w ed e f i n et h eg u e s s i n gd a t aa n dt e r mt ov e r i f yf o r m a l l y ；a n di n t r o d u c et h e mi n t ot h es t r a n d s p a c em o d e l t h e nw ep r e s e n tv e r i f y i n gr u l e sa n dv e r i f y i n ga l g o r i t h m so ft e r m s ；a n d l i t h ee x t e n s i o na n da p p l i c a t i o no fs t r a n ds p a c em o d e la n da u t h e n t i e a t i o n t e s t sa b s t r a c t i n t r o d u c et h e mi n t ot h ea u t h e n t i c a t i o nt e s tm e t h o d t h ee x t e n d e dm o d e la n dm e t h o dc a l l d e t e c tg u e s s i n ga t t a c k si ns e c u r i t yp r o t o c o l s t ov a l i d a t et h ee f f e c t i v e n e s so ft h ee x t e n d e ds t r a n ds p a c em o d e la n dt h ee x t e n d e d a u t h e n t i c a t i o nt e s tm e t h o d ，w ea n a l y z es s l 3 0a n dt l s1 0h a n d s h a k i n gp r o t o c o l 晰t 1 1t h e p r o p o s e d a p p r o a c h a n dv e r i f yt h ep r o p e r t i e so fa u t h e n t i c a t i o n ；a n dt h e na n a l y z e y a h a l o m - b a na n de x ep r o t o c o l ，f i n d i n gg u e s s i n ga t t a c k se x s i t i n gi nt h e s ep r o t o c o l s a n a l y s e sr e s u l t so ft h e s ee x a m p l e sd e m o n s t r a t ec o r r e c t n e s sa n de f f e c t i v e n e s so ft h e e x t e n d e dm o d e la n dt h ee x t e n d e dt e s tm e t h o d k e y w o r d s ：s t r a n ds p a c em o d e l ；a u t h e n t i c a t i o nt e s t ；c r y p t o g r a p h i cp r i m i t i v e ；g u e s s i n g a t t a c k i i i w r i t t e nb y f a n gy a n p i n g s u p e r v i s e db yz h a n gg u a n g q u a r t 图表索弓串空间模型及其认证测试方法的扩展与应用 图表索引 图2 1b o u n d l e 示意图1 1 图2 2n s p k 协议串空间模型1 3 图2 3n s p k 协议攻击1 4 图2 4 输出测试l 6 图2 5 输入测试1 6 图2 6 主动测试1 7 图3 1 输出测试扩展( 1 ) 2 6 图3 2 输出测试扩展( 2 ) 2 6 图3 3 输入测试扩展( 1 ) 2 6 图3 4 输入测试扩展( 2 ) 2 7 图3 5 主动测试扩展( 1 ) 2 7 图4 1e x e 协议攻击3 0 图4 2 输出测试扩展( 3 ) 。3 6 图4 3 输入测试扩展( 3 ) 3 7 图4 - 4 主动测试扩展( 2 ) 3 8 图5 1s s l 体系结构4 0 图5 2s s l 3 0 握手协议发起者串空间模型4 2 图5 3s s l 3 0 握手协议响应者串空间模型4 3 图5 4s s l 3 0 握手协议串空间模型。4 3 图5 5t l s l 0 握手协议发起者串空间模型。4 5 图5 6t l s l 0 握手协议响应者串空间模型。4 6 图5 7t l s l 0 握手协议串空间模型4 6 图5 8y a h a l o m b a n 协议状态转换4 8 图5 - 9y a h a l o m b a n 协议发起者串空间模型4 9 图5 1 0y a h a l o m b a n 协议响应者串空间模型4 9 图5 1 1y a h a l o m b a n 协议服务者串空间模型5 0 图5 1 2y a h a l o m b a n 协议串空间模型5 0 i v 串空间模型及其认证测试方法的扩展与应用图表索弓 图5 1 3e x e 协议发起者串空间模型5 4 图5 1 4e x e 协议响应者串空间模型5 4 图5 1 5e x e 协议串空间模型5 5 图5 1 6 改进后e x e 协议串空间模型一5 7 表2 1 测试方法分类17 v 苏州大学学位论文独创性声明及使用授权的声明 学位论文独创性声明 本人郑重声明：所提交的学位论文是本人在导师的指导下，独立进 行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不含 其他个人或集体己经发表或撰写过的研究成果，也不含为获得苏州大学 或其它教育机构的学位证书而使用过的材料。对本文的研究作出重要贡 献的个人和集体，均已在文中以明确方式标明。本人承担本声明的法律 责任。 研究生签名：礴日 学位论文使用授权声明 苏州大学、中国科学技术信息研究所、国家图书馆、清华大学论文 合作部、中国社科院文献信息情报中心有权保留本人所送交学位论文的 复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本 人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文 外，允许论文被查阅和借阅，可以公布( 包括刊登) 论文的全部或部分 内容。论文的公布( 包括刊登) 授权苏州大学学位办办理。 研究生签名： 导师签名f 。 日期：坦率 日期：旦弘 串空间模型及其认证测试方法的扩展与应用第一章绪论 1 1 研究背景及意义 第一章绪论 安全协议是在不可靠或敌意的通信环境下使用了密码技术，用于保护网络上传输 各种信息的通信协议，是构建网络安全的基石。安全协议的目标是为了保证网络上各 种协议的安全性，如认证协议的目标是为了认证参与协议主体的身份、协议主体之间 分配密钥或其它各种秘密。近年来，认证协议越来越多地用于保护i n t e m e t 传送的各 种信息，是网络安全的一个重要组成部分。另外其他安全协议可以完成协议的公平性、 不可否认性等安全性。 随着因特网的迅速发展，网络的安全问题已引起人们的高度重视。密码技术和安 全协议是实现网络安全两个主要内容，它们构成了网络安全的两个重要层次。为了更 精确的保证网络上传递信息的安全性，越来越多的密码技术被应用到安全协议中，如 散歹u ( h a s h ) 函数，签名( s i g n ) 运算等。安全协议以这些密码技术为基础，保证了网络 不同程度的安全性。 网络迅速发展的同时各种针对协议的攻击技术也不断出现。安全协议是很脆弱 的，很容易受到攻击。一个被动攻击者可以窃听协议部分或整个运行过程并获取敏感 信息，而一个主动的攻击者可以截获信息并对其进行任意的修改，甚至它可以伪装成 通信主体欺骗合法主体与其进行非法通信。常见的攻击有以下几种：中间人攻击 ( m a n - i n t h e - m i d d l ea t t a c k ) 、并行会话攻击( p a r a l l e ls e s s i o na t t a c k s ) 、重放攻击( r e p l a y a t t a c k s ) 、猜测攻击( g u e s s i n ga t t a c k s ) 和类型攻击( t y p ea t t a c k s ) 等。密码技术的发展促 进了密码运算的扩展，攻击者能够利用的密码运算和攻击软件也相应增加，这对安全 协议的形式化分析技术提出了更高的要求。 形式化方法用于安全协议分析是目前信息安全领域主流的研究方向之一，即对安 全协议进行准确地建模，然后应用数学的方法来证明该模型是否满足相应的性质。安 全协议形式化分析技术的基本前提假设是完善的密码学，即安全协议中所采用的密码 算法是不可攻破的，使得安全协议的研究者可以专心研究安全协议的内在安全性质。 实践证明形式化方法用于安全协议的分析是非常有效的方法，不仅能够分析安全协议 的安全性，而且还能够发现安全协议中存在的攻击。安全协议形式化方法经过二十多 第一章绪论串空间模型及其认证测试方法的扩展与应用 年的发展，已取得了丰硕的成果，成为一个研究热点。而串空间模型( s t a n ds p a c em o d e l ) 出现将安全协议形式化分析技术推向了一个新的高度。串空间模型充分吸收了前人的 研究成果，把协议的描述和目标安全属性转化为图的结构，有利于借助图的理论和算 法分析和证明协议的安全性。然而随着计算机网络应用范围的扩展，一些专门的安全 协议被设计出来，各种有效的形式化方法也将不断的提出并得到相应的扩展。针对基 于丰富密码学的安全协议和基于猜测攻击的安全协议，如何有效的用形式化方法分析 这些协议是安全协议形式化方法要解决的问题。 1 2 国内外研究现状 形式化方法用于安全协议分析已有二十多年的发展历史。d o l e v y a o 模型i l j 开创 了安全协议形式化方法的先河，定义了协议并发运行环境的形式化模型、密码算法无 关的验证以及攻击者行为等，奠定了安全协议形式化方法研究的基础。b a n 逻辑1 2 j 是安全协议形式化方法的里程碑，利用知识和信念逻辑来描述和推理认证协议，它大 大激发了形式化方法用于安全协议研究的兴趣，之后出现了许多形式化方法被应用于 安全协议的分析。b a n 类逻辑是弥补b a n 逻辑的不足，如：g n y 逻辑p j 、a t 逻辑 【4 】以及s v o 逻辑【5 】等等。逻辑推理方法可以发现安全协议设计出错的原因，但是由于 抽象性较高，不能发现协议存在的攻击且难以反映协议运行整个过程，有着自身的局 限性1 6 。模型检测技术【7 吲是验证有限状态系统的自动化分析技术，可以发现协议存在 的攻击。c s p 方法【9 】的成功应用促进了这一领域的发展，但模型检测技术最大的不足 就是无法避免状态空间爆炸问题。定理证明技术是用逻辑符号对安全协议进行模型 化，再用定理证明技术证明安全协议的正确性。具有代表性有p a u l s o n 的归纳法【l 川 和串空间模型【1 1 j 。 串空间模型是f - j t f a b r e g a , j c h e r z o g 和j d g u t t m a n 在1 9 9 8 年提出的一种安 全协议形式化模型。它是一种结合定理证明技术和协议迹的混合方法，吸纳了n r l 协议器【1 2 】、s c h n e i d e r 秩函数【1 3 】和p a u l s o n 归纳法等思想。串空间模型不仅能够证明 安全协议的认证性和秘密性，而且还可以构造攻击者的攻击行为，揭示安全协议的内 在缺陷”15 1 。该模型及相关理论的提出，推动了安全协议的形式化分析研究【1 6 - 2 0 1 。此 后，研究人员在此基础上开展了卓有成效的研究工作。 在模型扩展与应用方面，主要有以下几种方法： 2 串空间模型及其认证测试方法的扩展与应用第一章绪论 ( 1 ) 认证测试( a u t h e m i c a t i o nt e s t ) 方法：基于串空间模型基础的验证安全协议的一种 形式化方法【2 l 】。与串空间方法相比，认证测试方法在验证过程中具有更简洁、直 观、清晰的优点，避免了串空间方法证明协议繁琐、复杂的理论推导。 ( 2 ) 混合( m i x e d ) 串空间模型：包括了主串( p r i m a r ys t r a n d ) 空间和从串( s e c o n d a r y s t a l m d ) 空间【2 2 1 ，其中主协议对应的串空间称为主串空间，从协议对应的串空间称 为从串空间。混合串空间用于描述多个协议的运行，当多个协议同时运行时，只 要它们的密钥不相交，那么可以避免遭受组合协议攻击。 ( 3 ) 针对d i f f i e h e l l m a n 串空间模型：在串空间模型框架中讨论了d i f f i e h e l l m a n 田】 密钥交换问题，扩展了串空间模型，使得串空间模型能够更精确的描述基于 d i 衢e h e l l m a n 的安全协议。 ( 4 ) 串空间模型与其它形式化方法结合：将串空间与信任管理( 1 r h i m s tm a n g e m e n t ) 口4 1 结合起来，使得串空间模型除了分析安全协议的认证性和秘密性之外，还可以分 析其它安全协议属性；将串空间与时态逻辑( t e m p r o a ll o g i c ) 【2 5 】结合起来，为实现 自动化工具奠定了基础；将串空间线性逻辑( l i n e a r l o i g c ) 2 6 1 结合起来，使串空间 模型能够分析具有线性逻辑的安全协议；将串空间模型与区间时序逻辑( i n t e r v a l t e m p o r a ll o g i c ) 2 7 】结合起来，使串空间模型分析具有时间限制的安全协议。 ( 5 ) 动态( d y n a m i c ) 空间模型：在串空间模型中引入串活动结点的概念【2 引，使得串 空间模型能够模拟安全协议的动态执行过程。 ( 6 ) 通用( g e m e r a l ) 串空间模型：提出了通用串空间模型( s s m ) 以及o r a c l es t r a n d s 等新 类型串的概念【2 9 】，不仅可以证明安全协议的正确性，而且还可以构造出对错误协 议的攻击。 ( 7 ) 理想( i d e a l s ) 结构：用理想结构，定义了丛( b o u n d l e ) 最大结点、良序丛的概念【3 0 l ， 使得串空间理想结构不仅能够证明安全协议的认证性和秘密性，而且还能够证明 安全协议的的保密性、认证性、零知识性等安全性。 ( 8 ) 增强型认证测试e a t ( e n h a c e da u t h e n t i c a t i o nt e s t ) ：在认证测试方法中引入 c o r r e s p o n d e n c e 函数等概念【3 l 】，扩展了认证测试方法，提出了s t r a n d 参数一致性 定理，很好地解决了参数一致性的分析问题，从而更便于安全协议关联性分析自 动化的实现。 ( 9 ) 串空间图生成方法：定义开丛( o p e nb u n d l e ) 作为串空间图的结构单元，并在开丛 集基础上定义了前缀算子和组合算子【3 2 1 ，给出了无穷并发运行安全协议串空间图 3 第一章绪论串空间模型及其认证测试方法的扩展与应用 的生成方法。 在自动分析工具方面，主要有以下几种的方法： ( 1 ) a t h e n a 工具：对串空间模型进行扩展，结合模型检测技术与定理证明技术，用于 安全协议分析的自动化验证工具【3 3 】。a t h e n a 用一种简单的逻辑来描述安全协议的 性质，状态采用新的表示法，同时使用了一些消减规则，用来消减状态搜索空间， 使得a t h e n a 能够自动和快速的验证安全协议。 ( 2 ) t 模型：在串空间模型基础上，提出了自动验证模型1 3 4 。该模型利用标量来描述 协议，搜索过程采用变量替换，不再受参与者个数限制，并且可以根据攻击理论 的发展，添加新的攻击者串。 在安全协议设计方面，主要有以下几种协议： ( 1 ) 电子商务协议：将认证测试方法运用到电子商务设计领域，用于指导协议的设计， 提出了一个新的电子商务协议a t s p e c t ( a na u t h e n t i c a t i o nt e s t b a s e ds e c u r e p r o t o c o lf o re l e c t r o n i cc o m m e r c et r a n s a c t i o n s ) 3 5 1 。该协议可以按照目前绝大多数 信用卡公司采用的安全电子商务规范要求，提供交易过程中各阶段的安全性和功 能性的保证。 ( 2 ) i n t e m e t 密钥交换协议：利用人证测试方法，提出了一种具体地构建唯一满足两个 通信实体变换边的形式化协议设计方法，设计出了高效安全的i k e ( i n t e m e t e x c h a g ee x c h a n g e ) 协议【3 6 】。 随着计算机网络应用范围的扩展，串空间模型在很多方面还不是很完善，有待扩 展和改进，使其能够应用于更广泛的领域。 1 3 本文研究内容 安全协议在网络通信中起着关键的作用，对其安全性的验证尤其重要。形式化方 法用于安全协议验证是目前最有效的方法之一。随着网络技术的快速发展以及攻击者 能力的增强，现有的形式化方法在分析一些安全协议时还存在不足，因此需要对其进 行扩展。串空间模型和认证测试方法是目前安全协议形式化方法的研究热点之一，本 文将在串空间模型和认证测试方法及其应用方面进行深入研究。协议研究人员在安全 协议设计中使用密码学算法来增强网络的安全性，现有串空间模型和认证测试方法在 分析这些协议的时候还存在不足，因此必须扩展串空间模型，使其能够更精确的描述 4 串空间模型及其认证测试方法的扩展与应用第一章绪论 安全协议，并扩展认证测试方法，使其能够更精确的验证安全协议的安全性。随着攻 击者能力不断增强，针对协议的攻击技术也不断出现，这对安全协议的分析提出了更 高的要求。安全协议形式化方法不仅要能够验证协议的安全性，而且还能够发现协议 中存在的攻击，因此扩展串空间模型和认证测试方法，并能够发现协议中存在的攻击。 本文的研究内容主要包括以下几点： ( 1 ) 针对基于丰富密码学的安全协议，扩展了串空间模型的消息项、子项关系 以及自由假设，并扩展了攻击者模型。扩展后的串空间模型能够更精确的描述安全协 议密码学原语，模型能够更精确的描述安全协议运行过程。 ( 2 ) 由于认证测试方法以串空间模型为基础，因此串空间模型中存在的一些不 足在认证测试方法中同样存在，所以也需要对认证测试方法进行扩展。通过扩展测试 分量、转换边、被转换边、输出测试、输入测试以及主动测试，扩展了认证测试方法， 并其能够应用于更广泛的领域。 ( 3 ) 针对基于猜测攻击的安全协议，形式化定义了猜测数据、验证项，并将它 们引入到串空间模型的消息项中。由于串空间模型新数据类型加入，因此，也需要扩 展子项关系以及攻击者模型。扩展后的串空间模型能够更精确地描述基于猜测攻击的 安全协议。 ( 4 ) 由于认证测试方法在验证安全协议时，需要三个基本前提假设，因此难以 发现安全协议中存在的猜测攻击。针对此问题，定义了验证项判断规则，并在输出测 试、输入测试以及主动测试中引入了验证项判断算法，扩展了认证测试方法。扩展后 的认证测试方法能够发现安全协议中存在的猜测攻击。 1 4 本文组织结构 本文共分6 章，是根据从基础概念到具体工作，从基本理论到具体应用的思路来 组织安排的，具体如下： 第1 章绪论，主要介绍了课题的研究背景、意义及国内外的研究现状，并对本文 的主要工作给出了概要说明。 第2 章串空间模型及认证测试方法相关概念，详细介绍了串空间模型基本概念、 模型的基本要素以及攻击者模型；详细介绍了认证测试方法基本概念、方法原理以及 认证测试方法的分类。 第一章绪论串空间模型及其认证测试方法的扩展与应用 第3 章基于丰富密码学的认证测试方法扩展，针对基于丰富密码学的安全协议， 详细阐述了本文提出的基于丰富密码学的认证测试方法。首先，阐述了基于丰富密码 学的安全协议，对安全协议使用的散列函数、签名运算及d h 计算做了说明，形式化 定义了这些运算。其次，扩展了串空间模型，包括消息项、自由假设、子项关系以及 攻击者模型的扩展，然后，通过扩展测试分量、转换边、被转换边、输出测试、输入 测试以及主动测试，扩展了认证测试方法。 第4 章基于猜测攻击的认证测试方法扩展，首先，讨论了猜测攻击发生的相关概 念，定义了猜测攻击发生的条件，并以e x e 协议为例说明了猜测攻击发生的过程， 给出了猜测攻击的执行轨迹。其次，形式化定义了猜测数据及验证项，并将它们引入 到串空间模型中，同时扩展了串空间模型中子项关系和攻击者模型，然后，定义了验 证项判断规则，提出了验证项判断算法，最后，将验证项判断算法引入到认证测试方 法中，同时扩展了认证测试方法中测试分量、转换边、被转换边、输出测试、输入测 试以及主动测试。 第5 章认证测试方法应用实例分析，首先，以s s l 3 0 和t l s l 0 握手协议为例， 说明了扩展基于丰富密码学的认证测试方法的正确性，并验证了协议的认证属性，然 后，以y a h a l o m b a n 和e x e 协议为例，说明了扩展基于猜测攻击的认证测试方法的 正确性，并发现了协议存在的猜测攻击。 其中第3 、4 、5 章是本文的主要研究工作。 第6 章总结与展望，对本文的工作做了总结，并对下一步工作进行了展望。 6 串空间模型及其认证测试方法的扩展与应用第二章串空间模型及认证测试方法相关概念 第二章串空间模型及认证测试方法相关概念 本章主要介绍与串空间模型及认证测试方法的一些基本概念。首先，介绍了串空 间模型中的基础知识，这是分析安全协议的基础。然后，介绍了认证测试方法在串空 间模型基础上提出的新的概念以及测试方法的基本思想。最后，介绍了认证测试方法 的分类以及测试步骤。 2 1 串空间模型概述 串空间模型是f j t f a b r e g a , j c h e r z o g 和j d g u t t m a n 在1 9 9 8 年提出的一种安 全协议形式化模型，这是一种结合定理证明技术和协议迹的混合方法，它吸纳了n r l 协议器、s c h n e i d e r 秩函数和p a u l s o n 归纳法等思想，继承了前人的研究成果。串空间 模型把协议的描述和目标属性转化为图的结构，可以用图示方法辅助分析和证明协议 的正确性。 串空间模型是一种新型有效的形式化模型，不仅可以用来分析安全协议的正确性 以及构造攻击者的行为，发现安全协议存在的内在缺陷，而且还可以用于安全协议的 设计。与其它形式化方法相比，串空间模型具有以下特点： ( 1 ) 临时值和会话密钥等数据项具有新鲜性，并且仅在安全协议中的一次运行中出 现。 ( 2 ) 串空间模型精确地描述了系统中攻击的可能行为。在串空间模型中，可以给出与 具体安全协议无关的攻击者能力模型。 ( 3 ) 在串空间模型下，安全协议正确性的含义既包括了认证性，也包括了秘密性；扩 展了b a n 类逻辑的分析范围。 在串空间模型中，串是参与安全协议的主体可以执行的事件序列，即发送或接收 消息的序列集。对于合法的主体，该事件序列是根据协议定义，由发送事件和接收事 件组合而成。一个串只代表一个主体在协议的一次执行中的行为，不同主体的行为用 不同的串表示。攻击者串是攻击者所有可能发送或接收的消息序列，它能模拟攻击者 具有的攻击行为。 串空间是有某个安全协议的执行中所有可能出现串的集合，即所有合法者串和攻 7 第二章串空间模型及认证测试方法相关概念串空间模型及其认证测试方法的扩展与应用 击者串所组成的集合。 串空间模型中丛是串空间的子图，它描述了局部的消息交换和因果次序，代表一 轮协议的完整运行。串空间用子项关系和结点关系来描述协议中复杂消息结构，其中 子项关系描述了协议主体间收发消息的结构，结点关系描述了结点间协议主体收发消 息的顺序逻辑。 2 2 串空间模型 2 2 1 消息项 设消息项集合a ，它的元素就是安全协议中主体之间交换的所有可能的消息集 合，称为消息项空间。项( t e r m ) 表示a 中的元素。协议的主体即可以发送项( 消息) 也可以接收项。用符号”+ ”表示发送项，用符号。”表示接收项。 定义2 1 符号项 表示一个事件，其中，o 是”+ ”或l 。，a a 。一个符号项记 为+ t 或- t ，+ t 是发送项，t 表示接收项。( a ) + 是全体符号项的有序列集合，序列集 合中的元素使用 ， 表示，n 是序列长度 定义2 2 项表示a 中的元素，用t 来表示。由下列集合生成： 文本项t ( t e x tt e r m s ) ，用t 表示，包括： ( 1 ) 协议主体名字； ( 2 ) 临时值。 密钥项k ( k e y t e r m s ) ，用k 表示，包括： ( 1 ) 对称密钥； ( 2 ) 非对称密钥。 其中：tnk = ，t ，k 是a 的原子项，不可再拆分。 在这些项上的操作包括： 加密运算e n c r ：k a a ； 连接运算j o i n ：a a a 。 记：e n c r ( k ，m ) = m ) k ，j o i n ( a , b ) = a b a 是可以通过原子项t 和密钥项k 进行加密运算和连接运算这两种代数递归定 义得到。 8 串空间模型及其认证测试方法的扩展与应用第二章串空间模型及认证测试方法相关概念 应用串空间模型证明安全协议正确性时，需要用到如下自由假设。集合a 中的自 由假设：除非明文和密钥都相等，否则没有相同的密文。自由假设规定，一个密文只 能用一种方式看待。 自由假设定义如下： 自由加密假设 m ) k _ m ) k m = m a k = k ； 自由连接假设 m i m 2 m 3 m 4 m l - - - - - r n 3 a i t l 2 = m 4 ； 连接加密互斥 m l m 2 ： m 3 k , 原子不可拆分 m l m 2 仨t u k 在消息项空间中，可以递归定义a 中的元素的子项关系亡。子项关系表示不同的 运算从所属消息项中提取子项。 定义2 3 设a 是消息空间，子项关系定义如下： ( 1 ) t e t 时，a t ：t ，当且仅当a m ； ( 2 ) k e k 时，a 亡k 当且仅当a _ k ； ( 3 ) a t - g k ，当且仅当a r g 或ar - g ) k ； ( 4 ) a 曲，当且仅当a r g 、a e h 或a 亡g h ； ( 5 ) k e k 时，只有kr g ，才能kr - g ) k 。 其中：如g ，h e a 上述子项关系反应出子项能以解密、拆分等形式从其所属的消息中提取子项。( 1 ) 和( 2 ) 子项关系说明密钥和原子消息不可再分。( 3 ) 和( 4 ) 子项关系说明以解密、拆分提 取子项。( 5 ) 子项关系说明只有密钥被应用于加密明文，攻击者才可能从对应密文中 获得密钥。 2 2 2 串空间模型的基本要素 串空间模型是一种结合定理证明和协议迹的混合方法，具有直观、简洁和严格等 特点。其基本要素由下列元素组成： 9 第二章串空间模型及认证测试方法相关概念串空间模型及其认证测试方法的扩展与应用 结点：表示协议主体间交互消息的状态； 串：表示协议运行中同一主体结点序列； 串空间：表示协议运行合法和非法串的集合； 丛：表示一轮协议的完整运行； 子项关系：表示协议主体间收发消息的结构； 结点关系：表示结点间协议主体收发消息的顺序逻辑。 定义2 4 串是一轮协议运行到某个时刻时某个协议参与者所执行的事件的序列， 用映射t r 将一个串映射到消息项空间( a ) 。，映射1 1 称为迹映射，映射的像( 某个消 息序列) 称为原像( 串) 的迹。 定义2 5 串空间是一二元组( ，t r ) ，其中：是一个串的集合，t r 表示由到a 中元素组成的序列的一个映射，称为迹映射t r ：专( a ) + 。像的代表元记为 ， ，其中o i 代表+ 或，a i 代表a 中的元素。 一个确定串空间的一些基本概念： ( 1 ) 结点是二元组 s ，其中s 且i 为满足l _ i _ l e n g t h ( t r ( s ) ) 的整数。结点集合记为 n ，称结点 属于串s 。每个结点都属于唯一的一个串。 ( 2 ) 若n _ n ，则i n d e x ( n ) = i 且s t r a n d ( n ) = i 。定义为t e r m ( n ) 为( 仃( s ) ) i ，即s 轨迹的 第i 个符号项。对应的无符号项u n s _ t e r m ( n ) = ( 仃( s ) ) i ，即s 的迹中的第i 个符号项 的无符号部分。 ( 3 ) 存在一个边n i n 2 ，当且仅当t e r m ( n 1 ) 刮a 且t e r m ( n 2 ) = a ，其中a a 。这类边意味 着结点n l 发送消息a ，结点n 2 接收消息a ，记录了串空间的一种因果连接关系。 ( 4 ) 若1 1 l = n ，n 2 = e n ，则存在边n l j n 2 。这类边表示n l 、1 1 2 发生在同 一个串上，n l 是r 1 2 在串s 上的直接因果前继，用n j + n 表示n 是n 在同一个串上 的因果前继( 不一定是直接因果前继) 。i n d e x ( n 1 ) = i n d e x ( n 2 ) 一1 。 ( 5 ) 一个无符号项t 出现在n n 当且仅当t e t e r m ( n ) 。 ( 6 ) 一个无符号项t 起源在n e n ，当且仅当t e r m ( n ) - - + t ，其中t c t e r m ( n ) ，且对所有n 的 前继n j + n 有t c t e r m ( n ) 。 ( 7 ) 一个无符号项t 唯一起源在n n ，当且仅当t 起源在唯一的结点n n 。 ( 8 ) n 加上两种边集合n l n 2 和n l j n 2 就组成一个有向图。 ( 9 ) n l j + n 2 表示在同一个串n l 上经过一个或多个边到达n 2 。 串空间图可以用结点n 、边。_ ”和边”j ”组成一个有