（计算机软件与理论专业论文）安全协议及其ban逻辑分析研究.pdf

贵州大学博士学位论文安全协议及其b a n 逻辑分析研究 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究所取得的成果。除文中已经注明引用的内容外，本论 文不包含任何其他个人或集体已经发表或撰写过的科研成果。对本 文的研究曾做出重要贡献的个人和集体，均已在文中以明确方式标 明。本人完全意识到本声明的法律责任由本人承担。 论文作者签名 日期： ! ! ! ) 生立旦 关于学位论文使用授权的声明 本人完全了解贵州大学有关保留、使用学位论文的规定，同意 学校保留或向国家有关部门或机构送交论文的复印件和电子版，允 许论文被查阅和借阅；本人授权贵州大学可以将本学位论文的全部 或部分内容编入有关数据库进行检索，可以采用影印、缩印或其他 复制手段保存论文和汇编本学位论文。 ( 保密论文在解密后应遵守此规定) 论文作者签名导师签名：日期：! ! ! ) 生上旦 青州大学计算机软件与理论研究所 摘要 随着计算机网络的广泛应用和各种应用领域的不断扩大，信息的安全问题成为大家关注的 焦点。信息安全( i n f o r m a t i o ns e c u r i t y ) t 司题从某种程度上已成为制约计算机网络应用的一个瓶 颈。传统的对信息的安全性处理是依赖于好的加解密算法来保证。但是，随着网络应用的深入， 仅仅依赖一个好的加解密算法已经不能很好地解决信息的安全问题，它需要安全理论、安全措 施和安全技术来保证。在这些信息安全的理论、措施和技术中，安全协议起着至关重要的作用 在实际应用中，人们需要可信的机制来为通信的各方进行身份认证和分发密钥，这就迫使人们 研究和设计出了各种安全协议( s e c u r i t yp r o t o c 0 1 ) 。然而事与愿违，已有的安全协议往往被证实 并不如它们的设计者所期望的那样安全，开放的、复杂的网络环境使得攻击者可利用安全协议 设计中的缺陷和漏洞来实施各种各样的攻击，从而非法获取网络资源，窃取非授权使用的信息， 危及到网络的安全和应用。因此，安全协议自身的安全性成了网络安全的关键问题之一。考量 和分析一个安全协议的安全性称为安全协议的分析。目前，使用最为广泛的安全协议分析方法 是各种形式化分析方法，即采用各种形式化的语言或模型，为安全协议建立模型，并按照规定 的假设、分析和验证规则，验证安全协议的安全性。 本文以如何保障安全协议的安全性为切入点，研究和分析了与安全协议息息相关的密码学 的诸多问题，例如，对称密码体制、公钥密码体制、椭圆曲线密码体制、数字签名等基本算法。 进一步讨论了具有代表性的认证协议，密钥管理和分配的方法等。研究和分析了安全协议的非 形式化分析的方法和形式化分析方法，重点是对b a n 逻辑的分析和讨论，并利用b a n 逻辑 分析了部分认证协议。 本文通过b a n 逻辑的实例分析，说明了b a n 逻辑在分析认证协议中具有积极的作用， 发现了认证协议中一些原来没有发现的漏洞和冗余。但是，文中通过对两个认证协议的分析， 指出了b a n 逻辑在对中间人攻击和口令猜测攻击的安全协议分析中存在的缺陷，并对被分析 的认证协议进行了改进。最后提出了基于安全协议的电子公文安全流转方案和基于安全协议的 消息交换方案。将椭圆曲线密码体制引入到消息交换方案中，减少了消息交换中数字签名和密 钥协商的计算量，也利用椭圆曲线离散对数的难解性来增强了消息交换的安全性。 关键词安全协议：b a n 逻辑；形式化分析；消息交换；椭圆曲线 中图分类号t p 3 9 3 0 8 文献标识码a 4 - 青州大学博士学位论文 安全协议及其b n 逻辑分析研究 a b s t r a c t n o w a d a y s , i n f o r m a t i o ns e c u r i t yh a sa l r e a d yb t o m cab o t f l e n e e kt h a tr e s t r i c t sa p p l i c a t i o n so f c o m p u t e rn e t w o r k t h es e c u r i t yo fi n f o r m a t i o nn e e d sn o to n l ys o 鹏g o o de o c r y p t i o na l g o r i t h m sb u t a l s os o l e es e c u r i t yt h e o r i e s s e c u r i t yl m a s u l - e sa n ds e c u r i t yt e c h n o l o g i e s i nt h et h e o r i e s , i t * a s u r c $ a n dt e c h n o l o g i e s ，t h es e c u r i t yp r o t o c o li s p l a y i n gv e r yi m p o r t a n tr o l e i np r a c t i c a la 秘岫t i 墨， p e o p l er e q u i r e sc r e d i b l em e c h a n i s mt ov c f i l 3 ，i d e n t i t yo fc o m m u n i c a t i n gp a r t i e sa n dd i s t r i b u t ek e y s t h i sf o r c e sp e o p l et oh a v et or e s e a r c ha n dd e s i g nv a r i o u ss e c u r i t yp r o t o c o l s g e n e r a l l ys p e a k i n g , s e c m i t yp r o t o c o l sa r ep r o t o c o l st h a tu s ec r y p t o g r a p h yt od i s t r i b u t ek e y sa n da u t h e n t i c a t ep r i n c i p a l s a n dd a t ao v e ran e t w o r ka n da r eab a s i cg u a r a n t e eo fs e c u r ec o m m u n i c a t i o nt h r o u g ho p e na n d u n p r o t e c t e dn e t w o r k b u tp r o v e db yp r a c t i c e ，d e s i g na n da n a l y s i so fs e c u r i t yp r o t o c o lh a sb e e n r e c o g n i z e da sm u c hm o r ed i f f i c u l tt h a ni n i t i a l l yt h o u g h ta n dn d sar i g o r o u sf o r m a la p p r o a c ht o p r o v i d ec r e d i b l ea n a l y s i sg u a r a n t e e t h ec o m p l i c a t e dn e t w o r ke n v i r o n m e n tm a k e st h ea t t a c k e r st o e n a b l er e a l i z i n gv a r i o u sa t i a c bb ym e a u so ff l a w sa n dl e a k so fs e c u r i t yp r o t o c o l s , i l l e g a l l yo b t a i n t h en e t w o r kr e s o 眦c e sa n du n a u t h o r i z e di n f o r m a t i o n , a n dc o n s e q u e n t l ye n d a n g e rs e c u r i t ya n d a p p l i c a t i o no fan e t w o r k t h e r e f o r e , t h es e c u r i t yo fs e c u r i t yp r o t o c o l sh a sb e c o m eo n eo ft h ek e y p r o b l e m so fn e t w o r ks e c u r i t y t ov e r i f yt h es e c u r i t yo fs e c u r i t yp r o t o c o l si sc a l l e ds e c u r i t yp r o t o c o l a n a l y s i sa n dac u r r e n tr e s e a r c hh o ts p o to nn e t w o r ks e c u r i t y a tp r e s e n t ，m o s tw i l d l yu s e dp r o t o c o l v e r i f i c a t i o nm e t h o di sv a r i o u sf o r m a lo n e s b ym e a n so ft h ef o r m a lm o t h o d s , w em a ym a k eam o d e l f o rs e x u r i t yp r o t o c o lu s i n gf o r m a ll a n g u a g eo rm o d e la n dt h e nv m f yi t s s e c u r i t ya c c o r d i n gt o a s s u m p t i o n sa n dv e r i f i c a t i o nr u l e s h o wt oe u s m et h es e c u r i t yo fs e c o r i t yp r o t o c o li sm n s t a r t i n gp o i n to nn e t w o r ks e c u r i t yi nt h e p a p e r w er e s e a r c ha n da n a l y z es y m m e t r i ck e yc r y p t o g r a p h , p u b l i ck e yc r y p t o g r a p h , e l l i p t i cc u r v e c r y p t o g r a p h , a n dd i g i t a ls i g n a t u r ea l g o r i t h m s ，e t c w ef u r t h e l d i s c u s ss o l n et y p i c a la u t h e n t i c a t i o n p r o t o c o l s ，k e ym a n a g e m e n ta n dd i s t r i b u t i o nm e t h o d s ，e t c ，a n da n a l y z ei n f o r m a lm e t h o d sa n df o r m a l m e t h o d so fs e c u r i t yp r o t o c o l ，e s p e c i a l l yb a nl o g i c a n dt h e n , w ea n a l y z eaf e wa u t h e n t i c a t i o n p r o t o c o i sw i t hb a nl o g i c s o m ee x a m p l e st h a th a v eb e e na n a l y z e dw i t hb a n ，h a v es h o w nt h a tt h eb a nl o g i ch a st h e a c t i v ee f f e c ti na n a l y z i n gt h ea u t h e n t i c a t i o np r o t o c o l s ，a n df i n d ss o m ef l a w sa n dr e d u n d a n c yt h a t w e r en o td i s c o v e r e db e f o r e b u tt h r o u g ha n a l y z m gt w oa u t h e n t i c a t i o np r o t o c o l s ，b a nl o g i cd e f e c t i np r o t o c o la n a l y s i sa b o u tm a n - i n - t h e - m i d d l ea t t a c ka n dk e yg u e s s i n ga t t a c kw a sp o i n t c do u t ，a n dt h e i m p r o v e dp r o t o c o la g a i n s tam a n - i n - t h e - m i d d l ea t t a c ka n do n ea g a i m tk e yg u e s s i n ga t t a c ka r eg i v e n i nt h ep a p e r f i n a l l y , w ep u tf o r w a r dt h r e es e c u r i t ys c h e m e sb a s e do ns e c u r i t yp r o t o c a l ，t h ef i r s tf o r e l e c t r o n i co f f i c i a l d o c u m e m si n t e r c h a n g eb a s e do ne c c ，t h es e c o n df o rm e s s a g ei n t e r c h a n g eb a s e d 一5 一 贵州大学计算机软件与理论研究所 o i le c c , a n dt h el a s tf o rm e s s a g ei n t e r c h a n g es i g n e r y p t i n gb a s e do ne c c t h ee l l i p t i co l i v e c r y p t o g r a p h i ct e c h n i q u eh a sb e e nb r o u g h ti nm e s s a g ei n t e r c h a n g es c h e m e s t h ep r i m a r ya d v a n t a g e t h a te l l i p t i cc l l l v es y s t e m sh a v eo v e rs y s t e m sb a s e do nt h em u l t i p l i c a t i v eg r o u po faf i n i t ef i e l d ( a n d a l s oo v c ts y s t e m sb a s e do i lt h ei n t r a c t a b i l i t yo fi n t e g e rf a c t o r i z a t i o n ) i st h ea b s e n c eo fa s u b e x p o n e n t i a l - t i m ea l g o r i t h mt h a tc o u l df f m dd i s c r e t el o g a r i t h m si nt h e s eg r o u p s c o n s e q u e n t l y , w c c u s ea ne l l i p t i cc i h n eg r o u pt h a ti ss m a l l e ri ns i z ew h i l em a i n t a i n i n gt h es r i i kl e v e lo fs e c u r i t y t h er e s u l ti ss m a l l e rk e ys i z a $ ，b a n d w i d t hs a v i n g s , a n df a s t e ri m p l e m e n t a t i o n s i no t h e rw o r d s ，l | s c o fe l l i p t i cc u r v ec r y p t o g r a p h i ct e c h n i q u e sp r o v i d eg r e a t e rs e c u r i t y i n gf e w e rb i t s ，r e s u l t i n gi na p r o t o c o lw h i c hr e q u i r e sl o wc o m p u t a t i o n a lo v e r h e a d , a n dt h u s ，m a k i n gi ts u i t a b l ef o rd i g i t a l s i g n a t u r e , k e ya g r e e m e n ta n de x c h a n g ea n dm o r es o $ n l f ea n df a s t e rm e s s a g ei n t e r c h a n g ei nn e t w o r k k e yw o r d s ：s e c u r i t yp r o t o c o l ；b a nl o g i c ；f o r m a la n a l y s i s ；m e s s a g ei n t e r c h a n g e ；e l l i p t i cc u r v e - 6 - 责州大学博士学位论文安全协议及其b a n 逻辑分析研究 第一章引言 安全协议( s e c 耐t yp r o t o c 0 1 ) 是以密码学( c r y p t o g r a p h y ) 为基础的协议，在网络和信息系统的 安全中占据重要的地位。安全协议的目标与网络和信息系统的安全性有关例如，网络环境中 认证主体的身份：在主体之间协商和分配会话密钥( s e s s i o nk e y ) ；实现机密性( c o n f i d e n t i a l i t y ) 、 完整性o n t e g r i t y ) 、非否认性( h o n r e p u d i a t i o n ) 和公平性0 2 a i r n e s s ) 等功能要求。在一个开放的网 络环境中，人们通过安全协议来实现安全信息交换从而达到共享网络资源的目的。然而，在实 际应用中大量事例证明，安全协议大多都存在着某些缺陷和漏洞，给计算机网络应用的安全性 带来了极大的隐患。安全协议本身的安全性如何来得到保证，这一问题已成为网络和信息安全 的一个至关重要的问题。因此，对安全协议的研究已发展成为世界上信息与网络安全方面的一 个主流研究方向。 1 1 研究背景及意义 信息安全( i n f o r m a t i o ns e c u r i t y ) 问题随着计算机网络的应用范围和应用领域的不断扩大而 受到人们的越来越多的关注，从某种程度上说，信息安全问题已成为制约计算机网络应用的一 个瓶颈，并且随着计算机网络的迅猛发展，日益变得突出。早期的信息的安全性主要是依赖好 的加解密算法，然而，随着网络的开放性、复杂化和应用的多样性，信息的安全性已经不是仅 仅依赖一个好的加密算法就可以得以解决的问题，它需要一些综合的安全理论( s e c u r i t y t h e o r y ) 、安全措施( s e c u r i t ym e a s u r e ) 和安全技术( s e c u f i t yt e c h n o l o g y ) 来保证。在这些理论、措 施和技术中，安全协议起着至关重要的作用。在实际应用中，人们需要可信的机制来为通信实 体进行身份认证和分发密钥，这就迫使人们研究和设计出了各种安全协议嗍。然而事与愿违， 已有的安全协议往往被证实并不如它们的设计者所期望的那样安全，复杂的网络环境使得攻击 者可利用安全协议设计中的缺陷和漏洞来实施各种各样的攻击，从而非法获取网络资源，窃取 非授权使用的信息，对网络的正常使用和安全造成极大的威胁。因此，安全协议自身的安全性 成了网络安全的关键问题之一。考量和分析一个安全协议的安全性我们称之为安全协议的分 析。围绕着安全协议的安全性研究和讨论，出现了许多形式化分析方法，它们是目前使用最为 广泛的安全协议分析方法。所谓的形式化分析，是采用各种形式化的语言，为安全协议建立模 型，并按照规定的假设、分析和验证规则，验证安全协议的安全性。 安全协议的主要功能是应用密码技术例实现网络环境中的密钥分配( k e yd i s t r i b u t i o n ) 和实 体认i t 正( a u t h e n t i c a t i o n ) 。设计安全协议的目的是保证信息的安全，但安全协议自身的安全性由 什么来保证呢? 我们如何证明一个协议是安全的昵? 这个问题一直是长期以来困扰安全协议 的设计者和应用者的问题。安全协议中所采用的密码算法的好坏，能对协议的安全性形成一定 的影响，但是大量的事实证明，安全协议的很多缺陷和漏洞往往不是因为协议中使用的密码算 法而引起的，而是由协议自身结构设计不合理和其他因素而引起的。攻击者会利用协议中的缺 一 一 责州大学计算机软件与理论研究所 陷和漏洞，伪装成合法通信者，窃听秘密、重放消息或者更改信息，对网络系统所涉及的业务 范围，诸如教育部门、政府部门、金融部门、军事部门造成巨大的危害。这就给安全协议的设 计者提出一个更高的要求，要确保安全协议本身的正确性和可靠性，在安全之上建立安全。然 而不幸的是，安全协议的缺陷和漏洞往往在设计阶段是很难发现的，安全协议在设计阶段还没 有引入形式化的设计方法，因此无法证明所设计的协议是安全的，无法证明协议是否存在缺陷 和漏洞。这些缺陷和漏洞中的大多数都是在后来的使用中或者采用形式化分析方法验证中发现 的，缺陷和漏洞的发现经历了数年甚至更长的时间，由此可见安全的协议的设计【4 3 】的困难程 度。那么安全协议的安全性的保证有没有规律可循呢? 从以下两个方面着手是值得考虑的发展 方向：一是要有完善的理论和方法指导协议的设计过程，在协议的设计阶段引入形式化的设计 方法；二是在协议设计完成后有有效的手段和工具对协议进行安全性分析，在验证阶段要有完 善有效的形式化分析方法。形式化方法( f o r m mm e t h o d ) 大大地推动了协议分析和验证的发展， 同时也不断产生出各种形式化方法，使得这些方法得到不断地改进、发展和完善，开创了一个 很好的研究领域。尽管每一种形式化方法都有自己的应用范围，没有一种方法能够涵盖协议安 全的方方面面，但它代表着安全协议分析的一个颇有前途的发展方向。目前，形式化方法主要 有基于逻辑、基于模型检验、以及其他诸如基于专家系统、定理证明等通用的形式化技术。 安全协议形式化分析m n 叫从8 0 年代起至今，发展极为迅速，吸引了为数众多的学者和研 究人员致力于该项工作，目前已成为安全协议研究领域的一个极为重要的，颇具理论深度的前 沿问题i 咿1 。本文正是从这个角度出发，对安全协议及其b a n 逻辑分析进行了一些深入的研 究。 1 2 国内外研究现状及发展 随着网络和分布式系统的应用和发展，如何在分布式系统中建立安全协议，安全协议的正 解性等问题自然成为应用中要考虑的问题。安全协议的形式化分析的思想正是在这样的需求驱 动下而提出的。n e j l m m 和s c 3 r o e d e r 5 4 1 最早提出为进行共享和公钥认证的认证服务器系统的 实现建立安全协议，从而引发了安全协议领域的许多重要问题的研究。1 9 8 1 年d e n n i n g & s a c c o 在文献【3 7 】中指出了n s ( 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 模型首先假设网络为入侵者控制： 即入侵者能够获取通过网络传递的任何数据，能够破坏更新消息、创建消息，能对传输的数据 进行加解密操作等。因此，网上的用户将把他们收到的所有消息都当作是入侵者发出的，若入 侵者的目的是发现秘密消息，那么就可以分析出入侵者是通过重写消息来达到目的。d o l e v 和y a o 为这个分析使用了项重写系统的概念，并发展了一些分析算法。 在d o l e v - y a o 模型中，协议的安全性是指攻击者无法获知其不应知道的秘密消息。 d o l e v - y a o 模型对认证协议只能查漏洞，无法记录状态转换的状态信息，常用于分析传统协议。 一8 一 贵州大学博士学位论文 安全协议及其b n 逻辑分析研究 m i u e n 创建的i n t e r r o g a t o r 软件首先实现了该模型，要验证协议是否有漏洞，要通过穷尽搜索状 态空间来寻找。l o n g i e y - r g b yt o o l 和n r l a n a l y z e r 是另外两种可用于协议分析的软件，其中 n r l a n a l y z e r 的状态空间是无限的，因而能够实现多个协议运行时的协议分析n r l a n a l y z e r 已成功地用于许多协议的分析，有着广泛的应用前景。 另外，还有n i e h 等人提出的与d o l e v - y a o 模型接近的与状态空间有关的加密协议模型， d o l e v 、e v e n 和k a r p 等提出的d o l e v - e v e n - k a r p 模型。在加密协议模型的基础上，利用时序逻 辑( t e m p o r a ll o g i c ) 易于刻画状态变迁的特点，提出了一个基于时序逻辑的加密协议认证模型 t l - e p v m ，利用了时序逻辑比f s m ( f i n i t es t a t em a c h i n e , 有限状态机) 、p e t r i 网等模型更易于 刻画协议活动性质的特点，将密码系统状态间的关联性和时序逻辑的可达性相对应。它从形式 上规定密码设备的构成成分以及有关的密码操作，使用了形式逻辑的常量和状态不变量来表达 这些构成成分。有关的密码操作表达为状态转换，加密协议应保留的必要特性表达为临界不变 性表达式，然后验证这些不变性表达式。整个验证都在统一的逻辑框架体系下进行，形式化程 度较高。 自从形式化分析方法开创以来，发展出了很多安全协议形式化分析方法 8 s i 8 7 u 1 ，这些方 法大致可以分为三类【1 1 0 l ：形式逻辑方法，模型检测( m o d e lc h e c k i n g ) 方法和定理证明方法。 1 2 1 形式逻辑方法 基于知识和信仰 s s 4 s l “l 4 7 1 的形式逻辑分析方法 5 5 5 0 1 是迄今为止使用最为广泛的一种方 法，它的突出代表是b a n 逻辑 2 4 1 ，它是一种模态逻辑( m o d a ll o g i c ) 。直接、简单是模态逻辑 方法分析安全协议的主要特点，模态逻辑由一些命题和推理规则组成，命题表示主体对消息的 知识或信念，而推理规则可以从已知的知识和信念推导出新的知识和信念。围绕着b a n 逻辑 的研究和应用出现了许多扩展和改进的b a n 逻辑，称为b a n 类逻辑( b a n 1 i k el o g i c ) 。迄今 为止，在使用逻辑手段1 7 2 分析安全协议方面取得的进展大都以b a n 逻辑为基础。 1 9 8 9 年，b u r r o w s ，a b a d i 和n e e d h a m 独树旗帜地以逻辑形式方法提出了一种基于知识和 信仰的逻辑b a n 逻辑，用来描述和验证认证协议，其目的是在抽象层面上分析计算机通 信网络或分布式系统中认证协议的安全问题，使得可信的双方在网络环境下彼此通信，建立通 信的主体联系以及安全协议。b a n 逻辑的提出在解决安全协议分析( s e c u r i t yp r o t o c o la n a l y s i s ) 问题上迈出了一大步。b a n 逻辑是分析安全协议的一个里程碑，它成功地对 n e c d h a m - s c h r o e d e r 、k e r b e r o s 等几个著名的协议进行了分析，找到了其中已知和未知的漏洞。 b a n 逻辑在协议分析中的成功应用极大地激发了密码研究者对安全协议形式化分析的兴趣， 并导致许多安全协议形式化分析方法的产生。 b a n 逻辑在进行协议的形式化分析时，首先确定了协议初始时刻各参与者的知识和信仰， 并且形式化定义了协议的目标，通过协议中的步骤演进，消息的发送和接收产生新的知识，再 运用逻辑推导规则来得到最终的信仰和知识。如果得到最终的关于知识和信仰的语句集里不包 含所要得到的目标知识和信仰的语句时，就表明协议存在安全缺陷。b a n 逻辑之所以得到广 泛的应用，得益于它简单、直观，便于掌握和使用，而且效果明显，成功地发现协议中存在的 安全缺陷，它是在一个抽象层次上分析分布网络系统中认证协议的安全问题。但是，b a n 逻 一9 一 贵州大学计算机软件与理论研究所 辑的缺陷也是较为明显的，逻辑本身存在以下缺陷：初始假设的确定非形式化，理想化步骤非 形式化，逻辑不够严密( 如用共享密钥加密的数据的来源判断) ，缺乏精确定义的语义基础( 如主 体能够识别消息的含义是模糊的) ，无法探测对协议的攻击等。b a n 逻辑最为可取的是其自然 易用的逻辑语言及其结构和简明直观的推理规则。但其最大的问题是不够完备。 b a n 逻辑的局限性( u i n i t a t i o n ) 叫大大地限制了它的分析范围，为了突破b a n 逻辑的局 限，许多研究对b a n 逻辑进行了必要的改进或扩展，提出了各种各样的逻辑方法，其主要代 表有g n y 逻辑”“、m b 逻辑删、a t 逻辑1 3 2 j ，v o 逻辑【鹌l 和s v o 逻辑1 5 0 l 。g n y 逻辑拓展了 b a n 逻辑的范围，试图消除b a n 逻辑中对主体诚实性的假设、消息源假设、可识别假设等。 提出了“拥有”概念，并区分“拥有”和“相信”；增加了“可识别性”概念和“非信源”概念；增加了 推理规则，因此比b a n 逻辑更为全面和细致。但它的规则膨胀到加多个，大大增加了它的 使用难度，阻碍了它的应用推广。a t 逻辑从语义的角度分析了b a n 逻辑，并进行了改进， 同时给出了形式化语义，并证明了其推理系统的合理性。a t 逻辑因其良好的计算模型和形式 语义受到好评。v o 逻辑则在b a n 逻辑的基础上增加了对d i f f i e - h e l l m a n 密钥交换系统的处理 能力- 而s v o 逻辑吸收了b a n 逻辑、g n y 逻辑、a t 逻辑等的优点，同时又具有十分简洁 的推理规则和公理。它为逻辑系统建立了用于推证合理性的理论模型。在形式化语义方面， s v o 逻辑对些概念做了重新定义，从而取消了a t 逻辑系统中的一些限制。m b 逻辑因提出 格式化改写协议方法及引入集合概念而独具特色，并用高阶逻辑h o l 形式化了一个扩展的 g n y 逻辑，以此来分析安全协议。 1 9 9 7 年，g u r g e n s 设计了s g 逻辑，用于检测b a n 逻辑、g n y 逻辑、a t 逻辑以及v o 逻辑等其他的b a n 类逻辑都不能够识别的特定的重放或交叉攻击类型。 另外一些扩展的b a n 逻辑还有：g a b r i e l ew e d e l 和v o l k e rk e s s l e r 于1 9 9 4 年和1 9 9 6 年提 出的a u t o l o g 逻辑和g v 逻辑l ”l ，覆盖认证协议不同方面如证书( c e r t i f i c a t e ) 方面、密钥 协商协议方面的逻辑。 b a n 逻辑及b a n 类逻辑基本上是一种信念逻辑1 4 | i ，它的目的主要是证明主体相信某个 公式负有责任，不能证明保密性或其他的一些特性。因此，b a n 逻辑不适合分析电子商务协 议，原因在于信仰逻辑是要证明某个主体相信某一公式，而可追究性( a c c o u n t a b i l i t y ) 的目的在 于某个主体要向第三方证明另一方对某个公式负有责任。为此，k a i l a r 提出了新的用于分析电 子商务协议中可追究性的形式化分析方法，简称k a i l a r 逻辑。但是k a i l a r 逻辑同样存在缺陷： 只能分析协议的可追究性，不能分析协议的公平性( f a i r n e s s ) ，对协议语句的解释及初始化假设 是非形式化的，无法处理密文等。 还有一些不是基于b a n 的模型逻辑，包括b i e b e r 逻辑- - c k t 5 和s y v e r s o n 逻辑一k p l 以及其 他几种逻辑。s y v e r s o n 逻辑将攻击者具有的知识分为两类：一类是攻击者收到一条消息后所具 有的知识( 在看见一个比特串的含义下) ；另一类是攻击者可以识别消息时所具有的知识。然后， s y v e r s o n 逻辑可以对此进行推理。类似于s y v e r s o n 逻辑，b i e b e r 逻辑也区别看见一条消息和理 解一条消息，并能对安全协议中知识的演化进行推理。 b a n 类逻辑尽管存在这样那样的缺陷，但是，它在安全协议形式化分析领域仍具有举足 一1 0 一 青州大学博士学位论文安全协议及其b 麒逻辑分析研究 轻重的地位，而且它的简单、直观、易用性仍然受到很多人的欢迎，给我们带来了许多思路和 启发。可以断定，它在未来发展的组合方法中仍将起到重要的作用 1 2 2 模型检测方法 模型检测( m o d e lc h e c k i n g ) 技术是一种十分有效的协议形式化分析工具，也叫状态空闻搜 索法。状态空甸搜索法的基本思路是，把安全协议看成一个分布式系统，每个主体执行协议的 过程构成局部状态，所有局部状态构成系统的全局状态，每个主体的消息收发动作都会引起局 部状态的改变，从而也引起全局状态的改变。在系统可达的每个全局状态，检查安全属性是否 满足参考文献f 9 4 1 。 在1 9 9 6 年，g a v i nb m 首先使用c s p ( c o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e s ，通信顺序进程) 和模型检测技术对安全协议进行分析，并首次采用c s p 模型和c s p 模型检测工具 f d r l 4 0 j ( f a f l u r e sd i v e r g e n c e s r e f i n e m e n tc h e c k e r , 故障偏差精炼检测器) 来分析 n e o d h a m - s c h r o e d e r 公钥协议，并发现了一个近十七年来未发现的漏洞。c s p 将安全协议的问 题归约为c s p 进程是否满足其c s p 说明的问题。它将所分析的协议性质与具体的协议形式加 以区分，并在c s p 总体框架下对协议的性质进行分析与验证。c s p 具有良好的语义使其可以 较好地描述协议是否满足其安全属性这一问题，而且c s p 对协议的描述极为接近协议的本身 含义。模型检测技术( m o d e lc h e c k i n gt e c h n o l o g y ) 是验证有限状态系统的自动化分析技术，是 一种安全协议的自动验证工具。i o w e 等学者应用c s p 方法的成功，促进了这一领域的发展。 s c h n e i d e r 发表了一系列关于c s p 方法应用的论文，应用c s p 方法讨论安全协议的安全性质、 匿名等问题；分析了各种安全协议，例如n s p k 协议、非否认协议等。此外，c s p 的数学基 础是进程代数，其自身提供了比较丰富的演算手段，在c s p 模型的基础上，通过严格的数学 推演，可以得到一些协议性质的证明，这也是今后要研究的一个方向。 通用状态计数工具m u f f 也是一种分析工具，它是一种在工业协议方面，尤其是在多处理 器缓存同步协议和多处理器内存模式等领域应用很广的一种协议验证工具，可以用来分析安全 协议，可能到达的状态，进而得出安全协议是否安全的结论。它也代表着一种发展方向，即借 鉴其它领域的形式化工具，在其基础上增加有关的安全概念，并进而在网络结构设计时嵌入安 全协议模块加以分析。 用a s t r a l 这种实时系统形式化描述语言构造的模型检铡器也成功地对 n e e d h a m - s c h r o e d e r 公钥协议和t m n 协议进行了分析。 2 0 0 0 年，又出现了一种专门用于验证安全协议的b r u t u s 模型检测器。 s m v 系统是基于“符号模型检测1 s y m b o l i cm o d e lc h e c k i n g ) 技术的模型检测工具软件。 s m v 早期是一种对硬件验证的实验工具，是为了研究符号模型检测应用程序的可能性。发展 到今天，s m v 己成为国际上广为流行的分析有限状态系统的常用工具。s m v 系统是一种为了 要检测有限状态系统是否符合c t l ( c o m p u t a t i o nt r e el o g i c ) 逻辑所表达的系统属性的工具。近 几年，s m v 已作为分析安全协议的重要的模型检测工具。 另外，还有两个值得一提的工具，一是基于d e l o v y a o 模型的i n t e r r o g a t o r 模型，是将专 家系统用于协议的形式化分析中取得显著效果的个工具。该软件工具是用p r o l o g 语言，纳 一1 1 责州大学计算机软件与理论研究所 入了一个协议状态变迁模型。在i n t e r r o g a t o r 中，坍议被视为通信进程的集合，每一个进程育 一个可能的状态集合，而消息的传递将造成系统中状态的转换。系统是基于有限状态机的。 i n t e r m g a t c t 为协议达到一个不安全状态构造了不同的路径，如果存在一条路径是始发于协议 的一个初始状态，那么就表明协议是不安全的。另一个就是用p r o l o g 语言实现的典型专用验 证工具n r l 协议分析器，它的状态空间是无限的，因而能够实现多个协议运行时的协议分 析。n r l 不仅能记录人工证明，并在很多情况下可进行自动证明，它使得在搜索空间足够小 时穷举搜索成为可能。n r l 协议分析器已成功地用于许多协议的分析，有着广泛的应用前景。 实践证明，模型检测方法是协议分析的非常成功的方法娜l ，发现了协议的诲多以前未发 现的新的攻击，协议分析的自动化是人们所关注的，而模型检测在自动化程度方面表现较好， 验证过程中不需要用户参与；其次。如果协议有缺陷，能够自动产生反例。但它的缺点也很明 显： l 、容易产生难以解决的状态空伺爆炸问题，所以不能用于分析比较复杂的协议。 2 般需要指定运行参数，比如运行实例和主体的数量，发现错误说明协议确实存在缺 陷，但是没有发现错误并不能保证协议正确，也就是它不能证明协议正确。 模型检测能够实现完全自动化，即使是不熟悉形式化方法的协议设计和分析人员也很容易 使用，因此这种方法得到研究入员的关注。解决以上两个缺点的工作分为以下两个方面： 一方面的工作是解决状态空间爆炸问题，比如c l a r k 等使用偏序规约技术削减验证过程的 状态空间：s h m a t i k o v 等规定在合法主体可以发送消息时，攻击者就不发送消息来削减状态空 间：b r o a d f o o t 等通过把合法主体( 一般是可信第三方) 的c s p 进程合并到攻击者进程来实现状 态空间削减；x u 等提出根据攻击者的攻击目标来产生和削减状态空问；h u i 和g a v i ni o w e 提 出一种转换方法可把复杂协议转变成简单协议，并且简单协议能够体现复杂协议的安全缺陷， 这样就可用模型检测法来分析复杂的安全协议。 另外一方面的工作就是尽量实现模型检测方法的完备性。这方面的工作可以分为两种；一 是从理论上分析当一个协议存在攻击时，发现这个攻击所需要的运行实例的上界；二是设计出 可以用于无限状态空间的状态搜索方法。 第一种情况的研究工作主要包括：g a v i nl o w e 证明了在一定条件和执行环境下，如果一 个小系统没有攻击，那么不受限制的大系统也是安全的，但他的理论只适用于保密属性和有限 的协议类型；s t o n e r 给出一个方法来决定攻击一个协议时所需协议实例的上界；r o s c o e 等使 用数据独立技术给出了对实现攻击有用的随机数数量的上界。 第二种情况的研究工作中基本上都使用了符号技术，主要包括：h u i m a