Canonical narrowing with irreducibility and SMT constraints as a generic symbolic protocol analysis method. (English) Zbl 1517.94128
Bae, Kyungmin (ed.), Rewriting logic and its applications. 14th international workshop, WRLA 2022, Munich, Germany, April 2–3, 2022. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 13252, 45-64 (2022).
Summary: Nowadays, formal cryptographic protocol analysis relies on symbolic techniques such as narrowing and equational unification, e.g. Maude-NPA, Tamarin or AKISS crypto tools. In previous works, we developed a new narrowing strategy, called canonical narrowing, which manages to reduce the state explosion problem by introducing irreducibility constraints. In this paper, we extend canonical narrowing to handle conditional rules with SMT constraints. We demonstrate the viability of this method with the Brands and Chaum protocol [S. Brands and D. Chaum, Lect. Notes Comput. Sci. 765, 344–359 (1994; Zbl 0951.94511)] using time and location information described as SMT constraints on the real numbers.
For the entire collection see [Zbl 1499.68008].
For the entire collection see [Zbl 1499.68008].
Citations:
Zbl 0951.94511References:
| [1] | Aparicio-Sánchez, D.; Escobar, S.; Meadows, C.; Meseguer, J.; Sapiña, J.; Bhargavan, K.; Oswald, E.; Prabhakaran, M., Protocol analysis with time, Progress in Cryptology - INDOCRYPT 2020, 128-150 (2020), Cham: Springer, Cham · Zbl 1492.94055 · doi:10.1007/978-3-030-65277-7_7 |
| [2] | Aparicio-Sánchez, D., Escobar, S., Meadows, C., Meseguer, J., Sapiña, J.: Protocol analysis with time and space. In: Dougherty, D., Meseguer, J., Mödersheim, S.A., Rowe, P. (eds.) Protocols, Strands, and Logic. LNCS, vol. 13066, pp. 22-49. Springer, Cham (2021). doi:10.1007/978-3-030-91631-2_2 · Zbl 1492.94055 |
| [3] | Brands, S.; Chaum, D.; Helleseth, T., Distance-bounding protocols, Advances in Cryptology — EUROCRYPT ’93, 344-359 (1994), Heidelberg: Springer, Heidelberg · Zbl 0951.94511 · doi:10.1007/3-540-48285-7_30 |
| [4] | Chadha, R., Cheval, V., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1-23:32 (2016) · Zbl 1367.68184 |
| [5] | Clavel, M., et al: Maude Manual (Version 3.2.1). Technical report, SRI International Computer Science Laboratory (2022). http://maude.cs.illinois.edu |
| [6] | Comon-Lundh, H.; Delaune, S.; Giesl, J., The finite variant property: how to get rid of some algebraic properties, Term Rewriting and Applications, 294-307 (2005), Heidelberg: Springer, Heidelberg · Zbl 1078.68059 · doi:10.1007/978-3-540-32033-3_22 |
| [7] | Erbatur, S.; Bonacina, MP, Asymmetric unification: a new unification paradigm for cryptographic protocol analysis, Automated Deduction - CADE-24, 231-248 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68264 · doi:10.1007/978-3-642-38574-2_16 |
| [8] | Escobar, S.; Meadows, C.; Meseguer, J.; Aldini, A.; Barthe, G.; Gorrieri, R., Maude-NPA: cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design V, 1-50 (2009), Heidelberg: Springer, Heidelberg · Zbl 1252.94061 · doi:10.1007/978-3-642-03829-7_1 |
| [9] | Escobar, S.; Meadows, CA; Meseguer, J.; Santiago, S., State space reduction in the Maude-NRL protocol analyzer, Inf. Comput., 238, 157-186 (2014) · Zbl 1360.94307 · doi:10.1016/j.ic.2014.07.007 |
| [10] | Escobar, S.; Meseguer, J.; Guttman, JD; Landwehr, CE; Meseguer, J.; Pavlovic, D., Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method, Foundations of Security, Protocols, and Equational Reasoning, 15-38 (2019), Cham: Springer, Cham · Zbl 1533.68123 · doi:10.1007/978-3-030-19052-1_4 |
| [11] | Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program., 81, 7-8, 898-928 (2012) · Zbl 1291.68217 · doi:10.1016/j.jlap.2012.01.002 |
| [12] | Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand spaces: what makes a security protocol correct? J. Comput. Secur. 7, 191-230 (1999) |
| [13] | Jouannaud, J-P; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 4, 1155-1194 (1986) · Zbl 0665.03005 · doi:10.1137/0215084 |
| [14] | López-Rueda, R., Escobar, S., Meseguer, J.: An efficient canonical narrowing implementation for protocol analysis. In: Bae, K. (ed.) WRLA 2022. LNCS, vol. 13252, pp. 151-170. Springer, Cham (2022). Held as a Satellite Event of ETAPS, Munich, Germany, 2-3 April 2022, Proceedings |
| [15] | Meier, S.; Schmidt, B.; Cremers, C.; Basin, D.; Sharygina, N.; Veith, H., The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification, 696-701 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_48 |
| [16] | Meseguer, J., Conditioned rewriting logic as a united model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F |
| [17] | Meseguer, J.; Presicce, FP, Membership algebra as a logical framework for equational specification, Recent Trends in Algebraic Development Techniques, 18-61 (1998), Heidelberg: Springer, Heidelberg · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26 |
| [18] | Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080 · doi:10.1016/j.tcs.2016.12.026 |
| [19] | Meseguer, J., Generalized rewrite theories, coherence completion, and symbolic methods, J. Log. Algebraic Methods Program., 110, 100483 (2020) · Zbl 1496.68166 · doi:10.1016/j.jlamp.2019.100483 |
| [20] | 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) · Zbl 1115.68079 · doi:10.1007/s10990-007-9000-6 |
| [21] | TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003) · Zbl 1030.68053 |
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.
