Maude Tools: Maude-NPA

From The Maude System
Revision as of 23:05, 28 November 2016 by Malaga (Talk | contribs)

Jump to: navigation, search

Maude-NPA

This webpage describes Version 2.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 crypto systems that are not included in other tools. These include cancellation of encryption and decryption, Abelian groups (including exclusive-or), exponentiation, and homomorphic encryption. 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 commutative (C), associative-commutative (AC), and associative-commutative-identity (ACU) 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, 5, 8, 9]. Several optimizations included into Maude-NPA for improving the performance and reducing the search space are introduced in [4, 5]. Sequential protocol composition is introduced in [7].

A graphical interface for Maude-NPA was presented in [6] and is publicly available at http://users.dsic.upv.es/~ssantiago/Maude-NPA_GUI.

Maude Protocol Specification Language (Maude-PSL)

An experimental specification language for the Maude-NPA has been developed by Andrew Cholewa in Spring 2015. It has the following advantages:

  1. Syntax based off of a conservative extension of the Alice and Bob notation that is both easier to read and write than the current input language.
  2. More stringent error checking.
  3. Significantly less code repetition.

A github repository of the language can be found here. In addition to the source code, the repository also contains a collection of example specifications and a draft of Andrew Cholewa's master's thesis, which provides a thorough description of the language.

References

[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. 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. 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. 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. 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. DOI link

[6] S. Santiago, C. Talcott, S. Escobar, Catherine Meadows, J. Meseguer. A Graphical User Interface for Maude-NPA. In IX Jornadas sobre Programacion y Lenguajes (PROLE 2009). Electronic Notes in Theoretical Computer Science, volume 258, number 1, pages 3-20. Elsevier, 2009. DOI link

[7] S. Escobar, C. Meadows, J. Meseguer, S. Santiago. Sequential Protocol Composition in Maude-NPA. In Proc. of European Symposium on Research in Computer Security (ESORICS 2010), LNCS 6345, pages 303-318. 2010. DOI link

[8] R. Sasse, S. Escobar, C. Meadows, J. Meseguer. Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA. In proceedings of 6th International Workshop on Security and Trust Management (STM'10), Lecture Notes in Computer Science, Volume 6710, pages 163-178, 2011. Download: DOI link

[9] S. Escobar, D. Kapur, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, and R. Sasse. Protocol Analysis in Maude-NPA Using Unification Modulo Homomorphic Encryption In proceedings of 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'2011). Download: DOI link

Downloads

Maude-NPA manual v2.0

Maude-NPA tool zip file v2.0

Note that Maude-NPA v2.0 requires a proper installation of Maude 2.6, available at maude.cs.uiuc.edu.

Mailing List

We maintain the following mailing list related to Maude-NPA users, where you can post comments, problems or questions.

Please, click on the link below to subscribe.

maudenpa @ dsic.upv.es

Contact

Santiago Escobar

Catherine Meadows

José Meseguer

Copyright © 2012, University of Illinois

All rights reserved.

Santiago Escobar has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grants TIN 2007-68093-C02-02 and TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052.