Variant Narrowing and Equational Unification

DOI10.1016/j.entcs.2009.05.015zbMath1347.68194OpenAlexW2096506501MaRDI QIDQ5179131

José Meseguer, Santiago Escobar, Ralf Sasse

Publication date: 19 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.015

zbMATH Keywords

narrowingcryptographic protocol analysissymbolic reachability analysisequational unificationfinite variant property

Mathematics Subject Classification ID

Cryptography (94A60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)

Related Items (14)

Model Checking Security Protocols ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ An integrated framework for the diagnosis and correction of rule-based programs ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ On First-Order Model-Based Reasoning ⋮ Optimizing Maude programs via program specialization ⋮ Effectively Checking the Finite Variant Property ⋮ State space reduction in the Maude-NRL protocol analyzer ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Symbolic execution based on language transformation ⋮ Variant Narrowing and Equational Unification ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Termination Modulo Combinations of Equational Theories ⋮ Capturing constrained constructor patterns in matching logic

Uses Software

• Maude-NPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Conditional rewriting logic as a unified model of concurrency
• Equational rules for rewriting logic
• Matching, unification and complexity
• Effectively Checking the Finite Variant Property
• Complete Sets of Reductions for Some Equational Theories
• Lazy narrowing with simplification
• Variant Narrowing and Equational Unification
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Term Rewriting and Applications
• Term Rewriting and Applications

This page was built for publication: Variant Narrowing and Equational Unification