CVS at Work: A Report on New Failures upon Some Cryptographic Protocols

  • Antonio Durante
  • Riccardo Focardi
  • Roberto Gorrieri
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2052)


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.


Authentication Protocol Security Protocol Security Property Cryptographic Protocol Covert Channel 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi: Two Facets of Authentication. In: Proceedings of 11th IEEE Computer Security Foundations Workshop. IEEE press. (June 1998) 25–32Google Scholar
  2. 2.
    Abadi, M. and Needham, R.: Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering, 22(1) (January 1996)Google Scholar
  3. 3.
    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–84Google Scholar
  4. 4.
    John Clark and Jeremy Jacob: A Survay of Authentication Protocols Literature: version 1.0. Available at, (November 1997)
  5. 5.
    Diffie, W., van Oorschot, P.C., and Wiener, M.J.: Authentication and Authenticated Key Exchanges. Design, Codes and Cryptography, 2:107–125 (1992)CrossRefGoogle Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Durante, A.: Uno strumento automatico per la verifica di protocolli crittograci. Master’s thesis, Università degli Studi di Bologna (sede Cesena). (luglio 1998)Google Scholar
  8. 8.
    Durante, A.: Analysis of cryptographic protocols: the environment and the application. In: Proceedings of 15th IFIP SEC 2000. (August 2000)Google Scholar
  9. 9.
    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–212Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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–77Google Scholar
  12. 12.
    Focardi, R. and Gorrieri, R.: A Classification of Security Properties for Process Algebras. Journal of Computer Security, 3(1):5–33 (1995)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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–755Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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–20Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    Meadows, C.: The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2):113–131 (1996)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Antonio Durante
    • 1
  • Riccardo Focardi
    • 2
  • Roberto Gorrieri
    • 3
  1. 1.Dipartimento di Scienze dell’InformazioneUniversità di Roma “La Sapienza”Germany
  2. 2.Dipartimento di InformaticaUniversità Ca’ Foscari di VeneziaGermany
  3. 3.Dipartimento di Scienze dell’InformazioneUniversità di BolognaUSA

Personalised recommendations