（计算机软件与理论专业论文）时态认知逻辑的模型检测与安全协议验证.pdf

时态认知逻辑的模型检测与安全协议验证 专业：计算祝软件与理论 博士生：吴立军 撂导教爨：苏开乐 摘要 随着计算杌网络和通信技术的发展和普遍应用，安全协议作为网络安全的基 础，也迅速发展起来，并且已经成为计算机安全的一个重要方向。安全协泌是一 静通信给议，它主要邋过密码技术实现通信中的密码分发和努 ； 认证，从蕊保证 网络通信静安全往。然两设诗一个符合安全蚕标豹安全渗议楚十分蚕难静。有静 协议在被使用很多年膳才被发现存在漏洞，如n s ( n e e d h a m ，s c h r o e d e r ) 协议在使 用十多年后才发现其存在漏洞。因此，对协议进行安全性分榭和验证是计辫机安 全领域笈矮蔻滔豹重大漾邃之一。多年来天艇慕怒熬安全耱议验证方法主要楚影 式化方法。而形式化方法主要有模型检测和定理证明。模型梭测有两个主骚的优 势，其一、能够自动验证一个系统魁否满足其所设计的规范；其二、当规范不被 满足或捻测出协议存在漏洞时，模溅检测工具能提供导致该缭槊鲍事件序列，从 而为在诲浚中遵章亍漏澜定位帮协议改送撵供方便。模墼检溺技术一直 盖来主要是 检验用时态逻辑描述的规范，人们椴少注意认知逻辑的模型搬测问题，而在分布 式系统领域，系统和协议的规范已广泛地采用知识逻辑来描述。本文主要针对时 态谈翔避缮戆模型捡溅遗题送芎亍了魏步骚究，羲秀究成果终瑰在如下死方瑟： ( 1 ) 论文首先对安全协议验证的形式化方法进行了概括和总结。并讨论了今 后安全协议骏诋的一些研究方向。安全协议验证的形式化方法主娶包括 模型捡涎、是理送明、p e t r i 瓣方法、甄演算方法、c s p ( c o m m u n i c a t i n g s e q u e n t i a lp r o c e s s e s ) 方法和串空间方法等。从基本原理、方法及工兵到 在安全协议验证的应用等方面比较详细的讨论了计算机专家们在形式化 方法方面所做的工作。 ( 2 ) 在s m v ( s y m b o l i cm o d e lv e r i f i c a t i o n ) 等模型检测工具的麓穑上，裰据辩识 的语义和集合理论，提出了多智体系统时态队知逻辑模型检测方法。使 s m v 等模型检测工具的功能从时态逻辑扩展到时态认知逻辑。两翳寸态 认知逻辑已被广泛应用于分布式系统和协议的舰范描述。本文也以 t m n ( mt a t e b a y a s h i nm a t s u z a k i dbn e w m a n ) 协议为例，探讨了该算 法在安全掺议验证方嚣豹应爰。甄撼爨鳃模型检测睡态认知逻瓣算法主 要有以下几个优点： 与s m v 结合能检测带有知识算子的规范。 与s m v 缝台梭溺蒂育多滋箱谖熬援蔻。 与s m v 结合能检测带有公共知识的规范。 算法的时间复杂性是多项式时间的。 ( 3 ) 根据自动祝理论和知识静语义，提出了“o nt h ef l y ”模型裣测耩寸态诀知 规范的算法，该算法在模型检测带脊相识算子的时态规范时，往往只需 产生系统的小部分状态空间，就能找到一个反例，从而实现“o n t h e f l y ” 模墅裣溺瓣态谈酝纛蕊，显算法静嚣雩润复杂往楚多壤式时霪懿。算法氇 以t m n 协议为例，探讨了该算法在安全协议验证方面的应用。算法具 有以下几个优点： 能0 建，t 沁一f l y 骥墅裣溅嚣态谈翘逻辑，瑟系统褒藩往挂袋强对态 认知公式表示。 只需产生系统自动机的小部分状态，避免了时态认知规范的模型检 测中悫露不是和状态爆炸等霹题。 算法的复杂性是多项式时间的，而且往往找到一个反例之前只需产 生系统自动机的部分状态，达到o n t h e f l y 的效果。 秘) 遥过强议行为结稳熬定义，及露嚣灸窝毒亍莠缝稳瓣分辑，提出了一释豢 的密码协议秘密性的验证算法，该算法的时间复杂度是多项式时间的。 算法也以t m n 协议为例，探讨了该算法在安全协议验证方面的应用。 算法在凿邋徽规上( c p u 为1 8 g h z ，r a m 为2 5 6 m b ) 验证t m n 班议和 n s 协议的秘密往其需不到1 秒的辩澜。 关键词：安全协议；形式化方法；模型检测；时态认知逻辑；多智体系统；协议 验证；s m v ；t m n 密码协议；自动搬；秘密性； m o d e l c h e c k i n go ft e m p o r a ll o g i c so fk n o w l e d g ea n d s e c u r i t yv e r i f i c a t i o n m a i o r ： n a m e ： c o m p u m rs o f t w a r ea n dt h e o r y w u l i j u n s u p e r v i s o r ：p r o f s uk a i l e a b s t r a c t w i t ht h e d e v e l o p m e n ta n du n i v e r s a la p p l i c a t i o no fc o m p u t e rn e t w o r ka n d c o m m u n i c a t i o nt e c h n o l o g y , s e c u r i t yp r o t o c o l sa sb a s i so fn e t w o r ks e c u r i t yh a v e d e v e l o p e dr a p i d l ya n db e c o m et h ei m p o r t a n td i r e c t i o ni nc o m p u t e rs e c u r i t y s e c u r i t y p r o t o c o l sa r ec o m m u n i c a t i o np r o t o c o l s ， w h i c hi m p l e m e n tc r y p t o g r a md i s t r i b u t i o n a n di d e n t i t ya u t h e n t i c a t i o ni nc o m m u n i c a t i o nb yc r y p t o g r a p h i c a lt e c h n o l o g yi no r d e r t oe n s u r ec o m m u n i c a t i o ns e c u r i t y b u ti ti sv e r yd i f f i c u l tt o d e s i g nap r o t o c o li n a c c o r dw i t hs e c u r i t yg o a l 。s o m ep r o t o c o l sa r ej u s tf o u n dt oh a v el e a k sa f t e rt h e yh a v e b e e nu s e df o rm a n yy e a r s ，s u c ha sn e e d h a m s c h r o e d e r t h e r e f o r e ，t h ea n a l y s i sa n d v e r i f i c a t i o no fp r o t o c o l si sa ni m p o r t a r i tp r o j e c ti nt h ea r e ao f c o m p u t e rs e c u r i t y f o r m a n yy e a r s ，t h ea p p r o a c h e st op r o t o c o lv e r i f i c a t i o nt h a tp e o p l eh a v eu s e da r ef o r m a l m e t h o d s a n dt h e r ea r em a i n l ym o d e lc h e c k i n ga n dt h e o r e mp r o v i n gi nt h ef o r m a l m e t h o d s m o d e lc h e c k i n gh a sm a i n l yt w oa d v a n t a g e s t h ef i r s ta d v a n t a g ei st h a tl i t t l e u s e ri n t e r a c t i o ni sr e q u i r e da n dt h es p e c i f i c a t i o nc a nb ev e r i f i e da u t o m a t i c a l l y t h e o t h e ri st h a ti i it h ee a s e sw h e mt h es p e c i f i c a t i o ni sb r o k e n ，t h em o d e lc h e c k e ri sa b l e t oi n d i c a t et ot h eu s e rt h es e q u e n c eo fe v e n t st h a tl e dt oi tb e i n gb r o k e ni no r d e rt o l o c a t el e a k sa n di m p r o v et h ep r o t o c 0 1 m o d e lc h e c k i n gh a sb e i n gu s e dm a i n l yt o c h e c ki fa s y s t e ms a t i s f i e st h es p e c i f i c a t i o n se x p r e s s e di nt e m p o r a ll o g i c sa n dp e o p l e p a yl i t t i ea t t e n t i o nt ot h em o d e lc h e c k i n gp r o b l e mf o rl o g i c so fk n o w l e d g e h o w e v e r ， i nt h ed i s m b u t e ds y s t e m sc o m m u n i t y ，t h ed e s i r a b l es p e c i f i c a t i o n so fs y s t e m sa n d p r o t o c o l sh a v eb e e ne x p r e s s e dw i d e l yi nl o g i c so fk n o w l e d g e i nt h ep a p e r ，w ef o c u s o nt h ep r o b l e mo ft h em o d e lc h e c k i n go ft e m p o r a ll o g i c so fk n o w l e d g e t h em a i n r e s u l t so fm i st h e s i sa l ea sf o l l o w s ： ( 1 ) w ef i r s tg e n e r a i i z ea n ds u m m a r i z et h ef o r m a lm e t h o d so fv e r i f i c a t i o no f s e c u r i t yp r o t o c o l sa n dd i s c u s ss o m er e s e a r c hd i r e c t i o n si nv e r i f i c a t i o no f s e c u r i t yp r o t o c o l s t h ef o r m a lm e t h o d so fv e r i f i c a t i o no fs e c u r i t yp r o t o c o l s i n c l u d em a i n l ym o d e lc h e c k i n g ，t h e o r e mp r o v i n g ，p e t r in e t ，p ic a l c u l u s ， c s p ，s t r a n ds p a c ea n ds oo n w ed i s c u s si nd e t a i lt h ew o r kt h a tp e o p l eh a v e d o n ei nt h ef o r m a lm e t h o d sf r o mb a s i cp r i n c i p l e s ，a p p r o a c h e sa n dt o o l st o a p p l i c a t i o n s ( 2 ) o nt h eb a s eo fs m v ， a c c o r d i n gt ot h es e m a n t i c so fk n o w l e d g ea n ds e t t h e o r y ， s e v e r a l a p p r o a c h e s f o rm o d e l c h e c k i n gt e m p o r a ll o g i c o f k n o w l e d g ei nm u l t i a g e n ts y s t e m sa r ep r e s e n t e d t h e s ea p p r o a c h e sm a k e s m v sf u n c t i o n se x t e n d e df r o mt e m p o r a l l o g i c s t o t e m p o r a ll o g i c so f k n o w l e d g e a n dt e m p o r a ll o g i c so fk n o w l e d g eh a v eb e e nw i d e l yu s e di nt h e d i s t r i b u t e ds y s t e m sa n de x p r e s s i o no fp r o t o c o ls p e c i f i c a t i o n w eu s et m n c r y p t o g r a p h i cp r o t o c o la sac a s es t u d yt od i s c u s st h ea p p l i c a t i o no ft h e s e a p p r o a c h e si nv e r i f i c a t i o no fs e c u r i t yp r o t o c 0 1 a d v a n t a g e so fo u ra l g o r i t h m a r e ： o nt h eb a s i so fs m v ，t om o d e lc h e c kt h es p e c i f i c a t i o nw i t hk n o w l e d g e o p e r a t o r o nt h eb a s i so fs m v ，t om o d e lc h e c kt h es p e c i f i c a t i o nw i t hm u l t i l a y e r k n o w l e d g eo p e r a t o r o nt h eb a s i so fs m v ，t om o d e lc h e c kt h es p e c i f i c a t i o nw i t hc o t m n o n k n o w l e d g eo p e r a t o r t h et i m ec o m p l e x i t yo fo u ra l g o r i t h mi sp o l y n o m i a l ( 3 ) a c c o r d i n gt oa u t o m a t at h e o r ya n dt h es e m a n t i c so fk n o w l e d g e ，“o nt h ef l y ” m o d e lc h e c k i n ga p p r o a c h e sf o rt h e t e m p o r a ll o g i c o fk n o w l e d g ea r e p r e s e n t e d w h i l e w em o d e lc h e c kt h e s p e c i f i c a t i o n w i t h k n o w l e d g e o p e r a t o r ， w eo f t e no n l yn e e dt oc r e a t eas m a l lp a r to fs t a t es p a c eo fs y s t e m b e f o r ef i n d i n gac o u n t e r e x a m p l ea n ds or e a l i z e “o nt h ef l y ”m o d e lc h e c k i n g t h et e m p o r a ll o g i c so fk n o w l e d g e w eu s es t i l lt m n c r y p t o g r a p h i cp r o t o c o l a sac a s es t u d yt od i s c u s st h ea p p l i c a t i o no fo u ra p p r o a c h e si nv e r i f i c a t i o no f s e c u r i t yp r o t o c 0 1 a d v a n t a g e so ft h e s ea p p r o a c h e sa r e ： b ea b l et o “o nt h ef l y ”m o d e lc h e c kt h et e m p o r a ll o g i c so fk n o w l e d g 。 a n ds p e c i f i c a t i o no fs y s t e mi so f t e ne x p r e s s e di nt h et e m p o r a ll o g i c so f k n o w l e a g e o n l yt oc r e a t eal i t t l ep a r to fs t a t e so fs y s t e ma u t o m a t ama n ds oa v o i d m e m o r y 。s h o r t a g ea n ds t a t e ”e x p l o s i o ni nm o d e lc h e c k i n gt e m p o r a ll o g i c s o fk n o w l e d g e ( 黟t h e t i m e c o m p l e x i t y o f t h e a l g o r i t h m i s p o l y n o m i a l ，a n d w e o f t e n o n l y n e e dt oc r e a t eal i r l ep a r to fs t a t es p a c eo fs y s t e mb e f o r ef i n d i n ga c o u n t e r e x a m p l ea n ds or e a l i z e “o nt h ef l y ”m o d e lc h e c k i n gt h et e m p o r a l l o g i c so fk n o w l e d g e 漕) b yd e f i n i n gf r a m e w o r ko fa c t i o n so fp r o t o c o l sa n da n a l y z i n ga c t i o n so f p r o t o c o l sa n di t sf r a m e w o r k ， af l e wa l g o r i t h mf o rv e r i f i c a t i o no fs e c r e c y p r o p e r t i e so fc r y p t o g r a p h i cp r o t o c o l si sp r e s e n t e d t h et i m ec o m p l e x i t yo f t h ea l g o r i t h mi sp o l y n o m i a l ，w eu s et m n c r y p t o g r a p h i cp r o t o c o la sa c a s e s t u d yt od i s c u s st h ea p p l i c a t i o no ft h ea l g o r i t h mi nv e r i f i c a t i o no fs e c u r i t y p r o t o c 0 1 k e yw o r d s ：s e c u r i t yp r o t o c o l ；f o r m a lm e t h o d ；m o d e lc h e c k i n g ；t e m p o r a ll o g i co f k n o w l e d g e ；m u l t i a g e n ts y s t e m ；v e r i f i c a t i o no fp r o t o c o l ；s m v ；t m n c r y p t o g r a p g i cp r o t o c o l ；a u t o m a t a ；s e c r e c yp r o p e r t y 第 章绪论 本论文以在软伴学缀等剃物主发表豹遥麓论文为基磊塞【1 4 】，着重孬秀究 了安全协议验证，多智体系统中对态认知逻辑髂模鹫检测方法及矮在安全协议验 证中的应用。第2 章对安全协议验证的形式化方法进行概括和总结。第3 章根据 知识的语义和集合理论，将模型检测器s m v 的功能进行了扩展，使其能模烈检 溺霹态谈甄逶罄，劳将冀璃虱t m n 寮鹨耱议夔安全经验证。繁4 章，鬟臻囊魂 机理论，掇出了“o nt h ef l y ”高效模型枪测时态认知逻辑的方法，并以t m n 密鹇 协议作为实例进行了安全性验证。第5 章在引入协议的行为结构的基础上，氍旰究 了一秘多项式孵闯麴安全协议验证方法。 本章主黉介绍了论文需要用到的基本概念和璁论，其中包括安全协议、时态 逻辑和认知时态逻辑。 1 1安全协议 1 i 1 安全协议的基本概念 安全捺淡f 逸豫密码协议) 是戳密鸦迸论为基磷鹣漕息交换镑议，其髫的怒卷 网络环境中，提供各种安全服务。安全目标是多种多样的，饲魏，认证协议的匿 标是认证参加协议的主体的身份。此外认证协议往往还有一个附加目标，即敬主 体之间安全地分配密钥蠛其它各种秘密信息。非否汲协议的目标有两个，一个是 确谈发方落委谀( n o n r e p u d i a t i o no f o r i g i n ) ，夯及 否认协议窝绞受方提供不可羝 赖的证据，证明收到消息来源的正确性；另一个是确认收方的非否认 ( n o n - r e p u d i a t i o n o fr e c e i p t ) ，亦即非否认协议向发送方提供不可抵赖的证据，证明 接受方已收割了该条滔憋。电子巍务镑议豹曩标狳试证性、j 答谀蛙之乡 ，述 有可追究能、公平性等等( 本节内容部分参考了文献【1 9 】) 。 n e e d h a m 。s c h r o e d e r 协议 5 1 是最为著名的早期的认证协议，许多广泛使用的 认涯协议郝跫以n e e d h a m 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 s k 务 议和n s p k 协议。这些早期的经典安全协议是安全协议分析的试验床，亦即每当 出现一个新的形式化分孝厅方法，都要先分析这几个安全协议，骏证新方法的有效 第1 章绪论 性。同时，学者们也经常以它们为例，说明安全协泌的设计原则和各种不同分析 方法的特点。 安全协议及认证中经常使用以下概念及术语【6 】。 对称密钥：加密解密使用同一密钥的密钥。例如：用k 加密的信息 d a t a k 能被k 解密，那么k 就是对称密钥。 非对称密钥：是彼此互逆的密钥对。一个叫私钥，只有拥有者才知道。另 一个叫公钥，被向外界发布，能广泛使用。用公钥加密的数据能被用私钥 解密，同样用私钥加密的数据能被用公钥解密。 会话密钥：通信双方建立的只有双方才知道的密钥，用于秘密通信。 加密：由明文产生密文从而使明文无法识别的过程。在安全系统中，加密 涉及到一个密钥和一种已知的算法。 解密：由密文产生明文的过程。在安全系统中，加密涉及到一个密钥和 一种已知的算法。 认证协议：定义一个系统中传递的信息的规则集合，以便参与者证明其身 份。例如t h e n e e d h a m a n ds c h r o e d e r 协议就是早期著名的认证协议。 n o u n c e ：是新鲜性标识符，通常是一个大的随机数。n o n c e 的主要目的是 将两个消息联系在一起，以便能够判别一个应答是否具有新鲜性。一个 n o n c e 通常表示为虬或m 等形式。 1 1 2安全协议的分类 1 9 9 7 年，c l a r k 和j a c o b 【7 】对安全协议进行了概括和总结，列举了一系列有 研究意义和实用价值的安全协议。他们将安全协议进行如下分类： ( 1 ) 无可信第三方的对称密钥协议。属于这一类的典型协议包括以下i s o 系列 协议【8 1 ：i s o 对称密钥一遍单边认证协议、i s o 对称密钥二遍单边认证协议、 i s o 对称密钥二遍相互认证协议、i s o 对称密钥三遍相互认证协议、a n d r e w 安 全r p c 协议 9 1 等。 ( 2 ) 应用密码校验函数( c c f ) 的认证协议。属于这一类的典型协议包括以下i s o 系列协议【1 0 1 ：i s o 应用c c f 的一遍单边认证协议、i s o 应用c c f 的二遍单边 中山大学博士学位论文 3 认证协议、i s o 应用c c f 的二遍相互认证协议、i s o 应用c c f 的三遍相互认 证协议。 ( 3 ) 具有可信第三方的对称密钥协议。属于这一类的典型协议包括n s s k 协议 【5 】、o t w a y r e e s 协议【1 1 】、y a h l o m 协议【1 2 1 、大嘴青蛙协议【1 2 1 、d e n n i n g s a c c o 协议【1 3 】、w o o l a m 协议【1 4 】等。 ( 4 ) 对称密钥重复认证协议。属于这一类的典型协议有k e r b e r o s 协议版本5 、 n e u m a n s t u b b l e b i n e 协议【1 5 】、k a o c h o w 重复认证协议【1 6 1 等。 ( 5 ) 无可信第三方的公开密钥协议。属于这一类的典型协议包括以下 s o 系列 协议【1 7 】：i s o 公开密钥一遍单边认证协议、i s o 公开密钥二遍单边认证协议、 i s o 公开密钥二遍相互认证协潋、s o 公开密钥三遍相互认证协议、i s o 公开密 钥二遍并行相互认证协议、d i f f i e 。h e l h n a n 协议【1 8 】等。 ( 6 ) 具有可信第三方的公开密钥协议。属于这一类的典型协议有n s p k 协议【5 】 等。 1 1 3 安全协议的设计和验证 一、安全协议的基本假设 在设计安全协议时，首先必须注意对安全协议所作的基本假设。通常基本假 设有： ( 1 ) 密文块不能被篡改，也不能用几个小的密文块组成一个新的大密文块； ( 2 ) 一条消息中的两个密文块被视为分两次分别到达； ( 3 ) 密码系统是完善的( p e r f e c t ) ，即只有掌握密钥的主体才能理解密文消息； ( 4 ) 无加密项冲突，即若有 m ij k l = ( m 2 ) k 2 则一定有m l = m 2 ，k l = k 2 。 ( 5 ) 参与协议的主体包含诚实的合法用户和攻击者。合法用户将遵循阱议的规 定执行协议。攻击者也可以是系统的合法用户，但他不会完全遵守协议。 二、安全协议的设计原则 在安全设计协议时，必须遵循一定的设计原则才能保证协议能够满足保密 性、无冗余、认证身份等设计目标。卿斯汉在文献【1 9 1 中提出了以下安全协 议的设计原则： ( 1 ) 设计目标明确，无二义性； ( 2 ) 最好应用描述协议的形式语言，对安全协议本身进行形式化描述： 4第1 章绪论 ( 3 ) 通过形式化分析方法证明安全协议实现设计目标； ( 4 ) 安全性与具体采用的密码算法无关； ( 5 ) 保证临时值和会话密钥等重要消息的新鲜性，防止重放攻击； ( 6 ) 尽量采用异步认证方式，避免采用同步时钟( 时戳) 的认证方式： ( 7 ) 具有抵抗常见攻击，特别是防e 重放攻击的能力； ( 8 ) 进行运行环境的风险分析，作尽可能少的初始安全假设； ( 9 ) 实用性强，可用于各种网络的不同协议层； ( 1 0 ) 尽可能减少密码运算，以降低成本，扩大应用范围。 有关安全协议设计原则的进一步讨论，参见文献 6 6 1 。 三、安全协议的形式描述语言 设计安全协议时，需要用形式描述语言来描述。早期有代表性的描述安全协 议的形式语言有l o t o s 【2 0 】和i n aj o 【2 1 】等。 l o t o s 是基于c c s 的标准化语言，由两部分组成，其中一部分描述抽象数据类 型和密码操作，另一部分描述协议的实体行为。1 9 9 1 年，l o t o s 成为i s o 标准， 随后出现了扩展版本e l o t o s 。i n aj o 基于通信有限状态机的语言，它与l o t o s 不 同，用传统的形式规范语言描述安全协议。 为了统一安全协议描述的标准，出现了以c a s p l1 2 2 1 为代表、通用性较强 的描述安全| 力、议的形式语言。安全协议分析软件i n t e r r o g a t o r 【2 3 】率先应用了早 期版本的c a s p l 语言。当前版本的c a s p l 语言提供通用的描述格式，应用l e x 和y a c c 描述词法和语法，可以自动地分析安全协议格式，具有描述安全目标的 能力。 四、安全协议的验证 安全协议的验证的形式化方法主要有模型检测和定理证明。此外还有p e t r i 网方法、口i 演算方法、c s p 方法和串空间方法等。详细情况见第2 章。 1 1 4安全协议的攻击者模型及其攻击类型 尽管安全协议的发展已经2 0 多年 一个协议，也有许多验证的方法和手段 而且我们可以依据很多设计原则来设计 但是还没有一个协议没有任何漏洞。任 何协议都会成为攻击者潜在的攻击对象。所以我们必须对攻击对手及其攻击类型 有全面和深刻的认识，这有助于安全协议的设计和验证。 中山大举博士学位论文 5 一、攻毒囊攫垄 对于攻击者，普遍采用d o l e v y a o 攻击者模型 2 4 1 。在该模型中，攻击者 有很强的能力，主要能力如下： ( 1 ) 戆够窃瞬、隈囊、截获圈终主任簿漕惠。 ( 2 ) 能够发送消息、熏发消息。 ( 3 ) 能瓣消息进乎亍缀合和分解。 ( 4 ) 熟悉加解、解密、散列( h a s h ) 等密码运算，能进行加密操作，并在知道 解密密钥时，能对加密消息进行解密。 ( 5 ) 麓够嚣充任何按议参与者。 ( 6 ) 具有密码分析的知识和能力。 ( 7 ) 掌握各种攻击知识和手段，并能进行各种攻击。 二、攻击类登 c o l i nb o y d 和a n i s hm a t h u d a 在文献 2 5 】中，通过分析大量的协议及其 存在的攻击，归纳出如下协议攻击类型： ( 1 ，信患窃听。即攻击者捕获协议中发送的信感。应付该攻淹静有效办法楚 加密技术。 ( 2 ) 信息篡改。即攻毒者对窃听的信息进行修改。 f 3 ) 重放攻击。即攻潞者记录协议中发送的信惑并在后一琊议的运行期间发 送绘同一参与者或另一参与者。s y v e r s o n 程文献 2 6 1 中对重放攻击进 行了分类。 ( 4 ) 转发攻击( 反射酸击) 。攻击者将协议的消惑发送回消息的发送者。这可 以靖作重放攻击的特别情形。 f 5 ) 暇务撵缝攻击。攻毒耆茨止或隧碍合法参与若巍行协议。 ( 6 ) 类溅攻击。攻击者用一种类型的协议消息域代替另一种类型的消息域。 例如，作为参与者身份标记的消息域可能被作为密钥的消息域接受。典 型铡子是对著名o t w a y - r e e s 臻议的类型攻潦【2 5 】。 ( 7 ) 密码分析。攻击者在协议运行中获取加密信息后，通过密码分析，获淑 解密密钥，从而对获取的加密信息进行解密。 第1 章绪论 ( 8 ) 证书绦控攻击。杰公锾貉议中，袭击者遥遥选取或骖改 萎书信息对协议 运行进行攻击。一个典型例子怒m e n e z e s 【2 7 】等对m a t s u m o t o 等掇出 的密钥分配协议【2 8 】进行的攻击。 ( 9 ) 蛰议交镑玫壶。玻毒者选取一个掰垂| 孓议与一令己知按议交镫执雩亍。交链 攻击需要两圆台城多回台同时执行协议，著名的例子是l o w e 2 9 1 辩 n s p k 协议的攻击。 1 2静态逻辑 时态逻辑是一种包含时问概念的逻辑，其公式能够表述关于过去、现在和将 来状态的客观事实。时态逻辑的种类有很多，我们这里主要是考虑计算树逻辑 c t f 、分支辩态逻辑c t l ( c o m p u t a t i o nt r e el o g i c ) 霹：l 线往露态邋辑l t l ( l i n e a r t e m p o r a ll o g i c ) 【3 0 1 。 1 2 1 k r i p k e 结构 在毒隈状态莠发系统中，一个k r i 姝e 结稳掰藏楚一个三元缀 0 ，有( 韪，是+ j ) r 。 i 2 2 计算树逻辑c t l 从概念上朱说，c t l * 公式描述的是计算树的性质。计算树的形成如下：酋先 指定k r i p k e 结构中的一个状态终为初始状态，然露姆k r i p k e 缝擒展开戚一攥以 初始状态为横豹无限榜。阗她计算褥稻述了胰秘始状态开始的所有可麓静执行路 径。 c t l 8 公式有路径量溺鞫对态算予缀成。路径量词有两a f f o ra l ic o m p u t a t i o n p a t h s ”) 莘嚣e ( “f o rs o m ec o m p u t 越i o np a t h ”) 。基本时态簿子有5 静：x ( “n e x tt i m e ”) 、 f ( “e v e n t u a l l y ”o r “i n t h e f u t u r e ”) 、g ( “a l w a y s ”o r “g l o b a l l y ”) 、u ( “u n t i l ”) 和 r f “r e l e a s e ”，t h el o g i c a ld u a lo f t h eu o p e r a t o o 。 中山大学博士学位论文 7 一、c t l 8 戆语法 c t l * 有两类公式：状态公式和路径公式。在菜个特定状态为真的公式魑状 态公式。沿着某个特定路径为真的公式是路径公式。下列三个规则给出状态公式 豹语法： 如果p a p ，那么p 是状态公式。 如果f y r gg 是状态公式，那么再f v g 朝f a g 是状态公式。 翔巢，是路径公式，那么e f 帮矗厂是袄卷公式。 下列两个规则给出了路经公式的语法： 魏巢，是状态公式，那么，瞧是路径公式。 如果，和g 感路径公式，那么1 ，、f v g 、f a g 、x f f j g f , j v g 和吣 是路径公式。 c t l * 廷出上瑟纛粼产生兹狡悫公式鹁集会。 二、c t l * 的语义 我们嗣菇表示从s i 开始的硇后缀。如果，是状态公式，那么m ，嗣可意眯 着，在鸶爰态s 必真。螽聚歹是路径公式，箨么m ，露阿意味蓑，瀣若路爱霹为囊a 关系b 递归定义如下： ( 1 ) m ，s l = p惜p “s ) 。 一 ( 2 ) m ，s l _ _ 葫m ，s i v a 。 ( 3 ) m ，s l = f l v f 2甘m ，s 睁矗o rm ，s l = f 2 。 m ，s l = f j 蠛学m ，s l = f ；a n dm ，s l = f 2 。 ( 5 ) m ，s l = e g l喾存在一条从s 出发的路径历使得m ，n t = g t 。 ( 6 ) m ，s i = a 9 1铮对每祭从s 出发的路径高都有m ， 习i 。 ( 7 ) m ，蠢= 五 铮 对万豹第一个获态s ，有m ，s l = f t 。 ( 8 ) m ，硝= ，g l昔m ，卅g l 。 ( s ) m ，曩= g l v 9 2 甘m ，碉= g to r m ，震= 9 2 。 ( 1 0 ) m ，捌= g i 9 2 甘m ，硝= g ia n dm ，j 降9 2 。 q d m ，捌= x 9 1甘m ，l _ g t 。 第1 章绪论 m ，蠢= f g l营存在o ，楚褥m ，| - g 。 m ，捌= g 占j对所有丘d ，都肖m ，矿f _ g 。 m ，捌= g l u 9 2 耸存在t 抛，使得m ，e l = 9 2 ，且对所有。每戤， 罄畜 棚= 9 1 。 ( 1 5 ) 膨，司= g l r 9 2 学对所有j - 0 ，如果对每个矧m ，# | g l ，那么 m ，b 9 2 。 以上假定 和五是状态公式，g l 和9 2 是路径公式。 1 。2 。3分支薅态逻瓣c t l 分支时间逻辑c t l 魁c t l * 的一个约束子集，在c t l 逻辑中，时态算子x 、 f 、g 、u 和r 之前必须立即跟着一个路径量词，如a x 、e f 、a u 和e r 等。 受精确楚瑷，c t l 是通遭便爰下嚣援剩疆定路径公式戆语法蠡获褥敬c t l * 豹子 集，限定规则如下： 如果，和g 是状态公式，那么x f , f f , g f , _ ，吣和皿g 是路径公式。 畜卡个鏊本c t l 算乎： a x 牟日e x ， a f 翻e f ， a g 和e g ， a u 和e u 。 a r 裁e r 。 这十个算子都能用三个算子e x 、e g 和e u 来表示： a x f = 一e x l ，t 在( 女1 ) 步内从j 是g 可达的。 因此t 从s 是g 可达的当且仅当存在一条从状态s 到t 的路径，该路径的边 中山大学博士学位论文 l l 自g 中豹戒受标记。 命题1 1 ( m ，s ) 峰e a k t p 当且仅当对所有从s ，k 步内g 可达的状态t ，都有( m ，f ) 净尹。 命题1 2 ( 材，5 ) 辟q 妒当且仅当对所有从s ，g 可达的状态t ，都有( 辐 ) | _ 妒。 1 3 2 时态认知逻辑 时态认知逻辑由时态逻辑和认知逻辑组合而成，根据时态逻辑的不同有很多 糖方式。h a l p e m 和v a r d i 在文献 3 2 1 中讨论了蠢班l 对态邋辑和认知逻辑 组合的逻辑c k l ( c o m b i n a t i o no fk n o w l e d g ea n dl t l ) 并给出了模型检溅方法。 c k l 公式集w f f 定义如下【3 3 】： 弼瞥：= t r i t e l p芦p r i m i t i v ep r o p o s i t i o n s * l 一m 撕b产n e g a t i o n * | , 1 * d i s j u n c t i o n * io * n e x t * l u * u n t i l * ik , * a g e n tik n o w s + ， i c c 胪i ti sc o m m o nk n o w l e d g ei ngt h a t 。 吴立军等雀文蠢谨l 】中讨论tc t l 遗罄霸议煞遴辑组合弱c k c ( c o m b i n a t i o n o f k n o w l e d g ea n dc t l ) 并给出了模型检测方法。c k c 公式凹盯可定义如下： ：= t r u e lp 绣，为骧子鑫麓群 i - - , i v le x le g ie u c k c j s , i 第1 章绪论 l k , 1 c g k a i l es u 等在文献 3 4 1 中研究了由c t l * 平 i 认知逻辑组合逻辑，并给出模 型检测方法。 1 4论文的主要工作和章节安排