This directory contains the Maude modules specifying 
a Secure Proxy ToolKit (SPTK) with different levels
of protection.

All/*  contains the Maude specification of the SPTK framework,
       a generic application, a generic service class,
       attacker models and TEST files that compose
       and define patterns for analysis
summary-all.txt summarize the contents of files in All

L<i> contains the Maude specification for level <i> toolkit components
     (client and server toolkit and proxy classes)
     and TEST-<attackermodel> modules that composing the components
     and define parameters for test configurations.
summary-l<i>.txt summarize the contents of files in L<i>

To run the provided examples, start Maude in the directory for
the desired level, say L3, and load test-ether (to use attackers
in the ether) or test-lookup (to run with compromised lookup node.
For example

Maude> load test-lookup

The file runs3-lookup.txt shows sample commands to simply rewrite
intial configurations (and the results).  Note that the order
that items in the result configuration are printed by Maude 
may differ depending of the version of Maude, but since the
configuration is a multiset this is just different ways of 
printing the same thing.

The file search3-lookup.txt shows sample commands and results for analysis
-- searching for a reachable state satisfying different properties
expressed as patterns.  

Ditto for -ether and for other levels.