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.