SPEC version 0.3
----------------

Webpage: http://www.ntu.edu.sg/home/atiu/spec-prover/

About SPEC
----------
SPEC (for Spi-calculus Equivalence Checker) is an equivalence checker
for a version of Abadi and Gordon's spi-calculus. The spi-calculus has
been used to encode security protocols and, via a notion of
observational equivalence, been used to reason about security
properties such as secrecy and authentication.

SPEC implements a process equivalence checking procedure based on the
paper by Alwen Tiu and Jeremy Dawson (presented in the IEEE Computer
Security Foundations symposium in 2010).

SPEC is implemented on top of a modified version of the Bedwyr logical
framework (see http://slimmer.gforge.inria.fr/bedwyr).  The
modified Bedwyr codes are included in this distribution.


Compiling SPEC
--------------

Download and unpack the distribution in a directory of your
choice. Below we assume the directory is called `spec' in the user's
home directory.

SPEC, and the Bedwyr engine it relies on, are implemented using the
Ocaml language, so you will need to have Ocaml installed to compile
SPEC.

To compile the system, use the following commands:
# cd $HOME/spec
# ./configure
# make


Running SPEC
-------------
# src/spec

See the user manual included in the distribution (in the directory
`doc') for more information.