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

José Meseguer, Prasanna Thati

Research output: Contribution to journalArticle

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

Original languageEnglish (US)
Pages (from-to)153-182
Number of pages30
JournalElectronic Notes in Theoretical Computer Science
Volume117
Issue numberSPEC. ISS.
DOIs
StatePublished - Jan 20 2005

Keywords

  • Narrowing
  • Reachability
  • Rewriting logic
  • Security protocols

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols'. Together they form a unique fingerprint.

  • Cite this