@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@article{DKR-jcs09,
abstract = {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, \textit{e.g.}~for
verification of anonymity or strong secrecy
properties.},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
DOI = {10.3233/JCS-2010-0363},
journal = {Journal of Computer Security},
month = mar,
number = {2},
pages = {317-377},
publisher = {{IOS} Press},
title = {Symbolic bisimulation for the applied pi~calculus},
volume = {18},
year = {2010},
nmonth = {3},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs09.pdf},
}