MSR IMPLEMENTATION README
=========================

MSR homepage: http://formal.cs.uiuc.edu/stehr/msr_eng.html

Author: Stefan Reich <stefanr@uiuc.edu>
Date: 10/15/04

INTRODUCTION

  This is an implementation of the MSR security protocol specification
  language, built on top of a custom version of the rewriting engine Maude and
  the higher order rewriting language OCC. For further information on MSR,
  please see the enclosed user's guide or the MSR homepage.
  
FILES

  README             This file
  msr.maude          Main file (MSR integrated with OCC)
  msr-only.maude     Main file (just MSR)
  doc/userguide.pdf  User's Guide (PDF)
  doc/userguide.ps   User's Guide (PostScript)
  examples/          Example MSR specifications and various sample outputs
  src/               MSR sources
  lib/               MSR standard library
  occ/               OCC sources
  occ/lib/           OCC standard library
  
INSTALLATION

  Simply unpack the MSR implementation archive to a directory of your choice:

    tar xvfz msr.tgz

  For simplicity, you should install Maude in the same directory. If you are
  using a binary Maude distribution:

    tar xvfz maude-alpha-84c-linux.tgz

  (with linux being an example for the platform you are using).

  If you compiled Maude yourself, copy the maude binary as well as
  prelude.maude to the MSR directory.

INVOCATION

  Switch to the MSR directory and start MSR by typing:

    ./maude msr.maude
    
  For a special mode that runs just MSR, but not OCC, say: 

    ./maude msr-only.maude
    
  In this mode, the command (occ) dumps the OCC translaction on to the screen
  instead of switching to OCC mode.
  
  (Note: On Windows, write maude instead of ./maude!)
    
EXAMPLES

  The following examples from the examples/ directory are complete and work:
  
    otway-rees.msr         - the Otway-Rees protocol
    needham-schroeder2.msr - the 2-party Needham-Schroeder protocol 
    kerberos.msr           - a simplified model of the Kerberos 5 protocol
    timeout.msr            - a protocol demonstrating use of natural numbers
                             as timers
                             
RUNNING AN EXAMPLE

  First, start MSR:
  
    ./maude msr.maude
  
  Then load the example:
  
    in examples/otway-rees.msr
    
  This parses and type checks the example specification. Now you can run a
  rewrite command, such as:
  
    (rew)
    
  You can exit the interpreter at any time with
  
    quit