Skip to main content
SpringerLink
Log in

Planning Attacks to Security Protocols: Case Studies in Logic Programming

  • Chapter
  • First Online:
Book cover Computational Logic: Logic Programming and Beyond

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2407))

Abstract

Formal verification of security protocols has become a key issue in computer security. Yet, it has proven to be a hard task often error prone and discouraging for non-experts in formal methods.

In this paper we show how security protocols can be specified and verified efficiently and effectively by embedding reasoning about actions into a logic programming language.

In a nutshell, we view a protocol trace as a plan to achieve a goal, so that protocol attacks are plans achieving goals that correspond to security violations. Building on results from logic programming and planning, we map the existence of an attack to a protocol into the existence of a model for the protocol specification that satisfies the specification of an attack. To streamline such way of modeling security protocols, we use a description language \( \mathcal{A}\mathcal{L}_{SP} \) which makes it possible to describe protocols with declarative ease and to search for attacks by relying on efficient model finders (e.g. the smodels systems by Niemela and his group). This paper shows how to use \( \mathcal{A}\mathcal{L}_{SP} \) for modeling two significant case studies in protocol verification: the classical Needham-Schroeder public-key protocol, and Aziz-Diffie Key agreement protocol for mobile communication.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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 R. M. Needham. Prudent engineering practice for cryptographic protocols. Research Report SRC-125, Digital System Research Center, 1994.

    Google Scholar 

  2. M. Abadi and R. M. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, January 1996. Preliminary version in [1].

    Google Scholar 

  3. K. Apt. Logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers (North-Holland), Amsterdam, 1990.

    Google Scholar 

  4. A. Aziz and W. Diffie. Privacy and authentication for wireless local area networks. IEEE Personal Communications, 1(1):25–31, 1994.

    Google Scholar 

  5. G. Bella and L. C. Paulson. Kerberos version IV: Inductive analysis of the secrecy goals. In Proceedings of the Fifth European Symposium on Research in Computer Security (ESORICS’98), volume 1485 of Lecture Notes in Computer Science, pages 361–375. Springer-Verlag, 1998.

    Google Scholar 

  6. S. Brackin, C. Meadows, and J. Millen. CAPSL interface for the NRL Protocol Analyzer. In IEEE Symposium on Application-Specific Systems and Software Engineering Technology (ASSET-99). IEEE Computer Society Press, 1999. A complete specification of the Clark-Jacob Library [10] is available at http://www.cs.sri.com/~millen/capsl/.

  7. M. Burrows, M. Abadi, and R. Needham. A logic for authentication. ACM Trans. Comput. Syst., 8(1):18–36, 1990.

    Article  Google Scholar 

  8. L. Carlucci Aiello and F. Massacci. An executable specification language for planning attacks to security protocols. In P. Syverson, editor, IEEE Computer Security Foundation Workshop, pages 88–103. IEEE Computer Society Press, 2000.

    Google Scholar 

  9. L. Carlucci Aiello and F. Massacci. Verifying security protocols as planning in logic programming. ACM Transactions on Computational Logic, Vol. 2, No. 4, pages 542–580, 2001.

    Article  MathSciNet  Google Scholar 

  10. J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. Technical report, University of York, Department of Computer Science, November 1997. Available on the web at http://www-users.cs.york.ac.uk/~jac/.

  11. M. Denecker, L. Missiaen, and M. Bruynooghe. Temporal Reasoning with Abductive Event Calculus. In Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI’92), 1992.

    Google Scholar 

  12. Y. Dimopoulos, B. Nebel, and J. Koehler. Encoding planning problems in nonmonotonic logic programs. In S. Steel and R. Alami, editors, Proceedings of the Fourth European Conference on Planning (ECP’97), volume 1348 of Lecture Notes in Artificial Intelligence, pages 169–181. Springer-Verlag, 1997.

    Google Scholar 

  13. D. Dolev and A. Yao. On security of public key protocols. IEEE Transactions on Information Theory, IT-30:198–208, 1983.

    Article  MathSciNet  Google Scholar 

  14. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In R. Kowalski and K. Bowen, editors, Proceedings of the Fifth International Conference on Logic Programming (ICLP’88), pages 1070–1080. MIT-Press, 1988.

    Google Scholar 

  15. M. Gelfond and V. Lifschitz. Representing Actions and Change as Logic Programs. Journal of Logic Programming, 17:301–322, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  16. D. Gollmann. What do we mean by entity authentication? In Proceedings of the Fifteenth IEEE Symposium on Security and Privacy (SSP’96), pages 46–54. IEEE Computer Society Press, 1996.

    Google Scholar 

  17. H. Kautz and B. Selman. Planning as satisfiability. In Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI’92), pages 359–363. John Wiley & Sons, 1992.

    Google Scholar 

  18. L. Lorenzon. Un traduttore da CASPER ad \( \mathcal{A}\mathcal{L}_{SP} \) . Master’s thesis, Facoltà di Ingegneria, Univ. di Roma I “La Sapienza”, March 2000. In Italian.

    Google Scholar 

  19. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In T. Margaria and S. B., editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of Lecture Notes in Computer Science, pages 147–166. Springer-Verlag, 1996.

    Google Scholar 

  20. G. Lowe. Some new attacks upon security protocols. In Proceedings of the Ninth IEEE Computer Security Foundations Workshop (CSFW’96), pages 162–169. IEEE Computer Society Press, 1996.

    Google Scholar 

  21. G. Lowe. A hierarchy of authentication specifications. In Proceedings of the Tenth IEEE Computer Security Foundations Workshop (CSFW’96), pages 31–43. IEEE Computer Society Press, 1997.

    Google Scholar 

  22. G. Lowe. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 6(18–30):53–84, 1998.

    Google Scholar 

  23. Mastercard & VISA. SET Secure Electronic Transaction Specification: Business Description, May 1997. Available electronically at http://www.setco.org/set_specifications.html.

  24. C. Meadows. The NRL Protocol Analyzer: An overview. Journal of Logic Programming, 26(2):113–131, 1994.

    Article  Google Scholar 

  25. C. Meadows. Open issues in formal methods for cryptographic protocol analy sis. In Proceedings of DISCEX 2000, pages 237–250. IEEE Computer Society Press, 2000.

    Google Scholar 

  26. C. A. Meadows. Formal verification of cryptographic protocols: A survey. In Advances in Cryptology-Asiacrypt’94, volume 917 of Lecture Notes in Computer Science, pages 133–150. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  27. C. A. Meadows. Analyzing the needham-schroeder publik key protocol: A comparison of two approaches. In E. Bertino, H. Kurth, G. Martella, and E. Montolivo, editors, Proceedings of the Fourth European Symposium on Research in Computer Security (ESORICS’96), volume 1146 of Lecture Notes in Computer Science, pages 351–364. Springer-Verlag, 1996.

    Google Scholar 

  28. J. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murphi. In Proceedings of the Sixteenth IEEE Symposium on Security and Privacy (SSP’97), pages 141–151. IEEE Computer Society Press, 1997.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  30. I. Niemelä. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence, 25(3–4):241–273, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  31. I. Niemelä and P. Simmons. Smodels-an implementation of Stable Model and Well-founded Semantics for Normal Logic Programs. In Proceedings of the Fourth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’97), volume 1265 of Lecture Notes in Artificial Intelligence, pages 420–429. Springer-Verlag, 1997.

    Google Scholar 

  32. D. O’Mahony, M. Peirce, and H. Tewari. Electronic payment systems. The Artech House computer science library. Artech House, 1997.

    Google Scholar 

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

    Google Scholar 

  34. L. C. Paulson. Inductive analysis of the internet protocol TLS. ACM Transactions on Information and System Security, 2(3):332–351, 1999.

    Article  Google Scholar 

  35. P. Ryan and S. Schneider. An attack on a recursive authentication protocol. a cautionary tale. Information Processing Letters, 65(15):7–16, 1998.

    Article  Google Scholar 

  36. B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C John Wiley & Sons, 1994.

    Google Scholar 

  37. V. S. Subrahmanian and C. Zaniolo. Relating Stable Models and AI Planning Domains. In Proceedings of the International Conference on Logic Programming (ICLP-95), 1995.

    Google Scholar 

  38. P. Syverson and C. Meadows. A formal language for cryptographic protocol requirement. Designs, Codes and Cryptography, 7:27–59, 1996.

    MATH  MathSciNet  Google Scholar 

  39. D. S. Weld. Recent Advances in AI Planning. Artificial Intelligence Magazine, (Summer 1999):93–123, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. di Informatica e Sistemistica, Univ. Roma “La Sapienza”, Italy

    Luigia Carlucci Aiello

  2. Dip. di Ingegneria dell’Informazione, Univ. Siena, Italy

    Fabio Massacci

Authors
  1. Luigia Carlucci Aiello
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabio Massacci
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Cyprus, 75 Kallipoleos St., 1678, Nicosia, Cyprus

    Antonis C. Kakas

  2. Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen’s Gate, London, SW7 2BZ, UK

    Fariba Sadri

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Aiello, L.C., Massacci, F. (2002). Planning Attacks to Security Protocols: Case Studies in Logic Programming. In: Kakas, A.C., Sadri, F. (eds) Computational Logic: Logic Programming and Beyond. Lecture Notes in Computer Science(), vol 2407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45628-7_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-45628-7_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43959-2

  • Online ISBN: 978-3-540-45628-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation