《CBTC系统通信协议的设计和形式化分析.pdf》由会员分享，可在线阅读，更多相关《CBTC系统通信协议的设计和形式化分析.pdf（75页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、北京交通大学硕士学位论文CBTC系统通信协议的设计和形式化分析姓名：刘雨申请学位级别：硕士专业：交通信息工程及控制指导教师：唐涛20071201中文摘要摘要：在基于通信的列车运行控制(C o m m u n i c a t i o n s-b a s e dT r a i nC o n U o l,C B r I)系统中，各子系统问可靠的数据通信是保证整个系统安全的基础。为了达到数据传输安全的目的，论文设计实现了一个相对完备的通信协议供自主开发的C B T C 系统使用，并且引入形式化方法对其进行分析，证明了该协议的安全性。论文阐述了C B T C 系统通信协议的设计原理。首先根据自主开发的C
2、 B T C 系统在数据传输安全方面的需要，详细分析了通信协议的安全需求及性能指标；然后引入了安全传输规范，利用规范中提供的安全防护措施分层次地设计了C B l f C系统通信协议。论文选择形式化语言C P N(C o l o u r e dP e t dN e t)和它的支持工具C P NT o o l s 对C B T C 系统通信协议进行“自上而下”的建模。首先给出了C B T C 系统通信协议的顶层模型；而后深入研究了单链路协议模型的建立过程，从基本模型着手，逐步加入安全防护机制，最后得到完善的协议模型。基于所建模型，使用C P NT o o l s 对C B T C 系统通信协议进行
3、验证和性能分析。根据安全通信协议的分析方法，首先对模型进行必要的分解和简化，通过状态空间分析验证模型的有界性、活性等动态特性；而后考虑影响系统安全的各种危险因素，对通信协议的性能进行分析，并得出各种性能参数的均值；最后将这些性能参数的均值和既定的性能指标进行比较，证明所设计的通信协议是符合我们的C B T C 系统安全传输需求的。关键词：C B T C 通信协议；安全传输规范；着色P e t r i 网；建模；性能分析；分类号：U 4 9A B S T R A C TA B S T R A C I r：I nm eC o m m t m i e a t i o m-b a s 簋lT r a
4、i nC o n t r o l(C B r C)s y s t e m,t h er e l i a b l ed a t ae o m m t m i c a t i o nb e t w e e ne v e r ys u b-s y s t 舶i st h ef o u n d a t i o no ft h ew h o l es y s t e m ss a f e t y I no r d e rt ot r a n s f e ri n f o r m a t i o ns a f d Kas e l f-c o n t a i n e dc o m m u n i c a t
5、 i o np r o t o c o lo fC B T Cs y s t e mw a sd e s i g n e da n di m p l e m e n t e di nt h i sp a p e r,a n df o r m a l i z a t i o nm e t h o dW a Sb r o u g h ti nt oa n a l y z et h ep r o t o c o li no r d l 薯t op r o v ei t ss a f h yp e r f o r m a n c e I nt h ep a p e r,t h ed e s i g n
6、p r i n c i p l e so ft h ec o m m u n i c a t i o np r o t o c o lo ft h eC B T Cs y s t e mw 雠e x p a t i a t e d F i r s t l y,s a f e t yr e q u i r e m e n t sa n dc a p a b i l i t yt a r g 哟o ft l a ep r o t o c o lw c i r l。a n a l y z e da c c o r d i n gt ot h ed e m a n d so ft h eC B T C
7、s y s t e ma tt h ea s l 僦to fs a f ei n f o r m a t i o nm m s f e r r i n g；t h e nt h es a f e t yr e l a t e de o m m u n i e a d o ns t a n d a r dw a si n t r o d u c e d a n dt h ep r o t o c o lo ft h eC B T Cs y s t e m d e s i g n e dh i e r a r c h i c a l l yu s i n gt l a cs a f e t yd
8、e f e n e e sp r o v i d e di nt h es t a n d a r d I nt h ep a p e r,f o r m a l i z a t i o nl a n g u a g eC P N a n dC P NT o o l sw c 陀c h o s e nt ob u i l dt h em o d e l so f t h ep r o t o c o lf r o mt o pt ob o t t o m F i r s t l y,t h et o pm o d e lo f t h ep r o t o c o lo f t h eC B
9、T Cs y s t a nW a Sb u i l t；岫t h em o d e l i n gp r o c e s so f s i n g l el i n kp r o t o c o lW a Ss e r i o u s l ys t u d i e d S t a r t i n gw i t ht h eb a s a lm o d e l，t h ec o n s u m m a t em o d e lo ft h ep r o t o c o lW a So b t a i n e db ya d d i n ge a c hs a f e t yd e f e n
10、c es t e pb ys t c p T h ep r o t o c o lo ft h eC B T Cs y s t e m1,t t l l Sv a l i d a t e da n da n a l y z e db a s e dO nt h eb u i l tm o d e l sb yC P NT o o l s A c c o r d i n gt Ot h ea n a l y s i sm e t h o d so fs a f e t yc o m m u n i c a t i o np r o t o c o l，t h eb u i l tm o d e
11、l sw e r ee s s e n t i a l l yb r o k e ad o w na n dp r e d i g e s t e df i r s t l y,t h ed y n m i ec h a r a c t e r i s t i c so f t h em o d e l sW C I ev a l i d a t e db yu s i n gt h es t a t e ss p a c e sa n a l y s i s；t h e nc o n s i d e r i n gd i f f e r e n th a z a r d se f f e e
12、 t e dt h es y s t e ms a f e t y,t h ec a p a b i l i t yo ft h ep r o t o c o lW a Sa n a l y z e d a n dt h ea v e r a g ev a l u e so fd i f f e r e n tp a r a m e t e r sw 讹o b t a i n e d F i n a l l y,a f t e rc o m p a r i n gt h ea v e r a g e sw i t ht h e 矗】【e de a p a b i l i t yt a r g
13、e t s t h ec o n c l u s i o nt h a tt h ed e s i g n e dc o m m u n i c a t i o np r o t o c o ls a t i s f i 戗!t h ei n f o r m a t i o nt a a m f e r r i n gd e m a n d so f t h eC B T Cs y s t e mw 勰e d u c e d C B T Cc o m m u n i c a t i o np r o t o c o l；S a f e t yr e l a t e ds p e e i f i
14、 e i t o n；C I)N；M o d e l i n g；C a p a b i l i t ya n a l y s i sC L A S S N 0：U 4 9j 京銮盟太堂毯堂位论塞图塞到图索引图1 典型的C B T C 系统结构图2C B T C 系统整体结构。圈3E L r R O R A D I O 系统结构图4C B T C 安全通信协议所在层次结构图5 安全相关系统参考结构图6 安全相关信息模型图7C B T C 系统通信协议基本结构图8 传递信息结构图9 链接建立过程一1 31 81 9，2 22 3图1 0 对等实体认证过程图1I 双序列号传递过程图1 2 序列号合
15、法性图1 3 信息超时定义。图1 4 通信结束过程2 9图1 5 建模思想图1 6C B T C 系统上层模型。图1 7 单链接上层模型：图1 8 列车功能子模型图1 9 Z C 功能子模型。图2 0 双链路系统的上层模型图2 l 双链路系统Z C 子模型图2 2 加入双序列号机制的T r a i n 子模型4 4图2 3 加入双序列号机制的Z C 子模型。图2 4 加入超时机制的T r a i n 子模型一4 7图2 5 加入超时机制的Z C 子模型图2 6 链接建立过程T r a i n 子模型图2 7 链接建立过程系统和Z C 模型圈2 8 数据传输过程T r a i n 子模型一图2
16、9 数据传输过程Z C 子模型5 5图3 0 建链时间情况1 图3 l 建链时间情况2 图3 2 建链时间情况3 图3 3 接收信息超时情况对比图3 4 接收信息超时情况分布图3 5 链路异常情况6 1图3 6 链路异常情况曲线学位论文版权使用授权书本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关部门或机构送交论文的复印件和磁盘。(保密的学位论文在解密后适用本授权说明)学位论文作者签名：蒡f 劢导师签名：勿劈签字日期：弦吖年f)月日
17、签字日期：如订年f z 月可日独创性声明本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。学位论文作者签名：客1 确签字日期：加7 年，2，月6 日致谢研究生的学习生活就要接近尾声了。这三年是我成长最快的一段时间，付出了许多，也收获了许多。不仅获得了学业上的成就，更重要的，是关怀我，帮助我的老师、同学和朋友。在此，我要对我的导师、所有关心和教育我
18、的老师、一路陪伴我成长的同学、朋友表示最诚挚的谢意!首先，衷心感谢我的导师唐涛教授三年来对我的关心和指导!本论文的工作是在唐涛教授的悉心指导下完成的，唐老师严谨的治学态度和科学的工作方法给了我极大的帮助和影响，他的人格魅力深深影响着我，他所倡导的严谨求实的治学态度、一丝不苟的钻研精神、勤于思考的作风将使我终生受益。轨道交通控制与安全国家重点实验室的郜春海、李开成、马连川、刘波、张建明、黄友能等老师悉心指导我和同学们参与实验室的科研工作，将我们带入轨道交通这个充满挑战的领域，在学习上和生活上都无私的给予了我很大的关心和帮助，在此向各位老师表示衷心的谢意!徐田华、周达天、袁磊、王悉、赵波波老师对于
19、我的科研工作和论文都提出了许多的宝贵意见，在此对他们的耐心指导表示衷心的感谢在实验室工作及撰写论文期间，牛儒、陆启进、曹源、刘宏杰、王伟、王义惠等同学以及参与C B T C 项目的所有同学对我论文中的研究工作给予了热情帮助，在此向他们表达我的感激之情。另外要感谢我的家人，他们的关爱、支持与鼓励始终温暖着我。我的父亲也对我的论文提出了宝贵意见，还有我的母亲，她的理解和支持使我能够在学校专心完成我的学业。最后，衷心感谢为评阅论文和参与论文答辩而付出辛勤劳动的各位专家学者，感谢您的宝贵意见!1 绪论基于通信的列车运行控制系统(C o m m u a i e a t i o o s-b a s e d
20、T r a i nC o n t r o l，简称c B l r c)技术发源于欧洲连续式列车控制系统，经过多年的发展，取得了长足的进步【。系统独立于轨道电路，采用高精度的列车定位和连续、高速、双向的数据通信，通过车载和地面安全设备实现对列车的控制，现已成为列车控制系统发展的方向，可满足铁路运输高速化、信息化、网络化的发展。我国应加快发展适合于我国国情的列控系统，在消化吸收国外先进技术的同时，研究新一代基于移动通信的C B T C 列控系统。C B T C 系统是防护安全的复杂系统，各子系统间可靠的数据通信自然成为保证整个系统安全的基础，因此需要建立一个完备的数据通信协议来保证应用数据传输的安
21、全。为了能够有效而全面客观的对协议进行分析，涌现出多种研究方法。直到九十年代初，几个研究者利用形式化方法找到了一些安全协议尚未发现的安全漏洞后，形式化方法分析通信协议逐渐成为信息安全领域中的一个热门方向。目前存在着多种形式化分析方法对协议进行分析，其中比较突出的着色P e t r i 网是一种具有层次性的高级P e t r i 网，克服了普通P e t r i 网缺少数据概念、无层次的缺点。本章将简述自主开发的C B T C 系统基本原理、C B T C 系统通信协议的基本介绍，以及研究C B T C 系统通信协议的必要性；还将概述安全通信协议技术、协议验证技术的发展；比较几种形式化规范语言和
22、工具，简要介绍形式化建模语言一一着色P e t r i 网及其建模工具C P NT o o l s，综述国内外应用P e t r i 理论和工具对分析数据通信协议的研究情况，给出用C P N 语言和工具对铁路运输系统中的通信协议建模的可行性和实际意义，最后对全文的主要工作和结构安排进行概述。1 1 研究背景简介1 1 1C B T C 系统概述1 9 9 9 年，电气和电子工程师协会轨道交通运输车辆接口委员会(I E E ER a i lT r a n s i tV e h i c l eI n t e r f a c 七S t a n d a r d sC o m m i t t e e，I
23、 E E ER T v I S C)制定并颁布了C B T C技术标准I E E ES t d1 4 7 4 1 1 9 9 9 I E E E 基于通信列车控制的性能和功能要求(第一版)。该标准详细定义了C B T C 系统的功能，并规定了C B T C 系统的列车运行间隔、安全性和可用性等技术指标1 2 1。这就是C B T C 系统的起源。现在，c B T C 系统已成为国际上信号系统的发展方向，它抛开传统的轨道电路，而采用无线通信实现地面与列车之间的双向、大容量信息传输，实现列车的移动闭塞控制。该系统具有调度指挥灵活、提高运输效率、全寿命周期造价低、安全可靠等优点，是未来城市轨道交通实
24、现高速度、高密度、小编组的最佳解决方案。目前，西门子、阿尔斯通等国外企业均已有相关产品。2 0 0 5 年至今，我国耗资3 0亿元人民币在1 3 条新建城市轨道线路上引进国外基于通信的C B T C 系统技术，并开始研制具有完全自主知识产权的C B T C 系统【引。一般的C B l r C 系统包括地面无线闭塞控制中心、列车的车载设备、地一车双向信息传输系统。I E E EC B T C 标准列举的典型C B T C 系统功能结构如图1 所示。图1 典型的c B T c 系统结构F i g u r eIT y p i c a lC B T CS y s t e mS m l c t u r
25、eC B T C 系统最显著的特点是引入了通信子系统，建立车地之间连续、双向、高速的通信，列车的命令和状态可以在车辆和地面之间可靠交换，使系统的主体C B T C 地面设备和受控对象列车紧密地联结在一起。因此，。车地通信”是C B l 系统的基础，是整个系统的支柱之一。从通信的方式来说，主要有两种方式：一种是系统初期基于感应环线电缆的感应环线通信系统，另一种则是新近发展较快的无线通信系统。本文所研究的C B l 系统就是基于无线通信系统机制的。图2 显示的是该C B T C 系统整体结构框图。其中，地面无线闭塞控制中心的各组成部分主要有列车自动监控系统A T S(A u t o m a t i
26、 c T r a i nS u p e r v i s i o n)、数据库存储单元D S U(D a t a b a s eS t o r a g eU n i t)、区域控制器Z C(Z o n eC o n t r o l l e r)、计算机联锁C l(C o m p u t e rI n t e r l o c k i n g)，系统还包括车载控制器V O B C(V e h i c l eO nB o a r dC o n t r o l l e r)和地车双向数据通信系统D C S(D a t aC o m m u n i c a t i o nS y s t e m，包括骨干网
27、、网络交换2机、无线接入点及车载移动无线设备)。值得注意的是，地车采用2 4 G 的无线方式，依据I E E E S 0 2 1 1 协议构建地车信息双向传输网络。图2 C B T C 系统整体结构F i g u r e2C B T CS y s t e mS t r u c t u r e可见，在这样一个基于无线数据通信的列控系统中，安全的地车数据通信协议是保证C B T C 系统安全的支柱之一，在整个系统中有着至关重要的作用。如何设计出一个安全可靠的通信协议来保证整个系统的安全，成为了本文要重点研究的内容。1 1 2 开发C B T C 通信协议的作用和重要意义(1)C B T C 通信协
28、议的作用在C B T C 系统中，高速铁路中传统的信号系统被无线信号系统所代替，列车由地面设备通过无线信号来传输移动授权信息进行管理，但是由于无线网络是开放的，本身不能确保数据传输的安全。从上面对安全通信协议的介绍中我们可以得知，为了保证作为安全苛求系统的列控系统的可靠性，需要定义安全的数据通信协议。当前我国铁路正处在高速发展阶段，C T C S 技术标准正在制定过程中，对于协议方面的规范并不成熟。因此吸收和借鉴国外先进技术，对我国铁路的发展是很重要的。上一小节介绍的E T C S 系统通信协议作为一种先进的已被证明的安全通信协议，通过对其技术规范的研究，我们应该学习其中适合我们借鉴的思想和技
29、未。同时，我国铁路的当前情况与欧洲的起点、技术基础、标准内涵、实施策略、发展目标等方面有所不同，因此不能照搬欧洲的标准，而应在参考的基础上加以创别”。需要说明的是，本文主要研究的通信协议是各子系统应用层之间的数据通信协议，不包括底层主干网络以及各子系统内部网络的数据传输。我们设计的C B T C 通信协议需要具备的主要作用为：能够利用合理正确的防护机制来保证信息实时性；能够利用错误侦测数据传输协议来保证信息的安全性；具用清晰的分层次的系统结构；具有模块化和可移植性；将上层的信息在双冗余总线上传输。相关安全标准中规定：如果安全相关的电子系统包括跨区域的信息交换，那么其通信系统就成为安全相关系统的
30、一部分。传输系统可分为两大类型考虑：第一种是封闭式传输系统，它的组成可由安全系统设计者在一定程度上控制；第二种是开放式传输系统，由特性未知或部分未知的系统组成。我们的C B T C 通信协议是基于开放式的传输系统，因此势必存在一些未知的危险因素。这些危险与应用功能或网络特征功能并无关系，例如信息的重复、删除、乱序、损坏、延时和伪装等等。如何保证信息传输的安全性和可靠性，是通信协议要考虑的首要问题。我们可以采用数据传输系统(非安全相关、安全相关)已有的一些成熟的技术，为自主开发的控制和防护系统所用。(2)研究C B T C 通信协议的重要意义随着计算机和通信技术的发展，现代列车控制系统以功能和复
31、杂性的大幅增4长为特点不幸的是。这些增长并没有伴随发展和评估这些系统的技术和方法一起增长【习。尤其是对于实时安全苛求系统，逻辑和时间的正确性应该根据严格的安全标准来验证。基于通信的列车运行控制系统(C B T C)是城市轨道交通信号技术的发展方向，现在我国正在致力于完全自主产权的C B l r C 系统的研发。在研发过程中，安全、可靠的地车数据通信协议正是整个C B T C 的基础和关键技术之一。其作为保证列控系统安全的重要部分，除了实现应有的功能，即保证系统数据传输的正确性、有效性之外，一定要有有力的理论依据作为评估系统安全性和性能参数的标准，才能跟踪国际技术发展趋势，促进我国的安全标准的制
32、定，建立安全认证与评估体系，尽快使我国研制开发的具有自主知识产权的C B T C 系统得以应用。因此，设计出符合相关安全标准的C B T C 系统通信协议并通过形式化方法对其性能进行分析，以证明其安全性，是具有重要意义的。1 1 3 安全通信协议技术发展我们要设计的通信协议必须是安全通信协议，因此，有必要了解当前安全通信协议技术发展的相关情况，为我们的通信协议设计工作提供参考。(1)安全传输标准数据通信系统的安全要求取决于其可知或未知的特性。它必须保证端到端的通信能达到相关欧洲标准的安全性要求。我们要研究的C B T C 通信系统是基于开放式传输环境的，对于开放式传输环境中的安全传输协议，开放
33、式传输系统安全相关通信标准(E N 5 0 1 5 9 2)做出了规定【6】，下面列举了一些该标准对安全传输系统的要求。假设开放传输系统包括连接在传输系统上的两个或多个安全相关设备间的任何环节(硬件、软件、传输媒介等)，对安全相关传输系统的参考结构规定如下：基于非置信传输系统即不考虑内部是否有传输保护机制；具备安全相关传输功能；具备安全相关访问保护功能。开放式传输系统可能受下列因素影响：传输系统外的其他用户。系统控制和未知的用户以未知格式发送数量未知的信息；传输系统的用户。试图访问其他用户产生的数据，在未得到系统管理者的允许下读取和或伪造数据；对安全相关数据完整性的其他附加威胁对防护措旆基本要
34、求，可以看成逻辑防护的技术集合，但并不是一个完全集，将来可能会开发出新的技术，给设计者提供新的选择。为了减少上面确定的隐患的风险，最基本的系统外部要求就是要保证消息的真实性、完整性、实时性和有序性。对防护措施的总体要求如下：对开放网络带来的所有已经确认的隐患采用合适的防护措施。所有不予考虑的隐患都应该经过安全而且，或者铁路权威机构认可，并且在安全相关应用环境中注明；对防护措施的具体要求为确定每种隐患的风险等级(发生频率以及后果严重程度)，以及相关数据和进程的安全完善度等级；在系统需求规范和系统安全需求规范中应包括对防护措施的要求，而且形成安全论据中的“正确运行的保证”的输入。防护措施的实施应仅
35、在安全相关的传输设备中使用，也包括不在安全相关设备中使用的访问保护方法，如果是后者，访问保护进程的正确机能会得到合适的安全相关技术的检查。某些防护具有强制要求，使用这些措施时要遵守这些要求。一个安全系统的论据应该包括：对安全传输系统中使用的每种防护措施的分析和出现传输错误时的安全对策。(2)安全传输协议范例对于开放环境中的的安全通信协议，比较权威的是欧洲列车控制系统(E u r o p e a nT r a i nC o n t r o lS y s t e m,简称E T C S)的通信协议安全相关设备安全相关设备应用进程应用进程一安全相关信息一一安全层接入点安全层接八点安全相关传-安全相关
36、靖皇-安全相关传输系统输系统传输接八点匪垂-缸匾图3E U R O R A D I O 系统结构F i g u r e3E U R O R A D I OS y s t e mS m a c t m t6目前，欧洲铁路运输管理系统(E u r o p e a nR a i lT r a f f i cM a n a g e m e n tS y s t e m,简称E R T M S)协会为高速铁路线定义了一批规范，传统的信号系统被无线信号所代替，列车由地面设备通过无线信号来传输移动授权信息进行管理。E T C S 第2 级和第3 级规定了以G S M R 数字无线通信系统作为列车控制信息及其
37、相关信息的传输平台，因为G S M 本身不能确保数据传输的安全可接受程度，因此，一种安全协议，E U R O R A D I O，在E R T M S 标准中被定义出来。其系统结构如图3 所示【n。从其结构中可以看出，在E T C S 车载和轨旁终端设备的安全应用与通信功能之间加入安全相关传输层，它通过一个或多个安全层接入点，以安全原语的方式，与安全应用进行通信。安全传输层要确保只能在合法的用户之间建立一个安全的链接，同时，在这个安全链接存在的情况下，还要确保安全信息的安全传输。E U R O R A D I O 规范也是根据E N 5 0 1 5 9 2 安全标准建立的，并且已经被A n s
38、 a l d oS e g n a l a m e n t oF e r r o v i a r i o利用U M L 状态图进行了形式化分析，并验证其为安全通信协议。从上述的规定和范例中，我们可以得到一个安全传输协议的概念，并且也有了一个可遵循的规范，据此对我们自己的C B T C 通信协议进行设计，并利用该标准中的要求实现系统的安全。设计出通信协议，对于一个安全系统来说，不能立刻予以应用，一个更重要的工作就是对设计出的协议进行分析和验证，证明其是否符合整个系统的需要，以及是否满足系统的安全性要求1 2 安全通信协议验证技术随着安全要求的提高，通信协议的验证成为一个更加复杂和困难的过程。对于
39、安全通信协议的设计来说，需要有一系列方法论、协议工程方法和工具来支持现在，许多研究者倾向于使用形式化方法来进行协议的分析和验证。形式化方法是基于数学方法来描述目标系统性质的一门技术，用严格的数形式化方法能在早期发现系统中的不一致、歧义、不完全和错误等问题，目前己被证明是一种行之有效的减少设计错误、提高系统可信性的重要途径。形式化方法的意义在于它能帮助发现其他方法不太容易发现的系统描述的不一致、不明确或不完整之处，有助于增加开发人员对系统的理解。形式化方法和工程界的常规方法相比有明显的区别，它们的开发原则不同。形式化方法希望能直接构造出尽可能正确的系统，而常规方法主要是通过测试来发现系统的错误。
40、因此，形式化方法无论是从最初的用户需求到系统设计、实现、验证都能够为系统提供必要的支持。形式化方法包含两个重要研究内容：一是形式化规范(f o r m a ls p e c i f i c a t i o n)，它是对程序功能的数学描述，是用具有精确语义的形式语言书写的协议功能描述；二是形式化验证(f o r m a lv c f i 右矗衄)，验证已有的系统是否满足其规范的要求i s 。简单来说，形式化方法指的是一个系统的数学或者逻辑模型、系统需求以及一个有效的用来判定对该系统可以满足其需求的证明是否正确的程序。以我们要分析的安全通信协议来说，就是将系统及其运行环境进行形式化描述，利用一定的
41、规则推理或者空间搜索对其进行严密而全面的分析。(1)形式化方法用于安全通信协议分析的可行性协议工程用形式化方法描述在协议严格设计和维护中的各个活动，相应的形式化描述技术贯穿协议开发的各阶段，支持协议描述、验证、实现和测试。目前，P c t r i 网己成为网络协议分析和设计的典型形式模型之一，被广泛应用于通信协议描述、验证及许多其他领域。通过P c f f i 网我们可以用一种相当清晰且易于理解的方式来模拟并发和同步，这种模拟对于通信协议的分析特别有用。协议形式化分析的一个重要目标是对协议进行验证，即核实是否一个协议的规范包含并且仅仅包含协议预期的属性。在许多应用(包含P c h-i 网应用)
42、中使用比较广泛的两个方法是可达性分析和不变量分析。它们可用于验证协议的基本属性。在可达性分析中，以可达图(R e a c h a b i l i t yG r a p h，R G)或可达树(R e a c h a b i l i t y T r)的方式从协议说明生成协议的全局状态，并且验证是否所有约定状态都已经正确生成，以及在那些状态中是否出现了预计的或者不期望的属性。通常能验证到的属性应该包括死锁、未指明或没有预期的接受，发送、变迁的活性、标记(t o k e n)数目的有界性等。不变量分析的目的是寻找同P e t r i 网的某种执行模式相关，并且保持恒定的属性。这些不变量属性也可能用于间
43、接证明其他属性，诸如返回状态(h o m e-s t a t e s)、活性(1 i v e n c 芯s)和有界性(b o u a d e d n e 爆s)等由此可见，用形式化分析协议是必要且可行的。(2)应用范例【9 H 儿l1 9 6 2 年德国的C a r lA d a mP e t r i 在他的博士论文用自动机通信中首次使用网状结构模拟通信系统。形式化分析就此起源。对安全协议用形式化方法分析的工作最初出现在七、八十年代。直到九十年代初，几个研究者利用形式化方法找到了一些安全协议尚未发现的安全漏洞后，形式化发现通信协议漏洞的方法才引起人们的极大关注，并逐渐成为信息安全领域中的一个热
44、门方向。为了能够有效而全面客观地对协议进行分析，涌现出多种研究方法。下面按照时间顺序介绍比较著名的安全协议形式化分析案例：最早提出对安全协议进行形式化分析思想的是N e e d h a m 和S c h r o c d c r。他们为进行共享和公钥认证的认证服务器系统的实现建立了安全协议。1 9 8 1 年8D e n n i n g 和S a c c o 在文献指出了N S S K 协议的一个错误，使得人们开始关注安全协议分析。此时发展起来的大多数形式化分析工具都采用了状态探测技术，即定义一个状态空间。对其探测，以确定是否存在一条对应于攻击者的一次成功攻击的路径。有些工具采用了归纳定理推证技
45、术，如在N R L 协议分析器中就运用此技术证明搜索的空问规模已经可以确保安全性。早期阶段出现的形式化分析技术已成功地发现了协议中人工分析难以发现的缺陷，如N R L 协议分析器发现了S i m m o n s的选择性广播协议的缺陷，L o n-g l e y-R i g b y 工具发现了B a n k i n g 协议的缺陷，等等。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 逻辑通过对认证协议的运行进行形式化分析。来研究认证双方如何通
46、过相互发送和接收消息的方式，发展到协议运行最终要达到的目的认证双方B A N 逻辑的规则简洁直观，易于使用。它成功地对N e e d l m m-$c h r o e d e r 公钥协议、K 面f f t o$协议等几个著名的协议进行了分析，找到了其中若干已知和未知的漏洞，极大地激发了密码学家对安全协议形式化分析的兴趣，并导致许多安全协议形式化分析方法的产生。1 9 9 2 年，加拿大皇后大学的B N i e h 首先提出了使用有色P e t r i 网对密码系统进行描述的方法。此后，皇后大学有入继续用这种方法进行研究，但在方法上没有太大的变化。这种方法具有图形界面支持、结构清晰、可以采用矩
47、阵方程分析不安全状态的可达性等优点，其方法如下：首先对可能存在的不安全状态进行描述，然后用P e t r i 网的关联矩阵计算这个不安全状态是否可达。如果可达，则存在漏洞；否则，认为不存在这种攻击的可能；对信息元素的定义比较模糊。每一个身份、密钥、临时值和消息都用一个特定的标记来表示，没有对其进行分类；每个库所(P l a c e)对应于一个固定的身份、密钥、临时值或消息，但是这就使得在模型中列出所有可能出现的身份、密钥、临时值和消息无法实现。也就无法在模型中描述出协议执行的多种情况。根据具体情况确定所截获消息是否要直接转发或窜改后转发，虽然对怎样窜改消息没有具体的规定但这就是早期的入侵者模型
48、。(3)安全通信协议形式化方法的发展和现状【J2】综观近几年出现的大量文献，安全协议形式化分析理论与方法的研究过程可归纳为以下4 个阶段：早期阶段。这一阶段的研究主要集中于对具体协议的观测、分析：形式化分析初期阶段。以D o l e v 和Y a o 的工作为标志，B A N 类逻辑及C K T S等，基于知识逻辑的有效应用，标志着研究进入了以信念逻辑为主体的时期；转折阶段。以G-L o w e 发表其著名的论文“关于N e e d h a m S c h r o e d e r 公钥9协议的一个攻击”为标志，各种一般用途的模型检测方法被用于协议分析的研究；理论证明阶段。以1 9 9 9 年F
49、 a b r e g a、H e m o g 和G u t t m a 血的S t r a n ds p a c e 理论及P a u l s o n 的归纳方法为代表，开始了协议分析理论的发展时期。现有的一些典型的形式化分析方法可归纳为以下三类：基于推理的结构性方法。如B A N 逻辑，Q 逻辑，A T 逻辑，S V O 逻辑，K a i l a r 逻辑，C S 逻辑。基于攻击的结构性方法。如通信顺序进程理论，小系统理论，D o l e v-Y a o模型，m e r r i t t 模型，M e a d o w s 模型，W o o-L a i n 模型，N R L 协议分析器。基于证明
50、的结构性方法。如串空间方法，P a u l s o n 归纳法，h u m a n-r e a d a b l e证明法，A t t a c k s 限定法，M a u d e 分析法。(4)本文中形式化建模语言的选择【1 3 l-i 1 5 1目前存在着多种理论对协议进行形式化分析。本文经过对各种方法的比较，最终采用着色P e t r i 网(C o l o r e dP e t r iN e t s，C P N s)进行建模。有色P e l r i 网是P e l r i网的一种扩展形式，利用一般P e t r i 网的结构，但在变迁规则上引入了表示与具体应用相关的各种数据类型的颜色集，以