SATMC (SAT-based Model Checker) is a bounded model checker for security protocols. SATMC reduces the problem of checking whether a protocol is vulnerable to attacks of bounded length to the satisfiability of a propositional formula which is solved by a state-of-the-art SAT solver. SATMC is one of the back-ends of the AVISPA Tool. An overview of SATMC is in [csf2007, ijis2007, compagnaPhD2005].