Skip to main content
SpringerLink
Log in

Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties

  • Chapter
Foundations of Security Analysis and Design V (FOSAD 2009, FOSAD 2007, FOSAD 2008)

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

Abstract

In this tutorial, we give an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the analysis of cryptographic protocols using functions that obey different equational theories. We show the reader how to use Maude-NPA, and how it works, and also give some of the theoretical background behind the tool.

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 49.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. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  2. Anantharaman, S., Narendran, P., Rusinowitch, M.: Unification modulo CUI plus distributivity axioms. Journal of Automated Reasoning 33(1), 1–28 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  3. 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 

  4. Armando, A., Compagna, L., Lierler, Y.: SATMC: A SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS, vol. 3229, pp. 730–733. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 445–532. Elsevier and MIT Press (2001)

    Google Scholar 

  6. 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 

  7. Baudet, M., Cortier, V., Delaune, S.: YAPA: A generic tool for computing intruder knowledge. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 148–163. Springer, Heidelberg (2009)

    Google Scholar 

  8. Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, pp. 82–96. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  9. Boichut, Y., Héam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proceedings of Automated Verification of Infinite States Systems (AVIS 2004). ENTCS (2004)

    Google Scholar 

  10. Bursuc, S., Comon-Lundh, H.: Protocol security and algebraic properties: decision results for a bounded number of sessions. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 133–147. Springer, Heidelberg (2009)

    Google Scholar 

  11. Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. Inf. Comput. 206(2-4), 352–377 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  12. Ciobâcă, Ş., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 355–370. Springer, Heidelberg (2009)

    Google Scholar 

  13. Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Unification and Narrowing in Maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 380–390. Springer, Heidelberg (2009)

    Google Scholar 

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

    MATH  Google Scholar 

  15. 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 

  16. Contejean, E., Marché, C.: The CiME system: tutorial and user’s manual. Université Paris-Sud, Centre d’Orsay (manuscript)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  18. Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security. Journal of Computer Security, 677–722 (2004)

    Google Scholar 

  19. Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proc. 2nd International Workshop on Security and Rewriting Techniques, SecReT 2007 (2007)

    Google Scholar 

  20. Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoretical Compute Science 367(1-2), 162–202 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  21. Escobar, S., Meadows, C., Meseguer, J.: Equational cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proc. 1st International Workshop on Security and Rewriting Techniques (SecReT 2006). ENTCS, vol. 171(4), pp. 23–36. Elsevier, Amsterdam (2007)

    Google Scholar 

  22. Escobar, S., Meadows, C., Meseguer, J.: State space reduction in the Maude-NRL Protocol Analyzer. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 548–562. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA, version 1.0. University of Illinois at Urbana-Champaign (March 2009), http://maude.cs.uiuc.edu/tools/Maude-NPA

  24. Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Technical Report UIUCDCS-R-2007-2910, Dept. of Computer Science, University of Illinois at Urbana-Champaign (October 2007)

    Google Scholar 

  26. Escobar, S., Meseguer, J., Sasse, R.: Effectively checking the finite variant property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 79–93. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. In: Rossu, G. (ed.) Proc. 7th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2008) (to appear)

    Google Scholar 

  28. Fabrega, F.J.T., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security 7, 191–230 (1999)

    Article  Google Scholar 

  29. Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)

    Google Scholar 

  30. Millen, S.F.J.K., Clark, S.C.: The interrogator: Protocol secuity analysis. IEEE Transactions on Software Engineering, 274–288 (February 1987)

    Google Scholar 

  31. Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361–373. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

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

    Google Scholar 

  33. Lynch, C., Meadows, C.: On the relative soundness of the free algebra model for public key encryption. In: Workshop on Issues in Theory of Security 2004 (2004)

    Google Scholar 

  34. Lynch, C., Meadows, C.: Sound Approximations to Diffie-Hellman Using Rewrite Rules. In: López, J., Qing, S., Okamoto, E. (eds.) ICICS 2004. LNCS, vol. 3269, pp. 262–277. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  35. Meadows, C.: Language generation and verification in the NRL protocol analyzer. In: Ninth IEEE Computer Security Foundations Workshop, Dromquinna Manor, Kenmare, County Kerry, Ireland, March 10-12, pp. 48–61. IEEE Computer Society, Los Alamitos (1996)

    Chapter  Google Scholar 

  36. Meadows, C.: The NRL protocol analyzer: An overview. Journal of logic programming 26(2), 113–131 (1996)

    Article  MATH  Google Scholar 

  37. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  38. Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  39. Millen, J.: On the freedom of decryption. Information Processing Letters 86(3) (2003)

    Google Scholar 

  40. Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: IEEE Symposium on Security and Privacy. IEEE Computer Society, Los Alamitos (1997)

    Google Scholar 

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

    Article  Google Scholar 

  42. Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. In: 14th IEEE Computer Security Foundations Workshop, pp. 174–190 (2001)

    Google Scholar 

  43. Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol. a cautionary tale. Inf. Process. Lett. 65(1), 7–10 (1998)

    Article  MATH  Google Scholar 

  44. Santiago, S., Talcott, C., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Technical Report DSIC-II/02/09, Universidad Politécnica de Valencia (June 2009)

    Google Scholar 

  45. Shmatikov, V., Stern, U.: Efficient finite-state analysis for large security protocols. In: 11th Computer Security Foundations Workshop — CSFW-11. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  46. Stubblebine, S., Meadows, C.: Formal characterization and automated analysis of known-pair and chosen-text attacks. IEEE Journal on Selected Areas in Communications 18(4), 571–581 (2000)

    Article  Google Scholar 

  47. TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  48. Thati, P., Meseguer, J.: Symbolic reachability analysis using narrowing and its application verification of cryptographic protocols. J. Higher-Order and Symbolic Computation 20(1-2), 123–160 (2007)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Politécnica de Valencia, Spain

    Santiago Escobar

  2. Naval Research Laboratory, Washington, DC, USA

    Catherine Meadows

  3. University of Illinois at Urbana-Champaign, USA

    José Meseguer

Authors
  1. Santiago Escobar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Catherine Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Istituto di Scienze e Tecnologie dell’Informazione, Università degli Studi di Urbino “Carlo Bo”, Piazza della Repubblica 13, 61029, Urbino, Italy

    Alessandro Aldini

  2. IMDEA Software, UPM Facultad de Informatica, Campus Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  3. Dipartimento di Scienze dell’Informazione, Università degli Studi di Bologna, Mura Anteo Zamboni 7, 40127, Bologna, Italy

    Roberto Gorrieri

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Escobar, S., Meadows, C., Meseguer, J. (2009). Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds) Foundations of Security Analysis and Design V. FOSAD FOSAD FOSAD 2009 2007 2008. Lecture Notes in Computer Science, vol 5705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03829-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03829-7_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03828-0

  • Online ISBN: 978-3-642-03829-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation