State space reduction in the Maude-NRL protocol analyzer

DOI10.1016/j.ic.2014.07.007zbMath1360.94307MaRDI QIDQ462493

Sonia Santiago, José Meseguer, Santiago Escobar, Catherine A. Meadows

Publication date: 20 October 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2014.07.007

Mathematics Subject Classification ID

94A60: Cryptography

68Q42: Grammars and rewriting systems

68M12: Network protocols

Related Items

An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis, Strand spaces with choice via a process algebra semantics, Maude-NPA, Twenty years of rewriting logic, Protocol analysis with time and space, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude

Uses Software

• Maude
• OFMC
• NRL

Cites Work

• 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
• Computer security -- ESORICS 2008. 13th European symposium on research in computer security, Málaga, Spain, October 6--8, 2008. Proceedings
• Conditional rewriting logic as a unified model of concurrency
• The NRL Protocol Analyzer: An Overview
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Effectively Checking the Finite Variant Property
• On the security of public key protocols
• Folding Variant Narrowing and Optimal Variant Termination
• Variant Narrowing and Equational Unification
• Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption
• Symbolic Model Checking of Infinite-State Systems Using Narrowing