SAT-based Model-Checking of Security Protocols: Overview

The Problem

Even under the assumption of perfect cryptography, the design of security protocols is notoriously error-prone. Many published protocols have been implemented and deployed in real applications only to be found flawed years later. The problem is that often security protocols hide subtle flaws that are difficult to detect by a simple human inspection.

Our solution

We provide a fully automatic translation from security protocol specifications into propositional logic which can be effectively used to find attacks to security protocols. Our approach results from the combination of a reduction of protocol insecurity problems to planning problems and well-known SAT-reduction techniques developed for planning and LTL with the ultimate goal to build an automatic model-checker for security protocols based on state-of-the-art SAT solvers. We have implemented a SAT-based Model-Checker (SATMC) for security protocols. Experimental results obtained by thoroughly running SATMC against security protocols of growing complexity, from those in the Clark-Jacob's library to those, practically relevant in industrial environments, included in the AVISPA library clearly show that attacks are quickly found by state-of-the-art SAT solvers confirming the effectiveness of the SAT-based approach for the analysis of security protocols.

Future directions

We are currently investigating how to enhance our approach and our SATMC tool to scale at the level of services. Rather than security protocols, the security-relevant aspect of services and of their composition will be validated. Previous work on security protocol analysis will clearly provide one of the stepping stones for service validation as services often rely on security protocols to accomplish their goals. This is for instance the case of the SAML-based Single Sign-On service for Google Apps that uses SSL/TLS to secure the communication at the transport layer. SATMC has been recently run against the SAML-based Single Sign-On service for Google Apps service discovering a serious vulnerability. More information is available in [google2008].