LTL model-checking for security protocols

Article type: Other

Authors: Carbone, Roberto

Affiliations: Fondazione Bruno Kessler, Trento, Italy. Tel.: +39 0461 314 192; Fax: +39 0461 302 040; E-mail: carbone@fbk.eu

Abstract: This thesis is about the application of automated reasoning techniques to the formal analysis of security protocols. More in detail, it proposes a general model-checking framework for security protocols based on a set-rewriting formalism that, coupled with the use of Linear Temporal Logic, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analyzers. The approach successfully combines encoding techniques originally developed for planning with bounded model-checking techniques. The effectiveness of the approach proposed is assessed 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.

Keywords: Security protocols, bounded model-checking, planning, graphplan, propositional satisfiability (SAT)

DOI: 10.3233/AIC-2010-0489

Journal: AI Communications, vol. 24, no. 3, pp. 281-283, 2011