Beta 1


Title Using Static Analysis to Validate SAML Protocols
Author Skriver, Jakob
Hansen, Steffen M. (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Supervisor Nielson, Hanne Riis (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2004
Abstract Previous studies have successfully used static analysis to automatically validate security properties of classical protocols. In this thesis 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 protocols. The specifications of the protocols does not supply any security analysis. Different kinds of attacks are discussed and various recommendations on the security which must be used on each messages sent. We model the protocols using the process calculus LySa and using the static analysis tool LySa-tool we can analyse them. We are able to find flaws in the protocols even when following the recommendations of the specifications. The attacks found is also not discussed in the specifications. To help us writing the large LySa processes needed for SAML Single Sign- On we extend the LySa process calculus with macro language. This enables us to specify transport layer protocols and the protocols above with little effort.
Imprint Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
Keywords Protocol Validation; LySa; Static Analysis; Authentication; Authentication Protocols.
Fulltext
Original Postscript imm3396.ps (1.37 MB)
Derived PDF imm3396.pdf (0.73 MB)
Admin Creation date: 2006-06-22    Update date: 2012-12-21    Source: dtu    ID: 154802    Original MXD