Abstract
Several verification techniques based on theorem proving have been developed for the verification of security properties of cryptographic protocols specified by means of the spi calculus. However, to be used successfully, such powerful techniques require skilled users. Here we introduce a different technique which can overcome this drawback by allowing users to carry out the verification task in a completely automatic way. It is based on the definition of an extended labeled transition system, where transitions are labeled by means of the new knowledge acquired by the external environment as the result of the related events. By means of bounding the replication of parallel processes to a finite number, and by using an abstract representation of all explicitly allowed values in interactions between the spi process and the environment, the number of states and transitions remains finite and tractable, thus enabling the use of state-space exploration techniques for performing verification automatically.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35533-7_26
Chapter PDF
Similar content being viewed by others
References
M. Abadi, and A. D. Gordon, “A Calculus for Cryptographic Protocols The Spi Calculus”, Digital Research Report, vol. 149, January 1998, pp. 1–110.
M. Abadi, and A. D. Gordon, “A bisimulation method for cryptographic protocols”, Nordic Journal of Computing,Vol. 5, pp. 267–303, 1998. 170 L. Durante, R. Sisto and A. Valenzano
M. Boreale, R. De Nicola, and R. Pugliese, “Proof Techniques for Cryptographic Processes”, Proc. of the 14th IEEE Symposium Logic In Computer Science (LICS’99), IEEE Computer Society Press, pp. 157–166, 1999.
G. Lowe, “Breaking and fixing the Needham-Schroeder public-key protocol using FDR”, Proc. of TACAS’97, Springer LNCS 1055, 1996.
G.Lowe, “Casper: a compiler for the analysis of security protocols”, Proc. of 1996 IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 1996.
G. Lowe, B. Roscoe, “Using CSP to Detect Errors in the TMN Protocol”, IEEE Transactions on Software Engineering, Vol. SE-23, No. 10, pp. 659–669, October 1997.
J. K. Millen, S. C. Clark, and S. B. Freedman, “The Interrogator: Protocol Security Analysis”, IEEE Transactions on Software Engineering, Vol. SE-13, No. 2, pp. 274–288, February 1987.
G. Leduc, O. Bonaventure, L. Léonard, E. Koerner, and C. Pecheur, “Model-Based Verification of a Security Protocol for Conditional Access to Services”, Formal Methods in System Design, Vol. 14, No. 2, pp. 171–191, March 1999.
R. Milner, J. Parrow, and D. Walker, “A Calculus of mobile processes, parts I and II”, Information and Computation, pages 1–40 and 41–77, September 1992.
L. C. Paulson, “The inductive approach to verifying cryptographic protocols”, Journal of Computer Security, Vol. 6, pp. 85–128, 1998.
S. Schneider, “Verifying Authentication Protocols in CSP”, IEEE Transactions on Software Engineering, Vol. SE-24, No. 9, pp. 741–758, September 1998.
L. Durante, R. Sisto, and A. Valenzano, “A state-exploration technique for spi-calculus testing equivalence verification”, Technical Report DAI/ARC 1–00, Politecnico di Torino, Italy, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Durante, L., Sisto, R., Valenzano, A. (2000). A State-Exploration Technique for Spi-Calculus Testing-Equivalence Verification. In: Bolognesi, T., Latella, D. (eds) Formal Methods for Distributed System Development. PSTV FORTE 2000 2000. IFIP — The International Federation for Information Processing, vol 55. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35533-7_10
Download citation
DOI: https://doi.org/10.1007/978-0-387-35533-7_10
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5264-9
Online ISBN: 978-0-387-35533-7
eBook Packages: Springer Book Archive