Affiliations: [a] LSV, ENS Cachan & CNRS & INRIA, France | [b] School of Computer Science, University of Birmingham, UK
Note: [*] This work has been partly supported by the EPSRC projects EP/E029833, Verifying Properties in Electronic Voting Protocols and EP/E040829/1, Verifying Anonymity and Privacy Properties of Security Protocols, the ARA SESUR project AVOTÉ and the ARTIST2 NoE. Preliminary versions of this paper appeared in [13] and [14].
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, e.g. for verification of anonymity or strong secrecy properties.
Keywords: Applied pi calculus, observational equivalence, security protocols
