We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
SATMC: a SAT-based model checker for security protocols, business processes, and security APIs.
- Authors
Armando, Alessandro; Carbone, Roberto; Compagna, Luca
- Abstract
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 a variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for different 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 Profile, 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).
- Subjects
SECURITY systems software; COMPUTER network protocols; COMPUTER checkers; WEB browsers; ENCODING
- Publication
International Journal on Software Tools for Technology Transfer, 2016, Vol 18, Issue 2, p187
- ISSN
1433-2779
- Publication type
Article
- DOI
10.1007/s10009-015-0385-y