Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
From MaRDI portal
Publication:880981
DOI10.1007/s10990-007-9000-6zbMath1115.68079OpenAlexW2042987983MaRDI QIDQ880981
Publication date: 21 May 2007
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10990-007-9000-6
Related Items
Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Complete symbolic reachability analysis using back-and-forth narrowing, A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties, Sentence-normalized conditional narrowing modulo in rewriting logic and Maude, Rewriting modulo SMT and open system analysis, An integrated framework for the diagnosis and correction of rule-based programs, Optimization of rewrite theories by equational partial evaluation, José Meseguer: Scientist and Friend Extraordinaire, Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude, Two Decades of Maude, The Formal System of Dijkstra and Scholten, Twenty years of rewriting logic, An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis, Symbolic Specialization of Rewriting Logic Theories with Presto, Compositional Specification in Rewriting Logic, Strategies in conditional narrowing modulo SMT plus axioms, Optimizing Maude programs via program specialization, Modular Termination of Basic Narrowing, Effectively Checking the Finite Variant Property, State space reduction in the Maude-NRL protocol analyzer, Functional Logic Programming in Maude, A generic framework for symbolic execution: a coinductive approach, Symbolic execution based on language transformation, On the relationships between models in protocol verification, Programming with narrowing: a tutorial, Variant Narrowing and Equational Unification, A compact fixpoint semantics for term rewriting systems, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, A partial evaluation framework for order-sorted equational programs modulo axioms, Built-in Variant Generation and Unification, and Their Applications in Maude 2.7, Termination of narrowing revisited, Termination of Narrowing Using Dependency Pairs, A Non-Deterministic Multiset Query Language, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Narrowing and Rewriting Logic: from Foundations to Applications, Symbolic computation in Maude: some tapas
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An attack on a recursive authentication protocol. A cautionary tale
- An NP decision procedure for protocol insecurity with XOR
- Programming in equational logic: Beyond strong sequentiality
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
- Conditional rewriting logic as a unified model of concurrency
- Conditional narrowing modulo a set of equations
- Isabelle. A generic theorem prover
- Property preserving abstractions for the verification of concurrent systems
- Maude: specification and programming in rewriting logic
- Control and data abstraction: The cornerstones of practical formal verification
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- Fast narrowing-driven partial evaluation for inductively sequential programs
- Reachability Analysis of Term Rewriting Systems with Timbuk
- The NRL Protocol Analyzer: An Overview
- A needed narrowing strategy
- On the security of public key protocols
- The integration of functions into logic programming: From theory to practice
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- Functional and Logic Programming
- Algebra and Coalgebra in Computer Science
- Term Rewriting and Applications
- Term Rewriting and Applications
- Rewriting Techniques and Applications
- Well-structured transition systems everywhere!
