
The Rodin platform is the development environment for writing EventB models and proving them consistent. EventB is a formal method for modeling discrete state transition systems. EventB 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 ELTB and iProverSInE, that have been specially designed for problems with many irrelevant axioms. Currahee(E, iProver) uses the "ordinary" versions of E and iProver instead of ELTB and iProverSInE.
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 higherorder logic. It allows for both the efficient interactive construction as well as the automatic generation of machinechecked 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 scytherproof tool to provide machinechecked 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 scytherproof tool together with the repaired and provenly correct protocol models.
Simon Meier, Cas Cremers, and David Basin
HOLTestGen is a is a test case generator for specification based unit testing. HOLTestGen is built on top of the specfication and theorem proving environment Isabelle/HOL. HOLTestGen allows one to
Achim D. Brucker, Lukas Brügger, Matthias Krieger, and Burkhart Wolff
For more information (and dowload options) please visit the HOLTestGen homepage: http://www.brucker.ch/projects/holtestgen/.
HOLOCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higherorder Logic (HOL) instance of the interactive theorem prover Isabelle.
HOLOCL defines a machinechecked 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 higherorder logic (HOL), we can guarantee the consistency of the semantic model. Moreover, HOLOCL 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 HOLOCL homepage: http://www.brucker.ch/projects/holocl/.
HOLZ is a proof environment for Z and HOL specifications based on ZeTa on the one hand and the generic theorem prover Isabelle (Version 980) on the other. ZeTa is essentially used as a typechecker for literate specifications in Z, that can be integrated into XEmacs as a combined editing and typechecking 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 (*.thyfiles). 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 HOLZ homepage: http://www.brucker.ch/projects/holz/.
OFMC is an onthefly modelchecker for the analysis of security protocols. The latest features include support for userdefined 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 firstorder logic over the reals and integers with addition and ordering. LIRA contains a highperformance 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.
Gerhard Zaugg, Adrian Schüpbach, Beat Strasser (supervision by Diana von Bidder)
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 Firstorder 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
The midpoint construction framework synthesizes a formal model for a midpoint that enforces a twoparty 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 midpoint enforcing the protocol. The framework is presented in the OPODIS'11 paper "Constructing Midpoints for Twoparty 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