The NRL protocol analyzer: An overview. The NRL protocol analyzer is a prototype special-purpose verification tool, written in Prolog, that has been developed for the analysis of cryptographic protocols that are used to authenticate principals and services and distribute keys in a network. In this paper we give an overview of how the analyzer works and describe its achievements so far. We also show how our use of the Prolog language benefited us in the design and implementation of the analyzer.

References in zbMATH (referenced in 26 articles , 1 standard article )

Showing results 1 to 20 of 26.
Sorted by year (citations)

1 2 next

  1. Arapinis, Myrto; Duflot, Marie: Bounding messages for free in security protocols -- extension to various security properties (2014)
  2. Bella, Giampaolo: Inductive study of confidentiality: for everyone (2014) ioport
  3. Blanchet, Bruno: Automatic verification of security protocols in the symbolic model: the verifier proverif (2014)
  4. Escobar, Santiago; Meadows, Catherine; Meseguer, José; Santiago, Sonia: State space reduction in the Maude-NRL protocol analyzer (2014)
  5. Meseguer, José: Twenty years of rewriting logic (2012)
  6. Basin, David; Caleiro, Carlos; Ramos, Jaime; Viganò, Luca: Distributed temporal logic for the analysis of security protocol models (2011)
  7. Chevalier, Yannick; Rusinowitch, Michael: Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures (2010)
  8. Cervesato, Iliano; Scedrov, Andre: Relating state-based and process-based concurrency through linear logic (full-version) (2009)
  9. Escobar, Santiago; Meadows, Catherine; Meseguer, José: Maude-NPA: cryptographic protocol analysis modulo equational properties (2009)
  10. Mödersheim, Sebastian; Viganò, Luca: The open-source fixed-point model checker for symbolic analysis of security protocols (2009)
  11. Chevalier, Yannick; Rusinowitch, Michael: Hierarchical combination of intruder theories (2008)
  12. Udrea, Octavian; Lumezanu, Cristian; Foster, Jeffrey S.: Rule-based static analysis of network protocol implementations (2008)
  13. Cervesato, Iliano; Stehr, Mark-Oliver: Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types (2007)
  14. Meseguer, José; Thati, Prasanna: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols (2007)
  15. Escobar, Santiago; Meadows, Catherine; Meseguer, José: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties (2006)
  16. Thati, Prasanna; Meseguer, José: Complete symbolic reachability analysis using back-and-forth narrowing (2006)
  17. Basin, David; Mödersheim, Sebastian; Viganò, Luca: OFMC: a symbolic model checker for security protocols (2005) ioport
  18. Bozzano, Marco; Delzanno, Giorgio: Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols (2005)
  19. Chen, Qingfeng; Zhang, Chengqi; Zhang, Shichao: ENDL: A logical framework for verifying secure transaction protocols (2005) ioport
  20. Yang, Ping; Ramakrishnan, C.R.; Smolka, Scott A.: A logical encoding of the $\pi$-calculus: model checking mobile processes using tabled resolution (2004) ioport

1 2 next