Variant Narrowing and Equational Unification

DOI10.1016/j.entcs.2009.05.015zbMath1347.68194MaRDI 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

narrowing; cryptographic protocol analysis; symbolic reachability analysis; equational unification; finite variant property

Mathematics Subject Classification ID

94A60: Cryptography

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68Q42: Grammars and rewriting systems

Related Items

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

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