Software

• The scyther-proof security protocol verification tool
  
• fwtest
• HOL-TestGen
• HOL-OCL
• HOL-Z
• OFMC
• PSL2BA
• LIRA
• MonPoly
• Process algebraic mid-point construction framework
• SecFuzz
• Tamarin prover
• ProtoVeriPhy
  

The scyther-proof security protocol verification tool

scyther-proof implements a proof-generating version of the algorithm underlying the Scyther security protocol verification tool. The resulting proofs can be visualized and machine-checked using our security protocol verification theory formalized in Isabelle/HOL. Note that this theory is of independent interest, as it allows for both the efficient interactive construction as well as the automatic generation of machine-checked protocol security proofs. The paper "Strong Invariants for the Efficient Construction of Protocol Security Proofs" documenting this theory and its tool support was presented at CSF 2010. A journal version of this paper will appear in the Journal of Computer Security.

Verification of our fixes to the ISO/IEC 9798 standard

We also used the corresponding scyther-proof tool to provide machine-checked proofs of repaired versions of the authentication protocols from the ISO/IEC 9798 standard. The following two files provide the original protocol models to be used with the Scyther security protocol analysis tool and the scyther-proof tool together with the repaired and provenly correct protocol models.

• iso9798-original-scyther-models_20110513.tar.gz
• scyther-proof_and_iso-9798-repaired-model-proofs_20110513.tar.gz
  

Authors:

Simon Meier, Cas Cremers, and David Basin

Homepage:

See our homepage for additional information and downloads.

HOL-TestGen

HOL-TestGen is a is a test case generator for specification based unit testing. HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle/HOL. HOL-TestGen allows one to

• write test specifications in Higher-order logics (HOL)
• (semi-) automatically partition the input space, resulting in abstract test cases
• automatically select concrete test data
• automatically generate test harnesses (in SML)
• using a foreign language interface, implementations in arbitrary languages (e.g. C) can be tested.

Authors:

Achim D. Brucker and Burkhart Wolff

Homepage:

For more information (and dowload options) please visit the HOL-TestGen homepage: http://www.brucker.ch/projects/hol-testgen/.

HOL-OCL

Authors:

Achim D. Brucker and Burkhart Wolff

Homepage:

For more information (and dowload options) please visit the HOL-OCL homepage: http://www.brucker.ch/projects/hol-ocl/.

HOL-Z

HOL-Z is a proof environment for Z and HOL specifications based on ZeTa on the one hand and the generic theorem prover Isabelle (Version 98-0) on the other. ZeTa is essentially used as a type-checker for literate specifications in Z, that can be integrated into XEmacs as a combined editing and type-checking frontend. ZeTa has been extended by a plugin, that converts Z sections into a new format (*.holz) that can be loaded alternatively to Isabelles standard theory files (*.thy-files). Thus, theory contexts can be created in which theorem proving for specifications of realistic size can be realized.

Authors:

Achim D. Brucker and Burkhart Wolff

Homepage:

For more information (and dowload options) please visit the HOL-Z homepage: http://www.brucker.ch/projects/hol-z/.

OFMC

OFMC is an on-the-fly model-checker for the analysis of security protocols. The latest features include support for user-defined algebraic theories.
Download and more information at the OFMC homepage.

PSL to Büchi Automaton Translator

The psl2ba tool translates formulas of the IEEE standard "Property
Specification Language" (PSL) into Büchi automata. These automata are
used in the model checkers NuSMV, SMV, and SPIN.

Download:

Download the tool here.

Linear Integer/Real Arithmetic Solver

Decision procedures for Presburger arithmetic and the first-order logic over the reals and integers with addition and ordering. LIRA contains a high-performance automata library for deterministic finite automata and weak deterministic Büchi automata.Download and more information at the LIRA homepage.

fwtest

fwtest is a tool for firewall testing. fwtest reads a test specification as input, generates and injects the corresponding network packets (at the moment: TCP, UDP and ICMP) and then compares the test outcome with the expectations.

Authors:

Gerhard Zaugg, Adrian Schüpbach, Beat Strasser (supervision by Diana von Bidder)

Documentation & Software:

• original fwtest (TCP)
• UDP and ICMP extension
• NAT capability

MonPoly

MonPoly is a prototype monitoring tool that checks compliance of log files with respect to policies. Policies are specified by formulas in metric first-order temporal logic. The tool was presented at the RV'11 conference and it implements the algorithm presented in the FSTTCS'08 paper Runtime Monitoring of Metric First-order Temporal Properties by David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann. MonPoly can be download at https://projects.developer.nokia.com/MonPoly.

Process Algebraic Mid-Point Construction Framework

The mid-point construction framework synthesizes a formal model for a mid-point that enforces a two-party asynchronous protocol. The framework takes as an input the formal specifications of the protocol and the environment, given in the muCRL process algebraic language, and outputs a specification for a mid-point enforcing the protocol. The framework is presented in the OPODIS'11 paper "Constructing Mid-points for Two-party Asynchronous Protocols" by Petar Tsankov,  Mohammad Torabi Dashti, and David Basin.

Authors:

Petar Tsankov, Mohammad Torabi Dashti, and David Basin

Downloads:

• Download the framework for mid-point specification synthesis: mid-point.tar.bz2

