zbMATH — the first resource for mathematics

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. (English) Zbl 1272.68194
Martí-Oliet, N. (ed.), Proceedings of the fifth international workshop on rewriting logic and its applications (WRLA 2004), Barcelona, Spain, March 27–28, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 117, 153-182 (2005).
Summary: Narrowing was introduced, and has traditionally been used, to solve equations in initial and free algebras modulo a set of equations \(E\). This paper proposes a generalization of narrowing which can be used to solve reachability goals in initial and free models of a rewrite theory \(\mathcal{R}\). We show that narrowing is sound and weakly complete (i.e., complete for normalized solutions) under reasonable executability assumptions about \(\mathcal{R}\). We also show that in general narrowing is not strongly complete, that is, not complete when some solutions can be further rewritten by \(\mathcal{R}\). We then identify several large classes of rewrite theories, covering many practical applications, for which narrowing is strongly complete. Finally, we illustrate an application of narrowing to analysis of cryptographic protocols.
For the entire collection see [Zbl 1271.68050].

68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)
94A60 Cryptography
Full Text: Link