TY - JOUR
T1 - A Graphical User Interface for Maude-NPA
AU - Santiago, S.
AU - Talcott, C.
AU - Escobar, S.
AU - Meadows, C.
AU - Meseguer, J.
N1 - Funding Information:
1 S. Santiago and S. Escobar have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2007-68093-C02-02, and Generalitat Valenciana under grant GVPRE/2008/113. Carolyn Talcott is supported by the NSF under grant IIS-0513857. 2 Email: [email protected] 3 Email: [email protected] 4 Email: [email protected] 5 Email: [email protected] 6 Email: [email protected]
PY - 2009/12/25
Y1 - 2009/12/25
N2 - 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.
AB - 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.
KW - Graphical user interface
KW - IMaude
KW - IOP
KW - JLambda
KW - Maude
KW - Maude-NPA
UR - http://www.scopus.com/inward/record.url?scp=72049112277&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=72049112277&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2009.12.002
DO - 10.1016/j.entcs.2009.12.002
M3 - Article
AN - SCOPUS:72049112277
SN - 1571-0661
VL - 258
SP - 3
EP - 20
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 1
ER -