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
Share
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
10.1007/978-3-642-23082-0_2
An Introduction to Security API Analysis
Riccardo Focardi (2011)
10.1145/1456396.1456397
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)
10.1007/978-3-642-38631-2_63
Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols
Alessandro Armando (2013)
10.1007/978-1-4419-5906-5_873
Formal Analysis of Security APIs
Graham Steel (2011)
Requirements for modelling and ASLan v
AVANTSSAR. Deliverable 2.1 (2008)
10.1016/j.cose.2012.08.007
An authentication flaw in browser-based Single Sign-On protocols: Impact and remediations
Alessandro Armando (2013)
10.1561/2500000001
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)
10.1007/3-540-45657-0_29
NuSMV 2: An OpenSource Tool for Symbolic Model Checking
A. Cimatti (2002)
10.1007/978-3-540-24605-3_37
An Extensible SAT-solver
N. Eén (2003)
10.1007/11513988_27
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
A. Armando (2005)
10.1007/978-3-642-04444-1_21
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)
10.13053/CYS-12-1-1190
Formal Support to Security Protocol Development: A Survey
J. Pimentel (2008)
10.3233/JCS-2006-14101
A survey of algebraic properties used in cryptographic protocols
V. Cortier (2006)
Scyther documentation
C J F Cremers
10.1007/978-3-642-12459-4_6
Model Checking of Security-Sensitive Business Processes
A. Armando (2009)
10.1007/978-3-540-32033-3_15
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)
10.1007/11805618_21
The CL-Atse Protocol Analyser
Mathieu Turuani (2006)
10.3233/978-1-58603-929-5-457
Bounded Model Checking
Armin Biere (2009)
Analyzing a Library of Security Protocols using Casper and FDR
G. Lowe (1999)
10.1109/CSF.2012.27
Discovering Concrete Attacks on Website Authorization by Formal Analysis
Chetan Bansal (2012)
10.1007/978-3-642-04444-1
Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009. Proceedings
Michael Backes (2009)
10.1109/CSFW.2001.930138
An efficient cryptographic protocol verifier based on prolog rules
B. Blanchet (2001)
10.1016/S0304-3975(01)00141-4
Finite-state analysis of two contract signing protocols
Vitaly Shmatikov (2002)
10.1145/1866307.1866337
Attacking and fixing PKCS#11 security tokens
Matteo Bortolozzo (2010)
10.1007/978-0-387-09766-4_186
CSP (Communicating Sequential Processes)
A. W. Roscoe (2011)
10.3166/jancl.19.403-429
LTL model checking for security protocols
A. Armando (2009)
10.1016/S0004-3702(96)00047-1
Fast Planning Through Planning Graph Analysis
A. Blum (1995)
10.1007/3-540-49059-0_14
Symbolic Model Checking without BDDs
Armin Biere (1999)
10.1007/s10207-007-0041-y
SAT-based model-checking for security protocols analysis
A. Armando (2007)
10.1007/978-3-540-75227-1
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
10.1007/978-3-642-02002-5_5
Comparing State Spaces in Automatic Security Protocol Analysis
C. Cremers (2009)
10.1007/s10207-004-0055-7
OFMC: A symbolic model checker for security protocols
D. Basin (2004)
10.1007/978-3-642-19125-1_3
Security Validation of Business Processes via Model-Checking
Wihem Arsac (2011)
10.1109/TIT.1983.1056650
On the security of public key protocols
D. Dolev (1981)
10.1007/978-3-540-30227-8_68
SATMC: A SAT-Based Model Checker for Security Protocols
A. Armando (2004)
10.1007/978-3-642-54862-8_3
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)
10.3233/JCS-1998-61-204
Casper: a compiler for the analysis of security protocols
G. Lowe (1998)
10.3929/ETHZ-A-006744596
OFMC: A Symbolic Model-Checker for Security Protocols
D. Basin (2004)
10.1109/ICST.2013.63
Business Process Compliance via Security Validation as a Service
L. Compagna (2013)
10.1109/ICST.2013.75
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)
10.4236/ijcns.2010.310104
A Comparative Analysis of Tools for Verification of Security Protocols
Nitish Dalal (2010)
10.1007/978-3-642-28756-5_19
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