TY - GEN
T1 - An Efficient Canonical Narrowing Implementation for Protocol Analysis
AU - López-Rueda, Raúl
AU - Escobar, Santiago
AU - Meseguer, José
N1 - This work has been partially supported by the EC H2020-EU grant agreement No. 952215 (TAILOR), by the grant RTI2018-094403-B-C32 funded by MCIN/AEI/10.13039/501100011033 and ERDF “A way of making Europe”, by the grant PROMETEO/2019/098 funded by Generalitat Valenciana, and by the grant PCI2020-120708-2 funded by MICIN/AEI/10.13039/501100011033 and by the European Union NextGenerationEU/PRTR.
PY - 2022
Y1 - 2022
N2 - This work improves the canonical narrowing previously implemented using Maude 2.7.1 by taking advantage of the new functionalities that Maude 3.2 offers. In order to perform more faithful comparisons between algorithms, we have reimplemented Maude’s built-in narrowing using Maude’s metalevel. We compare these two metalevel implementations with Maude’s built-in narrowing, implemented at the C++ level, through a function that collects all the solutions, since the original command only returns one at a time. The results of these experiments are relevant for narrowing-based protocol analysis tools, as well as for improving the analysis of many other narrowing-based applications such as logical model checking, theorem proving or partial evaluation.
AB - This work improves the canonical narrowing previously implemented using Maude 2.7.1 by taking advantage of the new functionalities that Maude 3.2 offers. In order to perform more faithful comparisons between algorithms, we have reimplemented Maude’s built-in narrowing using Maude’s metalevel. We compare these two metalevel implementations with Maude’s built-in narrowing, implemented at the C++ level, through a function that collects all the solutions, since the original command only returns one at a time. The results of these experiments are relevant for narrowing-based protocol analysis tools, as well as for improving the analysis of many other narrowing-based applications such as logical model checking, theorem proving or partial evaluation.
KW - Canonical narrowing
KW - Maude
KW - Narrowing modulo
KW - Reachability analysis
KW - Security protocols
UR - http://www.scopus.com/inward/record.url?scp=85135860487&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85135860487&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-12441-9_8
DO - 10.1007/978-3-031-12441-9_8
M3 - Conference contribution
AN - SCOPUS:85135860487
SN - 9783031124402
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 151
EP - 170
BT - Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
A2 - Bae, Kyungmin
PB - Springer
T2 - 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Y2 - 2 April 2022 through 3 April 2022
ER -