SAT-based Model-Checking of Security Protocols: Software

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.