基于π演算的petri网和密码协议的形式化分析

《基于π演算的petri网和密码协议的形式化分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、上海交通大学博士学位论文摘要并发理论一直是计算机科学中最富有挑战性的一个研究方向之一，至今，已发展出了各种并发理论的分支，如：Petri网、CCS(CommunicationandConcurrenceSystem)、CSP(CommunicatingSequentialProcesses)、耳·演算(ACalculusofMobileProcesses)等等。如何建构一个统一的并发理论框架、特别是将Petri网与ILMilner的CCS、舻演算统一起来，一直是不少学者所追求的目标。英国计算机科学家R．Miln盯在1993年获得图灵奖所发表的演讲报告中就曾指出

2、：“把代数并发性方面所做的工作与C．A．Pe啊在Pe研网上早已取得的丰硕成果联系起来，是一个非常有希望的发展线索。然而，由于它们的概念基础并不完全吻合。所以还有困难。”关于Petri网与CCS问的研究已经有了许多很好的结果。但自Milner于九十年代初期提出伽演算理论后，由于其自身的复杂性，把Petri网与和演算结合起来便显得极为困难．目前，在这方面的工作仅有两位学者进行过，并各自得到了不成熟的结果．我们为此提出了舻网这一并发理论模型，并初步实现了将肛演算和Petri网统一到一个并发框架中的目标．受密码学的驱动，我们对m网进行了重新构建，将其应用到了对密码协议

3、的形式化研究中，并形成到了密码协议的舡网语言一一--EPL(EncryptionProtocolLanguage)语言。对密码协议的形式化工作始于70年代末期，到目前为止已经形成了多种研究途径．它们所关注的是密码协议的密钥传输和鉴别性问题，要解决的核心问题是试图能主动的发现协议的缺陷，并希望能在攻击者对其实施攻击之前就能找出协议的漏洞。但事实是，尽管人们利用了多种的手段，如代数的，逻辑的，微分的，PeUi网的，等等，但直至今天，问题依旧，并没有得到任何实质性的解决．EPL语言致力于该问题的研究．本文的主要贡献和创新点如下：1)提出了一类新型的基于小演算语义的模

4、块化的、具有代数演算能力的哥阿，昏网有机的将Petri网和哥演算统一到了一个并发模型框架上，在语义上实现了从加演算到Petri同的自动翻译，同时也解决了伽演算的分布式语义闷题，从而为Petri网的研究提供了一个新的研究内容．上海交适大学博士学位论文2)初步解决了英国计算机科学家R．Mliner在1993年提出来的公开问题。m演算是CCS的扩展。它们都是从九·演算和C．A．Hoare的CSP上发展出来的代数并发理论，CCS所能做的工作都能在静演算中得到完成，因此加网实际上起到了将R．Milner在代数并发理论上的全部工作与Petri网有机的统一起来了。证明了在结

5、构同余的条件下，肚演算是可以嵌入到兀·网的子集中去，即：甲伊)眇Ⅳ’但在伽网的强互模拟等价关系下，我们却可以把ll，(乃和尹。这二者看成是一致的，这一结论证实了m网是Petri网和舡演算的有机结合体．3)提出了密码协议的小网形式化模型，建立了密码协议的EPL语言．EPL语言继承了弘网的模块化和代数化的特点，通过引入项、buffer库所和解密变迁等新的建模元素，在卅网中建立了密钥管理和加密信息的传输机制，对密码协议进行了形式化描述和分析．∞利用EPL语言对密码协议进行了实例分析，通过对晰dcMouthFrog协议和Needham-Schroeder协议的分析，不

6、仅建立了相关协议的靠．网模型，同时还建立了对协议的攻击模型．·51提出了密码协议的观测等价概念，建立了密码协议的鉴别性和安全性的判别机制，为密码协议的,t-I碉形式化研究提供了一种研究方法和途径．关键词，Petri网，舡演算，静网，标号语义操作规则。强互模拟，密码协议。鉴别，安全，观测等价．n上海交遁大学博士学位论文A自噶臼aet’n彤r,oncurrcneytheoryisthemost,'hallenge印bjectineOmlmtet鲥e懈．There111"emanyresearchbranches，suchasPetrinet,CCS，CSP，n-c

7、alleulus，ete．Inlasty锄，peopleaimtoeonslitutcauniformframeworkforconcurrencytheory,卸dspecially10finda丘锄Fw伽lkbetweenJ'etrinetandCC$．Nowaplentyofattemptshavebeennlltdoinordertounderstandtherelationshipsbetwl期rltlaeseeoneurrerleytheories．ButsincelLMilnerproposedthe7t-r．aleul哪in1990’s，iti

8、smostdittieulttofin