Narrowing and Unification in the Maude Programming Language

Abstract

[ES] Los protocolos de seguridad en las comunicaciones evolucionan cada día buscando mejoras y corrección de errores, muchos de los cuales pueden llevar a vulnerabilidades con consecuencias fatales. Por ello, se vuelve de vital importancia el encontrar algoritmos y herramientas capaces de encontrar esas vulnerabilidades para poder solucio-narlas cuanto antes. Uno de estos algoritmos es el narrowing, implementado en Maude, un lenguaje utilizado por varias herramientas de análisis de protocolos, que, a pesar de ser potente y eficiente en muchos casos, tiene algunas limitaciones, que pueden ser resueltas mediante la utilización de variantes del algoritmo. Una posible variante es el canonical narrowing, que se basa en restricciones de irreductibilidad para descartar aquellas secuencias del narrowing estándar que pueden obviarse porque no representan secuencias de reescritura reales.

[EN] Communications security protocols evolve every day seeking improvements and bug fixes, many of which can lead to vulnerabilities with fatal consequences. For this reason, it becomes vitally important to find algorithms and tools capable of finding these vulnerabilities in order to fix them as soon as possible. One of these algorithms is narrowing, implemented in Maude, a language used by various protocol analysis tools, which, despite being powerful and efficient in many cases, has some limitations, which can be resolved by using variants of the algorithm. A possible variant is canonical narrowing, which relies on irreducibility constraints to discard those sequences of the standard narrowing that can be ignored because they do not represent actual rewrite sequences.