×

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. (English) Zbl 1115.68079

Summary: Narrowing was introduced, and has traditionally been used, to solve equations in initial and free algebras modulo a set of equations \(E\). This paper proposes a generalization of narrowing which can be used to solve reachability goals in initial and free models of a rewrite theory \(\mathcal R\). We show that narrowing is sound and weakly complete (i.e., complete for normalized solutions) under appropriate executability assumptions about \(\mathcal R\). We also show that in general narrowing is not strongly complete, that is, not complete when some solutions can be further rewritten by \(\mathcal R\). We then identify several large classes of rewrite theories, covering many practical applications, for which narrowing is strongly complete. Finally, we illustrate an application of narrowing to analysis of cryptographic protocols.

MSC:

68P25 Data encryption (aspects in computer science)

Software:

Timbuk; Isabelle; Maude; NRL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amadio R., Lugiez, D.: On the reachability problem in cryptographic primitives. In: Palamidessi, C. (ed.) 11th International Conference on Concurrency Theory (CONCUR ”00), vol. 1877 of Lecture Notes in Computer Science, pp. 380–394. Springer (2000) · Zbl 0999.94538
[2] Antoy, S.: Definitional trees. In: Proceedings of the 3rd International Conference on Algebraic and Logic Programming ALP”92, vol. 632 of Lecture Notes in Computer Science, pp. 143–157. Springer, Berlin (1992)
[3] Antoy, S., Echahed, R., Hanus, M.: Parallel evaluation strategies for functional logic languages. In: Proceedings of the Fourteenth International Conference on Logic Programming (ICLP”97), pp. 138–152. MIT Press (1997)
[4] Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000) · Zbl 1327.68141 · doi:10.1145/347476.347484
[5] Antoy, S., Ariola, Z.M.: Narrowing the narrowing space. In: International Symposium on Programming Languages, Implementations, Logics, and Programs, vol. 1292 of Lecture Notes in Computer Science, pp. 1–15. Springer (1997)
[6] Basin, D., Modersheim, S., Vigano, L.: Constraint differentiation: A new reduction technique for constraint-based analysis of security protocols. Technical Report TR-405, Swiss Federal Institute of Technology, Zurich (May 2003)
[7] Bockmayr, A.: Conditional narrowing modulo of set of equations. Appl. Algebra Eng. Commun. Comput. 4(3), 147–168 (1993) · Zbl 0776.68068 · doi:10.1007/BF01202035
[8] Bockmayr, A., Krischer, S., Werner, A.: An optimal narrowing strategy for general canonical systems. In: Rusinowitch, M., Rémy, J.L. (eds.) 3rd International Workshop on Conditional Term Rewrite systems, vol. 656 of Lecture Notes in Computer Science, pp. 483–497. Springer (1992)
[9] Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) 16th Annual Symposium on Theoretical Aspects of Computer Science, vol. 1563 of Lecture Notes in Computer Science, pp. 323–333 (1999) · Zbl 0926.03035
[10] Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification over infinite states. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 545–623. Elsevier Publishing (2001) · Zbl 1035.68067
[11] Chevalier, Y., Kusters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P., Radhakrishnan, J. (eds.) 23rd Conference on Foundations Software Technology and Theoretical Computer Science, vol. 2914 of Lecture Notes in Computer Science. Springer (2003) · Zbl 1205.94078
[12] Chevalier, Y., Kusters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS ”03), pp. 261–270 (2003) · Zbl 1068.68057
[13] Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
[14] Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994) · doi:10.1145/186025.186051
[15] Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications (2000) · Zbl 1003.03032
[16] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285, 187–243 (2002) · Zbl 1001.68059 · doi:10.1016/S0304-3975(01)00359-0
[17] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (version 2.2) (Dec. 2005) · Zbl 1038.68559
[18] Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS ”03), pp. 271–280 (2003)
[19] Denker, G., Meseguer, J., Talcott, C.L.: Protocol specification and analysis in Maude. In: Heintze, N., Wing, J. (eds.) Proceedings of Workshop on Formal Methods and Security Protocols, June 25, 1998, Indianapolis, Indiana (1998)
[20] Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983) · Zbl 0502.94005 · doi:10.1109/TIT.1983.1056650
[21] Durán, F., Eker, S., Lincoln, P., Meseguer, J.: Principles of Mobile Maude. In: Agent Systems, Mobile Agents, and Applications, ASA/MA 2000, vol. 1882 of Lecture Notes in Computer Science, pp. 73–85. Springer (2000)
[22] Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of Bounded Security Protocols. In: Workshop on formal methods and security protocols, FMSP (1999)
[23] Emerson, A., Namjoshi, K.: On model checking for nondeterministic infinite state systems. In: 13th IEEE Symposium on Logic in Computer Science, pp. 70–80 (1998) · Zbl 0945.68523
[24] Escobar, S.: Refining weakly outermost-needed rewriting and narrowing. In: Miller, D. (ed.) Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP”03, pp. 113–123. ACM Press, New York (2003)
[25] Escobar, S.: Implementing natural rewriting and narrowing efficiently. In: Kameyama, Y., Stuckey, P.J. (eds.) 7th International Symposium on Functional and Logic Programming (FLOPS 2004), vol. 2998 of Lecture Notes in Computer Science, pp. 147–162. Springer, Berlin (2004) · Zbl 1122.68371
[26] Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer: Grammar generation. In: Proceedings of the 3rd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code. ACM Press (2005) · Zbl 1153.94375
[27] Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) 16th International Conference on Rewriting Techniques and Applications, vol. 3467 of Lecture notes in computer science, pp. 279–293. Springer (2005) · Zbl 1078.68655
[28] Fay, M.: First order unification in equational theories. In: Bibel, W., Kowalski, R. (eds.) 4th Conference on Automated Deduction, vol. 87 of Lecture Notes in Computer Science, pp. 161–167. Springer (1979)
[29] Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1), 63–92 (2001) · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[30] Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: McAllester, D. (ed.) Automated Deduction–CADE 17, vol. 1831 of Lecture notes in artificial intelligence, pp. 271–290. Springer (2000) · Zbl 0963.94016
[31] Genet, T., Tong, V.V.T.: Reachability analysis of term rewriting systems with Timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds.) 8th International Conference on Logic for Programming, vol. 2250 of Lecture Notes in Computer Science, pp. 695–706 (2001) · Zbl 1275.68083
[32] Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Computer Aided Verification. 9th International Conference, CAV”97, Haifa, Israel, June 22–25, 1997, Proceedings, vol. 1254 of Lecture Notes in Computer Science, pp. 72–83. Springer (1997)
[33] Hanus, M.: The integration of functions into logic programming: From theory to practice. J. Log. Program. 19(20), 583–628 (1994) · Zbl 0942.68526 · doi:10.1016/0743-1066(94)90034-5
[34] Huet, G., Lévy, J.-J.: Computations in Orthogonal Term Rewriting Systems, Part I + II. In: Computational logic: Essays in honour of J. Alan Robinson, pp. 395–414 and 415–443. The MIT Press, Cambridge, MA (1992)
[35] Huima, A.: Efficient infinite state analysis of security protocols. In: Workshop on Formal Methods and Security Protocols, FMSP (1999)
[36] Hullot, J.M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) 5th Conference on Automated Deduction, vol. 87 of Lecture Notes in Computer Science, pp. 318–334. Springer (1980) · Zbl 0441.68108
[37] Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. In: Parigot, M., Voronkov, A. (eds.) Logic Programming and Automated Reasoning, vol. 1955 of Lecture Notes in Computer Science, pp. 131–160. Springer (2000) · Zbl 0988.68562
[38] Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: 10th International Colloquium on Automata, Languages and Programming, vol. 154 of Lecture Notes in Computer Science, pp. 361–373. Springer (1983) · Zbl 0516.68067
[39] Kapur, D., Narendran, P., Wang, L.: An e-unification algorithm for analyzing protocols that use modular exponentiation. In: Nieuwenhuis, R. (ed.) International Conference on Rewriting Techniques and Applications (RTA”03), vol. 2706 of Lecture Notes in Computer Science, pp. 165–179. Springer (2003) · Zbl 1043.94537
[40] Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Int. J. Softw. Tools Technol. Transfer 4(2), 328–342 (2000) · Zbl 1059.68589 · doi:10.1007/s100090050040
[41] Kirchner, H.: On the use of constraints in automated deduction. In: Podelski, A. (ed.) Constraint Programming: Basics and Trends, pp. 128–146. Springer LNCS 910 (1995)
[42] Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6, 1–36 (1995) · Zbl 0829.68053 · doi:10.1007/BF01384313
[43] Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Steffen, B., Margaria, T. (eds.) Tools and algorithms for construction and analysis of systems (TACAS ”96), vol. 1055 of Lecture Notes in Computer Science, pp. 147–166. Springer (1996).
[44] Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd. Edn., pp. 1–87. Kluwer Academic Publishers (2002). First published as SRI Tech. Report SRI-CSL-93-05 (Aug. 1993)
[45] Meadows, C.: The NRL protocol analyzer: An overview. J. Log. Program. 26(2), 113–131 (1996) · Zbl 0871.68052 · doi:10.1016/0743-1066(95)00095-X
[46] Meadows, C.: The NRL protocol analyzer: An overview. J. Log. program. 26(2), 113–131 (1996) · Zbl 0871.68052 · doi:10.1016/0743-1066(95)00095-X
[47] Meseguer, J.: Localized fairness: A rewriting semantics. In: Giesl, J. (ed.) International Conference on Term Rewriting and Applications, vol. 3467 of Lecture Notes in Computer Science, pp. 250–263. Springer (2005) · Zbl 1078.68660
[48] Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) Proceedings of ECOOP”02, Málaga, Spain, June 2002, pp. 1–36. Springer LNCS 2374 (2002) · Zbl 1049.68815
[49] Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and it application to verification of cryptographic protocols. In: Martí-Oliet, N. (ed.) International Workshop on Rewriting Logic and its Application, WRLA”04, vol. 117 of Electronic Notes in Theoretical Computer Science, pp. 153–182. Elsevier Sciences Publisher (2004) · Zbl 1272.68194
[50] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[51] Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In:Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314–390. The MIT Press (1993)
[52] Meseguer, J. Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) International Workshop on Algebraic Development Techniques, vol. 1376 of Lecture Notes in Computer Science, pp. 18–61. Springer (1998) · Zbl 0903.08009
[53] Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communications Security (CCS ”01), pp. 166–175 (2001)
[54] Millen, J., Shmatikov, V.: Symbolic protocol analysis with products and Diffie-Hellman exponentiation. In: 16th IEEE Computer Security Foundations Workshop (CSFW-16), pp. 47–61 (2003)
[55] Narendran, P., Meadows, C.: A unification algorithm for the group Diffie-Hellman protocol. In: Workshop on Issues in the Theory of Security (WITS”02) (2002)
[56] Nieuwenhuis, R.: On narrowing, refutation proofs and constraints. In: Hsiang, J. (ed.) 6th International Conference on Rewriting Techniques and Applications, vol. 914, pp. 56–70. Springer LNCS (1995)
[57] Ohsaki, H., Seki, H., Takai, T.: Recognizing boolean closed A-tree languages with membership conditional mechanism. In: Nieuwenhuis, R. (ed.) 14th International Conference on Rewriting Techniques and Applications, vol. 2706 of Lecture notes in computer science, pp. 483–498. Springer (2003) · Zbl 1038.68070
[58] Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS system guide, PVS language reference, and PVS prover guide version 2.4. Computer Science Laboratory, SRI International (2001)
[59] Paulson, L.: Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer (1994) · Zbl 0825.68059
[60] Ramos, J.G., Silva, J., Vidal, G.: Fast Narrowing-Driven Partial Evaluation for Inductively Sequential Systems. In: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), pp. 228–239. ACM Press (2005) · Zbl 1302.68067
[61] 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) · Zbl 1042.68009
[62] Ryan, P., Schneider, S.: An attack on a recursive authentication protocol. Inf. Process. Lett. 65, 7–10 (1998) · Zbl 1339.94062 · doi:10.1016/S0020-0190(97)00180-4
[63] Saïdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification. 11th International Conference, CAV”99, Trento, Italy, July 6–10, 1999, Proceedings, vol. 1633 of Lecture Notes in Computer Science, pp. 443–454. Springer (1999) · Zbl 1046.68608
[64] Sekar, R.C., Ramakrishnan, I.V.: Programming in equational logic: Beyond strong sequentiality. Inf. Comput. 104(1), 78–109 (1993) · Zbl 0803.68060 · doi:10.1006/inco.1993.1026
[65] Stehr, M.-O., Meseguer, J., Ölveczky, P.: Rewriting logic as a unifying framework for Petri nets. In: Unifying Petri Nets, vol. 2128 of Lecture Notes in Computer Science, pp. 250–303. Springer (2001) · Zbl 1017.68080
[66] Thati, P., Meseguer, J.: Complete symbolic reachability analysis using back-and-forth narrowing. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds.) Conference on Algebra and Co-algebra in Computer Science, vol. 3629 of Lecture Notes in Computer Science, pp. 379–394. Springer (2005) · Zbl 1151.68452
[67] Takai, T.: A verification technique using term rewriting systems and abstract interpretation. In: Halatsis et al., (eds.) Proceedings RTA 2004, vol. 3091 of Lecture Notes in Computer Science, pp. 119–133. Springer (2004) · Zbl 1187.68319
[68] Viry, P.: Rewriting: An effective model of concurrency. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE”94 Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4–8, 1994, Proceedings, vol. 817 of Lecture Notes in Computer Science, pp. 648–660. Springer (1994)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.