A pure labeled transition semantics for the applied pi calculus
A pure labeled transition semantics for the applied pi calculus
复制标题
DOI：
10.1016/j.ins.2010.07.008
复制
发表时间：
2010-11
期刊：
影响因子：
--
通讯作者：
Xiaojuan Cai
中科院分区：
文献类型：
--
作者：
Xiaojuan Cai
Abadi和Fournet提出的应用pi演算在安全协议分析中是成功的。它的语义主要依赖于几个结构规则。结构化规则便于规范，但在实现时效率低下。本文在纯标记转换系统的基础上建立了应用π微积分的新语义，并提出了标记双模拟的新表述。我们证明了新的标记双奇异性与观测等价性是一致的。最后以一个零知识协议为例说明了该语义的有效性。
The applied pi calculus proposed by Abadi and Fournet is successful in the analysis of security protocols. Its semantics mainly depends on several structural rules. Structural rules are convenient for specification, but inefficient for implementation. In this paper, we establish a new semantics for applied pi calculus based upon pure labeled transition system and propose a new formulation of labeled bisimulation. We prove that the new labeled bisimularity coincides with observational equivalence. A zero-knowledge protocol is given as an example to illustrate the effectiveness of this new semantics.