Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols

By José Meseguer and Prasanna Thati. Higher-Order and Symbolic Computation, 20(1-2):123–160, 2007.

Full Text:: Download PDF
Publisher Link:: http://dx.doi.org/10.1007/s10990-007-9000-6

Abstract

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 ℛ. We show that narrowing is sound and weakly complete (i.e., complete for normalized solutions) under appropriate executability assumptions about ℛ. We also show that in general narrowing is not strongly complete, that is, not complete when some solutions can be further rewritten by ℛ. 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.

Keywords Rewrite theories - Narrowing - Reachability - Security protocols

Research supported by ONR Grant N00014-02-1-0715 and NSF Grant CCR-0234524. A preliminary version of this paper appeared in [49].

BibTeX

@article{journals/lisp/MeseguerT07,
    author = "Meseguer, José and Thati, Prasanna",
    title = "Symbolic reachability analysis using narrowing and its
             application to verification of cryptographic protocols",
    ee = "http://dx.doi.org/10.1007/s10990-007-9000-6",
    journal = "Higher-Order and Symbolic Computation",
    keywords = "formal methods",
    number = "1-2",
    pages = "123-160",
    volume = "20",
    year = "2007",
}