The NRL Protocol Analyzer: An Overview
From MaRDI portal
Publication:3128627
DOI10.1016/0743-1066(95)00095-XzbMath0871.68052MaRDI QIDQ3128627
Publication date: 17 April 1997
Published in: The Journal of Logic Programming (Search for Journal in Brave)
Related Items (40)
Protocol insecurity with a finite number of sessions and composed keys is NP-complete. ⋮ 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 ⋮ Joshua Guttman: pioneering strand spaces ⋮ Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols ⋮ 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 ⋮ Threat scenarios as a means to formally develop secure systems ⋮ Twenty years of rewriting logic ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ State space reduction in the Maude-NRL protocol analyzer ⋮ Challenges in the Automated Verification of Security Protocols ⋮ Bounding messages for free in security protocols -- extension to various security properties ⋮ Relating State-Based and Process-Based Concurrency through Linear Logic ⋮ 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 ⋮ Refinement-Preserving Plug-In Components ⋮ Distributed temporal logic for the analysis of security protocol models ⋮ Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives ⋮ Automating Security Analysis: Symbolic Equivalence of Constraint Systems ⋮ Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures ⋮ Web security: Authentication protocols and their analysis ⋮ LTL model checking for security protocols ⋮ Automatic verification of temporal-epistemic properties of cryptographic protocols ⋮ Relating state-based and process-based concurrency through linear logic (full-version) ⋮ Key Substitution in the Symbolic Analysis of Cryptographic Protocols ⋮ NRL ⋮ Attacking Fair-Exchange Protocols ⋮ Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif ⋮ Analysis of security protocols as open systems ⋮ A new logic for electronic commerce protocols ⋮ Protocol Composition Logic (PCL) ⋮ Possibilistic Information Flow Control in the Presence of Encrypted Communication ⋮ Temporal Logics of Knowledge and their Applications in Security ⋮ Finite-state analysis of two contract signing protocols ⋮ Narrowing and Rewriting Logic: from Foundations to Applications
This page was built for publication: The NRL Protocol Analyzer: An Overview
