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)

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

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)