Symbolic bisimulation for the applied pi calculus

被引：20

作者：

Delaune, Stephanie ^{[1
,2
,3
]}

Kremer, Steve ^{[1
,2
,3
]}

Ryan, Mark ^{[4
]}

机构：

[1] ENS, LSV, Cachan, France

[2] CNRS, Paris, France

[3] INRIA, Rocquencourt, France

[4] Univ Birmingham, Sch Comp Sci, Birmingham, W Midlands, England

来源：

JOURNAL OF COMPUTER SECURITY | 2010年 / 18卷 / 02期

基金：

英国工程与自然科学研究理事会;

关键词：

Applied pi calculus; observational equivalence; security protocols;

D O I：

10.3233/JCS-2010-0363

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：317 / 377

页数：61

共 21 条

[11]

Delaune S., 2004, P 11 ACM C COMP COMM, P278

[12]

Delaune S., 2007, PREL P 5 INT WORKSH

[13]

Delaune S., 2008, LSV0832 ENS CACH

[14]

Delaune S., 2006, P 19 IEEE COMP SEC F, P28

[15]

Delaune S, 2007, LECT NOTES COMPUT SC, V4855, P133

[16] ON THE SECURITY OF PUBLIC KEY PROTOCOLS [J].

DOLEV, D ;

YAO, AC .

IEEE TRANSACTIONS ON INFORMATION THEORY, 1983, 29 (02) :198-208

[17]

Fujioka A., 1992, LNCS, V718, P244

[18] SYMBOLIC BISIMULATIONS [J].

HENNESSY, M ;

LIN, H .

THEORETICAL COMPUTER SCIENCE, 1995, 138 (02) :353-389

[19]

Kremer S, 2005, LECT NOTES COMPUT SC, V3444, P186

[20]

MILLEN J, 2001, P 8 ACM C COMP COMM, P166, DOI DOI 10.1145/501983.502007

← 1 2 3 →