Skip to main content
SpringerLink
Log in

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method

  • Chapter
  • First Online:
Foundations of Security, Protocols, and Equational Reasoning

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

Abstract

This work proposes canonical constrained narrowing, a new symbolic reachability analysis technique applicable to topmost rewrite theories where the equational theory has the finite variant property. Our experiments suggest that canonical constrained narrowing is more efficient than both standard narrowing and the previously studied contextual narrowing. These results are relevant not only for Maude-NPA, but also for symbolically analyzing many other concurrent systems specified by means of rewrite theories.

This work has been partially supported by the EU (FEDER) and the Spanish MINECO under grant TIN 2015-69175-C4-1-R, by Generalitat Valenciana under grants PROMETEOII/2015/013 and PROMETEO/2019/098, by the US Air Force Office of Scientific Research under award number FA9550-17-1-0286, and by NRL under contract number N00173-17-1-G002.

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

Notes

  1. 1.

    Note that the two first equations are not AC-coherent, but adding the last equation is sufficient to recover that property (see [44]).

  2. 2.

    Available at http://personales.upv.es/sanesro/canonical-narrowing.

  3. 3.

    Available at https://github.com/maude-team/full-maude/.

References

  1. 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, 21–25 August 2017. IEEE Computer Society (2017)

    Google Scholar 

  2. Armando, A., 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). https://doi.org/10.1007/11513988_27

    Chapter  Google Scholar 

  3. Ateniese, G., Steiner, M., Tsudik, G.: Authenticated group key agreement and friends. In: ACM Conference on Computer and Communications Security, pp. 17–26 (1998)

    Google Scholar 

  4. Basin, D., Cremers, C., Meadows, C.: Model checking security protocols. Handbook of Model Checking, pp. 727–762. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_22

    Chapter  MATH  Google Scholar 

  5. Basin, D.A., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15–19 October 2018, pp. 1383–1396. ACM (2018)

    Google Scholar 

  6. Blanchet, B.: Automatic verification of security protocols in the symbolic model: the verifier ProVerif. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012–2013. LNCS, vol. 8604, pp. 54–87. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10082-1_3

    Chapter  Google Scholar 

  7. Bull, J.: The authentication protocol. APM Report (1997)

    Google Scholar 

  8. Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1

    Book  MATH  Google Scholar 

  9. Clavel, M., et al.: Maude Manual (Version 2.7.1). SRI International - University of Illinois at Urbana-Champaign, July 2016

    Google Scholar 

  10. 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). https://doi.org/10.1007/978-3-540-32033-3_22

    Chapter  Google Scholar 

  11. Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_38

    Chapter  Google Scholar 

  12. Delaune, S., Hirschi, L.: A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J. Log. Algebr. Meth. Program. 87, 127–144 (2017)

    Article  MathSciNet  Google Scholar 

  13. Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9–12 July 2018, pp. 359–373. IEEE Computer Society (2018)

    Google Scholar 

  14. Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Talcott, C.: Built-in variant generation and unification, and their applications in Maude 2.7. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 183–192. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_13

    Chapter  Google Scholar 

  15. Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: Associative unification and symbolic reasoning modulo associativity in Maude. In: Rusu [39], pp. 98–114 (2018)

    Google Scholar 

  16. Erbatur, S., et al.: Effective symbolic protocol analysis via equational irreducibility conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73–90. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33167-1_5

    Chapter  Google Scholar 

  17. Erbatur, S., et al.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 231–248. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_16

    Chapter  Google Scholar 

  18. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA (Version 3.1.1), April 2018. http://maude.cs.uiuc.edu/tools/Maude-NPA

  19. Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Sequential protocol composition in Maude-NPA. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 303–318. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15497-3_19

    Chapter  Google Scholar 

  20. Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: A rewriting-based forwards semantics for Maude-NPA. In: Proceedings of the 2014 Symposium and Bootcamp on the Science of Security, HotSoS 2014. ACM (2014)

    Google Scholar 

  21. Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157–186 (2014)

    Article  MathSciNet  Google Scholar 

  22. Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Symbolic protocol analysis with disequality constraints modulo equational theories. In: Programming Languages with Applications to Biology and Security, pp. 238–261 (2015)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

  25. González-Burgueño, A., Aparicio-Sánchez, D., Escobar, S., Meadows, C.A., Meseguer, J., Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16–21 November 2018, EPiC Series in Computing, vol. 57, pp. 400–417. EasyChair (2018)

    Google Scholar 

  26. González-Burgueño, A., Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: Analysis of the IBM CCA security API protocols in Maude-NPA. In: Chen, L., Mitchell, C. (eds.) SSR 2014. LNCS, vol. 8893, pp. 111–130. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-14054-4_8

    Chapter  Google Scholar 

  27. González-Burgueño, A., Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: Analysis of the PKCS#11 API using the Maude-NPA tool. In: Chen, L., Matsuo, S. (eds.) SSR 2015. LNCS, vol. 9497, pp. 86–106. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27152-1_5

    Chapter  Google Scholar 

  28. Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)

    Article  MathSciNet  Google Scholar 

  29. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61042-1_43

    Chapter  Google Scholar 

  30. Meadows, C.: The NRL protocol analyzer: an overview. J. Log. Program. 26(2), 113–131 (1996)

    Article  Google Scholar 

  31. 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). https://doi.org/10.1007/978-3-642-39799-8_48

    Chapter  Google Scholar 

  32. Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

    Article  Google Scholar 

  33. Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-64299-4_26

    Chapter  Google Scholar 

  34. Meseguer, J.: Generalized rewrite theories and coherence completion. In: Rusu [39], pp. 164–183 (2018)

    Google Scholar 

  35. Meseguer, J.: Generalized rewrite theories, coherence completion and symbolic methods. Technical report, Computer Science Department, University of Illinois, December 2018

    Google Scholar 

  36. Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018)

    Article  Google Scholar 

  37. Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High.-Order Symb. Comput. 20(1–2), 123–160 (2007)

    Article  Google Scholar 

  38. Pereira, O., Quisquater, J.-J.: On the impossibility of building secure cliques-type authenticated group key agreement protocols. J. Comput. Secur. 14(2), 197–246 (2006)

    Article  Google Scholar 

  39. Rusu, V. (ed.): WRLA 2018. LNCS, vol. 11152. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99840-4

    Book  MATH  Google Scholar 

  40. 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  Google Scholar 

  41. Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using Maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162–177. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11851-2_11

    Chapter  MATH  Google Scholar 

  42. Sasse, R., Escobar, S., Meadows, C., Meseguer, J.: Protocol analysis modulo combination of theories: a case study in Maude-NPA. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) STM 2010. LNCS, vol. 6710, pp. 163–178. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22444-7_11

    Chapter  Google Scholar 

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

    Google Scholar 

  44. Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285(2), 487–517 (2002)

    Article  MathSciNet  Google Scholar 

  45. Yang, F., Escobar, S., Meadows, C., Meseguer, J., Narendran, P.: Theories of homomorphic encryption, unification, and the finite variant property. In: Proceedings of PPDP 2014, pp. 123–134. ACM (2014)

    Google Scholar 

  46. Yang, F., Escobar, S., Meadows, C., Meseguer, J.: Modular verification of sequential composition for private channels in Maude-NPA. In: Katsikas, S.K., Alcaraz, C. (eds.) STM 2018. LNCS, vol. 11091, pp. 20–36. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01141-3_2

    Chapter  Google Scholar 

  47. Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Cheney, J., Vidal, G. (eds.) Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, 5–7 September 2016, pp. 76–89. ACM (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DSIC-ELP, Universitat Politècnica de València, Valencia, Spain

    Santiago Escobar

  2. University of Illinois at Urbana-Champaign, Urbana, IL, USA

    José Meseguer

Authors
  1. Santiago Escobar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Santiago Escobar .

Editor information

Editors and Affiliations

  1. Worcester Polytechnic Institute, Worcester, MA, USA

    Joshua D. Guttman

  2. George Washington University, Washington, DC, USA

    Carl E. Landwehr

  3. University of Illinois, Urbana, IL, USA

    José Meseguer

  4. University of Hawai'i, Honolulu, HI, USA

    Dusko Pavlovic

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Escobar, S., Meseguer, J. (2019). Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method. In: Guttman, J., Landwehr, C., Meseguer, J., Pavlovic, D. (eds) Foundations of Security, Protocols, and Equational Reasoning. Lecture Notes in Computer Science(), vol 11565. Springer, Cham. https://doi.org/10.1007/978-3-030-19052-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-19052-1_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-19051-4

  • Online ISBN: 978-3-030-19052-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation