A Graphical User Interface for Maude-NPA

被引：6

作者：

Santiago, S. ^{[1
]}

Talcott, C. ^{[2
]}

Escobar, S. ^{[1
]}

Meadows, C. ^{[3
]}

Meseguer, J. ^{[4
]}

机构：

[1] Univ Politecn Valencia, Valencia, Spain

[2] SRI Int, Menlo Pk, CA 94025 USA

[3] Naval Res Lab, Washington, DC 20375 USA

[4] Univ Illinois, Urbana, IL USA

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 258卷 / 01期

关键词：

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

D O I：

10.1016/j.entcs.2009.12.002

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：3 / 20

页数：18

共 27 条

[1] CONCURRENT OBJECT-ORIENTED PROGRAMMING
AGHA, G
[J]. COMMUNICATIONS OF THE ACM, 1990, 33 (09) : 125 - 141
[2] Agha G.A., 1986, ACTORS MODEL CONCURR
[3] Anlauff M., 2006, P JOINT WORKSH FDN C
[4] Armando A., 2005, P CAV 05
[5] Baker H., 1977, IFIP CONGERSS, P987
[6] An efficient cryptographic protocol verifier based on prolog rules
Blanchet, B
[J]. 14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, : 82 - 96
[7] Boichut Y., 2007, P SAR SSI 2007 2 C S
[8] Clavel M., 2007, LECT NOTES COMPUTER, V4350
[9] Cremers C.J.F., 2006, SCYTHER SEMANTICS VE
[10] Denker G., 2004, ELECT NOTES THEORETI, V117

← 1 2 3 →