In this research paper, the authors study the Organization for the Advancement of Structured Information Standards (OASIS) Security Assertion Markup Language (SAML) single sign-on (SSO) protocol in the framework of the LySa process calculus, developed by the University of Pisa and the Technical University of Denmark (part of Design Environments for Global Applications (DEGAS)). The goal is to track all possible messages communicated on the network, and to record potential violations of the destination/origin annotations.

After a summary of the main features of the SSO protocol, the authors present a somewhat simplistic formalization of it, with no specific security measures for the message transfer. This is mainly to validate the approach, through the analysis of the reported violations. The documents describing the SSO protocol recommend the use of the transport layer security (TLS) protocol, however, so the authors develop a model of TLS in LySa and integrate it with SSO in various scenarios, focusing on the nature (unilateral or bilateral) of the TLS connections between the actors (user, source, and destination sites). The analyzer validates some of them, and challenges the others. The paper contributes a valuable method for tackling the formidable task of validating security protocols.