The NRL Protocol Analyzer: An Overview

DOI10.1016/0743-1066(95)00095-XMaRDI QIDQ3128627zbMATH OpenFDO

Authors Catherine Meadows

Publication date 17 April 1997

Published in The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0743-1066(95)00095-X

zbMATH Keywords

NRL protocol analyzerProlog language

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• Three systems for cryptographic protocol analysis
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• A formal language for cryptographic protocol requirements

Cited in

(42)

• Finite-state analysis of two contract signing protocols
• Analysis of security protocols as open systems
• A new logic for electronic commerce protocols
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Twenty years of rewriting logic
• Joshua Guttman: pioneering strand spaces
• Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures
• NRL
• Rule-based static analysis of network protocol implementations
• Hierarchical combination of intruder theories
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• Attacking fair-exchange protocols: parallel models vs. trace models
• Protocol composition logic (PCL)
• Temporal logics of knowledge and their applications in security
• Narrowing and rewriting logic: from foundations to applications
• Model Checking Security Protocols
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
• The CL-Atse Protocol Analyser
• Challenges in the Automated Verification of Security Protocols
• State space reduction in the Maude-NRL protocol analyzer
• Bounding messages for free in security protocols -- extension to various security properties
• Relating state-based and process-based concurrency through linear logic
• Refinement-preserving plug-in components
• Threat scenarios as a means to formally develop secure systems
• Tree automata for detecting attacks on protocols with algebraic cryptographic primitives
• LTL model checking for security protocols
• Automatic verification of temporal-epistemic properties of cryptographic protocols
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif
• Key Substitution in the Symbolic Analysis of Cryptographic Protocols
• Distributed temporal logic for the analysis of security protocol models
• Automating security analysis: symbolic equivalence of constraint systems
• Possibilistic information flow control in the presence of encrypted communication
• Web security: Authentication protocols and their analysis
• Symbolic Specialization of Rewriting Logic Theories with Presto
• Towards a quantitative analysis of security protocols
• Relating state-based and process-based concurrency through linear logic (full-version)
• Complete symbolic reachability analysis using back-and-forth narrowing
• 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
• Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types

This page was built for publication: The NRL Protocol Analyzer: An Overview

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3128627)