On Testing Equivalences For Asymmetric And Asynchronous Asymmetric χ-calculus

The rapid development of network technology makes information security increasingly important. Security protocols, the base of information security, become more and more crucial. By contrast, it is common that there have been several examples of protocols that were published, believed to be sound, and later shown to have several security flaws. The complexity of the network environment will make it available for intruder to raise attacks by taking advantage of various flaws of the protocols. So, it is a key problem whether a security protocol reaches the designed security criteria.The analysis of security protocols is very important techniques to guarantee the security properties and requirements met. Formal methods are both necessary and efficient for these purposes.Process calculus is a powerful tool to model concurrent systems. With strong ability of description and formal semantics, process calculus can precisely characterize the interaction between different participants of a security protocol. When applying process calculus, we can benefit from not only the basic verification theories and methods from it as an algebra model, but also program analysis methods from it as an abstract programming language.Protocols are represented as processes while their security properties are represented using the notion of protocol equivalence. Therefore, the focus of security becomes to describe equivalences.Testing equivalence is an important equivence relation which is a quite powerful means for expressing security properties of cryptographic protocols. Testing equivalences for asymmetric and asynchronous asymmetic x-calculus are introduced in this thesis.The main results are listed as follows:Syntax and semantics for the asymmetric and asynchronous asymmetic x-calculus are defined. We propose operators as syntax for asymmetic and asynchronous asymmetic x-calculus; we apply the labeled transition system to define operational semantics for asymmetric and asynchronous asymmetic x-calculus. Asynchronous communication is emphasized for asynchronous asymmetic x-calculus.Both testing equivalences for asymmetric and asynchronous asymmetic x-calculus and testing order are elaborated.Normal form and theorms of normal form are established. Especially, every process can be rewritten to normal process.We try to modify and transplant the axioms or laws of the exsiting mobile process calculus, such as CCS andπ-calculus, and construct the axioms which are special for asymmetric and asynchronous asymmetric x-calculus, and take advantage of these axioms or laws above to construct an axiomatic system.We prove the soundness and completeness of the axiomatic system.