Skip to main content
SpringerLink
Log in

AnBx - Security Protocols Design and Verification

  • Conference paper
Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS 2010)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 6186))

Abstract

Designing distributed protocols is challenging, as it requires actions at very different levels: from the choice of network-level mechanisms to protect the exchange of sensitive data, to the definition of structured interaction patterns to convey application-specific guarantees. Current security infrastructures provide very limited support for the specification of such guarantees. As a consequence, the high-level security properties of a protocol typically must often be hard-coded explicitly, in terms of low-level cryptographic notions and devices which clutter the design and undermine its scalability and robustness.

To counter these problems, we propose an extended Alice & Bob notation for protocol narrations (AnBx) to be employed for a purely declarative modelling of distributed protocols. These abstractions provide a compact specification of the high-level security guarantees they convey, and help shield the design from the details of the underlying cryptographic infrastructure. We discuss an implementation of the abstractions based on a translation from the AnBx notation to the AnB language supported by the OFMC [1,2] verification tool. We show the practical effectiveness of our approach by revisiting the iKP e-payment protocols, and showing that the security goals achieved by our declarative specification outperform those offered by the original protocols.

Work partially supported by MIUR Projects SOFT “Security Oriented Formal Techniques” and IPODS “Interacting Processes in Open-ended Distributed Systems”.

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 49.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 64.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. Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security 4(3), 181–208 (2005)

    Article  Google Scholar 

  2. Mödersheim, S., Viganò, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Foundations of Security Analysis and Design V, p. 194. Springer, Heidelberg (2009)

    Google Scholar 

  3. Dierks, T., Allen, C.: Rfc2246: The TLS protocol version 1.0. Internet RFCs (1999)

    Google Scholar 

  4. Abadi, M., Fournet, C., Gonthier, G.: Authentication primitives and their compilation. In: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 302–315. ACM, New York (2000)

    Google Scholar 

  5. Bugliesi, M., Focardi, R.: Language Based Secure Communication. In: IEEE 21st Computer Security Foundations Symposium, CSF 2008, pp. 3–16 (2008)

    Google Scholar 

  6. Adao, P., Fournet, C.: Cryptographically Sound Implementations for Communicating Processes. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 83–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Corin, R., Dénielou, P.M., Fournet, C., Bhargavan, K., Leifer, J.J.: Secure implementations of typed session abstractions. In: CSF 2007, pp. 170–186. IEEE, Los Alamitos (2007)

    Google Scholar 

  8. Bhargavan, K., Corin, R., Dénielou, P.M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF 2009 (2009)

    Google Scholar 

  9. Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P., Héam, P., Kouchnarenko, O., Mantovani, J., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Bellare, M., Garay, J., Hauser, R., Herzberg, A., Krawczyk, H., Steiner, M., Tsudik, G., Waidner, M.: iKP A Family of Secure Electronic Payment Protocols. In: Proceedings of the 1st USENIX Workshop on Electronic Commerce (1995)

    Google Scholar 

  11. Bellare, M., Garay, J., Hauser, R., Herzberg, A., Krawczyk, H., Steiner, M., Tsudik, G., Van Herreweghen, E., Waidner, M.: Design, implementation, and deployment of the iKP secure electronic payment system. IEEE Journal on selected areas in communications 18(4), 611–627 (2000)

    Article  Google Scholar 

  12. Maurer, U., Schmid, P.: A calculus for secure channel establishment in open networks. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, p. 175. Springer, Heidelberg (1994)

    Google Scholar 

  13. van Doorn, L., Abadi, M., Burrows, M., Wobber, E.: Secure network objects. In: Secure Internet Programming, pp. 395–412 (1999)

    Google Scholar 

  14. Kelsey, J., Schneier, B., Wagner, D.: Protocol interactions and the chosen protocol attack. LNCS, pp. 91–104. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  15. Lowe, G.: A hierarchy of authentication specifications, pp. 31–43. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  16. Cramer, R., Shoup, V.: Design and analysis of practical public-key encryption schemes secure against adaptive chosen ciphertext attack. SIAM Journal on Computing(Print) 33(1), 167–226 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. In: Proceedings of 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 122–136 (1994)

    Google Scholar 

  18. Mödersheim, S.: Algebraic properties in alice and bob notation. In: International Conference on Availability, Reliability and Security, pp. 433–440 (2009)

    Google Scholar 

  19. Backes, M., Hritcu, C., Maffei, M.: Type-checking zero-knowledge. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conference on Computer and Communications Security, pp. 357–370. ACM, New York (2008)

    Google Scholar 

  20. Corin, R., Deniélou, P.M., Fournet, C., Bhargavan, K., Leifer, J.J.: A secure compiler for session abstractions. Journal of Computer Security 16(5), 573–636 (2008)

    Article  Google Scholar 

  21. Bella, G., Massacci, F., Paulson, L.: An overview of the verification of SET. International Journal of Information Security 4(1), 17–28 (2005)

    Article  Google Scholar 

  22. Visa: Visa 3-D Secure Specifications. Technical report (2002)

    Google Scholar 

  23. O’Mahony, D., Peirce, M., Tewari, H.: Electronic payment systems for e-commerce. Artech House Publishers (2001)

    Google Scholar 

  24. Ogata, K., Futatsugi, K.: Formal analysis of the iKP electronic payment protocols. LNCS, pp. 441–460. Springer, Heidelberg (2003)

    Google Scholar 

  25. Abadi, M., Fournet, C., Gonthier, G.: Secure implementation of channel abstractions. Information and computation(Print) 174(1), 37–83 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  26. Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427–476 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  27. Bugliesi, M., Giunti, M.: Secure implementations of typed channel abstractions. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 251–262. ACM, New York (2007)

    Google Scholar 

  28. Guttman, J.: Security protocol design via authentication tests. In: Proceedings of 15th IEEE Computer Security Foundations Workshop. IEEE Computer, Los Alamitos (2002)

    Google Scholar 

  29. Guttman, J., Herzog, J., Ramsdell, J., Sniffen, B.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116–145. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università Ca’ Foscari Venezia, Italy

    Michele Bugliesi & Paolo Modesti

Authors
  1. Michele Bugliesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paolo Modesti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DIST Dipartimento di Informatica, Sistematica e Telematica, Università di Genova, Via le Causa 13, 16145, Genova, Italy

    Alessandro Armando

  2. Computing Laboratory, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Gavin Lowe

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bugliesi, M., Modesti, P. (2010). AnBx - Security Protocols Design and Verification. In: Armando, A., Lowe, G. (eds) Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security. ARSPA-WITS 2010. Lecture Notes in Computer Science, vol 6186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16074-5_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16074-5_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16073-8

  • Online ISBN: 978-3-642-16074-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation