2023/07/12 by Raúl López-Rueda, Santiago Escobar, López-Rueda, Raúl +3 · 1 citation
Computer Science · #Advanced Authentication Protocols Security #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Symbolic Computation (cs.SC) #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2307.06348
openalex publication_date 2023/07/12 · openalex created_date 2023/07/15 · openalex updated_date 2026/07/28
Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal cryptographic protocol analysis, which is why narrowing and unification are used in tools such as Maude-NPA, Tamarin and Akiss. In this work we present the implementation of a canonical narrowing algorithm, which improves the standard narrowing algorithm, extended to be able to process rewrite theories with conditional rules. The conditions of the rules will contain SMT constraints, which will be carried throughout the execution of the algorithm to determine if the solutions have associated satisfiable or unsatisfiable constraints, and in the latter case, discard them.