并发理论一直是计算机科学中最富有挑战性的一个研究方向之一,至今,已发展出了各种并发理论的分支,如:Petri网、CCS(Communication and Concurrence System)、CSP(Communicating Sequential Processes)、π-演算(A Calculus of Mobile Processes)等等。如何建构一个统一的并发理论框架、特别是将Petri网与R.Milner的CCS、π-演算统一起来,一直是不少学者所追求的目标。英国计算机科学家R.Milner在1993年获得图灵奖所发表的演讲报告中就曾指出:“把代数并发性方面所做的工作与C.A.Petri在Petri网上早已取得的丰硕成果联系起来,是一个非常有希望的发展线索。然而,由于它们的概念基础并不完全吻合,所以还有困难。”关于Petri网与CCS间的研究已经有了许多很好的结果,但自Milner于九十年代初期提出π-演算理论后,由于其自身的复杂性,把Petri网与π-演算结合起来便显得极为困难。目前,在这方面的工作仅有两位学者进行过,并各自得到了不成熟的结果。我们为此提出了π-网这一并发理论模型,并初步实现了将π-演算和Petri网统一到一个并发框架中的目标。受密码学的驱动,我们对π-网进行了重新构建,将其应用到了对密码协议的形式化研究中,并形成到了密码协议的π-网语言―――EPL(Encryption Protocol Language)语言。对密码协议的形式化工作始于70年代末期,到目前为止已经形成了多种研究途径。它们所关注的是密码协议的密钥传输和鉴别性问题,要解决的核心问题是试图能主动的发现协议的缺陷,并希望能在攻击者对其实施攻击之前就能找出协议的漏洞。但事实是,尽管人们利用了多种的手段,如代数的,逻辑的,微分的,Petri网的,等等,但直至今天,问题依旧,并没有得到任何实质性的解决。EPL语言致力于该问题的研究。本文的主要贡献和创新点如下:1)提出了一类新型的基于π-演算语义的模块化的、具有代数演算能力的π-网,π-网有机的将Petri网和π-演算统一到了一个并发模型框架上,在语义上实现了从π-演算到Petri网的自动翻译,同时也解决了π-演算的分布式语义问题,从而为Petri网的研究提供了一个新的研究内容。2)初步解决了英国计算机科学家R.Mliner在1993年提出来的公开问题。π-演算是CCS的扩展,它们都是从λ-演算和C.A.Hoare的CSP上发展出来的代数并发理论,CCS所能做的工作都能在π-演算中得到完成,因此π-网实际上起到了将R.Milner在代数并发理论上的全部工作与Petri网有机的统一起来了。证明了在结构同余的条件下,π-演算是可以嵌入到π-网的子集中去,即:Ψ(P)?PN,但在π-网的强互模拟等价关系下,我们却可以把Ψ(P)和PN这二者看成是一致的,这一结论证实了π-网是Petri网和π-演算的有机结合体。3)提出了密码协议的π-网形式化模型,建立了密码协议的EPL语言。EPL语言继承了π-网的模块化和代数化的特点,通过引入项、buffer库所和解密变迁等新的建模元素,在π-网中建立了密钥管理和加密信息的传输机制,对密码协议进行了形式化描述和分析。4)利用EPL语言对密码协议进行了实例分析,通过对Wide Mouth Frog协议和Needham-Schroeder协议的分析,不仅建立了相关协议的π-网模型,同时还建立了对协议的攻击模型。5)提出了密码协议的观测等价概念,建立了密码协议的鉴别性和安全性的判别机制,为密码协议的π-网形式化研究提供了一种研究方法和途径。