Software: Open source Fixedpoint Model-Checker v.2009
Downloading:
Software: SATMC 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 Version 3.0 (December 2008)
Software: CL-AtseCL-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 v1 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 were 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.
Downloading:
|
