scyther-proof

Automatic generation of Isabelle/HOL correctness proofs for security protocols.

Latest on Hackage:0.10.0.1

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

Maintained by Simon Meier

The scyther-proof security protocol verification tool

master branch build-status

  • Authors: Simon Meier , Andreas Lochbihler
  • Creation Date: 2011-05-13
  • Last Updated: 2015-02-20 by Andreas Lochbihler
  1. Introduction ===============

Every distribution of the scyther-proof tool contains a copy of the Isabelle/HOL theories formalizing its verification theory and a copy of the protocol models that were verified using scyther-proof. In particular, these examples include models for all of our repaired versions of the protocols from the ISO/IEC-9798 authentication standard. (In the source distribution of scyther-proof they can be found at data/examples/iso9798.)

In the following sections, we give step by step instructions to get the whole system working and we explain the usage of our tools and provide further information (e.g., building documentation).

  1. Installation instructions ============================

2.1 Installing scyther-proof

You need a working Haskell environment that provides a version of GHC from 7.0.x to 7.4.x 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 scyther-proof executable in the default installation location of cabal-install. The installation location is printed at the end of the build process.

Call

scyther-proof

without any arguments to get an overview of the arguments supported and the paths to the examples and the Isabelle/HOL theories.

2.2 Installing the Isabelle/HOL theories

Download and install full Isabelle2014 according to the installation instructions at

http://isabelle.in.tum.de/website-Isabelle2014/

The first time you call scyther-proof with the --isabelle flag it will build the logic image of the Isabelle/HOL theories formalizing the security protocol verification theory underlying scyther-proof.

  1. Usage ========

3.1 scyther-proof

Usage Example -------------

You can now execute the 'scyther-proof' binary without any arguments to get a list of the available flags. A simple example usage is (assuming 'scyther-proof' is in the PATH).

scyther-proof $EXAMPLE_DIR/classic/NS_Public.spthy --shortest

This will parse the NSL protocol modeled in the 'nsl.spthy' file and output all specified security properties together with the proof with the fewest number of chain rule applications to stdout.

To generate an Isabelle proof script, two additional options are required.

scyther-proof $EXAMPLE_DIR/classic/NS_Public.spthy --shortest --output=nsl_cert.thy --ASCII

The first one specifies the output file and the second one instructs scyther-proof to use Isabelle's ASCII notation as the output format.

To build the source code documentation you can use the call

cabal configure; cabal haddock

which will use cabal-install and Haskell's source code documentation tool 'haddock' to build the source code documentation. The location of this documentation is again output on the command line.

3.2 The Isabelle/HOL theories

Note that in many case the easiest way to start with constructing machine-checked proofs interactively is to use a proof script generated by scyther-proof.

Using the Isabelle/jEdit Prover IDE -----------------------------------

In the directory output by scyther-proof, load the Tutorial on interactive proof construction using the following commands

    cd <theory-dir-output-by-scytherproof>/src
    isabelle jedit -d $SCYTHER_PROOF_HOME/data/isabelle -l ESPL Tutorial.thy

where $SCYTHERPROOFHOME expands to the home directory of scyther-proof.


Happy Proving :)

In case of questions do not hesistate to contact Andreas Lochbihler (andreas.lochbihler@inf.ethz.ch) or Simon Meier (iridcode@gmail.com).

Changes

* 0.10.0.1
- make it compile with GHC 7.10.1

* 0.10.0.0
- upgraded dependency on Isabelle to Isabelle2014
- add support for explicit matching and non-matching steps in protocols
- new protocol example for optimistic fair exchange

* 0.8.0.0
- upgraded dependency on Isabelle to Isabelle-2013-2

* 0.6.0.0
- ported to Isabelle-2013 by Andreas Lochbihler
- removed buggy isabelle timout support
- tested compilation on GHC 7.4.2

* 0.5.0.0
- implemented proof generation for injective agreement
- fixed bug in unification of inverse-key constructors

* 0.4.1.0 Bugfixes and dropped export of library
- widen 'pretty' dependency
- update package description

* 0.4.0.0 Bugfixes and dropped export of library

- Compiles now with GHC 7.0.x, 7.2.x, 7.4.x
- Fixed some corner cases in unification code for key-inversion.
- Library is no longer exported, as there are no more users of it.
We split our internal development and the tamarin-prover provides its
own utility libraries.

* 0.3.2 Lexer improvements

- Also lex SLASH and BACKSLASH symbols.


* 0.3.1 Bugfix, small enhancement release

- Bugfix: Added missing cases for bidirectional shared keys in Message
deconstruction functions.

- Provide more precise warnings for internal certification checks. Improves
debugging experience.

- Updated documentation: UnionFind and .cabal project description

- Allow parsing of user-specified type assertions. For protocols with
nested encryptions, the inferred type assertions are sometimes not
precise enough. We handle these cases using user-specified type
assertions.

- Removed support for weak-atomicity, as it is subsumed by type assertions.

- Changed lexer to also recognize `!'

* 0.3.0 First public version

Aligned with paper submission for CCS'11: Provably repairing the ISO-9798
authentication protocols.
comments powered byDisqus