Using static analysis to validate the SAML single sign-on protocol
Steffen M. Hansen, Jakob Skriver, Hanne Riis Nielson · 2005
Previous studies have successfully used static analysis to automatically validate authentication and confidentiality properties of classical key distribution protocols. In this paper we show how the very same technique can be used to validate modern web-based protocols, in particular, we study the SAML Single Sign-On protocol. The description of the protocol does not supply any security analysis but only lists various recommendations. One of these is to use versions of the TLS protocol for establishing secure connections between the principals. Using our static analysis tool we illustrate how some instantiations of the Single Sign-On protocol are flawed whereas others are not.