（交通信息工程及控制专业论文）安全协议结构及其范式研究.pdf

西南交通大学博士研究生学位论文第1 页 摘要 i n t e r a c t 的普及以及在其上各种电子商务应用的开展，使得人们越来越 关注网上应用的安全性问题。这些应用的安全性在很大程度上取决于所用安 全协议的安全性，而缺乏安全性的安全协议在开放的分布式网络环境中极易 遭致入侵者的攻击。因此，抗攻击安全协议的研究对于为现在及将来开展和 普及安全的网上业务、促进国民经济和社会发展具有极其重要的现实意义与 应用价值。 本论文以抗各种攻击为目标，研究了认证协议时序模式、y a h a l o m 协议 及其变体时序缺陷、重放攻击层次分类、基于状态与信念绑定的安全协议消 息块构造方法，以及安全协议范式与规范化。 论文首先全面分析并总结出可覆盖目前几乎所有认证协议的时序模式， 得到了可行的1 2 个带t t p ( t r u s t e dt h i r dp a r t y ，可信第三方) 的协议时序 模式和5 个无r r p 的协议时序模式。这些时序模式满足认证协议的认证性 和高效性需求，通过与现有认证协议时序的比较匹配，在一定程度上验证了 分析结果的正确。另外，所有时序模式按单向认证和双向认证进行了分类。 进一步地，根据时序对称性，对带t t p 的认证协议时序模式进行了粗略评 价。 其次，分析了y a h a l o m 协议及其变体协议的时序缺陷以及由此引起的 攻击，从时序角度改进了y a h a l o m - p a u l s o n 协议。通过此分析与改进，说明 协议时序的固有缺陷将导致协议存在安全攻击。 然后，通过分析安全协议的各种重放攻击，发现重放攻击可以针对不同 的层次以及各层次存在的不同缺陷来实施，提出了基于“同块”、“块间”、 “步间”和“协议间”4 个攻击层次的重放攻击分类。通过示例说明了利用 此分类检查协议攻击的方法与步骤。该新分类不仅包含了s y v c r s o n 的分 类，还将重放攻击扩展到了协议层次；同时与协议中消息块的静态构成结 合，指出各层次可能利用的缺陷；此外，该分类可为寻找协议的重放攻击提 供明确的方向或路线。 接着，在重放攻击层次分类基础上，通过提炼和描述各层次为避免攻击 第页西南交通大学博士研究生学位论文 应具备的状态参数和信念参数，提出了一种基于状态绑定和信念绑定的安全 协议消息块设计方法。该方法针对安全协议各个层次可能存在的缺陷，以及 设计中容易忽视的信念，分别通过状态绑定和信念绑定来解决这些缺陷，可 较大限度地提高安全协议抗攻击的能力。 最后，在上述成果的基础上，提出了安全协议范式与规范化思想。定义 了4 种安全协议范式，说明各范式之间的包含关系，并通过示例说明了非范 式协议如何逐步向各级别范式转换的过程，总结归纳了协议规范化的基本步 骤。利用协议范式，不仅有助于判定安全协议抗攻击的级别，还可以分析和 改造已有协议，使其达到一定的范式级别，从而提高其抗攻击能力。 关键词：安全协议；抗攻击；时序模式；攻击层次；状态与信念绑定； 协议范式 西南交通大学博士研究生学位论文第m 页 a b s t r a c t w i t ht h e p o p u l a r i z a t i o no fi n t e r n c t a n dt h e d e v e l o p m e n to fv a r i o u s a p p l i c a t i o n sl i k ee l e c t r o n i cb u s i n e s so ni n t e r n e t , p e o p l ep a ym o r ea t t e n t i o n st ot h e s e c u r i t yo fs u c hn e t w o r ka p p l i c a t i o n s t h es e c u r i t yo ft h e s ea p p l i c a t i o n sd e p e n d s o nt h es e c u r i t yo f t h ec r y p t o g r a p h i cp r o t o c o l s ( o rs e c u r i t yp r o t o c o l s ) m e ye m p l o y , b u tt h es e c u r i t yp r o t o c o l sl a c ko fs e c u r i t yw i l l s u f f e rv a r i o u s a t t a c k sf r o m i n t r u d e r s0 1 1o p e nd i s t r i b u t e de n v i r o n m e n t t h e r e f o r e , r e s e a r c h e so na t t a c k - r e s i s t a n ts o e n r i t yp r o t o c o l sa l es i g n i f i c a n ta n dw o r t h yf o rt h ep o p u l a r i z a t i o no f n e t w o r kb u s i n e s sa tp r e s e n ta n di nf u t u r e , t h ea c c e l e r a t i o no fn a t i o n a le 虻n o m i c a a n dt h ed e v e l o p m e n to f s o c i e t y a i m i n ga td c s i g n i n go fa t t a c k - r e s i s t a n ts e c u r i t yp r o t o c o l s ，t h ed i s s e r t a t i o n r e s e a r c h e ss u c ht o p i c sa st h es e q u e n c op a t t e r n so ft h ea u t h e n t i c a t i o np r o t o c o l s ， t h es e q u e n c ef l a w so f y a h a l o m p r o t o c o la n d i t sv a r i a n t s ，h i c r a c h i c a lt a x o n o m yo f r e p l a ya t t a c k s ，ab u i l d i n ga p p r o a c hf o rm e s s a g eb l o c k so fs e c u r i t yp r o t o c o lb a s e d o ns t a t eb i n d i n ga n db e l i e fb i n d i n g , a n dn o r m a lf o r m sa n dn o r m a l i z a t i o no f s e c u r i t yp r o t o c o l s f i r s t l y , f r o mt h ev i e w p o i n to fp r o t o c o ls e q u e n c e ，t h ed i s s e r t a t i o na n a l y z e s t h es e q u e n c ep a t t e r n s c o v e r i n ga l m o s ta l l a u t h e n t i c a t i o np r o t o c o l sw i t ha n d w i t h o u tt h et r u s t e dt h i r dp a r t y ( 1 t p ) a tp r e s e n t t w e l v ef e a s i b l es e q u e n c ep a t t e r n s o fa u t h e n t i c a t i o np r o t o c o lw i t hr r pa n d5s e q u e n c ep a t t e r n sw i t h o u t1 v r pa r e g a i n e d t h e s eg a i n e ds e q u e n c ep a t t e r n sm e e ts u c hr e q u i r e m e n t sa sa u t h e n t i c a t i o n a n dh j l g he f f e c t i v i t y b yc o m p a r i n gw i t ht h es e q u e n c e so fc u r r e n ta u t h e n t i c a t i o n p r o t o c o l s t h ea n a l y s i sr e s u l t sa r cp r o v e nt os o m ee x t e n t i na d d i t i o n , a l lo ft h e s e q u e n c ep a t t e r n sa r ec l a s s i f l e di n t ou n i l a t e r a lo rb i l a t e r a la u t h e n t i c a t i o n f u r t h e r m o r e ，i nt e r m so f t h es e q u e n c es y m m e t r y , t h es e q u e n c ep a t t e r n sw i t ht t p a r eb r i e f l ye v a l u a t e d s e c o n d l y , t h ed i s s e r t a t i o na n a l y z e st h es e q u e n c ef l a wo ft h ey a h a l o m p r o t o c o la n di t sv a r i a n t s ，a n dt h ea t t a c kl e db yt h ef l a w f r o mt h ea n g l eo f 第页西南交通大学博士研究生学位论文 s e q u e n c e , t h ey a h a l o m p a u i s o np r o t o c o l i s i m p r o v e d f r o mt h ea n a l y s i sa n d i m p r o v e m e n t , i ti ss h o w n t h a tt h ei n h e r e n tf l a wo f p r o t o c o ls a 4 u e n c ew i l lr e s u l ti n a t t a c k0 1 1t h ep r o t o c 0 1 t h i r d l y , b yt h ea n a l y s i so fv a r i o u sr 印l a ya t t a c k so ns e c u r i t yp r o t o c o l s , i ti s f o u n dt h a tt h er e p l a ya t t a c k sc a nb el a u n c h e da ld i 丘缸l e v e l sa n du s i n g d i f f e r e n tf l a w se x i s t i n ga tl e v e l s t h u s at a x o n o m yo fr e p l a ya t t a c k sb a s e do n a t t a c kh i e r a r c h yi sp r o p o s e d0 1 1f o u rl e v e l so fa t t a c l 【so i ls e c u r i t yp r o t o c o l s ，i e m e s s a g eb l o c k , i n t e r - b l o c ki n s i d es t e p ，i n t e r - s t e p s ，a n di n t e r - p r o t o c o l s m o r e o v e r , t h ea p p r o a c ha n ds t e p so fc h e c k i n ga t t a c k sf o rp r o t o c o l su s i n gs u c hn 哪 t a x o n o m ya r ed e m o n s t r a t e d t h et a x o n o m yn o to n l yc o n t a i n st h es y v a r s o n t a x o n o m yo fr e p l a ya t t a c k s ，b u ta l s oe x t e n d st h er e p l a ya t t a c ku pt ot h ep r o t o c o l l e v e l m e a n w h i l e , t h et a x o n o m yp o i n t so u ta v a i l a b l ef l a w sa te a c hl e v e lb y c o m b i n i n gw i t h t h es t a t i cc o n s t r u c t i o no ft h em e s s a g eb l o c ki np r o t o c o l s a d d i t i o n a l l y , t h et a x o n o m y c a l ld i r e c tt oc h e c kr e p l a ya t t a c k so np r o t o c o l s f o u r t h l y , o nt h eb a s i so ft h eh i e r a r c h yo fr e p l a ya t t a c k s ，t h ep a r a m e t e r s n e c e s s a r yf o rs e c u r i t yp r o t o c o lt oa v o i dv a r i o u sa t t a c k sa r ea n a l y z e d , w h i c ha r e c l a s s i f i e da st h es t a t ep a r a m e t e ra n dt h eb e l i e fo n e , a n dt h e n , ab u i l d i n ga p p r o a c h f u rt h em e s s a g eb l o c k so fa t t a c k r e s i s t a n ts e c u r i t yp r o t o c o l si sp r o p o s e db a s e do n t h es t a t e - b i n d i n ga n db e l i e f - b i n d i n g a i m i n ga tp o s s i b l ef l a w sa tv a r i o u sa t t a c k l e v e l sa n dt h eb e l i e fe a s yt ob ei g n o r e d ，t h i sa p p r o a c hc a ns o l v et h e mb ys t a t e - b i n d i n ga n db e l i e fb i n d i n g , a n dt h u st h ea t t a c k - r e s i s t a n ta b i l i t yo ft h es e c u r i t y p r o t o c o l s i se n h a n c e dt ol a r g ee x t e n t f i n a l l y , o nt h eb a s i so fa b o v ea c h i e v e m e n t s ，a ni d e aa b o u tp r o t o c o ln o r m a l f o r m ( p n f ) a n dn o r m a l i z a t i o ni sp r o p o s e d ，a n df o u rp n f sa r ed e f i n e d t h e ni ti s d e m o n s t r a t e dh o wan o n p n fp r o t o c o li st r a n s f o r m e dg r a d u a l l yt op n fd e g r e e a s o t h ee l e m e n t a r ys t e p so f p r o t o c o ln o r m a l i z a t i o na s u m m a r i z e d t h ep n f i d e ai sh e l p f u ln o to n l yt oj u d g et h ea t t a c k - r e s i s t a n tl e v e lf o rs o c 加r i t yp r o t o c o l s ， b u ta l s ot oa n a l y z ea n dr e f o r mt h ee x i s t i n gp r o t o c o l s ，s oa st om a k et h e mr o a c h s o m ep n fd e g r e ea n dt oe n h a n c et h e i ra b i l i t i e so f a t t a c kr e s i s t a n c e 西南交通大学博士研究生学位论文第v 页 k e yw o r d s ：s e c u r i t yp r o t o c o l ；a t t a c kr e s i s t a n c e ；s c c l u c n c op a t t e r n ；a t t a c k h i e r a r c h y ；s t a t e - b i n d i n g & b e l i e f - b i n d i n g ；p r o t o c o ln o r m a lf o r m 第x 页西南交通大学博士研究生学位论文 符号说明简要对照 以下为本论文中使用的一些常见的符号简要说明，详细的符号说明请参 见第2 章2 3 2 节的符号约定。 彳、b ： s ： ，： 氲y ： 墨、j ： 岛： ： k ： 肌： 珊) 足： 枷) j ? ： ( f 力石一y ：m ： 几的一y m ： 轴玎1 9 ：m ： 特定的诚实主体a l i c e 和b o b 。 可信第三方( t t p ) 服务器。 入侵者( i n t r u d e r ) 。 一般性的主体，可以是彳，口或& 甚至是厶 x 的公钥和私钥。 石和y 的长期共享密钥。 x 和r 之间的短期会话密钥。 一般性的加密密钥，可以是长期共享密钥或短期会话密 钥，也可以公钥。 z 生成的一次性随机数( n o n c e ) 。 加密消息块。 签名消息块。 在第f 轮的第，步，z 向】，发送消息地 j 假冒x 向】，发送消息m 。 ，中途拦截x 发给】，的消息从 西南交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学 校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查 阅和借阅。本人授权西南交通大学可以将本论文的全部或部分内容编入有关 数据库进行检索，可以采用影印、缩印或扫描等复印手段保存和汇编本学位 论文。 本学位论文属于 1 保密口，在年解密后适用本授权书； 2 不保密团，使用本授权书。 ( 请在以上方框内打“4 ”) 学位论文作者签名口阚知彳 f 醐：1 钆啪粕 指导教师签名：彳犬_ 歹 日期： 矽年z 月，卯 西南交通大学 学位论文创新性声明 本人郑重声明：所呈交的学位论文，是在导师指导下独立进行研究工作 所得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或 集体已经发表或撰写过的研究成果。对本文的研究做出贡献的个人和集体， 均已在文中作了明确的说明。本人完全意识到本声明的法律结果由本人承 担。 本学位论文的主要创新点如下： ( 1 ) 从认证性、简洁高效性角度，全面分析了两方( 无t t p ) 和三方 ( 带t r p ) 认证协议的原子时序模式，通过与现有认证协议对序的比较匹 配，验证了分析结果的正确。进一步地，按单向认证和双向认证对所有时序 模式进行了分类；根据时序对称性，评价了带r r p 的三方认证协议时序模 式。( 详见3 1 3 4 ) ( 2 ) 提出协议时序缺陷和时序攻击概念。分析发现了y a h a l o m 协议及 其变体时序的缺陷以及由此引起的时序缺陷攻击，从时序角度改进了 y a h a l o m p a u l s o n 协议。通过此分析与改进，说明了协议时序的固有缺陷将 导致协议存在安全攻击。( 详见3 5 节) ( 3 ) 通过分析安全协议的各种重放攻击，发现重放攻击可以针对安全 协议不同的层次以及各层次存在的不同缺陷来实施，提出了基于“同块”、 “块间”、“步间”和“协议间”4 个攻击层次的重放攻击分类。该新分类不 仅包含了s y v e r s o n 的分类，还将重放攻击扩展到了协议层次；同时与协议 中消息块的静态构成结合，指出各层次可能利用的缺陷；此外，该分类可为 寻找协议的重放攻击提供明确的方向或路线。( 详见第4 章) ( 4 ) 通过提炼为避免各层次攻击应具备的状态参数和信念参数，提出 了一种基于状态绑定和信念绑定的安全协议消息块设计方法。该方法给出了 在协议设计时为避免攻击所需的一些参数，以及消息块构造时参数绑定的具 体方式，可为协议的设计提供具体的指导。( 详见第5 章) ( 5 ) 提出安全协议范式及规范化概念与方法。在( 3 ) 和( 4 ) 基础 上，定义了4 种安全协议范式，说明了非范式协议如何逐步向各级别范式转 换的过程，并归纳了协议规范化的基本步骤。利用范式，有助于判定安全协 议抗攻击的级别，范式级别越高，其抗攻击的能力愈强。还可以利用范式来 分析和改造已有协议，使其达到一定的范式级别，从而提高其抗攻击能力。 利用规范化步骤，将低安全级别的范式向高安全级别的范式转换，亦可将安 全协议的抗攻击能力提高到所需要的程度。( 详见第6 章) 学位论文作者签名：召司务文 日期：枷1 年i 月i 莎日 西南交通大学博士研究生学位论文第1 页 1 1 研究背景与意义 第1 章绪论 i n t e r n e t 的普及以及在其上各种商业交易应用( 如网上购物、电子转 账、电子支付等) 和其他应用业务( 如电子合同、电子拍卖、网上投票等) 的开展，使得人们越来越关注网上应用的安全性问题。这些应用的安全性在 很大程度上取决于所用安全协议( 亦称密码协议，s e c u r i t yp r o t o c o l 或 c r y p t o g r a p h i cp r o t o c 0 1 ) 的安全性，而缺乏安全性的安全协议在开放的分布 式网络环境中极易遭致入侵者( 或称攻击者，i n t r u d e r 或a t t a c k e r ) 的攻 击。因此，抗攻击安全协议的研究对于为现在及将来开展和普及安全的网上 业务、促进国民经济和社会发展具有极其重要的现实意义与应用价值。 从1 9 7 8 年第一个安全协议【l 】的提出至今，已有很多安全协议相继出 现，如k e r b e r o s 协议 2 - 4 1 、r p c ( r e m o t ep r o c e d u r ec a l l ，远过程调用) 5 , 6 1 等。然而，由于安全目标本身的微妙性、协议运行环境的复杂性、攻击者模 型的复杂性、安全协议本身的高并发性 7 1 ，以及安全协议交换的消息之间存 在着复杂的关系和制约，使得安全协议的设计极易出错，出现各种易被攻击 者利用的安全缺陷或漏洞。甚至，一些安全协议在闯世多年后仍被发现存在 严重的安全缺陷。例如，1 9 7 8 年发表的n s p k 协训1 】被l o w e t 8 】于1 9 9 5 年 发现其存在安全缺陷，其间过去了大约1 7 年之久，由此可见安全协议设计 的困难性非同寻常。 本论文将研究与安全协议相关的时序与攻击层次，以及以攻击层次为基 础的安全协议消息块设计方法与协议范式，希望为安全协议的设计提供具有 指导性的规范化理论与方法，丰富安全协议设计理论，促进安全协议的工程 化设计与应用。 1 2 安全协议研究现状 本节将从以下方面介绍与本课题相关的研究现状：安全协议的缺陷 与攻击；安全协议的分析方法；安全协议的设计原则与方法。 第2 页西南交通大学博士研究生学位论文 1 2 1 安全协议的缺陷与攻击 1 9 7 8 年，n e e d h a m 和s c h r o e d e r 【1 】提出了第一个安全协议，即著名的 n e n d h a m s c h r o e d e r 协议，该协议包括两种类型的协议，即n s s k ( n e e d h a m s c h r o e d e rs y m m e t r i ck e y ) 协议和n s p k ( n e e d h a m s c h r o e d e r p u b l i ck e y ) 协议。此后，许多安全协议相继被提出，如d e n n i n g s a c c o 协议 1 9 、o t w a y - r e e s 协议【1 0 1 、y a h a l o m 协议【1 1 1 、w i d e - m o u t h e d f r o g 协议【i l 】、 w o o l a i n 协议【1 2 1 、c c i t tx 5 0 9 协谢1 3 1 等等。1 9 9 7 年，c l a r k 和j a c o b 在文 献 1 4 】中按“不带t t p 的对称密钥协议( s y m m e t r i ck e yp r o t o c o l sw i t h o u t t r u s t e dl h i r dp a r t y ) ”、“利用密码检查函数的认证( a u t h e n t i c a t i o nu s i n g c r y p t o g r a p h i cc h e c kf u n c t i o n s ) ”、“带t t p 的对称密钥协议( s y m m e t r i ck e y p r o t o c o l si n v o l v i n gt r u s t e d t h i r d p a r t i e s ) ”、“按传统密钥加密的签名 ( s i g n a t u r e sw i t hc o n v e n t i o n a lk e ye n c r y p f i o n ) ”、“对称密钥重复认证协议 ( s y m m e t r i ck e yr e p e a t e da u t h e n t i c a t i o np r o t o c o l s ) ”、“不带t t p 的公钥协议 ( p u b f i ck e yp r o t o c o l sw i t h o u tt r u s t e dt h i r dp a r t y ) ”和“带t t p 的公钥协议 ( p u b f i ck e yp r o t o c o l sw i t ht r u s t e dt h i r dp a r t y ) ”等等，对当时出现的一系列 有研究意义和实用价值的安全协议进行了分类和分析。目前，在i n t e r n e t 网 上有一个共享的安全协议开放资源库s p o r e ( s e c u r i t yp r o t o c o lo p e n r e p o s i t o r y ) 1 5 1 ，从中可以查询到许多典型的安全协议及其改进版。 然而，所有这些协议以及它们的改进版不断地被分析并发现存在有这样 或那样的安全缺陷或攻击【1 ，9 ，1 睨。例如，1 9 8 1 年d e n n i n g 和s a c c o 9 】发现 n s s k 协议存在新鲜性攻击( f r e s h n e s sa t t a c k ) ，此外，该协议还被发现存在 拼接攻击( s p l i c i n ga t t a c k ) 圈、初始化攻击( i n i t i a l i z a t i o na t t a c k ) 【2 3 1 等； 1 9 9 5 年，l o w 发现n s p k 协议存在一种重放攻击( r e p l a ya t t a c k ) ：1 9 9 7 年，c l a r k 和j a c o b 【1 4 】总结并分析了当时的安全协议及其存在的若干攻击。 安全协议的缺陷可能由不完整或错误的协议规格说明( s p e c i f i c a t i o n ) 引起。不过，即使是正确的说明也不一定能保证协议某种实现的正确性。 1 9 9 4 年，c a r l s e n 1 8 搬据缺陷来源，将密码协议缺陷分为以下3 类：功能 性说明缺陷( f u n c t i o n a ls p e c i f i c a t i o nf l a w s ) ，由协议的高层说明逻辑缺陷引 起；依赖于实现的缺陷( i m p l e m e n t a t i o n d e p e n d e n tf l a w s ) l l ”，因协议说 明导致实现出现缺陷；实现缺陷( i m p l e m e n t a t i o nf l a w s ) ，正确的说明被 西南交通大学博士研究生学位论文第3 页 不正确实现。 1 9 9 7 年，g r i t z a l i s 和s p i n e l l i s l 2 l 】在c a r l s e n 的缺陷分类基础上，根据缺 陷病理学和攻击方法，将缺陷细分为以下6 类：基本协议缺陷 ( e l e m e n t a r yp r o t o c o lf l a w s ) ，因协议对攻击只提供很少的保护或根本就没 有提供保护而引起；口令密钥猜测缺陷( p a s s w o r d k e yg u e s s i n g f l a w s ) ，因用户的密钥空间小或者协议使用伪随机密钥而引起；陈旧消 息缺陷( s t a l em e s s a g ef l a w s ) ，因协议中的消息未包含时鲜值( n o n c e ) 而 引起；并行会话缺陷( p 盯m i ds e s s i o nf l a w s ) ，利用此缺陷攻击者通过恰 当的协议消息交换可获得所期望的信息；内部协议缺陷( i n t e r n a l p r o t o c o lf l a w s ) ，指协议中至少有一个协议主体不能完成所有必需的活动而 导致的缺陷：密码系统缺陷( c r y p t o s y s t e mf l a w s ) ，指协议中使用的密码 算法导致协议不能完全满足所要求的机密性、认证等需求而产生的缺陷。 为清楚地认识对安全协议的各种攻击，安全专家对已出现的攻击进行了 总结与分类。1 9 9 4 年，s y v c r s o n 2 0 基于消息源( m e s s a g eo r i g i n ) 和消息目 的( m e s s a g ed e s t i n a t i o n ) ，得到了著名的消息重放攻击分类( 以下称 s y v e r s o n 分类) 。s y v e r s o n 分类将重放攻击分为轮内攻击( r u ni n t e r n a l a t t a c k s ) 和轮外攻击( r u ne x t e r n a la t t a c k s ) 两种。轮内攻击分为偏射 ( d e f l e c t i o n ) 和直接重放( s t r a i g h tr e p l a y ，表示意定的收方收到消息，但 被延时了) ；轮外攻击分交错( i n t e r l e a v i n g , 又分偏射和直接重放) 和经典 重放( c l a s s i cr e p l a y , 也分偏射和直接重放) 。所有偏射均分为：反射 ( r e f l e c t i o n ) 回发方和偏射到第三方。1 9 9 6 年，c l a r k 和j a c o b l 2 3 】总结了当 时对认证协议的若干攻击，如：新鲜性攻击、类型缺陷攻击( t y p ef l a w a t t a c k ) 、并行会话攻击( p a r a l l e ls e s s i o na t t a c k ) 、依赖实现的攻击 ( i m p l e m e n t a t i o n d e p e n da t t a c k ) 和绑定攻击( b i n d i n ga t t a c k ) 等。2 0 0 0 年，c h o n gx u 等 z 4 1 基于攻击者发动攻击的目标和其扮演的角色，将攻击分 为：认证击破( a u t h e n t i c a t i o nb r e a c h ) ，攻击者可假冒合法的发起者与响 应者；认证击破以及秘密泄露( a u t h e n f i e a t i o nb r e a c h + s e c r e tr e t r i e y a l ) ， 攻击者假冒合法的秘密接收者；认证击破以及秘密重活( a u t h e n t i c a t i o n b r e a c h + s e c r e tr e v i v a l ) ，在该攻击中攻击者可以假冒秘密的生成者：认 证击破以及秘密注入( a u t h e n t i c a t i o nb r e a c h + s e c r e ti n j e c t i o n ) ，在该攻击中 第4 页西南交通大学博士研究生学位论文 攻击者可以假冒秘密的生成者；消息生成( m e s s a g eg e n e r a t o r ) ，攻击者 从运行的协议中获得其所需要的消息；秘密泄露( s e c r e tr e t r i e v a l ) ，攻 击者可获得协议中的秘密；会话劫持( s e s s i o n a e l d n g ) ，攻击者在协 议认证阶段后和秘密接收前接过协议会话。 协议缺陷或攻击的不断发现，使得安全领域的专家和学者考虑并研究如 何避免各种攻击。例如，1 9 9 3 年g o n g 等瞄l 提出通过引入一种足够大的随 机干扰数( c o n f o u n d e r ) 来阻止口令猜测攻击( p a s s w o r dg u e s s i n ga t t a c k ) 的方法；1 9 9 7 年a u r a 【冽提出了阻止重放攻击的5 条策略；2 0 0 0 年h e a t h e r 等【2 刀提出了阻止类型缺陷攻击的t y p e - t a g g i n g 方法。2 0 0 2 年m a l l a d i 等提 出采用会话标识和组件标识来阻止s y v e r s o n 分类中所有重放攻击的一般解 决方法。 国内学者在发现安全协议攻击方面做了一定的研究工作，例如，1 9 9 9 年王贵林掣2 9 】从协议设计和实现中的缺陷或错误出发研究了安全协议的攻 击方法分类；2 0 0 1 年王贵林等口0 】发现了3 个协议的6 种新的攻击方法，分 别是a ( o ) 协议 3 j 的3 种攻击、n s s k 协议和o t w a y - r e e s 协议及其改进版【3 2 i 各一种攻击；2 0 0 4 年刘秀英等【3 3 】从协议的保密性和认证性入手，结合攻击 者采用的攻击类型对t m n 协谢3 4 】的1 9 种攻击进行了系统分类；2 0 0 5 年卓 继亮等1 3 5 】从攻击者的能力和攻击后果两个角度，提出一种新的安全协议攻 击分类，分析了不同攻击类型的特点与机理，并在此基础上探讨了安全协议 的一种安全性评估框架；2 0 0 6 年缪祥华掣3 6 】发现了一种不需要泄漏会话密 钥而攻击n s s k 协议的方法。 1 2 2 安全协议的分析方法 安全协议是否存在安全缺陷，或者能否满足其安全目标，或者是否安 全，需要通过各种方法来分析验证。目前，对于安全协议的分析主要有3 种 方法【3 7 j 引，即：基于推理的结构性方法( i n f e r e n c e c o n s t r u c t i o nm e t h o d s ) 、 基于攻击的结构性方法( a t t a c k - c o n s t r u c t i o nm e t h o d s ) 和基于证明的结构性 方法( p r o o f - c o n s t r u c t i o nm e t h o d s ) 。 西南交通大学博士研究生学位论文第5 页 1 2 2 1 基于推理的结构性方法 基于推理的结构性方法主要是利用模态逻辑从用户收发的消息出发，通 过一系列的推理公理来分析协议是否满足其安全目标。这类方法中，最著名 的是由b u r r o w s ，a b a d i 和n e e d a m 于1 9 8 9 年提出的分析认证协议的b a n 逻辑【l l 】。 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 tx 5 0 9 协议，还发现了一些 协议中存在冗余，如：n e e d h a m s c l a r o e d e r 协议、k e r b e r o s 协议、o t w a y - r e e s 协议和c c i t tx 5 0 9 协议。不过，由于b a n 逻辑存在一些问题，如逻 辑语义不完备、理想化过程不标准、未考虑协议不同轮的交互等等。当然， 尽管有这些问题，仍然不能否认b a n 逻辑是安全协议形式化分析的一个里 程碑。 为改进b a n 逻辑中存在的问题，许多研究者在b a n 逻辑的基础上提 出了其它一些逻辑，如g n y 逻辑【3 9 1 、a t 逻辑 4 0 1 、s v o 逻辑，等等。由 于这些逻辑都是b a n 逻辑基础上的改进或扩展，故统称为b a n 类( b a n 1 i k e ) 逻辑。b a n 或b a n 类逻辑只用于推理认证性，不能用于证明秘密 性。此外，由于b a n 或b a n 类逻辑缺乏清晰的语义，很难提供可信的认 证性证明。 1 9 9 5 年，k a i l a r 提出了一种用于分析电子商务协议中可追究性 ( a c c o u n t a b i l i t y ) 的k a i l a r 逻辑【4 2 】，它是目前电子商务协议中主要的形式 化分析工具。 国内的研究者在基于推理的结构性方法方面也做了一些有益的研究。例 如，1 9 9 9 年周典萃等【4 那分析了k a i l a r 逻辑存在的3 种缺陷，即：不能分 析协议的公平性：对协议语句的解释及初始化假设是非形式化的，存在 局限性；无法处理密文。2 0 0 1 年，他们又提出了一种新的用于分析电子 第6 页西南交通大学博士研究生学位论文 商务协议的形式化分析方法】。2 0 0 4 年侯峻峰等h 5 1 在b a n 逻辑基础上提 出了一种新的安全协议的形式化验证逻辑。2 0 0 6 年缪祥华晰1 提出一种分析 和设计安全协议的新逻辑。 1 2 2 2 基于攻击的结构性方法 基于攻击的结构性方法是通过构造基于协议算法代数性质的可能的攻击 集合来分析协议，其目标是确保协议的认证性、正确性或安全特性。依据其 理论基础，该方法又分为以下3 类： 基于一般目的验证语言的方法。这类方法主要证明安全协议的正确 性，其不足是忽略了安全性，具有代表性的包括：有限状态机( f i n i t es t a t e m a c h i n e , f s m ) 4 7 , 4 8 1 、一阶谓词逻辑扩展 4 9 1 和k aj o 如1 、m u 岫验证系统 5 1 , 5 2 1 、c s p ( c o m m u n i c a t i o ns e q u e n c ep r o c e s s 通信顺序进程) 及其模型检 测工具f d r ( f a i l u r ed i v e r g e n c er e f i n e m e n tc h e c k e r , 故障偏差精炼检查器) 5 3 5 4 、l o t o s 5 5 1 、a s t r a l l 5 6 1 、小系统模型理论【5 7 1 ，等等。这类方法中最 经典