1LTL Model-Checking for Security Protocols Roberto Carbone ∗

Abstract. This thesis is about the application of auto-mated reasoning techniques to the formal analysis of security protocols. More in detail, it proposes a gen-eral model-checking framework for security protocols based on a set-rewriting formalism that, coupled with the use of Linear Temporal Logic, allows for the spec-ification of assumptions on principals and communi-cation channels as well as complex security properties that are normally not handled by state-of-the-art pro-tocol analyzers. The approach successfully combines encoding techniques originally developed for planning with bounded model-checking techniques. The effectiveness of the approach proposed is as-sessed against the formal analysis of relevant security protocols, with the detection of a severe security flaw in Google’s SAML-based SSO for Google Apps and a previously unknown attack on a patched version of the ASW contract signing protocol