Skip to main content
SpringerLink
Log in

Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols

  • Conference paper
  • First Online:
Logic Based Program Synthesis and Transformation (LOPSTR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2372))

Abstract

In this paper we define a sequent calculus to formally specify, simulate, debug and verify security protocols. In our sequents we distinguish between the current knowledge of principals and the current global state of the session. Hereby, we can describe the operational semantics of principals and of an intruder in a simple and modular way. Furthermore, using proof theoretic tools like the analysis of permutability of rules, we are able to find efficient proof strategies that we prove complete for special classes of security protocols including Needham-Schroeder. Based on the results of this preliminary analysis, we have implemented a Prolog meta-interpreter which allows for rapid prototyping and for checking safety properties of security protocols, and we have applied it for finding error traces and proving correctness of practical examples.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In Proc. POPL 2002, pages 33–44, 2002.

    Google Scholar 

  2. L. C. Aiello and F. Massacci. Verifying security protocols as planning in logic programming. Trans. on Computational Logic, 2001.

    Google Scholar 

  3. D. Basin. Lazy infinite-state analysis of security protocols. Secure Networking — CQRE [Secure]’ 99”, LNCS 1740, pages 30–42, 1999.

    Chapter  Google Scholar 

  4. G. Bella and L. C. Paulson. Kerberos version IV: Inductive analysis of the secrecy goals. In Proc.5th Symp. on Research in Computer Security, LNCS 1485, pages 361–375, 1998.

    Google Scholar 

  5. B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proc. CSFW’01, 2001.

    Google Scholar 

  6. M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Trans, on Computer Systems, 8(1):18–36, 1990.

    Article  Google Scholar 

  7. I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In Proc. CSFW’ 99, pages 55–69, 1999.

    Google Scholar 

  8. I. Cervesato, N. Durgin, J. Mitchell, Lincoln, and A. Scedrov. Relating strands and multiset rewriting for security protocol analysis. In Proc. CSFW’ 00, pages 35–51, 2000.

    Google Scholar 

  9. Y. Chevalier, F. Jacquemard, M. Rusinowitch, M. Turuani, and L. Vigneron. CAS-RUL web site. http://www.loria.fr/equipes/protheo/SOFTWARES/CASRUL/.

  10. Y. Chevalier and L. Vigneron. A tool for lazy verification of security protocols. In Proc. Int’l Conf. Automated Software Engineering, 2001.

    Google Scholar 

  11. Y. Chevalier and L. Vigneron. Towards efficient automated verification of security protocols. In Proc. VERIF’ 01, 2001.

    Google Scholar 

  12. G. Delzanno. Specifying and debugging security protocols via hereditary harrop formulas and lambda prolog. In Proc. FLOPS’ 01, pages 123–137, 2001.

    Google Scholar 

  13. D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Trans. on Information Theory, 29(2):198–208, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  14. N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. FMSP’99 (FLOC’ 99), 1999.

    Google Scholar 

  15. A. Huima. Efficient infinite-state analysis of security protocols. In Proc. FMSP’ 99 (FLOC’ 99), 1999.

    Google Scholar 

  16. F. Jacquemard, M. Rusinowitch, and L. Vigneron. Compiling and verifying security protocols. In Proc. LPAR 2000, LNCS 1995, pages 131–160, 2000.

    Google Scholar 

  17. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, (17):93–102, 1996.

    Google Scholar 

  18. G. Lowe. Casper: A compiler for the analysis of security protocols. In Proc.CSFW’ 97, pages 18–30, 1997.

    Google Scholar 

  19. G. Lowe. Towards a completeness result for model checking of security protocols. J. of Computer Security, 7(2–-3):89–146, 1998.

    Google Scholar 

  20. C. Meadows. Formal verification of cryptographic protocols: A survey. In Proc. ASIACRYPT’ 94, pages 133–150, 1995.

    Google Scholar 

  21. C. Meadows. The NRL protocol analyzer: An overview. J. of Logic Programming, 26(2):113–131, 1996.

    Article  MATH  Google Scholar 

  22. J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In Proc. 2001 ACM Conf. on Computer and Communication Security, pages 166–175, 2001.

    Google Scholar 

  23. J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol security analysis. IEEE Trans. on Software Engineering, 13(2):274–288, 1987.

    Article  Google Scholar 

  24. J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using murφ. In Proc. Conf. on Security and Privacy, pages 141–153, 1997.

    Google Scholar 

  25. R. M. Needham and M. D. Schroeder. Using encryption for authentication in large networks of computers. Comm. of the ACM, 21(12):993–999, 1978.

    Article  MATH  Google Scholar 

  26. L. C. Paulson. Mechanized proofs of security protocols: Needham-Schroeder with public keys. T.R. 413, Univ. of Cambridge, Computer Laboratory, January 1997.

    Google Scholar 

  27. L. C. Paulson. The inductive approach to verifying cryptographic protocols. J. of Computer Security, 6:85–128, 1998.

    Google Scholar 

  28. A. W. Roscoe. Modelling and verifying key-exchange protocols using csp and fdr. In IEEE Symp. on Foundations of Secure Systems, 1995.

    Google Scholar 

  29. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1999.

    Google Scholar 

  30. M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is np-complete. In Proc. CSFW’ 01, 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova, via Dodecaneso 35, 16146, Italy

    Giorgio Delzanno

  2. CWI, Amsterdam and Faculty of Computer Science, University of Twente, P.O.Box 217, 7500AE, Enschede, The Netherlands

    Sandro Etalle

Authors
  1. Giorgio Delzanno
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sandro Etalle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Rome Tor Vergata, Via del Politecnico 1, 00133, Rome, Italy

    Alberto Pettorossi

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Delzanno, G., Etalle, S. (2002). Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols. In: Pettorossi, A. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2001. Lecture Notes in Computer Science, vol 2372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45607-4_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-45607-4_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43915-8

  • Online ISBN: 978-3-540-45607-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation