Abstract
We propose a symbolic semantics for the finite applied pi calculus, which 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 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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Delaune, S., Kremer, S., & Ryan, M. (2007). Symbolic bisimulation for the applied Pi calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4855 LNCS, pp. 133–145). Springer Verlag. https://doi.org/10.1007/978-3-540-77050-3_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
