随着计算机网络的发展,信息安全问题已变得日益重要。信息的安全性已经不是仅仅依赖一个好的加密算法就可以得以解决的问题,它需要综合的安全理论、安全措施和安全技术来保证。其中,安全协议起着至关重要的作用。然而事与愿违,已有的安全协议往往被证实并不如它们的设计者所期望的那样安全,复杂的网络环境使得攻击者可利用安全协议设计中的缺陷和漏洞来实施各种各样的攻击。因此,安全协议自身的安全性成了网络安全的关键问题之一。运用有效的手段和工具对协议进行安全性分析是保证安全协议的安全性的重要一环。形式化分析方法是一种重要的安全协议分析方法。进程演算是描述交互系统的建模工具,具有强大的描述能力和严格的语义,可以很精确地刻划协议的运行过程。利用进程演算对安全协议分析时,既可借鉴其作为代数模型的基本验证理论和方法,又可使用其作为抽象程序设计语言的程序分析方法。在进程演算的框架内,安全性质可用进程之间的等价性描述。更确切地说,如果一个安全协议进程与对应的特定理想化进程是等价的,那么安全协议系统将与该特定理想化系统具有相同的安全性质。测试等价关系就是一种常见的等价关系。安全协议的安全属性很自然地可以被描述成特定进程项之间的测试等价关系。而非对称和异步非对称χ演算的测试等价关系便是本文的主要研究内容。本文的研究成果主要包括以下几个方面:●给出了非对称和异步非对称χ演算的语法和操作语义。在语法上,使用一组算子定义非对称和异步非对称χ演算的进程;在操作语义上,采用标号转移系统定义非对称和异步非对称χ演算的操作语义。而异步非对称χ演算强调异步通信。●定义了非对称和异步非对称χ-演算的测试等价关系,并给出了测试序。●定义了范式,并给出了范式的相关定理。特别给出了任意一个进程都可转换成范式进程的结论。●对现有的移动进程演算(如CCS,π演算)的一般公理和规则进行改造和移植,专门针对非对称和异步非对称χ演算的性质构造了其他一般公理,从而得到公理化系统。●给出了非对称和异步非对称χ演算的测试关系的性质和可靠完备结论。