Software

• Rodin
• Currahee
• An Embedded Security Protocol Logic in Isabelle/HOL
• Generation of Test Cases from Automata
• Fire Wall Testing Tool
• A Cocoa GUI for the AVISPA Protocol Analyzer
• HOL-TestGen
• HOL-OCL
• HOL-Z
• OFMC
• Scyther
• PSL2BA
• LIRA
• A Software-based TPM Emulator for Linux
• XML-Diff
• MonPoly
• Process algebraic mid-point construction
  

The Rodin platform is the development environment for writing Event-B models and proving them consistent. Event-B is a formal method for modeling discrete state transition systems. Event-B supports refinement allowing the user to start from an abstract view of the system and to incrementally introduce more details later on.

Authors:

Rodin has been developed during the Rodin and is being developed during the Deploy project and therefore has several contributors. See the respective project homepages for the details.

The contributors among the information security group are Thai Son Hoang, Andreas Fürst, and Matthias Schmalz.

Homepages:

Rodin
Event-B

Currahee(E, iProver) is a theorem prover for TPTP problems with many irrelevant axioms. Currahee(E,iProver) applies a number of axiom selection strategies in parallel, and passes the resulting smaller problems to E and/or iProver. Currahee(E, iProver) version 0.1 has achieved the second rank in the LTB division of the CADE ATP systems competition of 2010.Currahee uses the following axiom selection strategies:

• a technique resembling the original idea underlying SInE,
• (contextual) direct and indirect relevance (Roederer A., Puzis Y., Sutcliffe G. (2009), Divvy: an atp meta-system based on axiom relevance ordering, CADE, pp. 157-162),
• Meng and Paulson's relevance filter for Sledgehammer (Meng J., Paulson L. C. (2009), Lightweight relevance filtering for machine-generated resolution problems, J. Applied Logic, pp. 41-57).

Note that there are versions of E and iProver, namely E-LTB and iProver-SInE, that have been specially designed for problems with many irrelevant axioms. Currahee(E, iProver) uses the "ordinary" versions of E and iProver instead of E-LTB and iProver-SInE.

Authors:

Jann Röder and Matthias Schmalz

The embedded security protocol logic (ESPL) is a security protocol verification theory formalized in Isabelle/HOL as a conservative definitional extension of higher-order logic. 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 was presented at CSF 2010.We also used ESPL and 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

Additional information and downloads

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, Lukas Brügger, Matthias Krieger, 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 is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle.

HOL-OCL defines a machine-checked formalization of the semantics as described in the standard for OCL 2.0. This conservative, shallow embedding of UML/OCL into Isabelle/HOL includes support for typed, extensible UML data models supporting inheritance and subtyping inside the typed λ-calculus with parametric polymorphism. As a consequence of conservativity with respect to higher-order logic (HOL), we can guarantee the consistency of the semantic model. Moreover, HOL-OCL provides several derived calculi for UML/OCL that allows for formal derivations establishing the validity of UML/OCL formulae. Automated support for such proofs is also provided.

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

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 the tool here.

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 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 is a prototype implementation of a monitoring tool that detects policy violations in log files. Policies are formalized by MFOTL formulae. The tool 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.
You can download the tool from here.

Authors:

Eugen Zalinescu and Matus Harvan

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:

• Framework for mid-point specification synthesis: mid-point.tar.bz2

To use the framework you need to install the mCRL toolset and the JFLAP tool.

• mCRL toolset: http://homepages.cwi.nl/~mcrl/
• JFLAP tool: http://www.cs.duke.edu/csed/jflap/