An Improved Constraint-Based System for the Verification of Security Protocols

  • Ricardo Corin
  • Sandro Etalle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


We propose a constraint-based system for the verification of security protocols that improves upon the one developed by Millen and Shmatikov [30]. Our system features (1) a significantly more efficient implementation, (2) a monotonic behavior, which also allows to detect flaws associated to partial runs and (3) a more expressive syntax, in which a principal may also perform explicit checks. In this paper we also show why these improvements yield a more effective and practical system.


Security Protocol Mutual Authentication Cryptographic Protocol Parallel Session Strand Space 
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 and B. Blanchet. Secrecy types for asymmetric communication. In F. Honsel and M. Miculan, editors, Proc. Foundation of Software Science and Computation Structures (FoSSaCS 2001), volume 2030 of LNCS, pages 25–41. Springer-Verlag, 2001.CrossRefGoogle Scholar
  2. 2.
    M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pages 33–44, Portland, Oregon, 2002. ACM Press.Google Scholar
  3. 3.
    L. C. Aiello and F. Massacci. Verifying security protocols as planning in logic programming. Transactions on Computational Logic, 2(4):542–580, 2001.CrossRefMathSciNetGoogle Scholar
  4. 4.
    K. R. Apt. From Logic Programming to Prolog. International Series in Computer Science. Prentice Hall, 1997.Google Scholar
  5. 5.
    D. Basin. Lazy infinite-state analysis of security protocols. In R. Baumgart, editor, Secure Networking-CQRE (Secure)’ 99, International Exhibition and Congress, volume 1740 of LNCS, pages 30–42. Springer-Verlag, 1999.CrossRefGoogle Scholar
  6. 6.
    G. Bella and L. C. Paulson. Kerberos version IV: Inductive analysis of the secrecy goals. In J.-J. Quisquater, editor, Proc. 5th European Symposium on Research in Computer Security, volume 1485 of LNCS, pages 361–375, Louvain-la-Neuve, Belgium, 1998. Springer-Verlag.Google Scholar
  7. 7.
    B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In S. Schneider, editor, Proc. 14th IEEE Computer Security Foundations Workshop, 2001.Google Scholar
  8. 8.
    M. Boreale. Symbolic trace analysis of cryptographic protocols. In 28th Colloquium on Automata, Languages and Programming (ICALP), LNCS, pages 667–681. Springer-Verlag, 2001.CrossRefGoogle Scholar
  9. 9.
    M. Bozzano. Ensuring security through model checking in a logical environment (preliminary results). In G. Delzanno, S. Etalle, and M. Gabbrielli, editors, Proc. Workshop on Specification, Analysis and Validation for Emerging Technologies (SAVE01), 2001.Google Scholar
  10. 10.
    M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18–36, 1990.CrossRefGoogle Scholar
  11. 11.
    I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In PCSFW: Proc. 12th Computer Security Foundations Workshop, pages 55–69. IEEE Computer Society Press, 1999.Google Scholar
  12. 12.
    I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Relating strands and multiset rewriting for security protocol analysis. In PCSFW: Proc. 13th Computer Security Foundations Workshop, pages 35–51. IEEE Computer Society Press, 2000.Google Scholar
  13. 13.
    Y. Chevalier, F. Jacquemard, M. Rusinowitch, M. Turuani, and L. Vigneron. CASRUL web site.
  14. 14.
    Y. Chevalier and L. Vigneron. A tool for lazy verification of security protocols. In Proc. 16th IEEE International Conference Automated Software Engineering, 2001.Google Scholar
  15. 15.
    Y. Chevalier and L. Vigneron. Towards efficient automated verification of security protocols. In Proc. VERIF01, Verification Workshop in conjunction with IJCAR, pages 19–33, 2001.Google Scholar
  16. 16.
    J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0., 1997.
  17. 17.
    G. Delzanno and S. Etalle. Proof theory, transformations, and logic programming for debugging security protocols. In A. Pettorossi, editor, Proc. Eleventh International Workshop on Logic Program Synthesis and Transformation-LOP STR 2001, LNCS, pages 76–91. Springer-Verlag, 2002.Google Scholar
  18. 18.
    G. Denker, J. Meseguer, and C. Talcott. Protocol specification and analysis in Maude. In N. Heintze and J. Wing, editors, In Proc. of Workshop on Formal Methods and Security Protocols, 1998.Google Scholar
  19. 19.
    D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    M. Fiore and M. Abadi. Computing symbolic models for verifying cryptographic protocols, 2001.Google Scholar
  21. 21.
    J.C. Herzog F.T. Fabrega and J.D. Guttman. Strand spaces: Why is a security protocol correct? In Proceedings of The 1998 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 1998.Google Scholar
  22. 22.
    A. Huima. Efficient infinite-state analysis of security protocols. In Proc. Workshop Formal Methods and Security Protocols (FLOC 1999), 1999.Google Scholar
  23. 23.
    F. Jacquemard, M. Rusinowitch, and L. Vigneron. Compiling and verifying security protocols. In M. Parigot and A. Vonkorov, editors, Proc. LPAR: International Conference on Logic for Programming and Automated Reasoning, number 1995 in LNCS, pages 131–160. Springer-Verlag, 2000.CrossRefGoogle Scholar
  24. 24.
    J. W. Lloyd. Foundations of Logic Programming. Symbolic Computation-Artificial Intelligence. Springer-Verlag, Berlin, 1987. Second edition.zbMATHGoogle Scholar
  25. 25.
    G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1055, pages 147–166. Springer-Verlag, Berlin Germany, 1996.Google Scholar
  26. 26.
    G. Lowe. Some new attacks upon security protocols. In PCSFW: Proceedings of The 9th Computer Security Foundations Workshop. IEEE Computer Society Press, 1996.Google Scholar
  27. 27.
    G. Lowe. Casper: A compiler for the analysis of security protocols. In Proc. 10th IEEE Computer Security Foundations Workshop (CSFW’ 97), pages 18–30. IEEE, 1997.Google Scholar
  28. 28.
    C. Meadows. Formal verification of cryptographic protocols: A survey. In J. Pieprzyk and R. Safavi-Naini, editors, Advances in Cryptology-ASIACRYPT’ 94, LNCS, pages 133–150. Springer-Verlag, 1995.CrossRefGoogle Scholar
  29. 29.
    C. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113–131, 1996.zbMATHCrossRefGoogle Scholar
  30. 30.
    J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In Proc. 2001 ACM Conference on Computer and Communication Security, pages 166–175. ACM press, 2001.Google Scholar
  31. 31.
    J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol security analysis. IEEE Transactions on Software Engineering, 13(2):274–288, February 1987. Special Issue on Computer Security and Privacy.Google Scholar
  32. 32.
    J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using murø. In Proceedings of the 1997 Conference on Security and Privacy, pages 141–153. IEEE Press, 1997.Google Scholar
  33. 33.
    L. C. Paulson. Mechanized proofs of security protocols: Needham-Schroeder with public keys. Technical Report 413, University of Cambridge, Computer Laboratory, January 1997.Google Scholar
  34. 34.
    L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.Google Scholar
  35. 35.
    A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In IEEE Symposium on Foundations of Secure Systems, 1995.Google Scholar
  36. 36.
    A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1999.Google Scholar
  37. 37.
    M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is np-complete. In S. Schneider, editor, Proc. 14th IEEE Computer Security Foundations Workshop, 2001.Google Scholar
  38. 38.
    P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and analysis of security protocols, 2001.Google Scholar
  39. 39.
    D. X. Song, S. Berezin, and A. Perrig. Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security, 9(1/2):47–74, 2001.Google Scholar
  40. 40.
    T.Y.C. Woo and S. S. Lam. A lesson on authenticated protocol design. Operating Systems Review, 28(3):24–37, 1994.CrossRefGoogle Scholar
  41. 41.
    J. Zhou and D. Gollmann. An efficient non-repudiation protocol. In Proceedings of the 10th Computer Security Foundations Workshop (CSFW’ 97), pages 126–132, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Ricardo Corin
    • 1
  • Sandro Etalle
    • 1
    • 2
  1. 1.Faculty of Computer ScienceUniversity of TwenteEnschedeThe Netherlands
  2. 2.Center for Mathematics and Computer ScienceCWIAmsterdam

Personalised recommendations