OpenID 2.0 is a user-centric Web single sign-on protocol with over one billion OpenID-enabled user accounts, and tens of thousands of supporting websites. While the security of the protocol is clearly critical, so far its security analysis has only been done in a partial and ad-hoc manner. This paper presents the results of a systematic analysis of the protocol using both formal model checking and an empirical evaluation of 132 popular websites that support OpenID. Our formal analysis reveals that the protocol does not guarantee the authenticity and integrity of the authentication request, and it lacks contextual bindings among the protocol messages and the browser. The results of our empirical evaluation suggest that many OpenID-enabled websites are vulnerable to a series of cross-site request forgery attacks (CSRF) that either allow an attacker to stealthily force a victim user to sign into the OpenID supporting website and launch subsequent CSRF attacks (81%), or force a victim to sign in as the attacker in order to spoof the victim's personal information (77%). With additional capabilities (e.g., controlling a wireless access point), the adversary can impersonate the victim on 80% of the evaluated websites, and manipulate the victim's profile attributes by forging the extension parameters on 45% of those sites. Based on the insights from this analysis, we propose and evaluate a simple and scalable mitigation technique for OpenID-enabled websites, and an alternative man-in-the-middle defense mechanism for deployments of OpenID without SSL.