SATMC: a SAT-based Model Checker for Security-critical Systems

We present SATMC 3.0, a SAT-based bounded model checker for security-critical systems that stems from a successful combination of encoding techniques originally developed for planning with techniques developed for the analysis of reactive systems. SATMC has been successfully applied in variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for dierent purposes (design-time security analysis and security testing). SATMC strikes a balance between general purpose model checkers and security protocol analyzers as witnessed by a number of important success stories including the discovery of a serious man-in-the-middle attack on the SAML-based Single Sign-On (SSO) for Google Apps, an authentication flaw in the SAML 2.0 Web Browser SSO Prole, and a number of attacks on PKCS#11 Security Tokens. SATMC is integrated and used as back-end in a number of research prototypes (e.g. the AVISPA Tool, Tookan, the SPaCIoS Tool) and industrial-strength tools (e.g. the Security Validator plugin for SAP NetWeaver BPM).