Readme for tamarin-prover-0.1.1.0
======================================================================
README for the tamarin-prover for security protocol verification
======================================================================
Author: Simon Meier <simon.meier@inf.ethz.ch>
Creation Date: 8/02/2012
1. Introduction
===============
The tool is written in Haskell and provides two usage modes as described
below.
NOTE TO REVIEWERS:
to reproduce our results from the paper install the tool and run
make case-studies
in the root directory of this source distribution. This will create
a directory './case-studies' with the analyzed files and their proofs and
attacks.
2. Installation instructions
============================
2.1 Requirements
----------------
The tool was tested on Linux and Mac OsX. It relies on
- maude version 2.6 for AC unification
download and install "Full Maude 2.6" from http://maude.cs.uiuc.edu/download/
- the 'dot' tool from GraphViz for rendering proof states as graphs
download and install from http://www.graphviz.org/
(most Linux distributions have a corresponding package)
- GHC 7.0.4 and cabal-install
included in the Haskell Platform 2011.2.0.1
available from http://hackage.haskell.org/platform/
2.1 Installing tamarin-prover
----------------------------
You need a working Haskell environment that provides GHC 7 and the 'cabal
install' tool. The simplest way to get such an environment is to download and
install the Haskell Platform package for your OS.
http://hackage.haskell.org/platform/
Then call
cabal install
in the root directory of this source code package. This will use the
Haskell's deployment tool 'cabal-install' to download all missing libraries
from Hackage, the central Haskell library repository and install the
'tamarin-prover' executable in the default installation location of
cabal-install. The installation location is printed at the end of the build
process. Note that this may take a long time due to the large number of
dependencies of the built-in webserver used to serve the interactive mode.
3. Usage
========
the tamarin-prover can be used in two modes:
(1) a batch mode where it just tries to parse the given file (and if called
with --prove) to prove their specified lemmas.
(2) an interactive mode, which runs a webserver that allows to construct
and explore security proofs interactively.
This mode has to be run with an argument that specifies directory
containing the protocol models to be investigated.
See the help message output when calling 'tamarin-prover' without any flags
for more information.
4. Built-in Equational theories
===============================
There are several built-in equational theories which can be activated
for a given theory file by including:
> builtin: theoryname
The following theories are supported as builtins:
diffie-hellman:
functions: _ ^ _, inv(_), _*_
equations: see paper
hashing:
functions: h(_)
no equations
signing:
functions: sign(_,_), verify(_,_,_), pk(_), true
equations: verify(sign(m,sk), m, pk(sk)) = true
symmetric-encryption:
functions: senc(_,_), sdec(_,_)
equations: sdec(senc(m,k),k) = m
asymmetric-encryption:
functions: aenc(_,_), adec(_,_), pk(_)
equations: adec(aenc(m, pk(sk)), sk) = m
***
* Happy Proving :-)
*
* In case of questions do not hesistate to contact the authors
* simon.meier@inf.ethz.ch or benedikt.schmidt@inf.ethz.ch
***