This is the README.txt for the current (April 2017) version of the MaudeNPA
GUI.

=== Prerequisites

The zip files NPA-linux.zip and NPA-macintel.zip contains a version of
Maude and a version of IOP. NPA.zip contains only the MaudeNPA and GUI
code, assuming you have Maude and IOP already. To run MaudeMPA via the
GUI you will need a recent Java (e.g. 1.7) and Graphviz (i.e. dot),
information about the latter can be found here: www.graphviz.org. On
linux you will need openjdk's Java, unless you have gnome installed,
in which case you can pick either openjdk or Oracle's java.

It is assumed that you know how MaudeNPA works, and the following
just explains how to talk to MaudeNPA via the GUI.

=== Using NPA

Step 1. Download the appropriate zip file, and unzip it. It will unzip
to a directory or folder called NPA.

Step 2.

Running the start command (./start from a terminal or double clicking
in the Finder) displays the launcher window. From this window you can
choose a protocol to analyze. The Protocols tab allows you to select
from instances that are pre installed or that you have instantiated,
and may have saved data. (Select a protocol and press the Launch
button in the lower right.) The Examples tab allows you to select from
the suite of examples the come with Maude NPA. Selecting one of these
will create a new directory in the protocols directory. This may take
a little time as the grammar for pruning the search tree must be
generated. It will be saved, so next time you access this example
(from the protocols tab) it can simply be restored.

In either case you will get Protocol manager window with a list of
predefined attacks to explore. Selecting an attact and pressing accept
will launch a window with a tab for each accepted attack. Now you can
search by pressing Next, or clicking on a graph node and selecting the
search item. Information about the state represented by a graph node
can also be obtained by clicking on the node.

To create a new attack using the attack editor press the "Edit Attack"
button in the manager window (where the Accept button is). The Editor
window will become visible. An attack is specified by specifying the
attack strands and intruder knowledge items. Documentation for the
attack editor is availble by pressing the Help button at the bottom of
the editor window.

=== New Features

1. Searching from a particular node. If you click on a graph node
you will now be given the opportunity to search from that node.

2. Saving and restoring search state.  To save a search use the
menu item in the "File" menu of the search panel. To restore
a search use the "Restore Search" button in the Protocol manager window.


=== Caveat!

In order to use the attack editor, protocol roles need to be defined.
If none are defined by the user, the GUI will use the strands of the
constant STRANDS-PROTOCOL and give them arbitrary names (r0, r1 ...).
If you make your own protocol (or edit an instance in the protocols
folder) you can pick strands and names that you like, although the
most useful strands to build attacks from are generally the protocol
strands.  For example NSPK defines

  eq STRANDS-PROTOCOL
   = :: r ::
     [ nil | +(pk(B,A ; n(A,r))), -(pk(A,n(A,r) ; N)), +(pk(B, N)), nil ] &
     :: r ::
     [ nil | -(pk(B,A ; N)), +(pk(A, N ; n(B,r))), -(pk(B,n(B,r))), nil ]
  [nonexec] .

so a possible definition of roles is

  op initiator : -> Strand [metadata "role"] .
  eq initiator =
     :: r ::
     [ nil | +(pk(B,A ; n(A,r))), -(pk(A,n(A,r) ; N)), +(pk(B, N)), nil ]
  [nonexec metadata "role"] .

  op responder : -> Strand [metadata "role"] .
  eq responder =
     :: r ::
     [ nil | -(pk(B,A ; N)), +(pk(A, N ; n(B,r))), -(pk(B,n(B,r))), nil ]
  [nonexec  metadata "role"] .

You are free to choose any role names that you (and Maude) like.  It
is crucial that you add the metadata "role" attribute .

=== Using NPA with custom protocols

This version of NPA is designed to enable loading user defined
protocols, as long as they are placed in the appropriate directory
(i.e. a subdirectory of NPA/protocols), and are loadable by the
current maude-npa.

To make your own protocol folder, in protocols/ copy (-r) Template to
ProtocolName put your maude file ProtocolName.maude in that folder,
and replace NSPK by ProtocolName in the files load-npa-assist.maude
and load-npa-assist-genGrammar.maude

Double click on run_npa_gen the first time to generate and save the
grammar.  Once the grammar is saved you can use run_npa


=== Bug reports

Please send bug reports to ian.mason@sri.com.