A Graphical User Interface for Maude-NPA

S. Santiago, C. Talcott, S. Escobar, C. Meadows, J. Meseguer

Research output: Contribution to journalArticlepeer-review


This paper presents a graphical user interface (GUI) for the Maude-NPA, a crypto protocol analysis tool that takes into account algebraic properties of cryptosystems not supported by other tools, such as cancellation of encryption and decryption, Abelian groups (including exclusive or), and modular exponentiation. Maude-NPA has a theoretical basis in rewriting logic, unification and narrowing, and performs backwards search from a final attack state to determine whether or not it is reachable from an initial state. The GUI animates the Maude-NPA verification process, displaying the complete search tree and allowing users to display graphical representations of final and intermediate nodes of the search tree. One of the most interesting points of this work is that our GUI has been developed using the framework for declarative graphical interaction associated to Maude that includes IOP, IMaude and JLambda. This framework facilitates the interaction and the interoperation between formal reasoning tools (Maude-NPA in our case) and allows Maude to communicate easily with other tools.

Original languageEnglish (US)
Pages (from-to)3-20
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Issue number1
StatePublished - Dec 25 2009


  • Graphical user interface
  • IMaude
  • IOP
  • JLambda
  • Maude
  • Maude-NPA

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A Graphical User Interface for Maude-NPA'. Together they form a unique fingerprint.

Cite this