Maude-NPA: cryptographic protocol analysis modulo equational properties. (English) Zbl 1252.94061
Aldini, Alessandro (ed.) et al., Foundations of security analysis and design V. FOSAD 2007/2008/2009 tutorial lectures. Berlin: Springer (ISBN 978-3-642-03828-0/pbk). Lecture Notes in Computer Science 5705, 1-50 (2009).
Summary: 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.
For the entire collection see [Zbl 1173.68001].
For the entire collection see [Zbl 1173.68001].
MSC:
| 94A60 | Cryptography |
References:
| [1] | Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006) · Zbl 1153.94339 · doi:10.1016/j.tcs.2006.08.032 |
| [2] | Anantharaman, S., Narendran, P., Rusinowitch, M.: Unification modulo CUI plus distributivity axioms. Journal of Automated Reasoning 33(1), 1–28 (2004) · Zbl 1063.03006 · doi:10.1007/s10817-004-2279-7 |
| [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) · Zbl 1081.68523 · doi:10.1007/11513988_27 |
| [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) · doi:10.1007/978-3-540-30227-8_68 |
| [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) · Zbl 1011.68126 · doi:10.1016/B978-044450813-3/50010-2 |
| [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) · doi:10.1007/s10207-004-0055-7 |
| [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) · Zbl 1242.94018 · doi:10.1007/978-3-642-02348-4_11 |
| [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) |
| [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) |
| [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) · Zbl 1242.94020 · doi:10.1007/978-3-642-02348-4_10 |
| [11] | Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. Inf. Comput. 206(2-4), 352–377 (2008) · Zbl 1147.68396 · doi:10.1016/j.ic.2007.07.004 |
| [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) · Zbl 1250.03016 |
| [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) · doi:10.1007/978-3-642-02348-4_27 |
| [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) · Zbl 1115.68046 |
| [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) · Zbl 1078.68059 · doi:10.1007/978-3-540-32033-3_22 |
| [16] | Contejean, E., Marché, C.: The CiME system: tutorial and user’s manual. Université Paris-Sud, Centre d’Orsay (manuscript) |
| [17] | Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transaction on Information Theory 29(2), 198–208 (1983) · Zbl 0502.94005 · doi:10.1109/TIT.1983.1056650 |
| [18] | Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security. Journal of Computer Security, 677–722 (2004) · doi:10.3233/JCS-2004-12203 |
| [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) |
| [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) · Zbl 1153.94375 · doi:10.1016/j.tcs.2006.08.035 |
| [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) |
| [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) · doi:10.1007/978-3-540-88313-5_35 |
| [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) · Zbl 1203.68097 · doi:10.1007/978-3-540-73449-9_13 |
| [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) · Zbl 1347.68194 |
| [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) · Zbl 1145.68444 · doi:10.1007/978-3-540-70590-1_6 |
| [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) · Zbl 1347.68194 |
| [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) · doi:10.3233/JCS-1999-72-304 |
| [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) · doi:10.1007/3-540-10009-1_25 |
| [30] | Millen, S.F.J.K., Clark, S.C.: The interrogator: Protocol secuity analysis. IEEE Transactions on Software Engineering, 274–288 (February 1987) · doi:10.1109/TSE.1987.233151 |
| [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) · Zbl 0516.68067 · doi:10.1007/BFb0036921 |
| [32] | Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools 17, 93–102 (1996) |
| [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) · Zbl 1272.94049 |
| [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) · Zbl 1109.68475 · doi:10.1007/978-3-540-30191-2_21 |
| [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) · doi:10.1109/CSFW.1996.503690 |
| [36] | Meadows, C.: The NRL protocol analyzer: An overview. Journal of logic programming 26(2), 113–131 (1996) · Zbl 0871.68052 · doi:10.1016/0743-1066(95)00095-X |
| [37] | Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F |
| [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) · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26 |
| [39] | Millen, J.: On the freedom of decryption. Information Processing Letters 86(3) (2003) · Zbl 1162.68436 · doi:10.1016/S0020-0190(03)00211-4 |
| [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) |
| [41] | Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998) · doi:10.3233/JCS-1998-61-205 |
| [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) · Zbl 1042.68009 |
| [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) · Zbl 1339.94062 · doi:10.1016/S0020-0190(97)00180-4 |
| [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) · Zbl 1252.94061 |
| [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) |
| [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) · doi:10.1109/49.839933 |
| [47] | TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003) |
| [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) · Zbl 1115.68079 · doi:10.1007/s10990-007-9000-6 |
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.
