Symbolic Bisimulation for the Applied Pi-Calculus
Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Symbolic Bisimulation for the Applied Pi-Calculus. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp. 133–145, Lecture Notes in Computer Science 4855, Springer, New Delhi, India, December 2007.
doi:10.1007/978-3-540-77050-3_11
Download
[PDF] [PDF (long version)] [HTML]
Abstract
We propose a symbolic semantics for the finite applied pi calculus, which is a variant of the pi calculus with extensions for modelling cryptgraphic 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 symbolic terms. Based on the semantics, we define a sound symbolic labelled bisimulation relation. This 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 of protocols with a bounded number of sessions.
BibTeX
@inproceedings{DKR-fsttcs07,
abstract = {We propose a symbolic semantics for the finite
applied pi calculus, which is a variant of the pi
calculus with extensions for modelling cryptgraphic
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 symbolic terms. Based
on the semantics, we~define a sound symbolic labelled
bisimulation relation. This~is an important step
towards automation of observational equivalence for
the finite applied pi calculus, \emph{e.g.}, for
verification of anonymity or strong secrecy
properties of protocols with a bounded number of
sessions.},
address = {New~Delhi, India},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
DOI = {10.1007/978-3-540-77050-3_11},
editor = {Arvind, V. and Prasad, Sanjiva},
month = dec,
pages = {133-145},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Symbolic Bisimulation for the Applied Pi-Calculus},
volume = {4855},
year = {2007},
acceptrate = {40/135},
acronym = {{FSTTCS}'07},
nmonth = {12},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fsttcs07.pdf},
}