This webpage describes Version 1.0 of the Maude-NRL Protocol Analyzer (Maude-NPA) and gives instructions for its use.
Maude-NPA is an analysis tool for cryptographic protocols that takes into account many of the algebraic properties of cryptosystems that are not included in other tools. These include cancellation of encryption and decryption, Abelian groups (including exclusive-or), and exponentiation. Maude-NPA uses an approach similar to the original NRL Protocol Analyzer; it is based on unification, and performs backwards search from a final state to determine whether or not it is reachable. Unlike the original NPA, it has a theoretical basis in rewriting logic and narrowing, and offers support for a wider basis of equational theories that includes associative-commutative (AC) theories.
We provide below a detailed manual of installation and how to use Maude-NPA, with several protocol examples. A description of Maude-NPA's formal foundations in rewriting logic, together with a soundness proof, is given in [1]. Descriptions of how Maude-NPA handles different equational theories are given in [2, 3]. Several optimizations included into Maude-NPA for improving the performance and reducing the search space are introduced in [4].
The most up-to-date description of the Maude-NPA is given in [5].
[1] S. Escobar, C. Meadows, and J. Meseguer. A rewriting-based
inference system for the
NRL protocol analyzer and its meta-logical properties.
Theoretical
Computer Science,
367(1-2):162-202, 2006.
Download:
DOI link
[2] S. Escobar, C. Meadows, and J. Meseguer. Equational cryptographic
reasoning in the
Maude-NRL protocol analyzer. In Proc. 1st International Workshop on
Security and
Rewriting Techniques (SecReT 2006), pages 23-36. ENTCS 171(4) ,
Elsevier, 2007.
Download:
DOI link
[3] S. Escobar, J. Hendrix, C. Meadows, and J. Meseguer.
Diffie-Hellman
cryptographic reasoning in
the Maude-NRL protocol analyzer. In Proc. 2nd International Workshop
on Security
and Rewriting Techniques (SecReT 2007), 2007.
Download:
PDF
[4]
S. Escobar, C. Meadows, and J. Meseguer.
State Space Reduction in the Maude-NRL Protocol Analyzer.
In Proc. of 13th European Symposium on Research in Computer Security (ESORICS08), LNCS 5283, pages 548-562, Springer, 2008.
Download:
DOI link
[5]
S. Escobar, C. Meadows, J. Meseguer.
Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties.
FOSAD 2007/2008/2009 Tutorial Lectures, LNCS 5705, pages 1-50.
Springer-Verlag.
Download:
DOI link
Note that Maude-NPA requires a proper installation of Maude 2.4, available at maude.cs.uiuc.edu.
Copyright © 2008, University of Illinois
All rights reserved.
Santiago Escobar has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grants TIN 2004-7943-C04-01, TIN 2007-68093-C02-02, and Generalitat Valenciana under grant GVPRE/2008/113.