Design, Formal Specification and Analysis of Multi-Factor Authentication Solutions with a Single Sign-On Experience


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 protocol and can determine whether the concurrent execution of a finite number of sessions of the specified protocol satisfies the expected security properties inspite of the interference of a malicious intruder. The verification of the security properties is performed interfacing with state-of-the-art SAT solvers (MiniSat and zChaff are currently supported) and is based on the use of LTL logic.

For our analyses, we used SATMC (Version 3.5.7) launched within Eclipse using the STIATE Plugin (Version


  • SATMC+ STIATE Plugin + instructions to add STIATE Plugin in Eclipse are available here