SecFuzz: Fuzz-testing Security Protocols

SecFuzz tests security protocol implementation for failures. SecFuzz uses a concrete protocol implementation for generating valid inputs for the SUT and then mutates them using a set of fuzz operators. The SUT is checked for failures using a dynamic memory analysis tools such as Valgrind and IBM's Rational Purify. SecFuzz is implemented in Python and relies on Scapy for parsing messages. Currently, the tool can fuzz-test IKE implementations, but it can be extended to other message formats due to Scapy's flexibility.

Author:

Petar Tsankov

Downloads:

• ike_fuzzer-0.1.tar.bz2
• README.txt
  

Software dependencies:

• Python 2.6+
• Scapy (http://www.secdev.org/projects/scapy/)
• Openswan 2.6.37 (http://openswan.org/)
• Tcpdump (http://www.tcpdump.org/)

Tamarin Prover

The Tamarin prover is a security protocol verification tool that support both falsification and unbounded verification of security protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined subterm-convergent rewriting theory.

The paper explaining the theory behind the Tamarin prover has been accepted at CSF'12. An extended version of the paper is also available.

Authors:

Simon Meier, Benedikt Schmidt

Installation:

The Tamarin prover is implemented in Haskell and available from Hackage. It uses maude as a unification backend and GraphViz to visualize the constraint systems. It compiles on Linux, Mac OS X, and Windows using GHC 7.x. Below we give step-by-step instructions for installing the Tamarin prover from source code on Linux and Mac OS X. If you cannot compile from source code, you can try the binaries for Windows and Mac OS X. Please do not hesitate to contact us, if you encounter trouble installing or using the Tamarin prover.

Linux

1. Use your package manager to install maude, graphviz, and the zlib1g header files. On Ubuntu 11.10:
   

   sudo apt-get install maude graphviz zlib1g-dev

2. Use your package manger to install the Haskell platform, if available. Otherwise, install GHC 7.x, cabal-install, alex and happy. On Ubuntu 11.10:
   

   sudo apt-get install ghc happy alex cabal-install

3. Update the package database of the Haskell cabal tool
   

   cabal update
   

   and install the Tamarin prover together with all its Haskell library dependencies, which might take some time.
   

   cabal install tamarin-prover
   

   In some cases you might have to add the flag --force-reinstalls, as explained by the message output by cabal. Depending on your Linux distribution installing some of the dependencies might fail due to missing development packages. Check the installation log for the missing C-library and use your package manager to install the corresponding '-dev' package; e.g., zlib1g-dev for the zlib compression library on Ubuntu.

4. The 'tamarin-prover' executable is installed in '~/.cabal/bin'. Add this directory to your PATH or call the Tamarin prover as follows.
   

   ~/.cabal/bin/tamarin-prover
   

   This will display the possible options for calling the Tamarin prover. It also outputs the paths to the installed example protocol models and the case studies from our paper. We recommend opening the Tutorial.spthy example file in a text editor and start exploring from there. Happy proving :-)

Mac OS X

1. Install Core Maude 2.6 and graphviz and make sure that they are on your PATH.
   
2. Install the Haskell platform for Mac.
3. Update the package database of the Haskell cabal tool
   

   cabal update
   

   and install the Tamarin prover together with all its Haskell library dependencies, which might take some time.
   

   cabal install tamarin-prover
   

4. The 'tamarin-prover' executable is installed in '~/Library/Haskell/bin'. Add this
   directory to your PATH or call the Tamarin prover as follows.
   

   ~/Library/Haskell/bin/tamarin-prover
   

   Note that if you already have installed an older version of tamarin, 'tamarin-prover' can be found in a different directory which is printed at the end of the installation. The above command invocation will display the possible options for calling the Tamarin prover. It also outputs the paths to the installed example protocol models and the case studies from our paper. We recommend opening the Tutorial.spthy example file in a text editor and start exploring from there. Happy proving :-)

ProtoVeriPhy

ProtoVeriPhy is an Isabelle/HOL framework for analyzing physical protocols such as distance bounding protocols, secure time-synchronization protocols, and authenticated ranging protocols.

There are two versions of the framework. The original version and an extended version that accounts for overshadowing attacks.

The original version is described in the articles "Formal Reasoning about Physical Properties of Security Protocols" (TISSEC'11) and "Let's get physical: Models and Methods for Real-World Security Protocols" (TPHOLS'09). It includes support for reasoning about XOR and authenticated ranging, distance bounding, broadcast authentication, and secure time synchronization protocols as case studies:

Isabelle theories and proofs:

• Proof Outline: outline.pdf
• Proof Document: document.pdf
• Theory files: ProtoVerPhy-20090616.tar.gz

An extended version that accounts for overshadowing attacks is described in "Distance Hijacking Attacks on Distance Bounding Protocols" (Security&Privacy'12). This version includes proofs that the Brands-Chaum protocol and a wrongly fixed version are vulnerable to Distance-Hijacking attacks. Additionally, it contains proofs that our proposed fixes indeed prevent these attacks.

Isabelle theories and proofs:

• Proof Outline: outline.pdf
• Proof Document: document.pdf
• Theory files: ProtoVeriPhy-20120305.tar.gz

Authors:

Benedikt Schmidt, Patrick Schaller