A cryptographic protocol can be described as a system of concurrent processes, and analysis of the traces generated by this system can be used to verify authentication and secrecy properties of the protocol. However, this approach suffers from a state-explosion problem that causes the set of states and traces to be typically infinite or very large. In this paper, starting from a process language inspired by the spi-calculus, we propose a symbolic operational semantics that relies on unification and leads to compact models of protocols. We prove that the symbolic and the conventional semantics are in full agreement, and then give a method by which trace analysis can be carried out directly on the symbolic model. The method is proven to be complete for the considered class of properties and is amenable to automatic checking. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Boreale, M. (2001). Symbolic trace analysis of cryptographic protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2076 LNCS, pp. 667–681). Springer Verlag. https://doi.org/10.1007/3-540-48224-5_55
Mendeley helps you to discover research relevant for your work.