Abstract
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.
A preliminary version of this paper has been circulated as [5]. Research partly supported by the Italian MURST Project TOSCA (Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi, A.D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999.
M. Abadi, A.D. Gordon. A Bisimulation Method for Cryptographic Protocols. Nordic Journal of Computing, 5(4):267–303, 1998.
R. Amadio, S. Prasad. The game of the name in cryptographic tables. RR 3733 INRIA Sophia Antipolis. In Proc. of Asian’00, LNCS, 2000.
R.M. Amadio, S. Lugiez. On the reachability problem in cryptographic protocols. In Proc. of Concur’00, LNCS, 2000. Full version: RR 3915 Inria Sophia Antipolis.
M. Boreale. Symbolic analysis of cryptographic protocols in the spi-calculus. Manuscript, 2000. Available at http://www.dsi.unifi.it/~boreale/papers.html.
M. Boreale. STA: a tool for trace analysis of cryptographic protocols. ML object code and examples, 2001. Available at http://www.dsi.unifi.it/~boreale/tool.html.
M. Boreale, R. De Nicola, R. Pugliese. Proof Techniques for Cryptographic Processes. In Proc. of LICS’99, IEEE Computer Society Press, 1999. Full version to appear in SIAM Journal on Computing.
M. Burrows, M. Abadi, R.M. Needham. A logic of authentication. Proc. of the Royal Society of London, 426:233–271, 1989.
E.M. Clarke, S. Jha, W. Marrero. Using state exploration and a natural deduction style message derivation engine to verify security protocols. In Proc. of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET), 1998.
N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. Undecidability of bounded security protocols. In Proc. of Workshop on Formal Methods and Security Protocols, Trento, 1999.
D. Dolev, A.C. Yao. On the security of public key protocols. In IEEE Transactions on Information Theory 29(2):198–208, 1983.
A. Huima. Efficient infinite-state analysis of security protocols. In Proc. of Workshop on Formal Methods and Security Protocols, Trento, 1999.
G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In Proceedings of TACAS’96, (T. Margaria, B. Steffen, Eds.), LNCS 1055, pp. 147–166, Springer-Verlag, 1996.
G. Lowe. A Hierarchy of Authentication Specifications. In 10th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 1997.
G. Lowe. Towards a completeness result for model checking of security protocols. In 11th Computer Security Foundations Workshop, IEEE Computer Society Press, 1998.
D. Marchignoli, F. Martinelli. Automatic verification of cryptographic protocols through compositional analysis techniques. In Proc. of TACAS99, LNCS 1579:148–163, 1999.
R. Milner, J. Parrow, D. Walker. A calculus of mobile processes, (Part I and II). Information and Computation, 100:1–77, 1992.
L.C. Paulson. Proving Security Protocols Correct. In Proc. of LICS’99, IEEE Computer Society Press, 1999.
A.W. Roscoe. Modelling and verifying key-exchange using CSP and FDR. In 8th Computer Security Foundations Workshop, IEEE Computer Society Press, 1995.
A.W. Roscoe. Proving security protocols with model checkers by data independent techniques. In 11th Computer Security Foundations Workshop, IEEE Computer Society Press, 1998.
S. Schneider. Verifying Authentication Protocols in CSP. IEEE Transactions on Software Engineering, 24(8):743–758, 1998.
S. Stoller. A reduction for automated verification of security protocols. In Proc. Of Workshop on Formal Methods and Security Protocols, Trento, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boreale, M. (2001). Symbolic Trace Analysis of Cryptographic Protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds) Automata, Languages and Programming. ICALP 2001. Lecture Notes in Computer Science, vol 2076. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48224-5_55
Download citation
DOI: https://doi.org/10.1007/3-540-48224-5_55
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42287-7
Online ISBN: 978-3-540-48224-6
eBook Packages: Springer Book Archive