Using Static Analysis to Validate SAML Protocols |
Jakob Skriver, Steffen M. Hansen
|
| 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. |
| Keywords | Protocol Validation, LySa, Static Analysis, Authentication, Authentication Protocols. |
| Type | Master's thesis [Academic thesis] |
| Year | 2004 |
| Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU |
| Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby |
| Series | IMM-Thesis-2004-84 |
| Note | Supervised by Prof. Hanne Riis Nielson |
| Electronic version(s) | [pdf] [ps] |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |