## 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}, }