Applied pi-演算是用来表示和分析安全协议的演算。它从pi-演算中继承了通信，并发以及限制算子。它引入了原语函数和等值理论来表示安全协议中的相关操作。在applied pi-演算中，安全协议用进程来表示。安全性质，例如秘密性(secrecy)和认证性(authentication)，可以用可达性(reachability properties)来表示，即一种在路径上的性质(trace properties)。一些不能使用路径来表示的安全性质，例如匿名性(anonymity)，隐私性(privacy)和强秘密性(strongsecrecy)，则需要使用进程间的观察等价(observational equivalence)的概念来表示，这是一种从攻击者的角度来看的不可区分性。观察等价是一种基于上下文(context)的等价关系，即A≈B则对于任意的上下文C有C[A]≈C[B]。在任意的上下文中，进程A，B的行为是不可区分的。上下文表示的是主动攻击者(active attackers)，这类攻击者可以截获并伪造数据。因此观察等价可以用来表示存在攻击者时的一些安全性质。　　 任意的上下文使得观察等价很难验证。因此[2]中提出了标号互模拟(labeled bisimilarity)的概念。标号互模拟关系是基于对标号迁移的直接比较，而不是基于任意的上下文。与pi-演算、传值ccs等类似，applied pi-演算的标号迁移系统中任意的输入值会产生无穷的分支，即迁移a(x).Pα(M)→{M/x)中的M可能是无穷多的，这给标号互模拟的验证带来了困难。对于无穷分支，标准的做法是建立符号化语义(symbolic semantics)，定义等价的符号化互模拟(symbolic bisimulation)。符号化语义的基本思想是用符号变量及约束条件来代替无穷多的输入值。符号化语义对于传值CCS、pi-演算等都已成功的建立[12，24，28]。然而，如[22]中所述，在applied pi-演算上建立符号语义却远比想象中困难。迄今为止，applied pi-演算上的还没有一个完备的符号化语义，即便是针对演算中的有穷部分。不完备性会导致在协议的验证过程中检测出错误的攻击。另外，复制算子(replications)不在[22]中的符号化语义的处理范围内，这主要是由于复制中会产生无穷多的受限名，而[22]中的技术无法处理这一问题。　　 针对这些问题，提出了一个新的applied pi-演算上的符号化语义，定义了相对于观察等价可靠且完备的符号化互模拟。Applied pi-演算上的符号化互模拟是以约束条件(constraints)为参数的。一个约束条件由公式(formula)和可推导条件(deducibility)构成。公式是在通常的布尔代数中引入了加入了两个新的算子σ()Φ和Hn.Φ。直观上来讲，这两个算子表示的是在对公式Φ求值时所必须考虑的环境知识。可推导是一个在对安全协议的分析中广泛使用的概念，例如[5，19，22，33]，它用来表示攻击者根据已知的消息推导出新的消息的能力。对于复制算子，引入了一种“on-the-fly”的办法来处理它，使得复制的展开和变换交替的进行，从而克服无穷的受限名带来的问题。　　 在上述符号化互模拟的基础上，对于applied pi-演算中的有穷进程部分，提出了一个符号式证明系统来推导观察等价关系。等式推理(equationalreasoning)是进程代数中常用的技术。证明系统可以看作是先前证明系统[23，25，28，35]的一个一般性的扩展。相对于观察等价，证明系统是可靠的，并且在applied pi-演算的实际中常用的一个子集上是完备的。