（计算机应用技术专业论文）基于petri网的密码协议分析.pdf

山东科技大学硕士学位论文 摘要 密码协议的安全性分析对于保障计算机网络的安全通信具有重要意义。运用形式化 方法对密码协议进行分析一直是该领域的研究热点。目前密码协议的形式分析方法包括： 逻辑方法、模型检测方法、定理证明方法和p e t r i 网方法等，这些方法各自有它们的优 点和缺点。本文主要针对p e t r i 网方法在密码协议分析中存在的一些不足，研究将p e t r i 网方法和模型检测方法的一些理论成果结合起来对密码协议进行分析，取得了如下结果： 1 提出将运行模式法和p e t r i 网建模结合起来分析密码协议的思想，给出了协议运 行模式的基础p e t r i 网模型和攻击p e t r i 网模型的概念，并阐述了两者与密码协议分析 之间的关系。 2 给出协议运行模式的基础p e t r i 网模篓啪攻击p e t r i 网模型的构造方法，在此基 础上给出密码协议分析的具体步骤。 3 具体对n e e d h a m - - s c h r o e d e r 公钥协议，h e l s i n k i 协议以及t m n 协议进行了分析， 并对密码协议的一类攻击的特点做出了概括。 本文工作的特点是： 1 利用协议的运行模式来指导p e t r i 网建模，这使得我们的方法与一般p e t r i 网 方法分析密码协议的思路有所不同。 2 以一个协议的两个实例并行运行时可能存在的攻击为例，探讨了多个实例并行运 行情况下的协议安全问题。 关键词：密码协议，形式分析，p e t r i 网，模型检测，运行模式 山东科技大学硕士学位论文 a b s t r a c t a n a l y s i so fc r y p t o g r a p h i cp r o t o c o li ss i g n i f i c a n tf o rs e c u r ec o m m u n i c a t i o n b e t w e e nc o m p u t e rs y s t e m st h r o u g hn e t w o r k s u s i n gf o r m a lm e t h o d st oa n a l y z e c r y p t o g r a p h i cp r o t o c o lr e m a i n st h ek e yi s s u ei nt h i sf i e l d a tp r e s e n tt h ef o r m a l m e t h o d s i n c l u d el o g i cm e t h o d ，m o d e lc h e c k i n gm e t h o d ，t h e o r e mp r o v i n gm e t h o d ，p e t r i n e tm e t h o d se t c t h e s em e t h o d sa l ih a v et h e i ra d v a n t a g e sa n dd i s a d v a n t a g e s a i m i n g a tt h ew e a k n e s si nt h ea n a l y s i so fc r y p t o g r a p h i cp r o t o c o lu s i n gp e t r in e t m e t h o d ，t h et h e s i sm a i n l yd i s c u s s e sc o m b i n i n gp e t r in e tm e t h o dw i t hs o m er e s u l t s o fm o d e lc h e c k i n gt h e o r yf o rt h ea n a l y s i so fc r y p t o g r a p h i cp r o t o c 0 1 t h em a i n r e s u l t st h ea u t h o ro b t a i n e da r ea sf o l l o w s ： 1 c o m b i n er u n n i n g - m o d e sm e t h o dw i t hp e t r in e tm o d e l i n gt oa n a l y z e c r y p t o g r a p h i cp r o t o c o l ，g i v et h ec o n c e p t so fb a s i cp e t r in e tm o d e la n da t t a c k i n g p e t r in e tm o d e lo fp r o t o c o l s r u n n i n gm o d e sa n dc l a r i f yt h er e l a t i o n s h i pb e t w e e n t h et w om o d e l sa n da n a l y s i so fc r y p t o g r a p h i cp r o t o c 0 1 2 p r e s e n tt h em e t h o dt oc o n s t r u c tab a s i cp e t r in e tm o d e la n da na t t a c k i n g p e t r in e tm o d e l ，s u b s e q u e n t l yg i v ed e t a i l e ds t e p sf o ra n a l y s i so fc r y p t o g r a p h i c p r o t o c 0 1 3 a n a l y z et h en e e d h a m - s c h r o e d e rp r o t o c 0 1 h e l s i n k ip r o t o c o la n dn 州p r o t o c o l i nd e t a i la n ds u m m a r i z eat y p eo fa t t a c ko fc r y p t o g r a p h i cp r o t o c o l s t h ec h a r a c t e r i s t i c so fo u rw o r ka r ea sf o l l o w s ： 1 c o n s t r u c tp e t r in e tm o d e la c c o r d i n gt ot h ep r o t o c o l sr u n n i n gm o d e s ， w h i c hi sd i f f e r e n tf r o mu s u a lp e t r in e tm e t h o do fa n a l y s i so fc r y p t o g r a p h i c p r o t o c o l s 2 m a i n l yd i s c u s sap r o t o c o l ss e c u r i t y w h e nm a n yc a s e s ( t a k et w oc a s e sa s a ne x a m p l e ) a r ee x e c u t e di np a r a l l e l k e y w o r d s ：c r y p t o g r a p h i cp r o t o c o l ，f o r m a la n a l y s i s ，p e t r in e t ，m o d e lc h e c k i n g ， r u n n i n gm o d e s 声明 本人呈交给山东科技大学的这篇硕士论文，除了所列参考文献和世所公认 的文献外，全部是本人在导师指导下的研究成果。该论文尚没有呈交于其它任 何学术机关作鉴定。 研究生签名； 日期 a f f i r m a r i o n id e c l a r et h a tt h i sd i s s e r t a t i o n s u b m i t t e di nf u l f i l i m e n to ft h e r e q u i r e m e n t sf o r t h ea w a r do fm a s t e ro fe n g i n e e r i n g ，i ns h a n d o n g u n i v e r s i t yo fs c i e n c ea n dt e c h n o l o g y ，i sw h o l l ym yo w nw o r ku n l e s s r e f e r e n c e do fa c k n o w l e d g e t h ed o c u m e n th a sn o tb e e ns u b m i t t e df o r q u a l i f i c a t i o na ta n yo t h e ra c a d e m i ci n s t i t u t e s i g n a t u r e ： d a t e ： 扎一 k b ， 一 i l 码；b 些量型蔓查兰堡主堂堡堕苎 ：篁丝 1 绪论 1 1 课题的提出 随着i n t e m e t 技术的目益发展，网络上的信息安全问题日益突出特别是电子商务、 数字货币和网络银行等新业务的深入开展，信息的保密性、完整性和可用性等安全问题 成了关键之所在。解决这一问题的有效手段就是使用现代密码技术。数据加密技术是解 决网络上信息传输安全的主要方法。它不仅建立在数据加密算法设计上面，而且也取决 于所设计密码协议的安全性和正确性。目前，密码协议已广泛应用于计算机网络与分布 式系统中，包括现在电子商务主要应用的密码协议：s s l 协议和s e t 协议。如果协议设 计不当，无异于在坚固的堡垒中留下了个后门，入侵者不用击破密码体制就能得到信息 和产生假冒，自1 9 7 6 年d i f f i e 和h e l l m a n 提出第一个重要的密码协议 1 】以来，人们已经 设计出很多协议。然而许多协议常常刚一发表，便发现有漏洞，如n s 认证协议 2 1 在1 9 8 1 年被d e n n i n g 和s a e c o 发现存在安全缺陷。3 。另外，一些协议，可能有微小的安全漏洞 而长期不被人们发现，如对上述n s 协议虽然多次改进但1 9 9 6 以后仍然被检铡出易受到 重放攻击。造成协议受到攻击的原因是协议本身很复杂，缺乏对设计出的协议进行足够 的一致性和安全性分析。过去人们往往通过攻击方法对协议的正确性进行分析，但是这 种方法由于攻击手段的多样性和不可预测性，只能在一定程度上证明协议的正确性，不 能全面客观的分析协议。因此，人们寻求用形式化方法来分析协议，帮助我们查找漏洞 和证明协议的安全性。 一 1 2 密码协议分析的研究现状 目前，密码协议的形式分析方法大致分为四类： ( 1 ) 逻辑方法 基于信仰和知识的逻辑形式分析方法它以b a n 逻辑为代表，同时还包括大量的扩 展和改进的b a n 逻辑，我们将这一类称为b a n 类逻辑( b a n - l i k el o g i c ) 。 ( 2 ) 通用形式方法 这种方法采用一些通用的形式方法来说明和分析密码协议，如最弱前置谓词和p e t r i 这种方法采用一些通用的形式方法来说明和分析密码协议，如最弱前置谓词和p e t r i 山东科技大学硕士学位论文绪论 网等。 ( 3 ) 模型检测方法 基于代数方法构造一个运行协议的有限状态系统模型，再利用状态检测工具来分析密 码协议的安全性。 ( 4 ) 定理证疆方法 将密码协议的安全性作为定理来证明，这是一个新的研究热点。 由于论文内容与密码协议分析的模型检测方法和p e t r i 网方法有关，所以只介绍一下 这两种方法的研究现状。 ( 一) 模型检测方法 模型检测技术是一种验证有限状态系统的自动化分析工具，原是一种用于分析和模 拟硬件工作过程的形式化方法，随着形式化方法的日益进步和应用领域的推广，模型检 测现已用于软件分析和通信协议模拟等多个领域。1 9 9 6 年，g a v i nl o w e 首次使用c s p 和模型检测技术对密码协议进行分析【4 】，在这篇文章中，g a v i nl o w e 首次采用c s p 模型 和c s p 模型检测工具f d r 来分析n e e d h a m - s c h r o e d e r 公钥协议，并成功地找到一个以前 未发现的攻击。模型检测的成功，使学者们相继投入到这个领域5 h 】，发现了协议的许 多以前未发现的新的攻击。 对于协议分析来讲，模型检测已经证明是一条非常成功的途径，我国学者在这方面 也做了不少工作f 1 6 l ，文献 1 4 根据模型检测技术分析密码协议的若干结论，提出一种 两者密码协议的运行模式分析法，该方法的基本思想是建立一个包含入侵者的运行协议 的小系统，分析协议在此小系统上所有可能的运行模式来发现攻击。该方法的优点是： 一方面可以为用模型检测工具分析两者密码协议提供完备性；另一方面，由于掌握一种 模型检测工具需要一定的时间，利用该方法可以脱离模型检测工具，结合自己熟悉的方 法去分析密码协议。 ( 二) p e t r i 网方法 p e t r i 网的概念是1 9 6 2 年由德国的c a p e t r i 博士提出来的，作为一种并发系统建 模和分析的工具，p e t r i 网已被成功地应用在计算机科学的各个领域。9 0 年代以来，p e t r i 网特别是颜色网73 开始用来分析密码协议。如加拿大q u e e n su n i v e r s i t y 的q u e e n s c r y p t o g r a p h ya n dd a t as e c u r i t yl a b o r a t o r y 的t a v a r e s 教授课题组针对攻击者行为集合，采 用颜色网来模拟和分析攻击者行为，他们成功的分析了多个密码协议并发现了许多以前 2 山东科技大学硕士学位论文绪论 没有发现的缺陷，文献 1 8 ，1 9 ，2 0 反映了他们的研究成果；h c l s i n k iu n i v e r s i t yo f t e c h n o l o g yd i g i t a ls y s t e m sl a b o r a t o r y 的t a u r a 3 采用谓词变迁p e t r i 网成功分析了n s 认证协议；h a mn a mu n i v e r s i t y 的g a n g - s o ol e e 盼2 3 等引入了密码协议时间p c t r i 网来验 证分析了t m n 2 3 1 协议；u n i v e r s i t yo fc a m b r i d g e 的f c d c r i c oc r a z z o l a r a 2 4 。5 3 等借助于 p e t r i 网的进程网( 进程语言) 证明密码协议的安全性也取于导一定成果。以上是国外所从 事的这方面的工作。国内从事这方面工作的总的来说比较少【2 6 】。吲，例如：文献 2 6 利用 对象p e t r i 网来描述和分析认证协议，文献 2 8 利用时延p e t r i 网对协议进行分析和性能 的评估。 p e t r i 网作为一种形式方法已经成功地应用于密码协议的描述，验证和分析中，但我 认为该方法还存在着一些不足之处： ( 1 ) p c t r i 网能够直观清晰地描述密码协议和验证密码协议存在的攻击，但对于如 何分析协议，找到对它的攻击却没有很好的方法。通常我们用p c t r i 网分析密码协议的步 骤为：构造协议的p e t r i 网模型；分析该模型，找到协议的一些潜在弱点；根据 中找到的协议的弱点，构造协议带攻击者的p e t r i 网模型，确定模型的初始状态和不安全 状态，通过解状态方程或构造可达树分析不安全状态是否可达，如果可达，那么对应的 变迁发生序列即是攻击剧情。对于第步，如何通过模型去找协议的弱点进而构造带 攻击者的p e t r i 网模型，常常具有一定的盲目性和不全面性。 ( 2 ) 密码协议可以有多个实例并行运行，而且同一主体在不同的实例中可以担任不 同的角色，在分析过程中，常常要考虑交叉实例间消息的相互影响，比如并行会话攻击 就是在这种情况下产生的。对于这种情形，如何利用p e t r i 网来描述和分析呢? ( 3 ) 状态爆炸问题。随着密码协议复杂度增加，p e t r i 网豹规模和可达标识集膨胀 非常快，使得分析的难度增大，这也是p e t r t 网应用不容回避的个问题。 1 3 论文的研究思路和内容安排 1 3 1 论文的研究思路 本文的工作是在考虑上面提到的p e 伍网分析密码协议存在的一些问题的基础上进 行的： 对于第( 1 ) 个问题，文献 1 4 中提到的密码协议的运行模式法可以为我们如何构造 带攻击者的p e t r i 网模型提供明确的目标，这样我们就可以依据协议的运行模式直接构造 出带攻击者的p e t r i 网模型，然后在这个模型的基础上去分析入侵者对协议造成有效攻击 3 山东科技大学硕士学位论文 绪论 的条件就可以了，如果这样的条件能够找到，就等于找到了协议的攻击方法。具体的步 骤可以参看论文的第4 章。 针对第( 2 ) 个问题，我们在文中着重对一些密码协议两个实例并行运行的情形进行 了分析，具体例子可以参看论文的第4 ，5 章，该分析方法同样适用于n 个实例( n 2 ) 并行运行的情况。 对于第( 3 ) 个问题，我们采取了以下措施：在不影响密码协议分析的前提下，用 尽量少的库所和变迁来描述协议的运行，省略一些不必要的细节，让库所和变迁的意义 尽量的单纯。在协议分析过程中，必然要考虑各种信息，以及攻击者如何去利用这些 信息达到攻击的目的，我们把这个信息处理的过程从模型中独立出来，一方面有利于信 息的集中分析；另一方面也使得p e t r i 网模型的构造更加的简单清晰。我们提出的方法 采用了状态倒推的思想，降低了攻击路径的搜索量。 1 3 2 论文的内容安排 论文共分6 章，在第2 章介绍了密码协议的基本概念以及密码协议分析方法的分类 与进展情况：在第3 章中，我们首先简要介绍了p e t r i 网的应用情况，然后介绍了p e t r i 网的定义，系统模拟和性质分析方法；第4 章提出一种密码协议的分析方法，首先介绍 文献 1 4 中提出的密码协议分析的运行模式法，这是我们方法的基础，然后提出了协议 运行模式的基础p e t r i 网模型和攻击p e t r i 网模型的概念以及两者与密码协议分析的关系， 最后给出了密码协议分析的具体步骤并按照步骤分析了n e e d h a m - - s c h r o e d e r 公钥协议； 第5 章利用第4 章中给出的方法对h e l s i n k i 协议，t m n 协议进行了分析，并对一类密码 协议攻击的特点作出了概括；论文最后一章总结了所做的工作，并对进一步的研究内容 作了探讨。 4 山东科技大学硕士学位论文 密码协议的形式分析 2 密码协议的形式分析 2 1 密码协议基本概念 2 1 1 密码协议概念 所谓协议( p r o t o c 0 1 ) ，就是两个或两个以上的参与者为完成某项特定的任务而采取 的一系列步骤。这个定义包含三层含义：第一，协议自始至终是有序的过程，每一步骤 必须依次执行，在前一步没有执行完之前，后面的步骤不可能执行。第二，协议至少需 要两个参与者。一个人可以通过执行一系列的步骤来完成某项任务，但它不构成协议。 第三，通过执行协议必须能够完成某项任务。即使某些东西看似协议，但没有完成任何 任务，也不能成为协议，只不过是浪费时间的空操作。 我们把为了完成某种安全任务的协议称为安全协议。安全协议为了保证安全性，其 设计必须采用密码技术，因此，我们也将安全协议称作密码协议。下面我们给密码协议 下一个定义： 密码协议是建立在密码体制基础上的一种交互通信的协议，它运行在计算机通信网 或分布式系统中，借助于密码算法达到密钥分配，身份认证等目的。 应用于计算机通信网的密码协议始于1 9 7 8 年r m n e e d h a m 和m d s c h r o e d e r 发表的 n s 认证协议，这是第一个应用于计算机网络的密码协议。n s 认证协议的提出，使计算机 通信网络的安全性发生了革命性的变化，这也是密码协议设计的里程碑，以后很多著名 的协议比如k e r b e r o s 协议便是在此协议基础上发展起来的。 n s 认证协议提出后，1 9 8 1 年d e n n i n g 和s a c c o 发现n s 协议中存在安全缺陷：当一 个主动攻击者用一个旧的泄漏的会话密钥冒充新的会话密钥时，攻击便成功了。1 9 8 7 年 n e e d h a m 和s c h r o e d e r 提出了改进的n s 协议阻们，n s 协议中是使用一次性随机数来表示 其新鲜性，而k e r b e r o s 是利用时间戳来表示其新鲜性，要求认证主体之间要保持时钟同 步。到目前为止，密码协议设计中依然用时间戳和随机数来表示信息的新鲜性啪川。 在进行密码协议的设计时，常常要用到密码算法。这些算法可以是对称加密算法( 如 d e s ，i d e a ) ，也可以是非对称加密算法( 如r s a ) 。如对于常用的认证系统来讲，大多数 些奎型垫查兰堡主堂垡堡苎 童苎垫堡塑丝茎坌堑 系统是采用单钥体制的，并且这个密钥是通过安全地脱机方法建立的。而公钥体制中， 通常是利用证书机构颁发的公钥证书来认证主体的公钥和身份，而且证书具有一定的有 效期，超过有效期的证书都被认为是无效的，在这一方面典型的应用是c c i t t x 5 0 9 认证 框架。 2 1 2 密码协议分类 将密码协议进行严格分类是很难的事情，从不同的角度出发就有不同的分类方法。 例如，根据安全协议的功能，可以将其分为认证协议、密钥建立( 交换、分配) 协议、 认证的密钥建立( 交换、分配) 协议；根据i s o 的七层参考模型，又可以将其分成高层 协议和低层协议；按照协议中所采用的密码算法的种类，又可以分成单钥协议、公钥协 议或混合协议等。这里我们采用王育民教授在通信网的安全一理论与技术 3 2 3 中的分 类，把密码协议分成以下三类： ( 1 ) 密钥建立协议( k e ye s t a b l i s h m e n tp r o t o c 0 1 ) ：在两个实体之间建立共享密钥； ( 2 ) 认证建立协议( a u t h e n t i c a t i o np r o t o c 0 1 ) ：向一个实体提供对他想要进行通信 的另一个实体的身份的某种程度的确信。 ( 3 ) 认证的密钥建立协议( a u t h e n t i c a t e dk e ye s t a b l i s h m e n tp r o t o c 0 1 ) ，在一个 实体与另一个身份已被或可被证实的实体之间建立共享密钥。 2 2 密码协议的安全性 2 2 1 密码协议的安全性及攻击 目前设计出的密码协议已有很多，但是许多协议常常刚一发表，便发现有漏洞。造 成协议失败的原因很多，最主要的是因为协议的设计者对安全需求的定义研究的不够透 彻，并且缺乏足够的安全性分析。正像密码算法的设计一样，要证明协议的不安全性要 比证明其安全性要容易得多。 在分析密码协议的安全性时，常用的方法是对密码协议施加各种可能的攻击来测试 其安全度。密码协议攻击的目标通常有三种： ( 1 ) 协议中采用的密码算法； ( 2 ) 算法和协议中采用的密码技术： ( 3 ) 协议本身。 坐壅型垫查兰堡主兰垡丝苎 壁苎塑堡塑丝茎坌堑 我们这里将主要研究对协议自身的攻击，而假设协议中采用的密码算法和密码技术 均是安全的。对协议本身的攻击可以分为被动攻击和主动攻击两类p ”。 被动攻击是指协议外部的实体对协议执行的部分或整个过程实施窃听。攻击者对协 议的窃听并不影响协议的执行，他所能做的是对协议的消息进行观察，并试图从中获得 协议中涉及的各方的某些消息。他们收集协议各方之间传递的消息，并对其进行密码分 析。被动攻击的特点是难以检测，因此在设计协议时应该尽量防止被动攻击，而不是检 测它们。 攻击的第二种主要类型是主动攻击，这些攻击涉及某些数据流的篡改或一个虚假流 的产生。这些攻击还能进一步划分为四类：伪装、重放、篡改消息和拒绝服务。 伪装就是一个实体假装为一个不同的实体。伪装攻击通常包括其他主动攻击形式中 的一种，例如，鉴别序列能够被劫获并且在一个合法的鉴别序列发生后进行重放，通过 伪装具有这些特权的实体，从而导致一个具有某些特权的授权实体获得某些额外特权。 重放涉及一个数据单元的被动获取以及后继的重传，以产生一个未授权的效果。 消息的篡改意味着一个合法消息的某些部分被改变，或消息被延迟或改变顺序，以 产生一个未授权效果。例如，一条消息为“允许s m i t h 读机密文件a c c o u n t s ”被篡改为 “允许b r o w n 读机密文件a c c o u n t s ”。 拒绝服务防止或禁止通信设施的正常使用或管理。这种攻击可能具有一种特定目标， 例如，一个实体可能抑制所有的消息指向某个特殊的目的地( 如安全审计服务) 。另一种 形式的拒绝服务是使整个网络崩溃，或者通过使网络不能工作的手段，或者滥发消息使 之过载，以达到降低性能的目的。 2 2 2 密码协议的设计规范 在协议的设计过程中，一方面要求协议具有足够的复杂性以抵御组合攻击。另一方 面，还要尽置使协议保持足够的经济性和简单性，以便可应用于低层网络环境。如何设 计密码协议才能满足安全性、有效性、完整性和公平性的要求呢? 这就需要对我们的设 计空间规定一些边界条件。归纳起来，可以提出以下安全协议的设计规范。 1 采用一次随机数来替代时间戳 2 具有抵御常见攻击的能力 3 适用于任何网络结构的任何协议层 4 适用于任何数据处理能力 山东科技大学硕士学位论文密码协议的形式分析 5 可采用多种密码算法 6 。便于进行功能扩充 7 最少的安全假设 以上协议设计规范并不是一成不变的。我们可以根据实际情况作出相应的补充或调 整。但是，遵循上面提出的这凡条规范是设计一个好协议的基础。 2 2 3 密码协议的安全分析 协议分析是揭示密码协议中存在漏洞的重要途径。分析的方法有： 1 攻击检验方法一一非形式化方法 这种方法对协议进行分析一般是根据已知的各种攻击方法来对协议进行攻击，以攻 击是否有效来检验密码协议是否安全。由于存在许多未知的攻击方法。所以非形式化分 析只是停留于发现协议中是否存在着已知的缺陷而不能全面客观的分析密码协议。这是 密码协议早期的主要分析方法。 2 形式化分析方法 自九十年代初以来，密码协议的形式化分析成为研究热点，该方法的出发点是希望 将密码协议形式化，而后借助于人工推导，以及计算机的辅助分析来判别密码协议是否 安全可靠。与非形式化方法相比，它能全面、深刻的检测到密码协议中细微的漏洞。到 目前为止，我们可将密码协议的形式分析方法大致分为4 类：逻辑方法、模型检测方法、 定理证明方法和包括p e t r i 网方法在内的通用形式方法。 3 密码协议的形式分析3 4 ，3 5 l 2 3 1 密码协议形式分析的前提 1 完善加密( p e r f e c te n c r y p t i o n ) 前提 协议采用的密码系统是完美的，不考虑密码系统被攻破的情况； 必须知道解密密钥才能解密加密数据； 无加密项冲突，即若有e 。( m 1 ) = e t z ( m 2 ) 一定有m l - - - - m 2 ，k l k 2 成立。 2 协议的参与者 参与协议运行的主体分为诚实的合法用户和入侵者。诚实的合法用户将严格按照协 议规定参与协议运行。攻击者也可以是系统的合法用户，拥有自己的加密和解密密钥。 山东科技大学硕士学位论文 密码协议的形式分析 但入侵者不会按照协议规定参与协议运行，而是企图窃密或假冒其他诚实的合法用户。 3 入侵者的知识与能力 入侵者的知识： 了解现代密码学，知道加解密等运算操作； 知道参与协议运行的各主体名及其公钥，并拥有自己的加密和解密密钥； 每窃听或收到一个消息，即增加自己的知识。 入侵者的能力： 可窃听及中途拦截系统中传送的任何消息； 在系统中可插入新的消息： 即使不知道加密部分的内容，也可重放他所看到的任何消息( 其中可改变明文 部分) ； 可运用他知道的所有知识( 如临时值) ，并可产生新的临时值。 下面我们给出一个三者密码协议的分析框架图，从图2 1 中可以看出入侵者i 完 全控制了参与协议运行的三个参与者a 、b 、s 之间的信息交换。这正是我们对在密码协 议分析中，入侵者所具备能力的强有力假设。 图2 1 三者密码协议分析框架 2 3 2 密码协议形式分析方法的分类与进展 形式化分析协议的工作，普遍认为是从d o l e v 和y a o 呤们的研究开始的，此后的大多 数状态机分析都或多或少的受到他们的影响。在d o l e v y a o 模型里，攻击者能读任何 在网上传递的数据，或破坏消息，或创建消息，或执行某些动作如加解密。因此若攻击 者的目的是发现一秘密消息，那么就可以分析出攻击者是通过重写消息来达到目的， d o l e v 和y a o 为这个分析使用了术语重写系统的概念，并发展了一些分析算法。 经过近2 0 年的发展，形式化分析已取得了丰富的成果，目前，形式化分析协议主要 以下几类： 坐壅型垫；苎堂塑圭兰堡笙塞 矍竺垫望塑垩茎坌塑 ( 1 ) 逻辑方法 基于信仰和知识的逻辑形式分析方法，它以b a n 逻辑为代表，同时还包括大量的扩展 和改进的b a n 逻辑，我们将这一类称为b a n 类逻辑( b a n 一1 i k el o g i c ) 。 ( 2 ) 通用形式方法 这种方法采用一些通用的形式方法来说明和分析密码协议，如最弱前置谓词和p e t r i 网等。 ( 3 ) 模型检测方法 基于代数方法构造一个运行协议的有限状态系统模型，再利用状态检测工具来分析密 码协议的安全性。 ( 4 ) 定理证明方法 将密码协议的安全性作为定理来证明，这是一个新的研究热点。 2 3 2 1b a n 及类b a n 逻辑( b a n b a n - l i k el o g i c ) b a n 7 1 逻辑自1 9 8 9 年被提出以来，因其简单而实用得到了协议分析者的广泛关注和 研究。g n y ，a t ，v o ，s v o 3 8 3 9 舯川逻辑都是对b a n 逻辑的扩充和改进，我们称类b a n 逻 辑。b a n 逻辑形式化定义了协议的目标并且确定了协议初始时刻各参与者的知识和信任， 通过协议中信息的发送和接受步骤产生新的知识。运用推导规则来得到最终的经验和知 识。如果最终知识和信任的语句集里不包含所要得到的目标知识和信任的语句时，就说 明协议存在安全缺陷。b a n 逻辑简单直观。容易使用，这是它的优点。它的主要缺点有： d ) b a n 逻辑没有完整的语义，所以推理过程得到的某些命题，虽然语法正确，但没有明 确的含义。理想化过程没有严格定义，所以协议消息转换成逻辑公式后，可能包含原 协议消息中并不包含的信息。b a n 逻辑只能分析安全协议的认证属性，不能分析保密 属性。b a n 逻辑的抽象层次比较高，而且不能自动给出有缺陷协议的攻击实例。 2 3 2 2 模型检测方法 众所周知，模型检测技术原是一种用于分析和模拟硬件工作过程的形式方法，随着 形式方法的日益进步和应用领域的推广，模型检测技术现在己用于软件分折和通信协议 模拟等多个领域，但用于密码协议的分析还是这几年的新的应用。 在1 9 9 6 年，g a v i nl o w e 首先使用c s p 模型和c s p 模型检测工具f d r 分析n s 协议4 1 ， 并成功的找到一个以前从未发现的攻击。模型检测的成功，使学者们相继投入到这个领 j 0 些壅鲨查堂堡主堂垡堡壅童璺垫堡盟丝苎坌堑 域，其他用于密码协议分析的模型检测方法还有m u r 妙7 3 和b r u t u s 4 2 1 ，其中b r u t u s 是专 用于密码协议的模型检测工具。实践证明对于密码协议分析来讲，它是一条非常成功的 途径。 模型检测用于有限状态系统的分析，这就要求研究如何为密码协议构造有限状态系 统。即构造一个运行协议的小系统模型( 通常是一个有限状态转换系统) ，同时结合一个 有通常意义下的入侵者模型，它能与协议交互作用，利用状态探测工具来发现系统是否 进入一个不安全状态。有关具体内容参见文献 1 1 。 模型检测方法有着很明显的优点，首先是这种方法的自动化程度高，在验证过程中 不需要人参与；其次是如果协议有缺陷，能够自动产生反例。它的缺点是：容易产生 状态爆炸问题，所以不能用于比较复杂的协议或者处理复杂协议的效率不高；一般需 要指定运行参数，比如运行实例，主体数量，因而没有发现错误并不能保证协议正确； 该方法用于有限状态系统，一方面会限制它能分析的密码协议的种类；另一方面将面 惯如何将密码系统说明成有限系统而不增加或减少密码协议的安全性的问题；另外如何 评价和衡量不同的检测工具和方法也是值得考虑的问题。 许多研究人员做了很多工作去解决上面的问题，一方面的工作是解决状态空间爆炸 问题，也就是使用各种方法减小验证过程的状态数；另外一方面的工作是尽量实现模型 检测方法的完备性。这方面的工作可以分为两种：1 ) 从理论上分析当一个协议存在攻击 时，发现这个攻击所需要的运行实例的上界；2 ) 设计出可以用于无限状态空间的状态搜 索方法。第一种情况的研究工作主要包括：证明在一定条件和执行环境下，如果一个小 系统没有攻击，那么不受限制的大系统也是安全的；建立攻击大多数协议时所需实例的 上界。第二种情况的研究工作基本上都使用了符号技术，一个符号状态可以表示无限多 的具体状态，这种方法不器要限制攻击者的操作，也就是可以处理由于攻击者产生了无 限多的消息而引起的无限状态问题，但不能用于由于无限多的协议运行实例而造成的无 限状态问题。 2 3 2 3p e t r i 网方法 p e t r i 网是一种用于并发、异步系统建模和分析重要工具。经过四十余年的研究， p e t r i 网理论成果十分丰富，并且已开发出相应的理论分析工具和软件。它已经成功分 析了众多的通信协议，特别适合于分析协议的并发、并行、和异步特性。这方面的工作 主要有：v a r a d h r a j a n 用p e t r i 网来分析安全系统中的信息流的安全性。q u e e n s 1 1 坐奎型垫查兰堡圭兰垒丝奎 童塑塑堡蝗垄壅坌堑 u n i v e r s i t y 采用颜色网来分析协谢讳，1 9 】，并发现了一些协议的缺陷。他们通过建立状态 可达矩阵，采用状态分析来验证协议。通过引入攻击者模型，生成模型的可达树和攻击事 件序列来找到协议的不安全状态。 利用p e t r i 网分析密码协议常常要用到倒推分析的方法。倒推分析思想是由m i l l e n 教授和h e a d o w s 教授提出的【4 3 l 。在他们提出的系统中，用倒推搜索代替正向搜索。若用 户能够描述出一个不安全的状态，系统就能判断该状态是否可达。关于m i l l e n 教授的 “i n t e r r o g a t o r ”系统和m e a d o w s 教授的“n r lp r o t o c o la n a l y z e r ”的分析工具，可参 阅文献 4 4 ，4 5 。被验证是安全的协议一定会避免协议进入不安全的状态。所谓不安全状 态是由协议的易于攻击的地方、错误使用协议或使用协议过程中产生不想要的状态以及 背离协议初始目标所产生的状态组成的。倒推状态分析方法不能够提供协议安全的保证， 但能够决定协议在侵入检测攻击下，协议是否安全。换句话说，就是检查称为不安全状 态的状态是否可达。 p e t r i 网作为一种形式方法已经成功地应用于密码协议的描述，验证和分析中，对 于协议分析来讲它面临的也是状态爆炸和无法确保已被分析安全的协议是否真的安全这 两个关键问题。 2 ，3 2 4 定理证明方法 这是一个新的研究热点，同证明程序的正确性一样，将协议的证明规约到证明一些 循环不变式。这方面开始于k e n w n e r e r 的i n a3 0 和i t p 的研究【4 3 1 ，文献 4 6 尝试用 i s a b e l l e 这种定理证明系统描述k e r b e r o s 协议，并研究了k e r b e r o s 协议的安全性a 这 个领域里值得一提的还有b o l i g n a n a 的c o q 系统，d u t e r t r e 和s c h n e i d e r 的p v s 证明系 统【4 7 】以及s n e k k e n e s 的公理证明器h o l h 8 1 。 规约证明方法既可手动进行，也可自动证明：自动证明比较复杂，是目前一个发展 方向。关于协议验证的研究也是基于规约证明的，其自动化证明需进一步完善。 2 3 3 协议形式描述语言进展 另一个问题涉及到协议本身的形式描述。协议一般在经过形式描述后，再用分析工 具进行有效分析。为此，研究者发展了描述协议的形式语言，早期有l o t o s h 9 1 和i n a j o 叫 等。 l o t o s 是一种基于c c s 的标准化语言，适于描述分布式系统，它由两部分组成，首 先描述抽象数据类型和加密操作，其次描述协议实体行为。l o t o s 标准制定于1 9 9 1 年， l2 生查型垫查堂堡圭堂垡堕塞 查墨塑些塑丝茎坌堑 后来又有了扩展版本e - l o t o s 。 与l o t o s 不同的是，k e n m e r e r 用传统形式规范语言i n aj o 描述协议。该语言基于 通信有限状态机，它允许证明由状态变量定义的安全性。 但是不同系统都以方便自身进行分析的格式来重写协议，这种协议描述的标准不统 一是不同分析系统互补交流的严重障碍，也使得分析手段的应用在格式化协议时容易出 错。于是人们着力研究新的通用性较强的形式描述认证协议语言，c a s p l m 5 1 l 就是这些语 言的代表，它适用l e x ，y a c c 描述词法和语法，可以自动分析协议格式，具有描述实体 认证目标的能力，且至今仍在发展中。 2 3 4 形式分析小结 到目前来看，还很难找出一种方法把密码协议的各个方面全部包括进去，因此，要 找出一种分析方法能够发现或防止密码协议所有可能的漏洞似乎是不可能的。我们希望 的最好结果是，在给定合适的假设条件下，应能保证协议的正确性。 协议验证研究仍在发展中，通常真实的协议难于分析，原因有以下几点： ( 1 ) 协议描述不精确，协议实际特性比抽象出来的加密特性更加复杂； ( 2 ) 复杂协议通常还与加密算法和其它因素有关； ( 3 ) 信息的多样性很难考虑完全； ( 4 ) 协议的结构虽然简单，但实际执行情况却很复杂，可以有任意多的实例并行运行， 一个主体可以同时参与多个实例，而且在不同实例中可以有不同的角色，在分析过程中 要考虑交叉方式以及交叉实例间消息的相互影响，这个过程是很困难的。 ( 5 ) 攻击者有很多的攻击方式，而且它可以重复使用一种方式，也可阻多种攻击方式 同时使用，在分析协议时，要充分的考虑入侵者所具备的各种能力，这也是很困难的。 山东科技大学硕士学位论文p e 砸网概述 3 p e t ri 网概述 3 1p e t r i 网及其应用简介 p e 试网是1 9 6 2 年德国的c a p e t r i 博士在其博士论文中首先提出的一种用于并发系 统建模和分析的重要工具。同其它描述工具相比较，p e 啊网的优点主要在于： 一、它具有很强的描述能力。已经证明：对于带抑制弧的p e m 网，其描述能力与图 灵机( t u d n g m a c h i n e ) 是等价的。 二、它既有严格的形式定义，又有直观的图形表示，能够直观地表达系统中的并发、 顺序、冲突、同步、共享等关系。 三、它具有严谨的理论基础、丰富的理论成果和分析工具。我们可以利用这些成果 和分析工具对它模拟的系统的结构特性和动态特性进行分析，为了解系统的各方面的性 质进而去改善系统，设计新的系统提供理论依据。有关专家曾指出，p c t f i 网模型不只是 在众多模型中增加一种普通的系统建模工具，它必为信息论的发展奠定坚实的理论基础。 随着近年来p e 缸网研究的蓬勃发展，其应用领域也不断拓宽。p c u i 网已成为具有多 种抽象层次的“网状”系统的首选建模工具，已被用作对大型操作系统、分布式数据库、 并行程序、离散事件系统分析、柔性制造系统、自动控制、线路设计、软件工程、人工 智能、形式语义、计算机网络性能分析及通讯协议验证、并行程序的设计与分析、知识 表示与推理、人工神经元网络和决策模型以及许多计算机系统进行分析和设计的手段。 此外，在化学、工程技术、法律及其它领域里，也不乏p c t r i 网应用的实例。可以说，p c t d 网现在已经应用在社会的各个领域，并且其应用领域还在不断扩大。 3 2p e t r i 网定义1 5 2 j 定义3 1 满足下列条件的三元组n = ( p ，乃f ) 称为一个网 1 4 山东科技大学硕士学位论文petri网概述 1 ) p u t 2 ) 尸n 丁= 3 ) ，量( ( p x 幻u 口p ) ) 4 ) 如，u c o a ( f ) = p u 丁 其中：如以用= 仁p u 丁l 砂p u ，：伍力f