Formal security analysis of the Shibboleth Web Single Sign On System using a comprehensive model of the web

Abstract

SAML is an open standard that enables information exchange regarding authorization and authentication. A prominent implementation of SAML is Shibboleth. Typically, Shibboleth is used for Web Single Sign On Systems (Web SSO), which enables users to authenticate at multiple services (Relying Parties) using a central identity service (Identity Provider). In this master thesis, a comprehensive formal security analysis for Shibboleth based on the "Web Infrastructure Model" (WIM) is presented. The Web Infrastructure Model is the most comprehensive formal model of the web up to today. The security of Shibboleth with regard to Authentication and Session Integrity is formally proven by using the WIM. During the analysis, some security flaws of Shibboleth were uncovered, which are described in this thesis. Furthermore, mitigations against these attacks are proposed and used for proving the security of Shibboleth. A novel security property, called Single Logout Consistency (SLO Consistency) is defined, which describes the security of the logout flow. This thesis shows that Shibboleth satisfies SLO Consistency as well.

SAML ist ein offener Standard, welcher den Austausch von Informationen über Authorisierung und Authentifizierung ermöglicht. Eine prominente SAML-Implementierung stellt hierbei Shibboleth dar. Typischerweise wird Shibboleth für Web Single Sign On (Web SSO) verwendet. Dabei können Nutzer sich bei verschiedenen Diensten (Relying Parties) authentifizieren, indem sie einen zentralen Dienst (Identity Provider) nutzen. In dieser Masterarbeit wird eine umfassende formale Sicherheitsanalyse für Shibboleth basierend auf dem ”Web Infrastructure Model“ (WIM) präsentiert. Das WIM ist derzeit das umfangreichste formale Modell des Webs. Die Sicherheit von Shibboleth bezüglich der Sicherheitseigenschaften Authentication und Session Integrity wird formal bewiesen mithilfe des WIMs. Durch die Analyse wurden einige Sicherheitslücken in Shibboleth entdeckt, welche ebenfalls in dieser Arbeit beschrieben werden. Außerdem wird aufgezeigt, wie die beschriebenen Angriffe vermieden werden können, und die vorgeschlagenen Korrekturen werden verwendet, um die Sicherheit von Shibboleth zu beweisen. Eine neuartige Sicherheitseigenschaft, genannt Single Logout Consistency (SLO Consistency), wird definiert, welche die Sicherheit eines Logout Flows beschreibt. In dieser Thesis wird bewiesen, dass Shibboleth diese Sicherheitseigenschaft ebenfalls erfüllt.