| The concurrency theory is the most challenge subject in computer science. There are many research branches, such as Petri net, CCS, CSP,π-calculus, etc. In last years, people aim to constitute a uniform framework for concurrency theory, and specially to find a framework between Petri net and CCS. Now a plenty of attempts have been made in order to understand the relationships between these concurrency theories. But since R. Milner proposed theπ-calculus in 1990's, it is most difficult to find the relationship between theπ-calculus and Petri net. One of the reason is that the construction of theπ-calculus itself is very complicated. Up to now, there are only two researchers have made great effort in this field and obtained some immature results. Our main goal in this paper is to survey some of the main ideas behind this approach to concurrency. We present a new concurrency model---π-net, and at the same time realizes the function of integrating Petri net and theπ-calculus within one unified concurrency framework.Motivated by cryptography, we reconstruct theπ-net and apply it to formalize cryptographic protocols, and build the EPL language------the language for cryptographic protocols based on the semantics of theπ-net. To formalize cryptographic protocols started in 1970's. Now there are many approaches for describing cryptographic protocols. All of them pay close attention to transmission of keys and authentication in a protocol. The kernel problem is that try to find some drawback in a protocol actively. In fact, although a lot of methods are used to solve this problem, such as formal language, expert system, logic, etc., it has not been solved as before. The EPL language turns to the approach of the problem.The main contribution this dissertation is as follows:1) We present a new high-level modular Petri net------π-net based on the semantics of theπ-calculus. It integrates Petri net and theπ-calculus in the same concurrency model. Theπ-net can achieve the automatic semantics translation fromπ-calculus to Petri net. Besides, the problem of distributed semantics of theπ-calculus is also settled.2) We find the preliminary solution to the OPEN problem proposed by R.Milner in 1993. It has been proved that theπ-calculus can be imbedded into a subnet of theπ-net under the functionΨ, such thatΨ(P)?PN. And in the view of the strong bisimulation equivalence,Ψ(P) is even equivalent to PN. This conclusion indicates thatπ-net not only preserves the quality of Petri net, but also acquires the algebraic ability of theπ-calculus. Soπ-net is an effective compound system for Petri net and theπ-calculus.3) By preserving theπ-net's modular and algebraic merits and adding nodes as buffer places, and introducing decryption transitions with key management policies, we propose the extendedπ-nets and build the EPL language that can be used to model cryptographic protocols requirements. This newπ-nets enables us to consider cryptographic issues in detail.4) Based on the semantics of the EPL, we analyze two special cryptographic protocols, the Wide Mouth Frog protocol and the Needham-Schroeder protocol.5) We represent the concept of observation equivalence for cryptographic protocols. Based on theπ-nets, the authentication and exchanging of session keys are described and analyzed efficiently.
|
PDF Full Text Request