A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties

DOI10.1016/j.tcs.2006.08.035zbMath1153.94375OpenAlexW2058459987WikidataQ124982710 ScholiaQ124982710MaRDI QIDQ860906

Santiago Escobar, Catherine A. Meadows, José Meseguer

Publication date: 9 January 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.08.035

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Authentication, digital signatures and secret sharing (94A62)

Related Items (23)

A Finite Representation of the Narrowing Space ⋮ Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ Protocol analysis with time and space ⋮ Complete symbolic reachability analysis using back-and-forth narrowing ⋮ Efficiently deciding equivalence for standard primitives and phases ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types ⋮ Twenty years of rewriting logic ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Modular Termination of Basic Narrowing ⋮ Effectively Checking the Finite Variant Property ⋮ State space reduction in the Maude-NRL protocol analyzer ⋮ A metamodel of access control for distributed environments: applications and properties ⋮ Termination of narrowing via termination of rewriting ⋮ Variant Narrowing and Equational Unification ⋮ A decidable class of security protocols for both reachability and equivalence properties ⋮ A Modular Equational Generalization Algorithm ⋮ Termination of Narrowing in Left-Linear Constructor Systems ⋮ Termination of narrowing revisited ⋮ Termination of Narrowing Using Dependency Pairs ⋮ Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif ⋮ Narrowing and Rewriting Logic: from Foundations to Applications

Uses Software

• Maude
• OFMC
• NRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An NP decision procedure for protocol insecurity with XOR
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Conditional rewriting logic as a unified model of concurrency
• Maude: specification and programming in rewriting logic
• Matching, unification and complexity
• The NRL Protocol Analyzer: An Overview
• On the security of public key protocols
• Using encryption for authentication in large networks of computers
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science

This page was built for publication: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties