Software: Open source Fixedpoint Model-Checker v.2010
The Open-source Fixedpoint Model Checker OFMC consists of two complementary modules. The classical module performs verification for a bounded number of transitions of honest agents using a constraint-based representation of the intruder behavior. The fixedpoint module allows for verification without restricting the number of steps by working on an over-approximation of the search space that is specified by a set of Horn clauses using abstract interpretation techniques and counterexample-based refinement of abstractions.
The OFMC tool-suite (click here for a figure) supports specifications written in AVANTSSAR’s standard input language ASLan or in the language AnB, based on Alice-and-Bob notation with special support for algebraic properties of operators, pseudonymous secure channel notation, and zero-knowledge proofs.
ASLan specifications are validated by running in parallel both the classical and the fixedpoint modules. When an attack (a violation of a goal) is found, it is immediately reported to the user. When no attack is found, the bound on the steps is increased and the analysis is repeated, i.e., whenever a specification has been completely verified for a certain number of sessions, it automatically starts again with a larger number of sessions (cf. the arrow labeled with K <- K+1 in the figure). Thus, for a correct protocol/service, the classical module will not terminate.
In the case of a positive result, one can use the computed fixedpoint to automatically generate a proof certificate for the Isabelle interactive theorem prover, via the automatic proof generator OFMC/Isabelle that was developed in collaboration by IBM and SAP. The idea is to gain a high reliability, since after this step the correctness of the verification result does no longer depend on the correctness of OFMC and the correct use of abstractions.
Two versions of OFMC are available:
– stable OFMC version 2011 (does not support full ASLan)
– experimental AVANTSSAR version 2010c (does not support the AnB format)
OFMC has been developed in the context of AVANTSSAR and its forerunner projects AVISPA and AVISS (which developed the On-the-fly Model Checker, the previous OFMC).
SATMC (SAT-based Model Checker) is an open and flexible platform for model-checking security protocols via reduction to SAT. SATMC takes as input a security problem expressed either in the IF or SATE languages and returns an attack, if any. SATMC has been currently extended to handle LTL formulae as a means to express both more complex security properties and constraints capturing assumptions on principals and communication channels that are normally not handled by state-of-the-art protocol analysers. SATMC can be interfaced with state-of-the-art SAT solvers. Interfaces for MiniSat and zChaff are currently supported. SATMC Version 3.0 is available both for Linux and the Windows operating systems.
- SATMC Licence, Documentation and Download
- Licence, Documentation and Download are available here.
For more informations visit SATMC website
CL-Atse is an OCaml-based implementation of the deduction rules developed in the CASRUL tool-suite, the AVISPA European project, and the AVANTSSAR European Project.
These rules allows anyone to interpret and automatically “execute” a protocol or more generally a web service in every possible ways against an generic intruder with the Dolev-Yao deductional capabilities.
A protocol, written in the Avispa’s intermediate format or in the newest ASLan language for AVANTSSAR is executed over a finite (user decided) number of iterations, or entirely if no loop is involved. There are no other restrictions: either an attack is found, or the protocol is claimed to be secured over the given number of sessions. The search for attacks can be parametrised. In particular, the service’s objects can be typed or untyped, and the pair can be free or (partially) associative.
Moreover, the analysis take care of the algebraic properties of the Xoroperator, as well as the exponential. That is, as attack can rely on the properties of these operators, and security means that no attack exists even when relying on the properties of these operators. Finally, CL-Atse performs two kind of optimizations : First, the protocol specification itself
is simplified to accelerate the search for attacks (steps merged or removed, useless messages ignored, etc..). Second, various optimizations in the deduction rules try to reduce, and often eliminate, redundancies and uselessness in the protocol execution.
CL-Atse was developed in the context of the EU Project AVISPA (Automated Validation of Internet Security Protocols and Applications,
www.avispa-project.org IST-2001-39252). Earlier development on CL-Atse took place in the context of the predecessor project AVISS (Automated Verification of Infinite-State Systems IST-2000-26410).
CL-Atse is now developped in the context of the EU Project AVANTSSAR (Automated VAlidatioN of Trust and Security of Service-oriented ARchitectures, www.avantssar.eu FP7-ICT-2007-1 Project no. 216471).
Even if the EU Project AVISPA is now closed, support for the two specification languages it defined is still up. In particular, CL-Atse accepts either IF (the Intermediate Format) files created by the AVISPA’s translator hlpsl2if, or HLPSL files if the translator is available to CL-Atse, or the new ASLan specification language from the AVANTSSAR Project. With AVANTSSAR, a translator also exists from Aslan++ to Aslan.