Abstract
CVS is an automatic tool for the verification of cryptographic protocols, we have presented in [9], [10], that uses a non-interference based analysis technique which has been successfully applied to many case-studies, essentially most of those belonging to the Clark & Jacob’s library [4]. In this paper we report some new failures we have found. More precisely, we have been able to detect attacks upon two unflawed (to the best of our knowledge) protocols: Woo & Lam public key one-way authentication protocol and ISO public key two-pass parallel mutual authentication protocol; and new failures upon two flawed protocols: Encrypted Key Exchange and Station to Station protocols.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Abadi: Two Facets of Authentication. In: Proceedings of 11th IEEE Computer Security Foundations Workshop. IEEE press. (June 1998) 25–32
Abadi, M. and Needham, R.: Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering, 22(1) (January 1996)
Bellovin, S.M. and Merritt, M.: Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks. In: Proceedings of 1992 IEEE Computer Society Conference on Research in Security and Privacy. (1992) 72–84
John Clark and Jeremy Jacob: A Survay of Authentication Protocols Literature: version 1.0. Available at http://www.cs.york.ac.uk/jac/papers/drareview.ps.gz, (November 1997)
Diffie, W., van Oorschot, P.C., and Wiener, M.J.: Authentication and Authenticated Key Exchanges. Design, Codes and Cryptography, 2:107–125 (1992)
Donovan, B., Norris, P., and Lowe, G.: “Analizing a Library of Security Protocols Using Casper and FDR”. In Proceedings of the FLoC Workshop Formal Methods and Security Protocols, Trento (July 1999)
Durante, A.: Uno strumento automatico per la verifica di protocolli crittograci. Master’s thesis, Università degli Studi di Bologna (sede Cesena). (luglio 1998)
Durante, A.: Analysis of cryptographic protocols: the environment and the application. In: Proceedings of 15th IFIP SEC 2000. (August 2000)
Durante, A., Focardi, R., and Gorrieri, R.: CVS: a tools for the analysis of cryptographic protocols. In Proceedings of 12th IEEE Computer Security Foundation Workshop, (July 1999) 203–212
Durante, A., Focardi, R., and Gorrieri, R.: A Compiler for Analysing Cryptographic Protocols Using Non-Interference. To appear in ACM Transaction on Software Engeneering and Methodology (TOSEM) (2000)
Fabrega, F.J.T., Herzog, J.C., and Guttman, J.D.: Honest Ideals on Strand Spaces. In: Proceedings of 11th IEEE Computer Security Foundation Workshop. (June 1998) 66–77
Focardi, R. and Gorrieri, R.: A Classification of Security Properties for Process Algebras. Journal of Computer Security, 3(1):5–33 (1995)
Focardi, R. and Gorrieri, R.: The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. IEEE Transactions on Software Engineering, 23(9):550–571 (September 1997)
Focardi, R., Gorrieri, R., and Martinelli, F.: “Non Interference for the Analysis of Cryptographic Protocols”. In Proceedings of ICALP’00. LNCS 1853 (July 2000) 744–755
Focardi, R. and Martinelli, F.: A Uniform Approach for the Definition of Security Properties. In: Proceedings of World Congress on Formal Methods in the Development of Computing Systems (FM’99), LNCS 1708. Toulouse (France). Springer-Verlag LNCS. 794—813 (September 1999)
Goguen, J.A. and Meseguer, J.: Security Policy and Security Models. In: Proceeding—s of the 1982 Symposium on Security and Privacy. IEEE Computer Society Press (April 1982) 11–20
Gollman, D.: On the Verification of Cryptographic Protocols — A Tale of Two Committees. In: Workshop on secure architectures and information flow. Vol. 32 of ENTCS (2000)
International Organization for Standardization. Information technology — Security techniques — Entity authentication mechanism; Part 3: Entity authentication using a public key algorithm. ISO/IEC 9798-3 (1995)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol using FDR. In: Proceedings of Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96). Passau (Germany). Springer-Verlag, LNCS 1055. 146–166 (March 1996)
Lowe, G.: CASPER: A Compiler for the Analysis of the security protocols. In: Proceedings Tenth IEEE Computer Security Foundation Workshop, (CSFW’97). Rockport Massachusetts (USA). IEEE Press 18–30 (June 1997)
Meadows, C.: The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2):113–131 (1996)
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
Durante, A., Focardi, R., Gorrieri, R. (2001). CVS at Work: A Report on New Failures upon Some Cryptographic Protocols. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds) Information Assurance in Computer Networks. MMM-ACNS 2001. Lecture Notes in Computer Science, vol 2052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45116-1_28
Download citation
DOI: https://doi.org/10.1007/3-540-45116-1_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42103-0
Online ISBN: 978-3-540-45116-7
eBook Packages: Springer Book Archive