Variant Narrowing and equational unification

Santiago Escobar, Jose Meseguer, Ralf Sasse

Research output: Contribution to journalConference article

Abstract

Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = Δ {plus sign in big union} B with B a set of axioms for which a finitary unification algorithm exists, and = Δa set of confluent, terminating, and B-coherent rewrite rules. However, when B ≠ θ, effective narrowing strategies such as basic narrowing easily fail to be complete and cannot be used. This poses two challenges to narrowing-based equational unification: (i) finding effective narrowing strategies that are complete modulo B under mild assumptions on B, and (ii) finding sufficient conditions under which such narrowing strategies yield finitary E-unification algorithms. Inspired by Comon and Delaune's notion of E-variant for a term, we propose a new narrowing strategy called variant narrowing that has a search space potentially much smaller than full narrowing, is complete, and yields a finitary E-unification algorithm when E has the finite variant property. We also discuss applications to symbolic reachability analysis of concurrent systems specified as rewrite theories, and in particular to the formal analysis of cryptographic protocols modulo the algebraic properties of the underlying cryptographic functions.

Original languageEnglish (US)
Pages (from-to)91-105
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Dec 1 2008
Event7th International Workshop on Rewriting Logic and its Applications, WRLA 2008 (European Joint Conference on Theory and Practice of Software, ETAPS 2008) - Budapest, Hungary
Duration: Mar 29 2008Mar 30 2008

Fingerprint

Unification
Modulo
Union
Symbolic Analysis
Reachability Analysis
Cryptographic Protocols
Concurrent Systems
Formal Analysis
Axioms
Search Space
Strategy
Sufficient Conditions
Term

Keywords

  • Cryptographic protocol analysis
  • Equational unification
  • Finite variant property
  • Narrowing
  • Symbolic reachability analysis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Variant Narrowing and equational unification. / Escobar, Santiago; Meseguer, Jose; Sasse, Ralf.

In: Electronic Notes in Theoretical Computer Science, 01.12.2008, p. 91-105.

Research output: Contribution to journalConference article

@article{0e93f8923fdc48c8b7a90485f57f140b,
title = "Variant Narrowing and equational unification",
abstract = "Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = Δ {plus sign in big union} B with B a set of axioms for which a finitary unification algorithm exists, and = Δa set of confluent, terminating, and B-coherent rewrite rules. However, when B ≠ θ, effective narrowing strategies such as basic narrowing easily fail to be complete and cannot be used. This poses two challenges to narrowing-based equational unification: (i) finding effective narrowing strategies that are complete modulo B under mild assumptions on B, and (ii) finding sufficient conditions under which such narrowing strategies yield finitary E-unification algorithms. Inspired by Comon and Delaune's notion of E-variant for a term, we propose a new narrowing strategy called variant narrowing that has a search space potentially much smaller than full narrowing, is complete, and yields a finitary E-unification algorithm when E has the finite variant property. We also discuss applications to symbolic reachability analysis of concurrent systems specified as rewrite theories, and in particular to the formal analysis of cryptographic protocols modulo the algebraic properties of the underlying cryptographic functions.",
keywords = "Cryptographic protocol analysis, Equational unification, Finite variant property, Narrowing, Symbolic reachability analysis",
author = "Santiago Escobar and Jose Meseguer and Ralf Sasse",
year = "2008",
month = "12",
day = "1",
language = "English (US)",
pages = "91--105",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Variant Narrowing and equational unification

AU - Escobar, Santiago

AU - Meseguer, Jose

AU - Sasse, Ralf

PY - 2008/12/1

Y1 - 2008/12/1

N2 - Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = Δ {plus sign in big union} B with B a set of axioms for which a finitary unification algorithm exists, and = Δa set of confluent, terminating, and B-coherent rewrite rules. However, when B ≠ θ, effective narrowing strategies such as basic narrowing easily fail to be complete and cannot be used. This poses two challenges to narrowing-based equational unification: (i) finding effective narrowing strategies that are complete modulo B under mild assumptions on B, and (ii) finding sufficient conditions under which such narrowing strategies yield finitary E-unification algorithms. Inspired by Comon and Delaune's notion of E-variant for a term, we propose a new narrowing strategy called variant narrowing that has a search space potentially much smaller than full narrowing, is complete, and yields a finitary E-unification algorithm when E has the finite variant property. We also discuss applications to symbolic reachability analysis of concurrent systems specified as rewrite theories, and in particular to the formal analysis of cryptographic protocols modulo the algebraic properties of the underlying cryptographic functions.

AB - Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = Δ {plus sign in big union} B with B a set of axioms for which a finitary unification algorithm exists, and = Δa set of confluent, terminating, and B-coherent rewrite rules. However, when B ≠ θ, effective narrowing strategies such as basic narrowing easily fail to be complete and cannot be used. This poses two challenges to narrowing-based equational unification: (i) finding effective narrowing strategies that are complete modulo B under mild assumptions on B, and (ii) finding sufficient conditions under which such narrowing strategies yield finitary E-unification algorithms. Inspired by Comon and Delaune's notion of E-variant for a term, we propose a new narrowing strategy called variant narrowing that has a search space potentially much smaller than full narrowing, is complete, and yields a finitary E-unification algorithm when E has the finite variant property. We also discuss applications to symbolic reachability analysis of concurrent systems specified as rewrite theories, and in particular to the formal analysis of cryptographic protocols modulo the algebraic properties of the underlying cryptographic functions.

KW - Cryptographic protocol analysis

KW - Equational unification

KW - Finite variant property

KW - Narrowing

KW - Symbolic reachability analysis

UR - http://www.scopus.com/inward/record.url?scp=84890864053&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84890864053&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:84890864053

SP - 91

EP - 105

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -