Online citations, reference lists, and bibliographies.

SATMC: A SAT-based Model Checker For Security Protocols, Business Processes, And Security APIs

A. Armando, R. Carbone, L. Compagna
Published 2015 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
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).
This paper references
An Introduction to Security API Analysis
Riccardo Focardi (2011)
Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps
A. Armando (2008)
Encoding Plans in Propositional Logic
Henry A. Kautz (1996)
Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols
Alessandro Armando (2013)
Formal Analysis of Security APIs
Graham Steel (2011)
Requirements for modelling and ASLan v
AVANTSSAR. Deliverable 2.1 (2008)
An authentication flaw in browser-based Single Sign-On protocols: Impact and remediations
Alessandro Armando (2013)
Formal Models and Techniques for Analyzing Security Protocols: A Tutorial
Véronique Cortier (2011)
The SPIN Model Checker : Primer and Reference Manual
S. Nakajima (2004)
NuSMV 2: An OpenSource Tool for Symbolic Model Checking
A. Cimatti (2002)
An Extensible SAT-solver
N. Eén (2003)
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
A. Armando (2005)
Secure Pseudonymous Channels
S. Mödersheim (2009)
Formal Models and Techniques for Analyzing Security Protocols - Volume 5
Véronique Cortier (2011)
On the Specification of Secure Channels
G. Lowe (2007)
Formal Support to Security Protocol Development: A Survey
J. Pimentel (2008)
A survey of algebraic properties used in cryptographic protocols
V. Cortier (2006)
Scyther documentation
C J F Cremers
Model Checking of Security-Sensitive Business Processes
A. Armando (2009)
Call-by-Value Is Dual to Call-by-Name - Reloaded
P. Wadler (2005)
Handbook of satisfiability
Armin Biere (2009)
Nusmv version 2: an opensource tool for symbolic model checking
A. Cimatti (2002)
SATMC: A SATbased model checker for security-critical systems Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference
A Armando (2008)
PKCS#11: Cryptographic Token Interface Standard v2
Rsa Sec (2004)
The CL-Atse Protocol Analyser
Mathieu Turuani (2006)
Bounded Model Checking
Armin Biere (2009)
Analyzing a Library of Security Protocols using Casper and FDR
G. Lowe (1999)
Discovering Concrete Attacks on Website Authorization by Formal Analysis
Chetan Bansal (2012)
Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009. Proceedings
Michael Backes (2009)
An efficient cryptographic protocol verifier based on prolog rules
B. Blanchet (2001)
Finite-state analysis of two contract signing protocols
Vitaly Shmatikov (2002)
Attacking and fixing PKCS#11 security tokens
Matteo Bortolozzo (2010)
CSP (Communicating Sequential Processes)
A. W. Roscoe (2011)
LTL model checking for security protocols
A. Armando (2009)
Fast Planning Through Planning Graph Analysis
A. Blum (1995)
Symbolic Model Checking without BDDs
Armin Biere (1999)
SAT-based model-checking for security protocols analysis
A. Armando (2007)
Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers
T. Dimitrakos (2007)
FDR 2 System — Failures - Divergence Refinement
B. Donovan
Comparing State Spaces in Automatic Security Protocol Analysis
C. Cremers (2009)
OFMC: A symbolic model checker for security protocols
D. Basin (2004)
Security Validation of Business Processes via Model-Checking
Wihem Arsac (2011)
On the security of public key protocols
D. Dolev (1981)
SATMC: A SAT-Based Model Checker for Security Protocols
A. Armando (2004)
SATMC: A SAT-Based Model Checker for Security-Critical Systems
A. Armando (2014)
Improvements on the Genet and Klay technique to automatically verify security protocols
Yohan Boichut (2004)
Casper: a compiler for the analysis of security protocols
G. Lowe (1998)
OFMC: A Symbolic Model-Checker for Security Protocols
D. Basin (2004)
Business Process Compliance via Security Validation as a Service
L. Compagna (2013)
The SPaCIoS Project: Secure Provision and Consumption in the Internet of Services
Luca Viganò (2013)
P.,Nadeau, P.:Comparing state spaces in automatic security protocol analysis. In: Formal to practical security
C.J.F. Cremers (2009)
OFMC: A symbolic modelchecker for security protocols
D Basin (2004)
The CL-Atse protocol analyser Term rewriting and applications
M Turuani (2006)
A Comparative Analysis of Tools for Verification of Security Protocols
Nitish Dalal (2010)
The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
A. Armando (2012)

This paper is referenced by
Semantic Scholar Logo Some data provided by SemanticScholar