The OAuth 2.0 protocol allows users to grant relying parties access to resources at identity providers. In addition to being used for this kind of authorization, OAuth is also often employed for authentication in single sign-on (SSO) systems. OAuth 2.0 is, in fact, one of the most widely used protocols in the web for these purposes, with companies such as Google, Facebook, or PayPal acting as identity providers and millions of websites connecting to these services as relying parties. OAuth 2.0 is at the heart of Facebook Login and many other implementations, and also serves as the foundation for the upcoming SSO system OpenID Connect. Despite the popularity of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and were based on formal models which abstract from many web features or did not provide a formal treatment at all. In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization and authentication guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties and identity providers are considered as well. While proving security, we found two previously unknown attacks on OAuth, which both break authorization and authentication in OAuth. The underlying vulnerabilities are present also in the new OpenID Connect standard and can be exploited in practice. We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth provides the authorization and authentication properties we specify. More: http://arxiv.org/abs/1601.01229