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 ASLAN 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.3.4a is available at moment only for Linux. Release notes