（计算机应用技术专业论文）基于网络协议的petri网研究——利用着色petri网分析验证安全协议.pdf

摘要 摘要 在因特网技术飞速发展的今天，信息安全问题已经成为同益突出的问题。安全协议 的出现虽然在很大程度上提高了网络信息传输的安全性，但同时因为设计上的缺陷性， 安全协议也存在着很多漏洞。在当前，安全协议的形式化分析已经成了一个热点研究问 题。目前安全协议的形式化分析方法主要包括：形式逻辑方法【l 】、模型检测方法【2 】、定 理证明方法和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 网的可达性分析思想。而后，用两个安全协议实例来验证这种方法的有效性， 同时，发现随着安全协议复杂性的增加，p e t r i 网模型的状态空间爆炸问题也随之发生， 并且此模型只能验证已知的安全协议漏洞，无法检测未知的安全攻击。 3 尝试采用一种基于c p nt o o l s 的安全协议分析与验证方法来改进状态空间爆炸 问题，文中以t m n 协议为例，验证了该方法的有效性。方法中提出了d b p l a c e 概念， 使入侵模型变得简单明了，并且制定令牌传递机制来改善状态空间爆炸问题。 关键字：安全协议；协议漏洞；形式化分析：着色p e t r i 网；可达性；状态空间爆 炸；重放攻击；c p nt o o l s a b s t r a c t a b s t r a c t w i t ht h er a p i dd e v e l o p m e n to fi n t e r a c tt e c h n o l o g y ，t h ei s s u eo fi n f o r m a t i o ns e c u r i t yh a s b e c o m ea n i n c r e a s i n g l yp r o m i n e n tp r o b l e mt o d a y a l t h o u g ut h ee m e r g e n c eo fs e c u r i t y p r o t o c o l si m p r o v e dt h es a f e t yo fi n f o r m a t i o nt r a n s m i s s i o nt o al a r g ee x t e n t ，t h e r ea r es t i l l m a n yl o o p h o l e sb e c a u s eo ft h ef l a w so fd e s i g n f o r m a la n a l y s i so fs e c u r i t yp r o t o c o l sh a s b e c o m eah o tr e s e a r c hf i e l d a t p r e s e n t ，t h e m a i nm e t h o d so fa n a l y s i so fs e c u r i t y i n c l u d e ：f o r m a ll o g i cm e t h o d s ，d e t e c t i o nm e t h o d s ，, t h e o r e mp r o v i n gm e t h o d sa n dm e t h o d su s i n g p e t r in e t t h e yh a v et h e i ro w na d v a n t a g e sa n dd i s a d v a n t a g e s i nt h i sp a p e r , t h em e t h o dw eu s e d i sb a s e do nt h ef o r m a la n a l y s i so fp e t r in e t ，t h em a i nj o bw ec a r r i e do u ti s ： 1 i n t r o d u c e dt h eb a s i ck n o w l e d g eo fs e c u r i t yp r o t o c o la n dt h ec o m m o nm e t h o d so f f o r m a la n a l y s i so fs e c u r i t yp r o t o c o l ；i n t r o d u c e dt h ed e f i n i n i t i o no fp e t r in e ta n di t sd y n a m i c p r o p e r t i e s ，a n da l s oe x p o u n d e d t h ek n o w l e d g eo fc o l o r e dp e t r in e t , ， 2 u s e dam e t h o db a s e do nc o l o r e dp e t r in e t t h i sm e t h o da d o p t sr e v e r s ea n a l y s i sa n d r e a c h a b i l i t ya n a l y s i so fp e t r in e t f i n a l l y , w eu s e dt h r e ee x a m p l e so fs e c u r i t yp r o t o c o l st o v e n f yt h ev a l i d i t yo ft h i sa p p r o a c h a tt h es a m et i m e ，w i t ht h ei n c r e a s eo ft h ec o m p l e x i t yo f t h ep r o t o c o l ，w ef i n dt h a tt h es t a t es p a c ee x p l o s i o np r o b l e mo c c u r s ，a n dc a n td e c e c tt h e u n k n o w n s e c u r i t ya t t a c k s ，o n l yc a nv e r i f yt h el o o p h o l ew e h a v ak n o w n 3 t r i e dt oc r e a t eam e t h o do fu s i n gc p nt o o l st oa n a l y s ea n dv e r i f ys e c u r i t yp r o t o c o lt o r e d u c et h es t a t es p a c ee x p l o s i o n i nt h ep a p e r , w eu s e dt m n p r o t o c o la sa ne x a m p l et ov 谢矽 t h ev a l i d i t yo ft h em e t h o d i nt h em e t h o d ，w ep u tf o r w a r dt h ec o n c e p to fd b p l a c et om a k et h e i n t r u d e rm o d e lb e c o m es i m p l ea n di m p l e m e n tat o k e n - p a s s i n gs c h e m et oi m p r o v et h es t a t e s p a c ee x p l o s i o np r o b l e m 。 k e y w o r d s ：s e c u r i yp r o t o c o l ；s e c u r i y ；p r o t o c o ll o o p h o l e ；f o r m a la n a l y s i s ；c o l o r e dp e t r in e t ； r e a c h a b i l i t y ；s t a t es p a c ee x p l o s i o n ；r e l a ya t t a c k ；c p nt o o l s n 独创性声明 本人声明所呈交的学位论文是奉人在导师指导下进行的研究工作及取 得的研究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文 中不包含其他人已经发表或撰写过的研究成果，也不包含本人为获得江南 大学或其它教育机构的学位或证书而使用过的材料与我一同工作的同志 对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。 签 名： 期彳吐 授权的说明 本学位论文作者完全了解江南大学有关保留，使用学位论文的规定： 江南大学有权保留并向国家有关部门或机构送交论文的复印件争磁盘，允 许论文被查阅和借阅，可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文， 并且本人电子文档的内容和纸质论文的内容相一致。 保密的学位论文在解密后也遵守此规定。 签名：盔盐罩导师糨至丛茎堑 日 期：逝：f 2 ：毕 1 第一章绪论 第一章绪论 1 1 课题的提出 互联网的出现，为人们的生活、学习等各个领域都带来了很大的方便与好处。随着 i n t e m e t 技术的日益发展，给人们带来便利的同时，网络上的信息安全问题也日益突出。 由于因特网是一个公共的传输通道，没有严格的控制机制，不法分子容易进行非法窃听 甚至篡改传输数据。如果这样的事情发生在金融、政治、军事领域上，所造成的损失对 一个国家来说是不可估量的。因此，人们采用了加密方法对传输的数据进行加密，然后 再进行传输。这样，非法人员很难再窃听或者篡改传输的信息。但是，这种方法也有缺 点：密钥的管理没有规范，通信的个体越多，密钥就容易暴露；一旦密钥被暴露，消息 就会泄漏，这样势必会造成很大的损失。 为此，人们设计了能够分发密钥、对通信实体进行身份验证的一种体制，即网络通 信的安全协议。然而，这些协议都是根据设计者的直觉设计出来的，没有充分的证据证 明它们是没有安全漏洞的。事实证明，许多著名的安全协议在提出后多年，都被证明存 在着严重的安全漏洞。如果在协议设计时就采取某种方法来验证协议的正确性，并以此 方法来指导协议的设计，这样就可以防患于未然。因此，开展安全协议的形式化分析的 研究是非常有意义的。 1 2 安全协议研究现状 安全协议【5 】( 又叫密码协议) 是运行在计算机网络或分布式系统中借助密码算法来 实现密钥分析、身份认证以及公平完成电子交易等目的的一种高互通协议，是任何安全 系统的安全基础，是实现计算机网络安全的关键。 近年来，人们采用形式化的方法【6 7 1 来分析安全协议的安全性，其中主要的形式化分 析方法有： 1 2 1 逻辑方法 基于信仰和知识的逻辑形式分析方法，它以b a n t 8 】逻辑为代表，之后紧跟着又出现 了一些对b a n 逻辑扩展和改进后的逻辑，如g n y ，a t ，v o ，s v o t 9 m 】等。我们将这 些逻辑统称为b a n 类逻辑。我们称这一类为b a n 类逻辑( b a n 1 i k el o g i c ) 。 1 2 2 通用形式方法 这种方法采用一些通用的形式化方法来说明和分析安全协议，如最弱前置谓词和 p e t r i 网等。 p e r t i 网是一种用于并发、异步系统建模和分析的重要工具。经过四十多年的研究， p e r t i 网的理论成果十分丰富，并且已开发出相应的理论分析工具和软件。它已经成功分 析了众多的通信协议，特别适合于分析协议的并发、并行和异步特性。这方面的工作主 要有：v a r a d h r a j n a 用p e r t i 网来分析安全系统中的信息流的安全性。q u e n e su n i v e s r t i y 江南大学硕士学位论文 采用着色网来分析安全协议【1 3 , 1 4 】，并发现了一些协议中之前没有发现的缺陷。他们通过 建立状态可达矩阵，采用相关的状态分析来分析和验证协议。并且通过引入入侵者模型， 构建相关模型的可达树和攻击时间序列来寻找安全协议的可能出现的不安全状态。 1 2 3 模型检测方法 基于代数方法构造一个运行协议的有限状态系统模型，再利用状态检测工具来分析 安全协议的安全性。 模型检测技术是一种验证有限状态系统的自动化分析工具，原是运用于分析和模拟 硬件工作过程的形式化方法。随着形式方法的日益进步和应用领域的推广，模型检测技 术现在已经用于软件分析和通信协议模拟等多个领域，但用于密码协议的分析还是这几 年的新的应用。 在1 9 9 6 年，g a v i nl o w e 首先使用c s p 模型和分析n s 1 5 】协议并成功地找到一个以 前从未发现的攻击。模型检测的成功，使学者们相继投入到这个领域。 1 2 4 定理证明方法 将安全协议的安全性作为定理来证明，这是一个新的研究热点。 1 3 本文的研究重点 由于论文研究内容，这里只介绍利用p e t r i 网【1 6 郴】研究安全协议的研究现状：p e t r i 网是德国c a p e t r i 博士于1 9 6 2 年提出的，作为一种并发系统建模和分析工具，p e t r i 网 已被成功应用在计算机科学的各个领域。9 0 年代以来，p e t r i 网开始应用于安全协议的 分析。如加拿大的q u e e n su n i v e r s i t y 的q u e e n sc r y p t o g r a p h ya n dd a t as e c u r i t y l a b o r a t o r y 的t a v a r e s 教授课题组针对攻击者行为集合，采用颜色网来模拟和分析攻击 者行为，成功的分析了多个密码协议并发现了以前没有发现的缺陷，文献 1 8 ，1 9 ，2 0 分别 反映了他们的研究成果；h e l s i n k iu n i v e r s i t yo f t e c h n o l o gd 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 【2 l 】采用谓词变迁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 2 】等引入了安全协议时间p e t r i 网来验证分析了t m n 2 3 】协议；u n i v e r s i t yo f c a m b r i d g e 的f e d e r i c oc r a z z 0 1 a r a 【2 4 2 5 】等借助于p e t r i 网的进程网( 进程语言) 证明安 全协议的安全性也取得一定成果。以上是国外所从事的这方面研究工作。国内从事这方 面的工作比较少【2 睨9 1 ，例如：文献 2 6 】利用对象p e t r i 网来描述和分析认证协议，文献 2 8 】 利用时延p e t r i 网队协议进行分析和性能的评估。 本论文的研究目的是应用p e t r i 网对安全协议进行验证与分析。具体的相关工作如 下： 1 介绍安全协议相关知识，阐述其特点； 2 介绍p e t r i 网相关知识，给出其性质及分析方法： 3 给出一种基于着色p e t r i 网的安全协议验证方法，阐述该方法的理论，采取具体 的安全协议来验证该方法的有效性； 2 第一章绪论 4 提出一种基于c p nt o o l s 的安全协议分析与验证方法，来改进和预防第四章中出 现的空间爆炸问题。 1 4 论文的组织结构 本文中共有六章，分别是绪论( 第一章) 、安全协议的相关知识( 第二章) 、p e t r i 网相关知识( 第三章) 、基于着色p e t r i 网的安全协议研究( 第四章) 、一种基于扩展p e t r i 网模型的安全协议分析( 第五章) 、研究工作总结与展望( 第六章) 。 第一章绪论，主要阐述论文的研究背景和研究内容。 第二章安全协议相关知识，介绍安全协议的基本知识以及安全协议分类和常见的 具体安全协议以及常见的安全协议形式化分析方法。 第三章给出了基本p e t r i 网的定义和性质，并描述了高级p e l r i 网( 着色p e t r i 网) 的概念以及动态特性。 第四章给出一种基于着色p e t r i 网的安全协议验证方法，结合具体安全协议，利用 给出的方法对该安全协议进行分析与验证，发现安全协议的安全漏洞，给出分析结果。 发现该方法容易发生空间状态爆炸和无法检测未知安全漏洞问题。 第五章提出一种基于c p nt o o l s 的安全协议分析与验证方法来改进第四章中出现 的空间爆炸问题，并以t m n 协议为例来验证该方法的有效性。 第六章研究工作的总结与展望。对本文的研究工作进行总结，并对未来的研究工 作进行展望。 3 江南大学硕士学位论文 第二章安全协议的相关知识 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 n l 和m d s c h r o e d e l 发表了n s 认证协议，这是第一个应用于计算机网络的安全协议。n s 认证协议的发表， 给计算机通讯网络的安全带来了革命性的变化，也是安全协议的里程碑，许多后来著名 的协议( 如k e r b e r o s 协议) 是在n s 认证协议的基础上发展起来的。 n s 协议提出以后，1 9 8 4 年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 协议【3 0 】，n s 协议中使用一次性随数来 表示新鲜数，而k e r b e r o s 是用时间戳来表示其新鲜性，要求认证主体之间要保持时钟的 同步。现在为止，安全协议设计中依然用时问戳和随机数来表示消息的新鲜性 3 1 ，3 2 。 在进行安全协议设计时，常常要用到密码算法。这些算法可以是对称算法( 如d e s 算法) ，也可以是非对称算法( 如r s a 算法) 。如对于常用的认证系统来说，大多数系 统都是采用单密钥体制的，并且这个密钥是通过安全的脱机方法建立的。而公钥体制中， 通常是利用证书机构颁发的公钥证书来认证主体的公钥和身份，而且证书具有一定的有 效期，超过有效期这些证书都是被认为是无效的，c c i t t x 5 0 9 认证框架就是该方面应 用的典型。 2 1 2 安全协议分类 安全协议根据其目的可以分为以下四类： 4 第二章安全协议的相关知识 密钥交换协议：这类密钥主要用于完成会话密钥的建立，一般情况下是在参与协议 的两个或者多个实体之间建立共享的数据，如用于一次通信中的会话密钥，协议中的密 码算法可以采用对称密钥机制，也可以采用非对称密钥机制。 认证协议：认证协议包括实体认证( 身份认证) 协议、消息认证协议、数据源认证 协议和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。 认证密钥交换协议：这类协议将认证协议和密钥交换协议结合在一起，先对通信实 体的身份进行认证，在认证成功的基础上为下一步安全通信分配所使用的会话密钥，认 证密钥协议是网络通信中应用最多的密钥。认证密钥交换协议是网络通信中应用最普遍 的一种安全协议，常见的互联网密钥交换( i k e ) 协议，分布式认证协议( d a s s 协议) 、 k e r b e r o s 认证协议、x 5 0 9 协议等。 电子商务协议：与上述协议不同的是，电子商务协议中主体往往代表交易的双方， 其利益目的是不一致的，或者根本是矛盾的。因此电子商务协议关注的是就是公平性。 即协议应保证交易双方都不能通过损害对方利益而得到它不应得到的利益。常见的电子 商务协议有s e t 协议、i k p 协议等。 2 2 常见的安全协议 自从n e e d h a m s c h r o e d e r 安全协议于1 9 7 8 年诞生以来，经过很长时间的发展，出现 了各式各样的安全协议【3 3 - 3 5 1 。很多安全协议在被提出后，都会被发现该协议存在着安全 漏洞，人们对这些安全协议的漏洞进行改进，或者提出更加完善的安全协议。以下是常 见的这些协议种类： 1 无可信第三方的对称密钥协议：这类协议需要有两个通信实体，依靠相互间发送 共享密钥加密的认证消息来进行认证。例如，i s o 对称密钥两遍双向认证协议( i s o s y m m e t r i ck e y t w o p a s sm u r a la u t h e n t i c a t i o np r o t o c 0 1 ) 1 3 6 1 。 2 应用密码校验函数的认证协议：这类协议使用一些密码检查函数危。( x ) 对x 进 行加密。允。( x ) 根据的值，返回x 的h a s h 函数值。例如，带c c f s 的i s o 两遍双 向认证协议( i s ot w o p a s sm u t u a la u t h e n t i c a t i o nw i t hc c f s ) 【j 。 3 具有可信第三方的对称密钥协议：这类协议使用对称密钥加密，并且共有一个可 信的第三方，即服务器s 。s 与其他的每个通信实体之间都共享两个不同的对称密钥。 当通信实体之间想进行身份认证时，就向s 发出请求，由s 处理、转发请求消息，最后 完成认证，并相互都拥有由s 分发的共享对称密钥。例如n e e d h a m s c h r o c d c r 密钥协议。 4 对称密钥重复认证协议：这类协议进行重复认证，就是说要反复地、不止一次 地进行认证。最著名的协议是k e r b e r r o sv e r s i o n5 协议p 引。 5 具有可信第三方公开密钥协议：这类协议使用公钥加密技术，其中有一个可信 的第三方进行密钥分发服务。最著名的就是n e e d h a m s e h r o e d e r 公钥协议。 6 无可信第三方公开密钥协议：这类协议用公钥加密技术通信。没有一个可信的第 三方提供密钥分发服务。靠通信实体x 利用对方y 不知道的、自身的私钥k 1 1 ，或者加 5 江南大学硕士学位论文 密请求和应答消息，对方y 接到后，用x 公开的相应的公钥k y 解密，完成认证。例如， i s o 公钥两遍双向认证协议o s op u b l i ck e yt w o m u t u a la u h t e n t i c a t i o np r o t o c 0 1 ) p 引。 2 3 安全协议的安全性 2 3 1 安全协议的实现目标 作为一种在公共网络上为信息传输提供安全保障的手段，安全协议应当实现如下几 个安全目标： 机密性：机密性也称为保密性，即入侵者可能够通过某种渠道知道主体a 向主体b 发送了一个消息，甚至清楚知道消息传送的时间，却无法知道传递消息的内容。 认证性：是最重要的安全服务之一，许多的安全应用都依赖于认证服务。它是用来 获取对谁或对什么事情信任的一种方法，包括数据源认证和身份认证两个方面。 身份认证：通过消息的交互来确认对话者的身份。它可以是单向的或是双向的。所 谓单向身份认证是指通信双方中只有一方向另一方进行认证。所谓双向认证是指通信双 方相互认证。 完整性：是指数据在传输或者存储的过程中没有损坏( 修改、丢失、重排序或替换) 。 在具体应用的时候，我们是通过针对数据的任何篡改都会被检测出来来保证数据的完整 性。在某种意义上，我们认为完整性是协议正确运行的前提，即每一步正常协议动作的 执行都隐含着消息的完整性。 不可否认性：主要应用于电子商务协议。对于大多数安全目标，我们总假设合法主 体是诚实可信的，也就是他们将遵循协议规范。但在电子商务协议中，则是另一种情况。 因为利益的驱使，合法主体可能会欺骗通信的对方以便获取利益。安全协议的基于以上 需要实现的目标，一方面要求协议具有足够的复杂性以抵御组合攻击。另一方面，还要 尽量使协议保持足够的经济性和简单性，以便可以应用于低层网络环境。 如何设计协议才能满足安全性、有效性、完整性和公平性的要求，这就需要协议尽 量采用随机数来替代时间戳，最少的安全假设。 2 3 2 安全协议的安全性及攻击 对协议的攻击可以分为被动攻击和主动攻击两类。 被动攻击是指安全协议外部的入侵者对协议执行的部分或整个过程实施监听。攻击 者的窃听行为并不影响协议的执行，而只是观察或者储存协议中用于传输的机密信息， 以备将来的不时之需。 攻击的第二种主要类型时主动攻击，这些主动攻击涉及某些数据流的篡改或一个虚 假消息的产生。这些主动攻击还可以被进一步分为四类攻击：伪装、重放、篡改消息和 拒绝服务。 伪装就是一个入侵者伪装为一个不同的合法的参与协议实体。伪装攻击通常包括其 他主动攻击形式中的一种。 6 第二章安全协议的相关知识 重放攻击涉及一个数据单元的被动获取以及后继的重传，以产生一个未授权的效 果。 消息的篡改意味着一个合法消息的某些部分被改变，或消息被延迟或改变顺序，以 产生一个未授权效果。 拒绝服务防止或禁止通讯设施的正常使用或者管理。这种攻击手段一般具有特定的 目的，例如，一个实体可能抑制所有的消息指向某个特殊的目的地( 如安全审计服务) 。 另一种形式的拒绝服务是使整个计算机网络崩溃，或者通过使网络不能工作的手段，或 者通过滥发消息的方法使网络负荷超载，已达到降低网络的传输性能。 2 4 安全协议形式化分析方法 协议分析是揭示安全协议中存在漏洞问题的重要方法。而主要的分析的方法有： 1 攻击检验方法一非形式化方法 这种方法对协议进行分析一般是根据已知的各种攻击方法来对协议进行攻击，以攻 击是否有效来检验安全协议是否安全。由于存在许多未知的攻击方法，所以非形式化分 析只是停留于发现协议中是否存在已知的缺陷而不能全面客观的分析安全协议。这是安 全协议早期的主要分析方法。 2 形式化分析方法 9 0 年代以来，安全协议的相关形式化分析已经成为了当前的研究热点，这种方法的 出发点是希望将安全协议进行形式化，然后借助于人工的推导，并且借助计算机的辅助 分析来判断安全协议是否是安全的。与非形式化分析方法相比，它更能全面、深刻的检 测安全协议中可能存在的极其细微漏洞。到现在为止，我们可将安全协议的形式分析方 法大致分为4 类：形式逻辑方法、模型检测方法、定理证明方法和包括p e t r i 网的分析 方法在内的通用形式方法，具体相关内容已经在第一章中有比较详细的介绍。 2 5 本章小结 本章重点介绍了安全协议的基本知识和常见的四种常见的协议形式化分析方法：形 式逻辑方法、模型检测方法、定理证明方法和p e t r i 网方法，并且介绍了各种方法的优 点和缺点。 7 江南大学硕士学位论文 第三章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 网己发展成为具有严密数学基础、 多种抽象层次的“网状”建模工具，在离散事件系统分析、柔性制造系统( f m s ) 、自动控 制、计算机网络性能分析及协议验证、并行程序的设计与分析、知识推理、和决策模型 等领域得到广泛应用。 与此同时，从基本p e t r i 网模型还衍化出许多扩展的模型系统，如谓词动作p e t r i 网、 时间p e t r i 网( t p n ) 、着色p e t r i 网( c p n ) 、面向对象p e t r i 网( o o p n ) 、随机p e t r i 网( s p n ) 以及模糊p e t r i 网( f p n ) 等，它们都是为了适应不同领域建模、分析、规范和验证的需求。 例如多媒体网络协议最核心的问题是媒体流间的同步问题，引入时间限制的p e t r i 网更 适合建立形式化模型；面向对象p e t r i 网由于能够映射软件工程的基本思想方法，如继 承和类。高级p e t r i 网系统更多地应用于分布式系统的辅助设计；将代数的抽象数据类 型融合在高级网结构中，为描述协议和服务提供了极大的方便。 3 1p e t r i 网定义 定义3 1 有向网的定义 三元组n ( p ，t ；f ) 称为有向网的充分必要条件是： ( 1 ) 尸n t = 矽； ( 2 ) pu t 矽； ( 3 ) f p t u t x p ； ( 4 ) d o m ( f ) u c o d ( f ) = p u 丁 其中： d o m ( f ) = x | 3 y ：( 工y ) f ) ， c o d ( f ) = yi 孔：( x y ) f ) ，分别为定义域和值域。 p 称为有向网n 的库所( p l a c e ) ，t 成为n 的变l - 壬( t r a n s t i t i o n ) 集，f 为流关系( f l o w r e l a t i o n ) 。 定义3 2 设n ( p ，r ；，) 为一个网，对x p u t ，记 z = 秒j p u 丁l ( ) ，石) ， x = j ，尸u 丁i ( x ，y ) f ) 这里，称x 为x 的前集或者输入集，x 。为x 的后集或者输出集，xk 3 x 称为元素x 的外延。 定义3 3 设n ( p ，t ；f ) 为一个网，o 为非负整数集，映射m ：p 一o 称为网n 的一个标识，二元组( ，m ) 称为标识网。 定义3 4 一个网系统是一个标识网= ( n , m ) = ( p ，t ；f ，m ) ，并且有下面的变迁发 生规d j ( t r a n s i t i o nf i r i n gr u l e ) ： 第三章p e t r i 网概述 对于t t ，如果砌。t ：m ( p ) l ，则我们称m 授权t 发生，记为m t ( 当。t = 时，t 在任意标识下都有发生权) ，t 在这种情况下是使能的。 若标识m 授权t 发生，则变迁t 在标识m 下可以发生( f i r e ) ，从m 发生t 得 到新的标识m ( 记作m t m ) ，对v p p ： l m ( p ) - 1 当p e t - t m ( p ) = m ( p ) + l 当p f 一t 【m ( p ) 其它 ( 3 1 1 ) 一个有向网系统都具有一个初始的标识，这里我们记为m 。可能有若干个变迁t 在情况下初始标识m n 有发生权，随意选择其中一个或者一组发生的话，就会得到一个 新的标识m ( 不同的变迁发生的情况下，可能产生的新标识是不同的) 。在m 情况下， 又可能有别的若干变迁发生，就会产生新的标识，这样下去，就会构成一个连续的网系 统。这类系统就是c a p e t r i 博士最早在其博士论文中提出的网系统，我们称之为p e t r i 网。p e t r i 网只是一个比较笼统的说法，经过多年的发展，在基础的p e t r i 网之上，又形 成了多种高级p e t r i 网如：着色p e t r i 网，随机p e t r i 网等等。 3 2p e t r i 网系统模拟 p e t r i 网模型的提出是为了模拟一个系统或者模型，具体来说，p e t r i 网可以模拟的 系统是由一些离散事件所组成的系统，在时间之间肯定有着联系，这些依赖之间的联系 是由系统的状态反映出来的。在系统的特定的一些情况下，某些事件可能发生，事件的 发生改变了系统的当前状态，在新状态下，一些事情的发生条件会被满足，因此，这些 事件也会发生。 这里我们通过两个简单的例子说明怎样用p e t r i 网来进行模拟。 例3 1 简单的加工车间系统 有： t l p lt 2 p 2t 3p 3 t 4 p 4 图3 - 1 简单加工车间的p 确网模型 f i g 3 - 1s i m p l ep r o c e s sw o r k s t a t i o np e t r in e r om o d e l 车间等待有工件来到，便进行加工，然后把加工好的工件送出去。这个系统的条件 a 车间在等待；( p 4 ) b 工件到达并等待加工；( p 1 ) c 车间正在加工工件；( p 2 ) 9 江南大学硕十学位论文 d 工件加工完毕。0 3 ) 这个系统的事件可以是： 1 一个工件送来；( t 1 ) 2 车间开始加工工件；( t 2 ) 3 工件的加工完成；( t 3 ) 4 把加工好的工件送出去。( t 4 ) 例3 2 进程之间的通信协议的p e t r i 网模型 发送消息缓冲寄存器 接收消息 进 程 a 接收心答 缓冲寄存器发送应答 图3 - 2 进程之间的通信协议的p e t r i 网模型 f i g 3 - 2p e t r in e t sm o d e lo ft h ep r o c e s s e s sc o m m u n i c a t i o n p r o t o c o l p 7 进 t 6 程 b p s 进程a 准备好的信息( s 1 ) 想进程b 发送( t 2 ) ，先送到缓冲寄存器( s 4 ) 。如果进程b 做 好接受信息的准备( s 7 ) ，便从s 4 中接受( t 4 ) 进程a 发送的消息，并向进程a 发送应答( t 5 ) ， 应答信息通过缓冲寄存器( s 5 ) 回送到进程a 。以上过程可以重复多次。 3 2p e t r i 网性质 p e t r i 网的性质包括动态性质和结构性质两种，这里我们只介绍动态性质。 3 2 1p e t r i 网的动态性质 我们以p e r t i 网( 不包含容量函数和权函数的p e t r i 网系统) 为模型，定义和讨论p e t r i 网系统运行过程中表现出来的性质，并把这些性质称为p e t r i 网的动态性质( d y n a m i c p r o p e n i e s ) 或者又叫做行为。i 生质( b e h a v i o u r a lp r o p e r t i t e s ) 。这些性质同p e r t i 网所模拟的实 际系统某些方面的性能有密切的联系。在其他的高级p e t r i 网系统中，这些动态性质的 定义很容易的被延伸。 1 可达性( r e a c h a b i l i t y ) 可达性是p e r t i 网模型最最基本的动态性质，其他的各种动态性质都需要通过可达 性来表达。 定义3 5 设= ( p ，t ；f m ) 为一个p e t r i 网系统，如果对于任意的t t ，使得 m t m ，则称m 为从状态m 是直接可达的。如果存在变迁序列t 。，t 2 ，t i 和标识 序列m 。，m ：，m i 使得 m t l m l f 2 m 2 朋七_ i 心 m i 1 0 第三章p e t r i 网概述 则称m r 从m 是直接可达的。从m 可达的一切标识的集合记为r ( m ) 。这里我们约 定m r ( m ) 。 用p e t r i 网来模拟一个实际的系统时，网( p r ；f ) 描述系统的结构，初始标识m 。表 示系统的初始状态标识，而r ( m 。) 给出了系统运行过程中所有可能出现的状态的集合。 定义3 6 设= ( 只r ：f ，m o ) 为一个p e t r i 网，其中m o 是p e t r i 网系统的初始标识， 的所有标识集r ( m 。) 定义为满足以下两个条件的最小集合： ( 1 ) m o r ( m o ) ； ( 2 ) 若m r ( m o ) ，并且存在对于任意的t t 使得m t m ，则m r ( m o ) 对于有界的p e t r i 网，由于其可达标识集r ( m 。) 是一个有限集，因此我们可以把 r ( m 。) 作为顶点的集合，以标识之间的直接可达关系为弧集构成一个有向图。因此，我 们称这种有向图为p e t r i 网可达标识图( r e a c h a b l em a r k i n gg r a p h ) 。 2 有界性和安全性( b o u n d e d n e s sa n ds a f e n e s s ) 定义3 7 设= ( p ，t ；f m 。) 为一个p e t r i 网模型，对于任意的p p ，如果存在这样 的正整数b ，使得跏r ( m o ) ：m ( p ) b ，则称库所p 是有界的( b o u n d e d ) 。并将满足 此条件的最小正整数b 为库所p 的界，记为b ( p ) 。即 召( p ) = m i n iv m r ( m o ) ：m ( p ) 曰) 当b ( p ) = 1 时，库所p 为安全的( s a f e ) 。如果每个p p 都是有界的，则称为有界 p e t r i 网。称 b ( ) = m a x b ( p ) ip 尸) 为的界。当口( ) = 1 时，称为安全的。 有界性( 安全性) 反映了被模拟系统运行过程中对有关资源容量的要求。在实际系统 的设计中，必须使得网中的每个库所在任何状态下的标识数小于库所的容量，这样才能 保证系统的正常运行，不至于产生溢出现象。 3 活性( 1 i v e n e s s ) 定义4 8 设= ( p ，t ；f 2 1 4 0 ) 为一个p e t r i 网，m o 是的初始标识，t t 。如果 v m r ( m 。) ，都存在m r ( m ) ，使得m ， f ，则称变迁t 是活的。如果v t t 都是 活的，则称为活的p e t r i 网。 4 持续性( p e r s i s t e n c y ) p e t r i 网的持续性是这样的一种性质：如果在可达标识m 下变迁t 有发生权，那么 从m 发生了其它任意变迁或任意不包含t 的变迁序列后，t 仍有发生权。如果一个p e t r i 网中对任意可达标识和任意变迁t ，上面所述性质都成立，就称该网为持续网。 定义4 9 设= ( p ，t ；f m o ) 为一个p e t r i 网，如果对任意m r ( m o ) 和任意： ( m f 1 m t 2 m ) jm i t l 则称是一个持续网。 江南大学硕士学位论文 3 2 2p e t r i 网性质分析方法 p e t r i 网具有多种形式化分析方法，主要方法包括：可达标识图与可覆盖性树、关联 矩阵与状态方程、p e t r i 网语言与p e r t i 网进程等。这些方法都建立在坚实的数学理论基础 之上，各有各的优点跟缺点。 1 可达标识图与可覆盖性树 定义3 1 0 设= ( p ，t ；f a h t o ) 为一个p e t r i 。的可达标识图定义为一个三元组 r g ( e ) = ( r ( m 。) ，e ，) ，其中 e = ( m f ，m ) im f ，m ，r ( m o ) ，3 t 女t ：m 廖t m ，) f ：e t ，f ( m ，m ，) = t i ，当且仅当m f 气 m ， 这里称r ( m o ) 为r g ( z ) 的顶点集，e 为r g ( z ) 的弧集，若f ( m ，m ，) = t 则称t 为弧 ( 膨，膨) 的旁标。 当不是有界p e t r i 网时，由于r ( m