Skip to main content
SpringerLink
Log in

Alice and Bob Meet Equational Theories

  • Chapter
  • First Online:
Logic, Rewriting, and Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9200))

Abstract

Cryptographic protocols are the backbone of secure communication over open networks and their correctness is therefore crucial. Tool-supported formal analysis of cryptographic protocol designs increases our confidence that these protocols achieve their intended security guarantees. We propose a method to automatically translate text-book style Alice&Bob protocol specifications into a format amenable to formal verification using existing tools. Our translation supports specification modulo equational theories, which enables the faithful representation of algebraic properties of a large class of cryptographic operators.

Dedicated to Jose Meseguer on his 65th Birthday.

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 EPUB and 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

References

  1. Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: 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 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  3. Basin, D., Keller, M., Radomirović, S., Sasse, R.: Alice&Bob protocols. http://www.infsec.ethz.ch/research/software/anb.html

  4. Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817–846 (2013)

    Article  MATH  Google Scholar 

  5. Basin, D., Cremers, C., Kim, T.H.-J., Perrig, A., Sasse, R., Szalachowski, P.: ARPKI: attack resilient public-key infrastructure. In: Ahn, G.-J., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 3–7 November 2014, Scottsdale, AZ, USA, pp. 382–393. ACM (2014)

    Google Scholar 

  6. Blanchet, B.: Proverif automatic cryptographic protocol verifier user manual. CNRS, Departement d’Informatique, Ecole Normale Superieure, Paris (2005)

    Google Scholar 

  7. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop (CSFW), pp. 82–96. IEEE (2001)

    Google Scholar 

  8. Caleiro, C., Viganò, L., Basin, D.: Deconstructing Alice and Bob. Electron. Notes Theoret. Comput. Sci. 135(1), 3–22 (2005). Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2005

    Article  MATH  Google Scholar 

  9. Caleiro, C., Viganò, L., Basin, D.: On the semantics of Alice&Bob specifications of security protocols. Theor. Comput. Sci. 367(1–2), 88–122 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Chevalier, Y., Rusinowitch, M.: Compiling and securing cryptographic protocols. Inf. Process. Lett. 110(3), 116–122 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  11. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  12. Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Cremers, C.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: ACM Conference on Computer and Communications Security (CCS), pp. 119–128. ACM (2008)

    Google Scholar 

  14. Denker, G., Millen, J.K.: CAPSL intermediate language. In: Proceedings of FMSP 1999 (1999). http://www.csl.sri.com/users/millen/capsl/

  15. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cyptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Logic Algebraic Program. 81(7–8), 898–928 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  17. Fabrega, F.J.T., Herzog, J., Guttman, J.: Strand spaces: what makes a security protocol correct? J. Comput. Secur. 7, 191–230 (1999)

    Article  Google Scholar 

  18. Keller, M.: Converting Alice and Bob protocol specifications to Tamarin. Bachelor’s thesis, ETH Zurich (2014). http://www.infsec.ethz.ch/research/software/anb.html

  19. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS, pp. 147–166 (1996)

    Google Scholar 

  20. Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Workshop on Computer Security Foundations, CSFW 1997, pp. 31–43, Washington, DC, USA. IEEE Computer Society (1997)

    Google Scholar 

  21. Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1), 53–84 (1998)

    Article  Google Scholar 

  22. McCarthy, J., Krishnamurthi, S.: Cryptographic protocol explication and end-point projection. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 533–547. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Meier, S.: GitHub repository of scyther-proof Project. https://github.com/meiersi/scyther-proof

  24. Meier, S., Cremers, C., Basin, D.: Strong invariants for the efficient construction of machine-checked protocol security proofs. In: CSF, pp. 231–245. IEEE Computer Society (2010)

    Google Scholar 

  25. Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Mödersheim, S.: Algebraic properties in Alice and Bob notation. In: ARES, pp. 433–440. IEEE Computer Society (2009)

    Google Scholar 

  27. Neuman, B.C., Ts’o, T.: Kerberos: an authentication service for computer networks. Communications 32(9), 33–38 (1994)

    Google Scholar 

  28. Schmidt, B.: Formal analysis of key exchange protocols and physical protocols. Ph.D. dissertation, ETH Zurich (2012)

    Google Scholar 

  29. Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE (2012)

    Google Scholar 

  30. Schmidt, B., Sasse, R., Cremers, C., Basin, D.: Automated verification of group key agreement protocols. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, 18–21 May 2014, Berkeley, CA, USA, pp. 179–194. IEEE Computer Society (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Institute of Information Security, ETH Zurich, Zurich, Switzerland

    David Basin, Michel Keller, Saša Radomirović & Ralf Sasse

Authors
  1. David Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michel Keller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Saša Radomirović
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ralf Sasse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ralf Sasse .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Basin, D., Keller, M., Radomirović, S., Sasse, R. (2015). Alice and Bob Meet Equational Theories. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23165-5_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23164-8

  • Online ISBN: 978-3-319-23165-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation