Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer

Santiago Escobar, Catherine Meadows, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

The NRL Protocol Analyzer (NPA) is a tool for the formal specification and analysis of cryptographic protocols that has been used with great effect on a number of complex real-life protocols. One of the most interesting of its features is that it can be used to reason about security in face of attempted attacks on low-level algebraic properties of the functions used in a protocol. Recently, we have given for the first time a precise formal specification of the main features of the NPA inference system: its grammar-based techniques for (co-)invariant generation and its backwards narrowing reachability analysis method; both implemented in Maude as the Maude-NPA tool. This formal specification is given within the well-known rewriting framework so that the inference system is specified as a set of rewrite rules modulo an equational theory describing the behavior of the cryptographic symbols involved. This paper gives a high-level overview of the Maude-NPA tool and illustrates how it supports equational reasoning about properties of the underlying cryptographic infrastructure by means of a simple, yet nontrivial, example of an attack whose discovery essentially requires equational reasoning. It also shows how rule-based programming languages such as Maude and complex narrowing strategies are useful to model, analyze, and verify protocols.

Original languageEnglish (US)
Pages (from-to)23-36
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Volume171
Issue number4
DOIs
StatePublished - Jul 10 2007

Keywords

  • Cryptographic Protocol Verification
  • Equational Reasoning
  • Maude
  • Narrowing
  • Rewriting Logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer'. Together they form a unique fingerprint.

Cite this