（计算机软件与理论专业论文）基于知识结构的认证协议验证.pdf

摘要 知识推理作为人工智能领域中的一个重要研究方向，应用领域非常广泛 安全协议作为网络通信的基础，在信息安全中具有重要作用，安全协议验证的 形式化方法也在最近三十年蓬勃发展起来o b d d 作为一种数据结构，在模型 检测等领域中得到了很好的应用本文的主要研究成果主要体现在如下几个方 面： 1 给出了一个知识推理的框架一知识框架在该框架下变量忘记作为一基本 操作，智能体可用其来对自己或其他智能体的知识进行推理在该框架下， 最弱充分条件起作重要作用给定一背景知识库t ，及针对智能体i 的可观 察变量集d ，我们证明了：智能体 知道公式妒成立这一问题，可被转化为妒 在t 下依赖0 ；的最弱充分条件是否成立问题进一步，我们给出如何利用 一般化最弱充分条件来定义和获得公共知识c o m m o nk n o w l e d g e ) 该方法 本质上是基于语义的，但通过使用知识结构，我们给出了一种基于语法的 简洁形式来表示克里普克结构，所以在一定程度上避免了状态爆炸问题 2 通过构造协议的知识结构，把知识逻辑的语义应用到认证协议分析和验 证中去与类b a n 逻辑相比，我们的方法可完全自动化，这是因为它是基 于协议定义本身，而不需进行任何所谓理想化( i d e a l i z a t i o m ) ( 无法用算法 实现1 处理该方法的另一个显著特点是我们能够证明协议的正确性，而 不是去找漏洞并且我们实现了可以自动进行安全协议验证和分析的工 具：s p v 3 o b d d 由于其精致的结构，具有压缩空间的特点，加上高效算法，使 得o b d d 在模型检测等领域得到了很好的应用我们利用o b d d 的特点， 设计出基于o b d d 的整数集合运算算法，并把该算法应用到图像处理中 去+ 关键词：知识推理，知识框架，形式化方法，安全协议验证，o b d d ，s a t 集合运算，图像处理 a b s t r a c t k n o w l e d g er e a s o n i n gi so n eo fi m p o r t a n tt o p i c si na ia n dv e r yu s e f u li n m a n yd o m a i n s e c u r i t yp r o t o c o li sf u n d a m e n t a lt on e t w o r kc o m m u n i c a t i o na n d v e r yi m p o r t a n tt om a i n t a i ns e c u r i t y s e c u r i t yp r o t o c o lv e r i f i c a t i o n ，e s p e c i a l l yb y u s i n gf o r m a lm e t h o d ，i sd e e p l yd e v e l o p e di nr e c e n t3 0y e a r s o b d di so n ek i n d o fd a t as t r u c t u r ea n de f f i c i e n t l yu s e di nm a n yd o m a i n ，s u c ha sm o d e lc h e c k i n g t h i sp a p e r sm a i nc o n t r i b u t i o ni n c l u d e s ： 1 w ei n v e s t i g a t ek n o w l e d g er e a s o n i n gw i t h i nas i m p l ef r a m e w o r kc a l l e dk n o w l e es t r u c t u r e w eu s ev a r i a b l el o w e t t i n ga sab a s i co p e r a t i o nf o ro n ea g e n t t or e a s o na b o u ti t so w no ro t h e ra g e n t s k n o w l e d g e i no u rf r a m e w o r k ，t w o n o t i o n sn a m e l ya g e n t s o b s e r v a b l ev a r i a b l e sa n dt h ew e a k e s ts u f f i c i e n tc o n d i t i o np l a yi m p o r t a n tr o l e si nk n o w l e d g er e a s o n i n g g i v e nab a c k g r o u n d k n o w l e d g eb a s et a n das e to fo b s e r v a b l ev a r i a b l e s 馥f o re a c ha g e n ti ，w e s h o wt h a tt h en o t i o no fa g e n tik n o w i n gaf o r m u l a 妒c a nb ed e f i n e da sa w e a k e s ts u f f i c i e n tc o n d i t i o no f 妒o n0 tu n d e rt m o r e o v e r ，w es h o wh o wt o c a p t u r et h en o t i o no fc o m m o nk n o w l e d g eb yu s i n gag e n e r a l i z e dn o t i o no f w e a k e s ts u f f i c i e n tc o n d i t i o n o u ra p p r o a c hi se s s e n t i a l l yas e m a n t i c a lo n e ， b u tw eg i v eas y n t a c t i c a la n dc o m p a c tw a yt or e p r e s e n tk r i p k es t r u c t u r e s b yu s i n gk n o w l e d g es t r u c t u r e s ，a n dh e n c ec a na v o i dt h es t a t e - e x p l o s i o n p r o b l e mt os o m ee x t e n t 2 w ed e m o n s t r a t e dh o wt oa p p l yt h es e m a n t i c so fk n o w l e d g el o g i ct oa n a l y z e a u t h e n t i c a t i o np r o t o c o l s ，v i ab u i l d i n gk n o w l e d g es t r u c t u r e sf o rt h e m c o r n p a r e dw i t hb a n - l i k ef o g i e s ，o u rm e t h o da r ea u t o m a t i c a l l yi m p l e m e n t a b l e a n dw eh a v ei m p l e m e n t e di tb e c a u s ei to p e r a t e so i 2t h ea c t u a ld e f i n i t i o n o ft h ep r o t o c o l s n o to ns o m ed i 伍c u l t t o - e s t a b l i s hj u s t i f i c a t i o n so ft h e m ， a n dt h ep r o c e s so fv e r i f i c a t i o no fs p e c i f i c a t i o n si nk n o w l e d g el o g i cc a nb e r e d u c e dt op r o p o s i t i o n a lr e a s o n i n g a n o t h e rs a l i e n tp o i n to fo u ra p p r o a c h i st h a tw ec a np r o v et h ec o r r e c t n e s so fap r o t o c o lr a t h e rt h a nf i n d i n gab u g 基于知识结构的认证协议验证 o fi t w eh a v ed e v e l o p e das e e u r i t yp r o t o c o lv e r i f i c a t i o nt o o l s ：s p v 3 o b d dh a sb e e nu s e de f f i c i e n t l yi nm a n yd o m a i n s ，s u d la sm o d e lc h e c k i n g ， t h a n k st oi t sc o m p a c ts t r u c t u r ea n de f f i c i e n ta l g o r i t h m s w ed e s i g n e ds y m - b o l i ci n t e g e rs e to p e r a t i o n sa l g o f i t h m sb yu s i n go b d da n da p p l i e dt h e m i ni m a g ep r o c e s s i n g k e y w o r d s ：k n o w l e d g er e a s o n i n g ，k n o w l e d g es t r u c t u r e ，f o r m a lm e t h o d ，s e - c u r i t yp r o t o c o lv e r i f i c a t i o n ，o b d d ，s a t ，s e to p e r a t i o n s ，i m a g ep r o c e s s i n g 第一章绪论 本文的主要研究内容是知识推理及其在安全协议验证中的应用为了使读 者对知识推理及安全协议验证有一个大致的了解，在本章中，首先对知识推理的 背景，如知识推理的研究内容、现状、应用等进行简单的回顾，给出相关概念其 次，对安全协议验证的研究内容、研究现状及存在的问题做简要介绍再次，由于 本文的方法是基于符号化算法，b j o b d d ( 有序二叉判定图) 、s a t ( 命题公式可 满足问题) ，& x t - - 者进行简单介绍最后，给出论文的主要研究成果及论文安排 认证协议验证是安全协议验证的主要内容之一，因为本文主要研究的是认证协 议验证，所以除特殊情况( 由上下文) 外，安全协议验证即指认证协议验证 1 1知识推理 认识论，即对知识的研究，从古希腊哲学家开始，在哲学中有很长的研 究历史以及良好的传统f 3 7 1 对诸如问题“我们知道什么”、什么能够被 知道”、“说某人知道什么到底意味什么”等等，在哲学文献中有很多讨论 v o nw r i g h t 在1 9 5 0 年代的工作 1 0 7 i 给出了对知识推理进行形式化分析的思想 在1 9 6 2 年，h i n t i k k a 4 s 第一个以书本的形式给出了认知逻辑一知识逻辑的形式化 研究随后，关于知识的研究在哲学界蓬勃发展起来，主要兴趣之一是如何抓 住知识的本质特征各种关于知识的公理系统建立起来更近一些，在不同领 域( 如经济学，语言学、人工智能以及理论计算机科学) 的学者们都对知识推理 发生兴趣关于知识的研究也随之扩大，在很多领域蓬勃发展起来，如博弈论、 经济学、机器人、知识库等，研究问题如机器人如何获得知识并进行推理以采 取下一步行动、数据库何时回答叼；知道”、商务智能体( 8 9 e n t ) 如何收集信息以 做决策等其次，计算知识的复杂度也是一个研究方向另外，知识推理研究的 重点是针对群体智能体( ag r o u po fa g e n t s ) 的情况( 本文也如此) ，丽非单个智能 体( 哲学家们偏向于研究) 的情况这是因为对话、谈判、或者是分布式系统中进 程间的协议，都是智能体间的交互行为 3 7 1 2 基于知识结构的认证协议验证 1 1 1 语法、语义及性质 令k ( 西) 为原子命题集庐上的通过使用合取( c o n j e c t i o n ) 、非( n e g a t i o n ) 操作 及模态算子甄，所能生成的公式集合算子k 妒读着“智能体i 知道妒”， 妒读着“g 中的每个智能体都知道妒”，p 读着“妒为g 中的公共( c o m m o n ) 知 识”，d g 妒读着“妒为g 中的分布( d i s t r i b u t e d ) 知识”+ 所谓“可能世界”，即除了事件为t r u e 的状态外，还有事件的其他状态根据 当前信息，智能体可能不能够判断出到底哪些可能世界刻画了事件的真实状 态称智能体知道事实协如果在其认为可能的所有世界中，妒都为t r u e 可能 世界模型可用克里普克( k r i p k e ) 结构加以形式化对于定义在妒上的n 个智能体 的克里普克结构m 为元组( 只7 r ，k 1 ，恐，) ，其中s 为可能状态和世界集合， ”为解释，即把s 中的每个状态下的原子命题和真值赋值联系起来( 对于每个s s ，7 r ( s ) ：妒_ ( t r u e ，f a l s e ) ；k 为s 上的二值关系( b i n a r yr e l a t i o n ) ，即s 中元 素对的集合，关系可能具有三种( 自反、对称、传递) 性质中的某些组合性质，同 时具有自反、对称、传递三种性质的关系尬称为等价关系“可满足关系”定义如 下 3 7 】： 1 ，( m ，s ) p ( p 为庐中的原子命题) 当且仅当7 r ( s ) ( p ) = t r u e 2 ( m ，s ) 妒a 妒7 当且仅当( m ，s ) 妒并且( m ，s ) 妒7 3 ( m ，5 ) ，妒当且仅当( m ，s ) 萨庐 4 ，( ms ) k 妒当且仅当( m ，) 妒，对于所有t 使得( s ，t ) k 5 ，( m ，s ) e c 砂当且仅当( m ，8 ) 砒对于所有i g 。 6 ( m ，s ) g b 妒当且仅当( m ，s ) 磁妒，对于七= 1 ，2 ， 7 ( m ，s ) d y e 当且仅当( m ，t ) 妒，对于所有，使得( s ，t ) n 。g 墨 有以下性质 3 7 】： 定理1 1 对于任意公式妒和妒，任意克里普克结构m ，其中每个可能关系凰都为 等价关系，对于所有智能倒= 1 ，2 ，他，有 m ( 妒a 蜀( p 号妒) ) 啼尬妒 第一章绪论 3 2 如幕m 妒，则m 托妒， 3 m 甄妒：争妒， 4 ，m b k t 【p 辛k 。k i 9 ， 5 m 一p = k ，匠妒 定理1 2 对于任意公式妒和妒，任意克里普克结构m ，任意非空子集g 1 ，2 ，扎 ，有 1 ，m e g l p a i e g k 婶， 2 m 妒甘岛( 咿a 妒) ， 3 ，如果m 妒= 岛仲a 妒) ，则m 妒垮e g o 1 1 2完备性、复杂性及可判性 用上( 咖) 表示k 加上模态词d g 后的语言，三g ( ) 表示l n 加上模态词及e ，后 的语言，l p ( 庐) 表示l 。加上模态词c 台、d g 及如后的语言克里普克结构鸠“( 曲) 表 示其中关系墨为自反( r ) 、对称( s ) 及传递关系( t ) ，即等价关系，其他情况可类似 定义 满足下列公理及推理规则的公理系统称为k 。： 公理a i ：所有命题演算重言式 公理a 2 ：( 恐a k = 妒) ) 辛甄妒，i = 1 , 2 ，“ 推理规则r i ：从妒和妒= 币推出母 推理规则r 2 ：从妒推出凰妒 则有 3 7 】， 定理1 3 对于l 。中的公式，k ；关于 矗是完备的 考虑其他公理： 公理a 3 ：k i 妒辛妒，i = 1 , 2 ，n 公理a 4 ：噩妒辛凰尬l p ，i = 1 , 2 ，n 公理a 5 ：，妫妒辛尬、k 妒，i = 1 , 2 ，n 公理a 6 ：、k i ( f a l s e ) ，i = l ，2 ，1 1 4 基于知识结构的认证协议验证 传统上，公理a 2 称为k ，a 3 成为t ，a 4 称为4 ，a 5 称为5 ，a 6 称为d 通过公 理的不同组合，可得到不同的公理系统，如前所述具有a 1 ，a 2 ，r 1 ，r 2 的称为k 代表性的公理系统( 有模态词甄，i = l ，2 ，n ) 有：t 竹( 具有k t ) ，s 4 n ( 具有k t 4 ) ， s 5 。( 具有k t 4 5 ) ，以及k d 4 5 。( 具有k ，d ，4 ，5 ，a 1 ，r 1 ，r 2 ) 可得【3 7 】： 定理1 4 对于l 。中的公式，则有 j 关于蜂是完备的 2 岛。关于 舒是完备的， g s 关于螺“是完备的 ；k d 4 5 n 关f f - m e “是完备的f 其中e 表示欧几理德- 建质( e n c l i d e a n ) ，即对于 任意s ，t ，u s ，当( s ，t ) 耳且( s ，“) k ，则有( t ，u ) k i1 表示连续 性扫e n o u ，即对于任意s s ，则存在t ，使得( s ，t ) k j 关于可判性( d e c i d a b i l i t y ) 有： 定理1 5 m 。的有效性问题和的可证性问题都是可判定的 定理1 6 螺、鸠、蟛“及 霸“的有效性问题和、蹁、眠及肋# 矗的可证 性问题都是可判定的 增加公共知识算子c r g 及分布知识算子) g 后的三。，有类似的可判定结果，这 里不再一一列出 1 1 3 模型检测多智能体系统中的知识 在多智能体系统中，集成时间使得模型具有更强的表达能力和更广的应用 领域在本节中将首先介绍集中知识和时间、从而具有很强的表达能力的逻辑 语言e k k ，然后给出模型检测多智能体系统中知识的进展 第一章绪论5 1 1 3 1 鳃释系统 在多智能体系统中，每个智能体在任意时间点上，都处于某种状态，称之为 智能体的局部状态，从而和系统的状态相区别f 即全局状态) 智能体的局部状态 拥有的信息完全刻画了此状态系统状态可用( 3 。，s 。) 表示令丘为智能体i 的 可能局部状态集合，则g 互l l l 。为系统的可达全局状态集合g 上的一 个运行( r “n ) 是从时间域( 自然数) 到g 上的一个函数，则一个运行可用g 中的一 个全局状态的串表达运行r 和时间m 组成点( r ，m ) ，n ( m ) 表示智能体i 在运行r 中 时间点m 的局部状态 令庐为原子命题集，则解释系统( i n t e r p r e t e ds y s t e m ) i ：为( r ，7 r ) ，其中r 为全 局状态集上的运行的集合，”为赋值函数：赋予r 中每点上原子命题的值 为t r u e 3 7 为在解释系统中定义知识，对于每个智能体有一个在点集合上的等价 关系一i ：u ) 一i ( ，口) 当且仅当r i ( u ) = ( ) 如果一f ：( _ ) 一( ，z r ) ，则 称( r ，) 和( r 7 ，口) 对于智能体l 是不可分辨的，即智能体 在( r ，“) 和( r ， ) 具有同样 的信息 为刻画公共知识语义，f 3 7 】引入关系：一尹和一f ，二者可分别定义为u 。r 一， 和一# 的传递闭包 1 1 3 2 c k k 语言及其语义 线性时态逻辑l 弛 7 3 为命题逻辑加上将来时问算子0 ( 下一步) 和v ( 到为 止) 语言c k l 为命题时态逻辑语言加上模态词k ( 对于每个智能体) ，以及公共 知识算子凸( r 为一组智能体) c k l 。的语义通过满足关系“ c k l 给出，定义 如下：给定原子命题集破解释系统i = ( r ，7 r ) 和点( r 乱) ，有： ( ，r ， t z ) 。p 当且仅当p i r ( r ， ) ，其中p 为一原子命题， ( ，r ，u ) g 耳l 。、妒当且仅当并非( j ，r ，t ) c 耳kp ， ( j ，r ，让) c k l 。妒a 妒当且仅当( j ，r ，t 1 ) c 蜀工。妒及( ，n u ) g k 二。妒 ( ，r ，u ) 口k “k 妒当且仅当( ， ) c 耳“妒，对于所有的( r ， ) 有( r ，牡) 一i ( 一，u ) ， nu ) a 矗。o 妒当且仅当( ，r 7 ， ) 辟。耳l 。妒，对于所有的( r ， ) 有( r ，“) f ( r ，t ，) ， 6 基于知识结构的认证协议验证 ( ，r ，u ) 。耳l 。o 妒当上l 仅当( ，r ( t + 1 ) ) o w l 。妒， ( ，r ，t ) 。k “妒矿l f ，当且仅当存在t ，有( ，r ，) d “妒，并且对于 所有t ”，牡t ”牡7 ，有( j _ ，r ，) c 耳k 妒 1 1 3 3 模型检测知识 在知识逻辑中模型检测知识最先由h a l p e r n 和v a r d i 提出【4 5 】文献 7 6 ，7 7 】给 出了一些模型检测认知规范的算法及其复杂度的讨论，但是他们没有给出一 个实用的关于知识和时间的模型检测r a o 和g e o r g r e f f 陷5 1 考察了s i t u a t e d r e a s o n i n gs y s t e m s 的模型检测问题，没有考虑s 5 知识逻辑系统以及如何实现 b e n e r e c e t t i 和g i u n c h i g l i a 【8 ，9 】给出了对于一些时态模态逻辑的基于特殊的( 非 克里普克结构) 语义的模型检测技术m e y d e n 和s u 【1 0 4 给出了模型检测带有 知识的匿名规范，他们假设智能体具有完美记忆，没有考虑认知模态词的嵌 套h o e k 和w o o l d r i d g e 4 9 】给出了把g k 的模型检测问题转化为线性时态逻 辑l t l 的模型检测问题的一种方法，但该方法的处理过程需要人工输入 在文献【9 7 】中，k a i l es u 给出了基于带有局部变量1 3 4 ，3 5 】解释系统语义的一 种符号化模型检测c k l 。的方法，可直接实现 第一章绪论 7 1 2 安全协议验证 安全协议是保护信息系统安全的重要手段之一，也是保证网络安全的基础 但设计一个符合安全规范的协议非常困难，必须有方法对其进行分析和验证，其 中形式化方法是最重要的方法安全协议，是在分布式网络环境中，以密码学为 基础的的消息交换协议，从而实现密钥分配、数据交换和认证的通信目的，有时 也称之为密码协议网络往往是不安全的，因为在其上可能存在能对网络上的 数据进行窃听、修改和删除的黑客，而后者本身可能能够控制网络上的一些合 法用户安全协议必须能够在面临黑客攻击的情况下实现安全通信目标 一般来说，形式化方法是通过建立系统和其规范的数学和逻辑模型，及一 个有效方法，从而判定系统满足其规范的证明是否正确f 7 4 1 最早提及用形式化 方法进行安全协议分析的是n e e d h a m 和s c h r o e d e r 8 9 最早给出种形式化分 析方法的是d e l o v ；和l y a o 2 5 ，稍后是d o l e v ，e v e n 和k a r p 2 4 d o l e v 和y a o 的工作 非常重要，因为他们第个给出了协议同时有多个实例在执行的环境下的形式 化模型，面加密算法被看作为遵从一定代数性质的黑盒子，环境包括一个能读、 改变、破坏通信或控制些合法个体的黑客随后的安全协议验证工作都是基 于该模型或其变种 分析安全协议的形式化方法主要可分为二类f 1 1 ： 1 模型检测该方法考虑协议行为的一个相对大，但有限的状态空间，以检 测其是否满足一定的正确性条件相对于证明协议的正确性，模型检测方 法更适合于发现针对协议的攻击 2 定理证明该方法考虑所有可能的协议行为，以检测它们是否满足一定的 正确条件相对于发现攻击，定理证明方法更适合于证明协议的正确性 下面将给出当前最受关注的安全协议验证的形式化方法的介绍 1 f d r 英国牛津大学的l o w e 【7 0 】年首先提出使用通信进程代数( c s p ) 【4 的 模型检测器f d r ：来进行安全协议的分析。这种方法成功地首次检验 至u n e e d h a m - s c h r o e d e r 公钥协议的一种攻击，因而在学术界引起广泛 的反响和兴趣，从而启发研究人员用通用的模型检测器( 如s m v ， m a u d e ，s p i n 等等) ，来进行安全协议分析的可行性。这种方法的思 想，是把安全协议模型化为一个进程通信系统m ，协议的执行者的一 8 基于知识结构的认证协议验证 系列动作看成是一个个进程p ，通信的过程模型成为事件e ( e v e n t ) ，触 发进程状态的转化。通信系统的安全规范s ，如安全协议应满足的对应 性( c o r r e s p o n d e n c e ) ，秘密性( s e c r e c y ) ，转化为对应的c s p 语言进行描 述。最后输入给f d r ，来检测是否m s 。由于模型检测器的穷举性，可 以搜索所有情况，令人信服地验证协议的安全，即使当协议不满足规范 时，还可以输出反例，发现新的攻击。l o w e 在这点意义上可以说开创了安 全协议验证的一个新方向。由于c s p 语言的复杂性，用户比较难把握。为 了提供给用户一个更加友好的界面，l o w e 开发了c a s p e r 转换- 器 4 2 1 ，提 供一种友好的语言脚本，可以方便地自动转化成c s p 语言。它大大地方便 了用户使用l o w e 的方法来进行安全协议的分析。 2 m u r p h i 自从l o w e 提出以上方法后，很多学者都尝试用通用的模型检测 器进行安全协议分析。其中比较著名的是s t a n f o r d 大学的m i t c h e l l 等人【7 8 使用m u r p h i 进行的分析。m u r p h i 是s t a n f o r d 大学开发的模型检测器，但 他的前台描述语言不是基于c s p ，而是自己定义的，与f d r 相比，他们有 以下不同点： ( a ) f d r 显式地使用通道( c h a n n e l ) 来描述通信过程，而m u r f h i 使用共 享变量来进行进程通信。 ( b ) m u r p h i 在前台语言种提供了更多的可调参数，来改进搜索效 率，而f d r 没有。 因此，m u r p h i 分析了更多的更复杂的协议，如t m n 协议，k e r b e r e s 协议， 甚至s s l 协议。他们都可以迅速地找到已有地攻击，而且首次发现了s s l 中 一个潜在的问题( 但不是攻击) 。 3 b r u t u s 除了通用的模型检测器外，有学者还专门针对安全协议验证来开 发相应的模型检测工具。如c m u 的c l a r k 【3 3 等人开发的b r u t u s ，就是其中 的一个。b r u t u s 也是一种基于穷举搜索的模型检测分析器，他提供了一种 专门针对描述安全协议验证的前台语言。他的主要思想，是把安全协议模 型化为信息的组合和交换。信息完全由密钥( k e y s ) ，主体名字( p r i n d p a l n a m e s ) ，随机数( n o n c e s ) ，数字证书( d i g i t a lc e r t i f i c a t e s ) 等等组成。并且 密文信息要满足完美加密( p e r f e c te n c r y p t i o n ) ，即m 女只能由m 与k 组 成，( m 1 ) k l = ( m 2 ) 2 ( m l = m 2 ) a ( k l = k 2 ) 第一章绪论9 b r u t u s 后台的核心算法是基于状态空间的穷举搜索。协议开始时，执 行主体都处于初始的状态，每执行一步协议，则主体的状态改变一次。 所有执行主体的可能的状态空间，就是他们所有可能状态的异步合 成( s y n c h r o n o u sc o m p o s i t i o n ) 。很明显，状态空间虽然囊括和考虑了协 议执行时的所有可能的情况，但是她是组合爆炸的，因此为了使这种 方法真正实用，c l a r k 弓i 入了一系列规约技术( r e d u c t i o n ) ，包括偏序规 约( p a r t i a l0 r d e rr e d u c t i o n ) 和对称规约( s y m m e t r yr e d u c t i o n ) ，大大 减少了冗余的状态，使b r u t u s 可以检测工业级的电子商务协议，如i k p 协议族等。b r u t u s 的前台规范( s p e c i f i c a t i o n ) 语言，使用一阶逻辑加上 一个过去时态算子，来表达安全协议的对应性( c o r r e s p o n d e n c e ) ，秘密 性( s e c r e c y ) ，匿名性( a n o n y m i t y ) 及非抵赖性n o n r e p u d i a t i o n ) 等等。 4 n r l 协议分析器除了b r u t u s ，美国海军研究院( n a v a lr e s e a r c hl a b o - r a t o r y ) 也开发了自己的专门的安全协议模型检测器。n p a ( n r lp r o t o - c o la n a l y z e r ) f 2 0 】。n p a 使用p r o l o g 开发的模型检测器，他是基于证伪 的( f a l s i t i c a t i o n ) ，用户首先给出一个不安全的状态，即一种潜在的攻 击，n p a 然后进行反向搜索，看是否能可以从协议的初始状态可达，若 有，则协议不是安全的，找到的路径就是一个攻击。所有的状态转换规则 用p r ol o g 来表达。并且显式地定义黑客的行为。n p a 里协议的描述由以下 组成。 ( a ) 系统状态：包括黑客事先知道的信息，执行主体，己发生的时间序 列。 ( b 1 协议规则：每个执行主体的具体动作，及每个动作执行后主体和黑客 状态的变化，即黑客能得到的信息。黑客的行为用d o l e v - y a o 模型来 描述。 f c l 重写规则：即原子消息的合成分解与加解密的代数描述。 由于使用p r o l o g ，n p a 实质上是半定理证明和半模型检测的，但他的主要 思想是模型检测的。他也使用了一些状态规约的技巧。n p a 已, 成功地运用 到了分析许多安全协议的漏洞中 2 1 1 。 5 b a n 逻辑除了以上的计算机的自动分析和验证，也有一些研究者提 出一些手动分析的数学工具。如b u r r o w s ，a b a d i 和n e e d h a m 提出的b a n 逻 1 0 基于知识结构的认证协议验证 辑 1 4 】。b a n 逻辑是一套基于信念逻辑( b e l i e fl o g i c ) 的数学公理体系，他 为安全协议分析提供一种耳目一新的新方法，即把协议执行映射到执 行主体信念的变化，把状态的转换映射成信念的变化，用公理系统来 表达信念的变化规则用相互信任( m u t u a lb e l i e f s ) 来表征安全协议的规 范。b a n 定义了一套逻辑语言，形式化地描述通信过程中主体信念地变 化，把主体名，密钥，n o n c e s 等等定义为原子命题，然后定义公理系统和推 理规则，以下是其中几条重要的推理规则： ( a ) 消息解读规则：生毳! g 笋； ( b ) 消息新颖性规则：毒g 笛； ( c ) n o n c e 验证规则：盐举邕导笋 ( d ) 判定规则：生盈掣笛 垒丝； 其中，p x ，p 相信x ，x 表达的事实是真的；p q x ，p 看了x ，p 收 到并看到x 这个命题；p 卜x ，p 曾经说了x ，p 曾经发了x 这个消息：p 净 x ，p 对x 进行了判断，p 相信x 的真实性；# 暇) ，x 是新颖的，表示x 在以 往通信过程( r u n ) 中重未用过；p 占口，p 与q 使用私钥k 进行通信；溉表 示x 使用密钥k 进行加密。 用户首先把一个协议抽象成b a n 表达的命题形式，然后进行推理，若最终 能推出p q x 和q p x ，即通信双方对某一事实可以通过这个 安全协议达成共识，形成相互信任( m u t u a lb e l i e f s ) 。b a n 开创了使用信 念和知识推理来分析安全协议的方向，但由于其语义定义不清晰，主要靠 用户的主观判定和抽象，所以会产生很多问题，所以之后很多研究者提出 了很多改进方案，形成a t 【3 ，g n y 6 5 ，v o 【s o ，s v o 【l o o 等等逻辑系 统。 6 串空间模型串空间模型是另一种手动分析安全协议的数学工具， 由f a b r e g af 3 8 等人提出。串空间是一种基于图论的分析方法，他把安 全协议的通信过程抽象成一种过程关系图，定义了两种偏序关系一和辛， 其中前者表示通信协议消息发送接受的时间先后关系，后者定义消息的收 发关系，在串空间模型中，用d o l e v - - 吣模型显式地定义黑客的行为，并 用串进行描述。当用户分析安全协议时，首先抽象成图，然后进行偏序关 星= 里堑堡 ! ! 系上的归纳法，分析协议在黑客情况下是否满足安全协议的对应性和秘 密性a 虽然串空间模型用提供了另一种全新的角度去描述和分析安全协 议中的通信过程关系，成功地分析了大量的协议，但他本身比较复杂，用 户比较难掌握和运用，因此有一定的局限性。不过可喜的是s o n gf 9 4 1 等 人，使用串空间模型作为理论基础，开发了a t h e n a 这个安全协议的自动验 证器，a t h e n a 是一个极其高效的针对安全协议的模型检测器，他妙在使 用“串”在表达一个状态，而不是传统的用“时间点”。因而状态空间大大 减少，成功的验证了一些很大的工业上的协议。 7 归纳法另一种分析安全协议的数学工具是用归纳法。代表是剑桥 大学p a u l s o n 利用通用的高阶逻辑h i g h e ro r d e rl o g i c ( h o l ) 的定理证明 器i s a b e l l e 7 ，来对安全协议进行归纳分析。归纳法是基于证明论的数学 方法，和模型检测的方法不同，他不用遍历所有可能的状态，而是把安全 协议的通信过程，抽象成一个动态的不断增长的时间集合，在这个集合 上应用数学归纳法，因为p ( i ) 寺p ( i + 1 ) ，所以p ( n ) ，进行安全规范的检 验，进而得出在怎样的情况下安全的结论。数学归纳法可以对无穷可能 状态的情况下对安全协议进行验证，这是他比模型检测优越的一个地方。 归纳法对于通信过程中不断增长的消息集h ，定义t p a r t s ，a n a l z 和s y n t h 这些对集合的操作，与d o l e v - - y a o 模型对应。一个黑客的攻击则可以表示 为s y n t h ( a n a l zh ) 。p a u l s o n 利用i s a b e l l e 提供的前台语言h o l ，描述安全 协议的归纳证明和规范，然后交给i s a b e l l e ：进行自动验证，成功地分析了火 量的协议。虽然这种方法有强大的通用数学定理证明器提供支持，但由 于定理证明是半自动的，运行中需要用户进行干预，而模型检测是全自动 的。并且由于高阶逻辑的复杂性，使定理证明的效率也受到影响。 根据以上方法，各种相应的安全协议验证工具开发出来，将在本文的第四 章中介绍我们开发的安全协议验证工具s p v ，以及它们之间的比较 1 2 基于知识结构的认证协议验证 1 3 符号化算法 所谓符号化算法，是基于对问题进行二值编码的基础上使用逻辑( 或数 学) 的方法对问题进行求解的方法目前构成符号化算法的重要基础是二叉判定 图( 0 b d d ) 和命题公式可满足问题( s a t ) 二者目前应用的领域非常广泛，其中 包括模型检测【3 2 】、规划f 57 | 【3 1 】、图论【7 1 】等等本节对二者作一简介 1 3 1o b d d 二叉判定图( b d d ) 是一种表示布尔函数的高效方法b d d 的一个简单情 形是二叉判定树，二叉判定树也被用于表示布尔函数，它的非终端( 叶) 节点是 布尔变量x ，y ，z ，而它的终端( 叶) 节点则是布尔值1 或0 由于包含了一些 冗余，二叉判定树未能为布尔函数提供紧凑的表示，事实上，它和真值表的大小 是一样的b r y a n t 1 3 给出了如何得到布尔函数的规范表示的方法，该方法是在 二叉判定树上加上两个限制，得到二叉判定图第一个限制是，从树的根节点到 终端节点的每一条路径上，布尔变量的出现顺序必须一致第二个限制是，在图 中不能有同构的子树或冗余的顶点基于以上分析，得到三种转换规则，用于简 化b d d ： 1 删除重复的终端节点：对于同样为o ( 或1 ) 值的终端节点，只保留其中的 一个，删除其它的0 ( 或1 ) 节点，并让原来指向被删除的o ( 或1 ) 节点的弧 指向唯一剩下的0 ( 或1 ) 节点 2 ，删除重复的非终端节点：如果b d d 中两个节点n 和m 是结构相同的两个 子b d d 的顶点，那么删除其中一个，并让原本指向这一节点的弧指向另 个节点 3 删除满足下列条件的其中一个节点：如果对于两个非终端节点u 和v ， 有v ”( u ) = v a r ( v ) ，l o w ( u ) = l o w ( v ) 并且l l i 酶( u ) = h i g h ( v ) ，那么去掉u ( 或v ) ， 并让原来指向u ( 或v ) 的弧指向v ( 或u ) 这里v a r ( v ) 表示节点v 所指的变 量，l o w ( v ) 和h i g h ( v ) 分别表示v 所指的左右节点 对一个b d d 不断使用上述规则进行简化，直到无法再简化为止，这样就 得多j t b d d 的规范形式b r y a n t 给出了自底向上化简b d d 的过程，该过程对于 原b d d 的大小来说，是线性时间的【1 3 1 由上述方法得到的图称为有序- - - x 判定 第一章绪论 1 3 a b + 氧c + b 5 d 图1 1 ：一布尔公式及其o b d d 图( o b d d ) ，它是布尔函数的一种规范表示形式对于一个用o b d d 表示的布 尔函数f ，当我们规定了其中的某一个变量x i 为常量t r u e 或f a l s e 时，我们就得到了 一个新函数，求新函数的算法对于原o b d d 的大小来说，是线性时间的不仅如 此，o b d d 的所有1 6 个二元逻辑运算都能在线性时间内高效实现 本文约定符号”一”，”+ ”，”和”v ”分别代表布尔运算：蕴涵，析取，合取 及异或，而蕾表示。的非图1 1 给出了一个用o b d d 表示布尔函数的例子 本文中的知识推理框架底层就是用o b d d 实现的，这在一定程度上避免了 状态爆炸 1 3 2s a t 命题公式可满足问题( s a t ) 是数理逻辑和计算机理论中一个中心问题， 是n p c o m p l e t e i 司题的代表在一些领域中，s a t 问题是解决问题的关键，其中 包括：自动推理，计算机辅助设计、机器视觉、数据库构建和维护、机器人规划、 集成电路设计、计算机框架设计和计算机网络等而解决8 a t 问题的高效算法 是其应用的关键，而通过近些年对s a t 的研究，如变量分组、消解、局部搜索、 全局优化、数学规划等技术的的引进和发展，使得s a t 问题规模大大提高 4 4 】 作为s a t 问题的一个例子，一布尔公式由三部分组成： 1 一变量集合：z 1 ，。2 ，z n 2 一文字( 1 i t e r a l s ) 集合，一个文字为个变量( z ) 或变量的非( 虿) 组成 1 4 基于知识结构的认证协议验证 3 m 个子句( c l a u s e s ) ：c 1 ，c 2 ，c ，每个