A Graphical User Interface for Maude-NPA

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.