scyther-proof: Automatic generation of Isabelle/HOL correctness proofs for security protocols.

[ program, security, theorem-provers ] [ Propose Tags ]

scyther-proof is a security protocol verification tool based on a similar algorithm as the Scyther tool developed by Cas Cremers (http:/people.inf.ethz.chcremerscscytherindex.html). The theory underlying scyther-proof is described in the paper "Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs" by Meier, Cremers, and Basin. Parts of the infrastructure underlying scyther-proof are reused in other projects by the same author. Therefore, most of its modules are exported in the corresponding scyther-proof library. However, this library is not yet thought for general use. Please contact the author, if you would like to build upon/extend scyther-proof.

[Skip to Readme]
Versions [RSS] [faq] 0.3.0, 0.3.1, 0.4.0,,,,,,
Dependencies array (==0.3.*), base (==4.*), cmdargs (>=0.6.8 && <0.7), containers (>=0.3 && <0.5), directory (>=1.0 && <1.2), filepath (>=1.1 && <1.3), json (==0.4.*), mtl (==2.0.*), parsec (==3.1.*), pretty (==1.0.*), process (==1.0.*), safe (==0.2.*), tagsoup (==0.12.*), time (>=1.1 && <1.3), uniplate (==1.6.*) [details]
License LicenseRef-GPL
Copyright Simon Meier, ETH Zurich, 2009-2011
Author Simon Meier <>
Maintainer Simon Meier <>
Category Security, Theorem Provers
Home page
Uploaded by SimonMeier at 2011-05-13T18:37:08Z
Distributions NixOS:
Executables scyther-proof
Downloads 5676 total (23 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs uploaded by user
Build status unknown [no reports yet]





Build with support for multithreaded execution


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


Maintainer's Corner

For package maintainers and hackage trustees


Readme for scyther-proof-0.3.0

[back to package description]
README for the scyther-proof security protocol verification tool

Author: Simon Meier <>

Creation Date: 13/05/2011

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).

2. Installation instructions

2.1 Installing scyther-proof

  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.
  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


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

3.2 Installing the Isabelle/HOL theories

    Download and install full Isabelle2009-1 according to the installation
    instructions at

    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.

    For enabling interactive processing of theory files based using our
    extensions to Isabelle's ISAR proof language use one of the following two

      Variant a: Brute Force

          Overwrite the standard Emacs keywords file
          with the Emacs keywords file provided with the ESPL distribution.

          This is needed in order to make the new ISAR keywords "role",
          "protocol", "sources", and "prefix_close" available in the Emacs

      Variant b: Elegance

          A more elegant way is to copy the keywords file provided with our
          distribution to


          and start Isabelle using the -k switch as follows.

              isabelle emacs -k ESPL <your-theory-file.thy>


3. 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.

  In order to generate an Isabelle proof script two additional options need to
  be added

    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

   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 emacs Tutorial.thy

    or if you've chosen the elegant variant

	isabelle emacs -k ESPL Tutorial.thy

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

* Happy Proving :-)
* In case of questions do not hesistate to contact me at