Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Engineering Societies in the Agents World

ESAW 2005: Engineering Societies in the Agents World VI pp 106–124Cite as

Security Protocols Verification in Abductive Logic Programming: A Case Study

  • Conference paper

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

Abstract

In this paper we present by a case study an approach to the verification of security protocols based on Abductive Logic Programming.

We start from the perspective of open multi-agent systems, where the internal architecture of the individual system’s components may not be completely specified, but it is important to infer and prove properties about the overall system behaviour. We take a formal approach based on Computational Logic, to address verification at two orthogonal levels: ‘static’ verification of protocol properties (which can guarantee, at design time, that some properties are a logical consequence of the protocol), and ‘dynamic’ verification of compliance of agent communication (which checks, at runtime, that the agents do actually follow the protocol).

In order to explain the approach, we adopt as a running example the well-known Needham-Schroeder protocol. We first show how the protocol can be specified in our previously developed SOCS-SI framework, and then demonstrate the two types of verification.

We also demonstrate the use of the SOCS-SI framework for the static verification of the NetBill e-commerce protocol.

This paper is a revised version of work discussed at the Twentieth Italian Symposium on Computational Logic, CILC 2005, whose informal proceedings are available from the URL: http://www.disp.uniroma2.it/CILC2005/

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Davidsson, P.: Categories of artificial societies. In: Omicini, A., Petta, P., Tolksdorf, R. (eds.) ESAW 2001. LNCS (LNAI), vol. 2203, pp. 1–9. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Guerin, F., Pitt, J.: Proving properties of open agent systems. In: Castelfranchi, C., Lewis Johnson, W. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Part II, Bologna, Italy, pp. 557–558. ACM Press, New York (2002)

    Chapter  Google Scholar 

  3. Societies Of ComputeeS (SOCS): a computational logic model for the description, analysis and verification of global and open societies of heterogeneous computees. IST-2001-32530 (2001), Home Page: http://lia.deis.unibo.it/Research/SOCS/

  4. Alberti, M., Ciampolini, A., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: A social ACL semantics by deontic constraints. In: Mařík, V., Müller, J.P., Pěchouček, M. (eds.) CEEMAS 2003. LNCS (LNAI), vol. 2691, pp. 204–213. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Specification and verification of agent interactions using social integrity constraints. Electronic Notes in Theoretical Computer Science 85 (2003)

    Google Scholar 

  6. The socs protocol repository (2005) Available at: http://lia.deis.unibo.it/research/socs/partners/societies/protocols.html

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

    Article  MATH  Google Scholar 

  8. Lowe, G.: Breaking and fixing the Needham-Shroeder public-key protocol using CSP and FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS (LNAI), vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

    Google Scholar 

  9. Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24, 533–536 (1981)

    Article  Google Scholar 

  10. Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: An Abductive Interpretation for Open Societies. In: Cappelli, A., Turini, F. (eds.) AI*IA 2003. LNCS (LNAI), vol. 2829, pp. 287–299. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Jaffar, J., Maher, M.: Constraint logic programming: a survey. Journal of Logic Programming 19-20, 503–582 (1994)

    Article  MathSciNet  Google Scholar 

  12. Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive Logic Programming. Journal of Logic and Computation 2, 719–770 (1993)

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  14. Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: The SCIFF abductive proof-procedure. In: Bandini, S., Manzoni, S. (eds.) AI*IA 2005. LNCS (LNAI), vol. 3673, pp. 135–147. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Fung, T.H., Kowalski, R.A.: The IFF proof procedure for abductive logic programming. Journal of Logic Programming 33, 151–165 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  16. Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: On the automatic verification of interaction protocols using g-SCIFF. Technical Report DEIS-LIA-04-004, University of Bologna (Italy), LIA Series no. 72 (2005)

    Google Scholar 

  17. Cox, B., Tygar, J., Sirbu, M.: Netbill security and transaction protocol. In: Proceedings of the First USENIX Workshop on Electronic Commerce, New York (1995)

    Google Scholar 

  18. Russo, A., Miller, R., Nuseibeh, B., Kramer, J.: An abductive approach for analysing event-based requirements specifications. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 22–37. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Basin, D.A., Mödersheim, S., Viganò, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Blanchet, B.: Automatic verification of cryptographic protocols: a logic programming approach. In: PPDP 2003: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 1–3. ACM Press, New York (2003)

    Chapter  Google Scholar 

  21. Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52, 102–146 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  22. Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. Armando, A., Compagna, L., Lierler, Y.: Automatic compilation of protocol insecurity problems into logic programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 617–627. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Google Scholar 

  25. Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: CCS 2001, Proceedings of the 8th ACM Conference on Computer and Communications Security, pp. 166–175. ACM press, New York (2001)

    Chapter  Google Scholar 

  26. Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 326–341. Springer, Berlin (2002)

    Chapter  Google Scholar 

  27. Song, D.X.: Athena: a new efficient automatic checker for security protocol analysis. In: CSFW 1999: Proceedings of the 1999 IEEE Computer Security Foundations Workshop, Washington, DC, USA, p. 192. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

  28. Özkohen, A., Yolum, P.: Predicting exceptions in agent-based supply-chains. In: Dikenelli, O., Gleizes, M.-P., Ricci, A. (eds.) ESAW 2005. LNCS, vol. 3963, pp. 168–183. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  29. Yolum, P., Singh, M.: Flexible protocol specification and execution: applying event calculus planning using commitments. In: Castelfranchi, C., Lewis Johnson, W. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Part II, Bologna, Italy, pp. 527–534. ACM Press, New York (2002)

    Chapter  Google Scholar 

  30. Yamaguchi, S., Okayama, K., Miyahara, H.: The design and implementation of an authentication system for the wide area distributed environment. IEICE Transactions on Information and Systems E74, 3902–3909 (1991)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ENDIF, Università di Ferrara, Via Saragat, 1, 44100, Ferrara, Italy

    Marco Alberti, Marco Gavanelli & Evelina Lamma

  2. DEIS, Università di Bologna, Viale Risorgimento, 2, 40126, Bologna, Italy

    Federico Chesani, Paola Mello & Paolo Torroni

Authors
  1. Marco Alberti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Federico Chesani
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marco Gavanelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Evelina Lamma
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Paola Mello
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Paolo Torroni
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Engineering, Ege University, 35100, Bornova, Izmir, Turkey

    Oğuz Dikenelli

  2. IRIT – Paul Sabatier University, 118, Route de Narbonne, 31062, Toulouse, Cedex 9, France

    Marie-Pierre Gleizes

  3. DEIS, Alma Mater Studiorum, Università di Bologna, Italy

    Alessandro Ricci

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P. (2006). Security Protocols Verification in Abductive Logic Programming: A Case Study. In: Dikenelli, O., Gleizes, MP., Ricci, A. (eds) Engineering Societies in the Agents World VI. ESAW 2005. Lecture Notes in Computer Science(), vol 3963. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11759683_7

Download citation

  • DOI: https://doi.org/10.1007/11759683_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-34451-3

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation