State space reduction in the Maude-NRL protocol analyzer
From MaRDI portal
Publication:462493
DOI10.1016/j.ic.2014.07.007zbMath1360.94307OpenAlexW2066904164MaRDI 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
Related Items (7)
Protocol analysis with time and space ⋮ Twenty years of rewriting logic ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Strand spaces with choice via a process algebra semantics ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Maude-NPA
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: State space reduction in the Maude-NRL protocol analyzer
