Symbolic bisimulation for the applied pi calculus
Symbolic bisimulation for the applied pi calculus
复制标题
DOI：
10.3233/jcs-2010-0363
复制
发表时间：
2007-12
期刊：
影响因子：
--
通讯作者：
S. Delaune;S. Kremer;M. Ryan
中科院分区：
文献类型：
--
作者：
S. Delaune;S. Kremer;M. Ryan
我们提出了一个符号语义的有限应用π演算。应用的pi演算是pi演算的一个变种，扩展了密码协议的建模。通过象征性地对待输入，我们的语义避免了由于来自环境的输入而导致的执行树的潜在无限分支。正确性是通过将每个过程与一组术语约束相关联来维护的。我们定义了一个符号标记的互模拟关系，这是健全的，但不完整的标准互模拟。我们探讨了缺乏完整性，并证明了符号互模拟关系是足够的许多实际例子。这项工作是一个重要的一步，自动化的观察等价有限应用π演算，例如验证匿名性或强保密性。
We propose a symbolic semantics for the finite applied pi calculus. The applied pi calculus is a variant of the pi calculus with extensions for modelling cryptographic protocols. By treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms. We define a symbolic labelled bisimulation relation, which is shown to be sound but not complete with respect to standard bisimulation. We explore the lack of completeness and demonstrate that the symbolic bisimulation relation is sufficient for many practical examples. This work is an important step towards automation of observational equivalence for the finite applied pi calculus, e.g. for verification of anonymity or strong secrecy properties.