Hackage :: [Package]

tamarin-prover: The tamarin prover for security protocol analysis.

[ deprecated, program, theorem-provers ] [ Propose Tags ]
Deprecated

The tamarin prover is a tool for the analysis of security protocols. It implements a constraint solving algorithm that supports both falsification and verification of security protocols with respect to an unbounded number of sessions. The underlying security protocol model uses multiset rewriting to specify protocols and adversary capabilities, a guarded fragment of first-order logic to specify security properties, and equational theories to model the algebraic properties of cryptographic operators.

The paper describing the theory underlying the tamarin prover is currently under submission to CSF 2012. Drop us (simon.meier@inf.ethz.ch or benedikt.schmidt@inf.ethz.ch) a mail, if you would like to obtain a copy of the paper.

The tamarin prover supports both a batch analysis mode and the interactive construction of security proofs using a GUI. Example protocols and the user guide are installed together with the prover. Just call the tamarin-prover executable without any arguments to get more information.

The tamarin prover uses maude (http://maude.cs.uiuc.edu/) as a unification backend and GraphViz (http://www.graphviz.org/) to visualize constraint systems. Detailed instructions for installing the tamarin prover are given here: http://www.infsec.ethz.ch/research/software#TAMARIN

[Skip to Readme]

Flags

Automatic Flags
NameDescriptionDefault
threaded

Build with support for multithreaded execution

Enabled
test-coverage

Build with test coverage support

Enabled
build-tests

Build unit test driver

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.1.1.0, 0.4.0.0, 0.4.1.0, 0.6.0.0, 0.6.1.0, 0.8.0.0, 0.8.1.0, 0.8.2.0, 0.8.2.1, 0.8.4.0, 0.8.5.0, 0.8.5.1, 0.8.6.0, 0.8.6.1, 0.8.6.2, 0.8.6.3
Change log CHANGES
Dependencies aeson (>=0.3 && <0.4), array (>=0.3 && <0.4), base (>=4 && <5), binary (>=0.5 && <0.6), blaze-builder (>=0.3 && <0.4), bytestring (>=0.9 && <0.10), cmdargs (>=0.6.8 && <0.7), containers (>=0.3 && <0.4.2), data-default (>=0.2 && <0.3), deepseq (>=1.1 && <1.2), derive (>=2.5 && <2.6), directory (>=1.0 && <1.2), fclabels (>=1.0 && <1.1), filepath (>=1.1 && <1.3), hamlet (>=0.8 && <0.9), http-types (>=0.6 && <0.7), monad-control (>=0.2 && <0.3), mtl (>=2.0 && <2.1), old-locale (>=1.0 && <1.1), parallel (>=3.2 && <3.3), parsec (>=3.1 && <3.2), process (>=1.0 && <1.1), safe (>=0.2 && <0.4), syb (>=0.3.3 && <0.4), tamarin-prover-term (>=0.1 && <0.2), tamarin-prover-utils (>=0.1 && <0.2), template-haskell (>=2.5 && <2.6), text (>=0.11 && <0.12), threads (>=0.4 && <0.5), time (>=1.2 && <1.3), transformers (>=0.2 && <0.3), uniplate (>=1.6 && <1.7), wai (>=0.4 && <0.5), wai-extra (==0.4.3), warp (>=0.4 && <0.5), yesod-core (>=0.8 && <0.9), yesod-form (>=0.1 && <0.2), yesod-json (>=0.1 && <0.2), yesod-static (>=0.1 && <0.2) [details]
License LicenseRef-GPL
Copyright Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012
Author Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>, Simon Meier <simon.meier@inf.ethz.ch>
Maintainer Simon Meier <simon.meier@inf.ethz.ch>
Category Theorem Provers
Home page http://www.infsec.ethz.ch/research/software#TAMARIN
Uploaded by SimonMeier at 2012-02-10T20:42:51Z
Distributions Arch:1.8.0
Reverse Dependencies 1 direct, 0 indirect [details]
Executables tamarin-prover
Downloads 11359 total (46 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-25 [all 6 reports]

Readme for tamarin-prover-0.1.0.0

[back to package description] 
======================================================================
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
***