State space reduction in the Maude-NRL protocol analyzer. (English) Zbl 1360.94307
Summary: The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties that includes many crypto-systems of interest such as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks for attacks by searching backwards from an insecure attack state, and assumes an unbounded number of sessions. Because of the unbounded number of sessions and the support for different equational theories, it is necessary to develop ways of reducing the search space and avoiding infinite search paths. In order for the techniques to prove useful, they need not only to speed up the search, but should not violate completeness, so that failure to find attacks still guarantees security. In this paper we describe some state space reduction techniques that we have implemented in Maude-NPA. We also provide completeness proofs, and experimental evaluations of their effect on the performance of Maude-NPA.
References:
| [1] | Amadio, R.; Lopez, V., On the reachability problem in cryptographic protocols, (Concur ’00 (2000), Springer), 380-394 · Zbl 0999.94538 |
| [2] | Basin, D.; Cremers, C.; Meadows, C., Model checking security protocols (2013), in press |
| [3] | Basin, D.; Mödersheim, S.; Viganò, L., OFMC: a symbolic model checker for security protocols, Int. J. Inf. Secur., 4, 3, 181-208 (2005) |
| [4] | Basin, D. A.; Mödersheim, S.; Viganò, L., An on-the-fly model-checker for security protocol analysis, (Snekkenes, E.; Gollmann, D., ESORICS. ESORICS, Lect. Notes Comput. Sci., vol. 2808 (2003), Springer), 253-270 |
| [5] | Blanchet, B., An efficient cryptographic protocol verifier based on prolog rules, (14th IEEE Computer Security Foundations Workshop. 14th IEEE Computer Security Foundations Workshop, CSFW-14 (Jun. 2001), IEEE Computer Society: IEEE Computer Society Cape Breton, Nova Scotia, Canada), 82-96 |
| [6] | Chevalier, Y.; Küsters, R.; Rusinowitch, M.; Turuani, M., Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption, ACM Trans. Comput. Log., 9, 4 (2008) · Zbl 1367.94304 |
| [7] | Cremers, C., Scyther - semantics and verification of security protocols (2006), Eindhoven University of Technology, Ph.D. thesis |
| [8] | Cremers, C. J.F., Unbounded verification, falsification, and characterization of security protocols by pattern refinement, (Ning, P.; Syverson, P. F.; Jha, S., ACM Conference on Computer and Communications Security (2008), ACM), 119-128 |
| [9] | Dolev, D.; Yao, A., On the security of public key protocols, IEEE Trans. Inf. Theory, 29, 2, 198-208 (1983) · Zbl 0502.94005 |
| [10] | Escobar, S.; Hendrix, J.; Meadows, C.; Meseguer, J., Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer, (Proc. 2nd International Workshop on Security and Rewriting Techniques. Proc. 2nd International Workshop on Security and Rewriting Techniques, SecReT 2007 (2007)) |
| [11] | Escobar, S.; Meadows, C.; Meseguer, J., A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties, Theor. Comput. Sci., 367, 1-2, 162-202 (2006) · Zbl 1153.94375 |
| [12] | Escobar, S.; Meadows, C.; Meseguer, J., Equational cryptographic reasoning in the Maude-NRL protocol analyzer, (Proc. 1st International Workshop on Security and Rewriting Techniques. Proc. 1st International Workshop on Security and Rewriting Techniques, SecReT 2006 (2007), Elsevier), 23-36, ENTCS 171(4) |
| [13] | Escobar, S.; Meadows, C.; Meseguer, J., State space reduction in the Maude-NRL Protocol Analyzer, (Jajodia, S.; López, J., Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security. Proceedings. Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security. Proceedings, Málaga, Spain, October 6-8, 2008. Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security. Proceedings. Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security. Proceedings, Málaga, Spain, October 6-8, 2008, Lect. Notes Comput. Sci., vol. 5283 (2008), Springer), 548-562 · Zbl 1477.68017 |
| [14] | Escobar, S.; Meadows, C.; Meseguer, J., Maude-NPA: cryptographic protocol analysis modulo equational properties, (Aldini, A.; Barthe, G.; Gorrieri, R., FOSAD 2008/2009 Tutorial Lectures. FOSAD 2008/2009 Tutorial Lectures, Lect. Notes Comput. Sci., vol. 5705 (2009), Springer), 1-50 · Zbl 1252.94061 |
| [15] | Escobar, S.; Meadows, C.; Meseguer, J. (2009), Maude-NPA manual version 2.0 |
| [16] | Escobar, S.; Meseguer, J., Symbolic model checking of infinite-state systems using narrowing, (Proceedings of the 18th International Conference on Rewriting Techniques and Applications. Proceedings of the 18th International Conference on Rewriting Techniques and Applications, RTA’07. Proceedings of the 18th International Conference on Rewriting Techniques and Applications. Proceedings of the 18th International Conference on Rewriting Techniques and Applications, RTA’07, Lect. Notes Comput. Sci., vol. 4533 (2007)), 153-168 · Zbl 1203.68097 |
| [17] | Escobar, S.; Meseguer, J.; Sasse, R., Effectively checking the finite variant property, (Voronkov, A., Rewriting Techniques and Applications, 19th International Conference. Proceedings. Rewriting Techniques and Applications, 19th International Conference. Proceedings, RTA 2008, Hagenberg, Austria, July 15-17, 2008. Rewriting Techniques and Applications, 19th International Conference. Proceedings. Rewriting Techniques and Applications, 19th International Conference. Proceedings, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Lect. Notes Comput. Sci., vol. 5117 (2008), Springer), 79-93 · Zbl 1145.68444 |
| [18] | Escobar, S.; Meseguer, J.; Sasse, R., Variant narrowing and equational unification, Electron. Notes Theor. Comput. Sci., 238, 3, 103-119 (2009) · Zbl 1347.68194 |
| [19] | Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, (Ölveczky, P. C., Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Revised Selected Papers. Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Revised Selected Papers, Paphos, Cyprus, March 20-21, 2010. Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Revised Selected Papers. Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Revised Selected Papers, Paphos, Cyprus, March 20-21, 2010, Lect. Notes Comput. Sci., vol. 6381 (2010), Springer), 52-68 · Zbl 1306.68069 |
| [20] | Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program. (2011) · Zbl 1306.68069 |
| [21] | Fabrega, F. J.T.; Herzog, J.; Guttman, J., Strand spaces: what makes a security protocol correct?, J. Comput. Secur., 7, 191-230 (1999) |
| [22] | Huima, A., Efficient infinite-state analysis of security protocols, (Proc. FLOC’99 Workshop on Formal Methods and Security Protocols. Proc. FLOC’99 Workshop on Formal Methods and Security Protocols, FMSP’99 (1999)) |
| [23] | Meadows, C., Language generation and verification in the NRL protocol analyzer, (Ninth IEEE Computer Security Foundations Workshop. Ninth IEEE Computer Security Foundations Workshop, March 10-12, 1996, Dromquinna Manor, Kenmare, County Kerry, Ireland (1996), IEEE Computer Society), 48-61 |
| [24] | Meadows, C., The NRL protocol analyzer: an overview, J. Log. Program., 26, 2, 113-131 (1996) · Zbl 0871.68052 |
| [25] | Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043 |
| [26] | Meseguer, J., Membership algebra as a logical framework for equational specification, (Parisi-Presicce, F., Proc. WADT’97. Proc. WADT’97, Lect. Notes Comput. Sci., vol. 1376 (1998), Springer), 18-61 · Zbl 0903.08009 |
| [27] | Millen, J. K.; Shmatikov, V., Constraint solving for bounded-process cryptographic protocol analysis, (Reiter, M. K.; Samarati, P., ACM Conference on Computer and Communications Security (2001), ACM), 166-175 |
| [28] | Mödersheim, S.; Viganò, L.; Basin, D. A., Constraint differentiation: search-space reduction for the constraint-based analysis of security protocols, J. Comput. Secur., 18, 4, 575-618 (2010) |
| [29] | Sasse, R.; Escobar, S.; Meadows, C.; Meseguer, J., Protocol analysis modulo combination of theories: a case study in Maude-NPA, (Cuéllar, J.; Lopez, J.; Barthe, G.; Pretschner, A., Security and Trust Management - 6th International Workshop, Revised Selected Papers. Security and Trust Management - 6th International Workshop, Revised Selected Papers, STM 2010, Athens, Greece, September 23-24, 2010. Security and Trust Management - 6th International Workshop, Revised Selected Papers. Security and Trust Management - 6th International Workshop, Revised Selected Papers, STM 2010, Athens, Greece, September 23-24, 2010, Lect. Notes Comput. Sci., vol. 6710 (2011), Springer), 163-178 |
| [30] | Shmatikov, V.; Stern, U., Efficient finite-state analysis for large security protocols, (11th Computer Security Foundations Workshop. 11th Computer Security Foundations Workshop, CSFW-11 (1998), IEEE Computer Society Press) |
| [31] | (TeReSe, Term Rewriting Systems (2003), Cambridge University Press: Cambridge University Press Cambridge) · Zbl 1030.68053 |
| [32] | Thati, P.; Meseguer, J., Symbolic reachability analysis using narrowing and its application verification of cryptographic protocols, High.-Order Symb. Comput., 20, 1-2, 123-160 (2007) · Zbl 1115.68079 |
| [33] | Weidenbach, C., Towards an automatic analysis of security protocols in first-order logic, (Ganzinger, H., CADE. CADE, Lect. Notes Comput. Sci., vol. 1632 (1999), Springer), 314-328 · Zbl 1038.94548 |
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.
