ETH Zuerich - Homepage
Information Security



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.


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.




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:

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.


Jann Röder and Matthias Schmalz

An Embedded Security Protocol Logic in Isabelle/HOL

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.


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


Achim D. Brucker, Lukas Brügger, Matthias Krieger, and Burkhart Wolff


For more information (and dowload options) please visit the HOL-TestGen homepage:



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.


Achim D. Brucker and Burkhart Wolff


For more information (and dowload options) please visit the HOL-OCL homepage:


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.


Achim D. Brucker and Burkhart Wolff


For more information (and dowload options) please visit the HOL-Z homepage:


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

Fire Wall Testing Tool

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.


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.


Eugen Zalinescu and Matus Harvan

Process algebraic mid-point construction

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.


Petar Tsankov, Mohammad Torabi Dashti, and David Basin


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


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 15 September 2011