An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
From MaRDI portal
Publication:6052948
DOI10.1016/j.jlamp.2023.100895arXiv2307.06348OpenAlexW4385252025MaRDI QIDQ6052948
Julia Sapiña, Raúl López-Rueda, Santiago Escobar
Publication date: 25 September 2023
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2307.06348
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- State space reduction in the Maude-NRL protocol analyzer
- Strict coherence of conditional rewriting modulo axioms
- 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
- Folding variant narrowing and optimal variant termination
- Protocol analysis with time
- Protocol analysis with time and space
- Generalized rewrite theories, coherence completion, and symbolic methods
- Programming and symbolic computation in Maude
- Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method
- A Survey of Satisfiability Modulo Theory
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Completion of a Set of Rules Modulo a Set of Equations
- Variant-Based Satisfiability in Initial Algebras
- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way)
- Term Rewriting and Applications
This page was built for publication: An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
