An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis

Raúl López-Rueda, Santiago Escobar, Julia Sapiña

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 a…