PaperlayerView exact revision on arXiv

Source-linked AI summary

A Comprehensive Formal Security Analysis of OAuth 2.0

Daniel Fett, Ralf Kuesters, Guido Schmitz

arXiv:1601.01229v4cs.CR

TL;DR

OAuth 2.0 is widely deployed, but prior analyses generally focused on implementations or simplified web models. This paper formally analyzes all four grant modes in an expressive web model, discovers and fixes four attacks, and proves strong OAuth security properties under recommended practices.

  • Problem

    Prior OAuth security work largely analyzed specific implementations and did not comprehensively model all modes and realistic web interactions.

  • Method

    The paper builds an expressive formal web model of OAuth covering all four grant types, simultaneous executions, recommended practices, and malicious parties.

  • Results

    The analysis found four practical attacks, proposed fixes, and proved authorization, authentication, and session integrity for fixed OAuth under recommended practices.

  • Takeaways & Limitations

    The results provide implementation guidelines for secure OAuth and show that security cannot be guaranteed when recommendations and best practices are not followed.

  • Takeaways & Limitations

    The model does not include expiration, revocation, or user logout, and the OAuth proof does not directly imply OpenID Connect security.

Abstract

from arXiv · show

The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols and also serves as the foundation for the new SSO standard 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, authentication, and session integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types (authorization code grant, implicit grant, resource owner password credentials grant, and the client credentials grant) are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identity providers, and browsers are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed, in order to avoid obvious and known attacks. When proving the security of OAuth in our model, we discovered four attacks which break the security of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect. 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 (with security recommendations and best practices in place) provides the authorization, authentication, and session integrity properties we specify.

1. Introduction

The paper addresses the lack of comprehensive formal security analysis for OAuth 2.0 by modeling all four modes in an expressive web setting. It identifies four attacks, proposes fixes, and proves strong security properties for the fixed protocol under recommended practices.

  • Research gap: Existing OAuth analyses mostly targeted specific implementations and commonly omitted simultaneous execution of all modes or comprehensive web features.The paper argues that realistic browser and server interactions are needed to assess web-based security risks.
  • Scope and model: The analysis covers authorization code, implicit, resource owner password credentials, and client credentials modes, including simultaneous runs across RPs and IdPs.Malicious relying parties, identity providers, and browsers/users are included in the model.
  • Scope and model: The OAuth model uses an expressive Dolev-Yao-style web model that captures substantial browser, server, HTTP, HTML5, JavaScript, and web-messaging behavior.The model includes windows, documents, iframes, cookies, navigation rules, web storage, postMessage, and XHRs.
  • Security properties: The paper formalizes authorization, authentication, and session integrity as three central OAuth security properties.Session integrity concerns both authorization and authentication.
  • Attacks and fixes: The analysis discovered four attacks affecting OAuth and OpenID Connect, verified them on actual implementations, and produced fixes confirmed by the respective working groups.The attacks include credential forwarding, IdP mix-up, forced attacker login, and substitution of an attacker’s resource.
  • Security results: With fixes and recommended security practices in place, the authors prove strong authorization, authentication, and session integrity properties for OAuth.The results provide implementation guidelines, while noncompliance leaves security unguaranteed.
  • Scope boundary: The OAuth proof does not directly establish OpenID Connect security because OpenID Connect adds protocol-specific details.A formal analysis of OpenID Connect is left for future work.

Structure of this Paper.

This section introduces OAuth’s purpose, registration and authorization-code flow, related grant modes, and the paper’s organization. It explains how tokens support authorization or authentication and how user intention is tracked across identity providers.

  • OAuth overview: OAuth lets users grant relying parties access to protected resources held by identity providers, and it is also commonly used for authentication.The paper gives IFTTT accessing Facebook data as an authorization example and Facebook-to-Pinterest login as an authentication example.
  • Registration: Before interacting with an identity provider, a relying party registers credentials and one or more redirection endpoint URIs.The identity provider assigns a public client ID and optionally a client secret; redirect URI registration may use exact URIs or patterns.
  • Authorization code mode: In authorization code mode, the user authenticates at the identity provider, returns with an authorization code, and the relying party exchanges it for an access token.The exchange includes the client ID, client secret, and redirect URI checks.
  • Token use: The relying party uses the access token either to access protected resources or to retrieve a user identifier and issue a session cookie.The latter path supports authentication at the relying party.
  • User intention tracking: Multi-identity-provider relying parties track user intention either through distinct redirect URIs or by storing the intended provider in a session.These are called naïve and explicit user intention tracking, respectively.
  • Other grant modes: In implicit mode, the identity provider returns an access token in the URI fragment, which relying-party JavaScript retrieves because fragments are not sent in HTTP requests.The relying party can then use the token for authorization or authentication.
  • Other grant modes: The resource owner password credentials mode gives the relying party the user’s identity-provider credentials and is intended for highly trusted applications or browserless settings.The relying party authenticates to the identity provider on the user’s behalf.
  • Other grant modes: Client credentials mode runs without user interaction and obtains a token for resources belonging to the relying party.The paper’s example is access to advertising-performance reports.

3. Attacks

The analysis identifies four OAuth attacks, including credential leakage through 307 redirects and IdP mix-up attacks that enable impersonation or unauthorized access. The attacks also apply to OpenID Connect, while requiring specific protocol or deployment conditions.

  • Overview: Four attacks are identified: 307 redirect, IdP mix-up, state leak, and naïve RP session integrity attacks.The analysis presents fixes and formally evaluates their sufficiency for OAuth security.
  • Scope: The attacks apply to OpenID Connect, and the authors verified them on actual OAuth and OpenID Connect implementations.The attacks were reported to the relevant working groups, which confirmed them.
  • 307 Redirect Attack: A malicious RP can learn user credentials when an IdP redirects a credential-submitting POST request with HTTP 307.The browser preserves the POST body and sends it to the RP; the attack breaks authorization and authentication.
  • 307 Redirect Attack: OAuth’s redirect wording permits arbitrary user-agent redirection methods, although only HTTP 303 unambiguously drops a POST body.The proposed fix requires 303 redirects for the relevant credential-submission steps.
  • IdP Mix-Up Attack: In an IdP mix-up attack, a network attacker makes the RP confuse the chosen honest IdP with a malicious IdP, exposing an authorization code or access token.The attacker can then use the information to impersonate the user or access user data; the attack applies to authorization code and implicit modes.
  • IdP Mix-Up Attack: The IdP mix-up attack relies on manipulating the user–RP exchange, supporting multiple honest and malicious IdPs, and using explicit user-intention tracking with shared redirect URIs.The attack does not require intercepting server-to-server communication; manipulation of the initial messages can suffice.

Attack on Authorization Code Mode.

The authorization-code analysis identifies IdP mix-up as a protocol flaw that can break authorization and authentication, alongside related session attacks and proposed fixes.

  • IdP Mix-Up Attack: An attacker can replace the honest IdP with an attacker-controlled IdP, causing the RP to redeem a code at the wrong provider.The RP misattributes the nonce to the attacker-controlled IdP, leaking the code to the attacker.
  • Breaking Authorization: If no client secret protects the honest IdP registration, the attacker can redeem the leaked code for an access token and access the user’s protected resources.This breaks the authorization property.
  • Breaking Authentication: The attacker can also use the obtained code in a new login session to impersonate the honest user at the RP.The attack uses a fresh state parameter and session cookie to imitate a real login.
  • Web-Attacker Variant: A web-attacker variant redirects a user from an attacker-controlled IdP to the honest IdP without intercepting network messages.The unexpected IdP transition may be detectable by a vigilant user.
  • Fix: The fundamental flaw is that redirects do not reliably identify their originating IdP, even when HTTPS protects communication.The proposed fix adds an attacker-influence-resistant IdP identity parameter to the redirect URI, which the RP checks.

State Leak at IdPs.

The state-leak attack uses referrer leakage to compromise RP session integrity, while the proposed mitigations limit state reuse and suppress sensitive referrer data.

  • Fix: The proposed fix limits state to a single use and applies referrer policies that suppress or reduce the Referer header.The model permits only the origin in Referer headers for RP and IdP pages, and the proof shows protection against state and code leakage.
  • Naïve RP Session Integrity: A separate naïve-RP session-integrity attack remains possible because the RP does not track which IdP the user intended to use.The attacker redirects an authentication result from the honest IdP through the attacker-controlled IdP.
  • OpenID Connect: The four attacks also apply to OpenID Connect, with the 307 redirect, state leak, and naïve session-integrity attacks transferring directly.The IdP mix-up attack applies to OpenID Connect authorization-code and hybrid modes.
  • Implementation Checks: The researchers verified selected attacks in several implementations and reported them to the relevant working groups, which confirmed the attacks.The IdP mix-up attack led to a draft RFC using the proposed fix.

4. FKS Model

The FKS model provides a Dolev–Yao-style formal web environment for representing browsers, servers, scripts, attackers, messages, and protocol executions.

  • Model Foundation: The analysis extends the FKS model, an application-independent Dolev–Yao web model designed to mirror web standards and specifications.The model is intended to capture realistic browser-server interactions.
  • Communication and Execution: Processes communicate through events carrying messages and sender and receiver addresses, with executions formed by nondeterministic event delivery.A process updates its state and emits events after receiving an event.
  • Message Representation: Web requests are formal terms containing nonces, methods, domains, paths, URI parameters, headers, and bodies.HTTPS requests encrypt the request and a fresh symmetric key under the responder’s public key.
  • Equational Theory: The equational theory defines term equivalence and cryptographic operations such as asymmetric encryption and decryption.For example, decrypting an encrypted term with the corresponding private key yields the original term.
  • Attackers: The model represents attackers as processes that derive and output all messages possible from their recorded information.Network attackers can listen to and spoof all addresses, while web attackers are restricted to their own addresses.
  • Browsers and Scripts: Browser models include windows, documents, cookies, web storage, scripts, HTTP(S) requests, XHRs, and relevant headers.Scripts receive accessible browser state and return commands plus updated internal state.

5. Analysis

The analysis instantiates the web model for OAuth with comprehensive configuration choices, attacker capabilities, and security recommendations intended to support formal security proofs.

  • Analysis Setup: The analysis models OAuth with the proposed fixes, formalizes its security properties, and states a theorem establishing security for the fixed protocol.The proof details appear in Appendices F–I.
  • Analysis Setup: The OAuth model follows RFC6749, incorporates security recommendations and web best practices, and extends the FKS model with HTTP Basic Authentication and Referrer Policies.These additions address protocol underspecification and known implementation attacks.
  • Configuration Scope: Every relying party and identity provider may run any of OAuth’s four modes, including simultaneous execution.The modes may run within the same or different parties.
  • Attacker and URI Assumptions: The model permits corruption of relying parties, identity providers, and browsers by the attacker at any time.It also allows loose redirect-URI checking, which strengthens the security guarantees proved.
  • Web and Session Assumptions: The model permits HTTP and HTTPS use, arbitrary navigation and multiple simultaneous login flows, while representing RP sessions with cookies.Strict-Transport-Security is recommended in practice but not required by the model.
  • Authentication and Honest-Party Assumptions: The analysis assumes username-password authentication at IdPs and excludes untrusted third-party JavaScript, open redirectors, and XSS at honest parties.The user sends passwords only through encrypted channels to their intended IdP or trusted RP.
  • Security Requirements: The model uses session-bound fresh state nonces, origin checks, access-token client-id checks, and explicit user-intention tracking.These requirements address CSRF, token misuse, and the naïve RP session-integrity attack.
  • Security Concepts: OAuth protected resources are modeled abstractly as resources an RP can use at an IdP after authorization.The abstraction follows RFC6749 and covers data or services.

Concepts Used in Our Model.

The model represents OAuth web systems with relying parties, identity providers, browsers, and attackers, then defines authorization, authentication, and session-integrity properties. It also states modeling boundaries, including omitted token expiration, revocation, logout, resource scoping, and error messages.

  • OAuth Web Systems: OAuth web systems contain finite sets of relying parties, identity providers, and browsers, modeled alongside either a network attacker or web attackers.The network-attacker system includes OAuth flows and mitigations; the web-attacker system is used to analyze session integrity.
  • Model Limitations: The model omits expiration, revocation, logout, detailed resource scopes, and identity-provider error messages.It overapproximates refresh-token behavior by leaving access tokens unexpired and gives relying parties full access to user data at the identity provider.
  • Security Properties: Authorization requires that attackers obtain protected resources only when the identity provider, user’s browser, or trusted relying party is corrupted.Resources acquired in client credentials mode are not bound to a user.
  • Security Properties: Authentication requires that attackers obtain an honest relying party’s service token for a user only when the identity provider, user’s browser, or trusted relying party is corrupted.The service token represents being logged in at the relying party under that identity.
  • Security Properties: Session integrity requires user initiation of OAuth flows and, with an honest identity provider, completion under the same identity the user selected.The authorization formulation concerns access to protected resources, while the authentication formulation concerns the resulting login identity.
  • Session Integrity: Session-integrity analysis uses web attackers because network attackers can force login under their own account and defeat existing CSRF defenses.The paper notes that more robust solutions using web messaging or web storage are conceivable but less common and typically outside the OAuth standard.

Main Theorem.

The paper provides an extensive formal analysis of OAuth 2.0 in a comprehensive web model, revealing attacks and proving security after fixes and recommended practices are applied.

  • Security conditions: The security guarantee depends on following OAuth security recommendations and best practices; otherwise, security cannot be guaranteed.The paper therefore provides precise implementation guidelines, while noting that individual deployments may not satisfy them.
  • Prior limitations: Earlier work largely focused on implementation errors, limited OAuth modes, or web models that omitted important browser and web features.Related formal results often imposed restrictions such as one identity provider per relying party or honest identity providers.
  • Scope and contribution: The analysis targets OAuth 2.0 itself rather than specific implementations, covering all modes, options, malicious parties, and corrupted browsers or users.It also models simultaneous operation across the same and different relying parties and identity providers.
  • Attacks and fixes: The analysis revealed four attacks affecting OAuth and OpenID Connect, verified them, proposed fixes, and reported them to the relevant working groups.The working groups confirmed the attacks, and fixes or recommendations were under discussion or incorporated into an RFC draft.
  • Main theorem: With the fixes applied, the authors proved strong authorization, authentication, and session integrity properties for OAuth 2.0.Session integrity concerns both authorization and authentication.
  • Future work: A formal analysis of OpenID Connect is identified as an obvious next step because OAuth underlies that protocol.The paper presents its OAuth analysis as a starting point for that future work.

A. OAuth 2.0

This section introduces OAuth’s modes, endpoints, assumptions, and protocol flows, then describes attacks affecting OAuth and OpenID Connect.

  • Protocol setup: OAuth uses authorization endpoints for user authentication and consent, token endpoints for access tokens, and registered redirection endpoints for browser returns.The analysis follows HTTPS and common session-cookie practices, while registration details remain outside the protocol.
  • Protocol setup: The analysis covers OAuth options including client secrets, redirect-URI selection, URI patterns, and state values bound to browser sessions.These choices are included in the formal analysis to model CSRF defenses and deployment variations.
  • OAuth modes: In implicit mode, the IdP sends an access token directly through the browser in the redirect URI fragment rather than issuing an authorization code.The mode is more suitable for browser applications because the RP does not authenticate with a client secret.
  • Attacks: The IdP mix-up attack redirects the browser among attacker- and honest-IdP endpoints, causing the RP to use a token with the wrong IdP.The attack can leak tokens and enable impersonation of the honest user.
  • Attacks: The identified attacks also affect OpenID Connect, including credential forwarding through HTTP 307 redirects and authorization or authentication failures in hybrid mode.The hybrid-mode attacks can expose protected resources or let an attacker impersonate the honest user.

Atomic Dolev-Yao Processes.

This section defines the formal terms and processes used to model web systems, attackers, scripts, messages, dictionaries, URLs, origins, and cookies.

  • Processes and systems: Derivable terms are constructed from ground messages and placeholders using terms over substituted variables.The derivability relation underlies Dolev-Yao process outputs.
  • Processes and systems: A Dolev-Yao process restricts initial states and transitions so outputs are derivable from the triggering event and process state.This formalizes symbolic message processing.
  • Processes and systems: Scripts model client-side technologies such as JavaScript and output derivable state-plus-command terms interpreted by the browser.The attacker script outputs everything derivable from its input.
  • Processes and systems: A web system partitions processes into honest, web-attacker, and network-attacker sets, with address restrictions distinguishing local spoofing from network interception.Runs begin from an infinite event sequence that triggers system processes.
  • Web notation: The notation defines dictionaries, pointers, URLs, origins, and cookies used to represent browser data and web messages.Cookie attributes determine HTTPS transmission, deletion on browser close, and JavaScript access.
  • Web notation: Cookies are named values with secure, session, and httpOnly flags, while HTTP requests include a nonce that maps each response to its request.The secure and httpOnly attributes constrain network and script access respectively.

D.7. DNS Servers

The model introduces a flat DNS abstraction and formalizes browser state, navigation, document access, cookies, and browser-event processing.

  • D.7. DNS Servers: DNS queries are answered directly by one server using a fixed domain-to-address mapping.The model notes that hierarchical DNS could instead be modeled for attacks on DNS itself.
  • Web browser model: Browser windows contain documents, with exactly one active document when nonempty and a nonce serving as the window reference.The opener field records the nonce of a window that opened a top-level window.
  • Web browser model: Subwindows and active documents are represented as minimal pointer sets that recursively follow active document subwindows.Extended variants additionally include inactive documents and their subwindows.
  • Web browser model: Clean restricts a script’s browser view by removing inactive documents, limiting non-same-origin documents, and hiding document headers.The function determines which window and document information a script can access.
  • Web browser model: CookieMerge and AddCookie update cookie sequences while removing HttpOnly script outputs, resolving duplicate names, or replacing same-name cookies.Both functions are simplified or based on the RFC6265 storage mechanism.
  • Web browser model: The browser relation processes input events nondeterministically, emits protoevents, and uses placeholders to generate fresh nonces.The main algorithm is defined over an input message, browser state, output messages, and a new state.

Main Algorithm..

The browser main algorithm handles triggers, navigation, scripts, requests, corruption, DNS responses, and encrypted HTTP responses through state transitions.

  • Main Algorithm..: The algorithm initializes the next state, collects incoming messages, and nondeterministically selects attacker-derived messages and source addresses.Corrupted browsers instead collect incoming messages and emit derivable messages.
  • Main Algorithm..: Trigger events nondeterministically select script execution, URL-bar navigation, reload, forward, or back operations.The algorithm chooses an existing subwindow and, where possible, a nonempty top-level window.
  • Main Algorithm..: URL-bar navigation may create a new window or reuse a top-level window, construct a URL and GET request, and send the request.Reload and history navigation operate on selected windows and documents.
  • Main Algorithm..: Closing a corrupted browser clears secrets, windows, pending DNS and HTTP state, session storage, and session cookies.Non-session cookies are retained when the browser closes.
  • Main Algorithm..: The browser stores pending requests and validates encrypted HTTP responses by matching their nonce with the recorded request.Successful responses are passed to response-processing logic after removal from pending requests.

F. Formal Model of OAuth with a Network Attacker

The OAuth formal model represents browsers, relying parties, identity providers, and a network attacker as communicating Dolev–Yao processes with explicit domains, secrets, identities, and corruption states.

  • F. Formal Model of OAuth with a Network Attacker: The OAuth web system combines honest browsers, relying parties, and identity providers with a network attacker process.The model omits DNS servers because the network attacker subsumes them.
  • F.2. Addresses and Domain Names: The system assigns finite address and domain sets to network, relying-party, and identity-provider processes, while browsers have no domain.The addr and dom mappings associate atomic processes with their addresses and domains.
  • F.3. Keys and Secrets: The nonce partition separates general process nonces, SSL keys, signing keys, passwords, relying-party secrets, and protected resources.SSL keys are injectively assigned to domains, and passwords represent browser–IdP credentials.
  • F.3. Keys and Secrets: Protected resources are assigned injectively to combinations of identity provider, client, and user, including resources without a specified user or relying party.The resource therefore depends on the IdP, user identity, and relying party.
  • F.4. Identities, Passwords, and Protected Resources: Identities are username–domain terms governed by the process owning their domain, with mappings for passwords, browser ownership, trusted relying parties, and client identifiers.Client identifiers are bijective for each identity provider.
  • F.4. Identities, Passwords, and Protected Resources: Browsers store user secrets under the corresponding IdP and trusted-RP origins, while relying parties can receive credentials in the password grant mode.In that mode, the relying party has full access to the user’s IdP account without identity-dependent limitations.
  • F.5. Corruption: Relying parties and identity providers can be corrupted and then collect incoming messages and emit messages derivable from their state.Honest processes are those whose corruption state remains ⊥.
  • F.6. Processes in W (Overview): Relying parties manage login and service sessions and may launch client-credentials flows, whereas identity providers authenticate users and serve authorization requests.All processes begin with public keys and private keys for their respective domains.

Client Credentials Mode.

The relying-party model processes OAuth token and introspection responses, supports client-credentials initiation, and applies origin and registration checks before issuing responses or service tokens.

  • Client Credentials Mode.: After receiving an access token, the relying party prepares an HTTPS introspection request and records the associated request information.The model permits construction without a client secret, but the IdP drops such unauthenticated requests.
  • Client Credentials Mode.: For authorization, the relying party retrieves the protected resource and returns it to the browser address recorded for the initiating request.For authentication, it verifies the client identifier, records a fresh service token for the user and IdP, and sends it in a cookie.
  • Client Credentials Mode.: A relying party stores domains, private keys, IdP registrations, service tokens, login sessions, and pending DNS and HTTPS requests, accepting only HTTPS.Its initial state includes IdP registration records and a key mapping shared with browsers.
  • Client Credentials Mode.: The relying-party relation validates encrypted responses, matches pending requests, and handles DNS responses before processing HTTP requests.It serves the index page and rejects malformed or mismatched requests.
  • Client Credentials Mode.: Client-credentials introspection does not issue a service token, while ordinary responses return the relying party index script and an origin referrer policy.The relying party may also start interactive login after checking the request origin and registered IdP.
  • Client Credentials Mode.: In client-credentials mode, the relying party sends a POST request with its client authorization and grant_type=client_credentials to the IdP token endpoint.The request is prepared after DNS resolution and recorded as pending.

G.1. DNS Server

The OAuth web-system model formalizes honest and attacker processes, messages, connected steps, sessions, and security properties. Its proof strategy shows that attackers cannot learn passwords, authorization codes, access tokens, or protected resources under the stated conditions.

  • Model: The web system includes honest browsers, web servers, DNS servers, and attackers with different network capabilities.Web attackers use only their own addresses, whereas network attackers may listen to and spoof all addresses.
  • Security properties: Authorization requires that attackers cannot obtain protected resources unless the IdP, relevant browser, or trusted relying parties are corrupted.The definition also treats using an IdP service under a victim’s name as access to the protected resource.
  • Security properties: Authentication requires that an attacker cannot obtain an honest RP’s service token for a user identity unless the browser owning that identity is fully corrupted.Being logged in at an RP is modeled as possessing such a service token.
  • Sessions: Sessions are sequences of causally connected processing steps, and OAuth sessions begin with a browser’s identity-selection request and end when authorization or login completes.The formal definitions distinguish these OAuth sessions from browser sessions identified by cookies.
  • Proof strategy: The proof outline derives authentication from three lemmas showing that attackers do not learn passwords, usable authorization codes, or usable access tokens.A further argument excludes other ways of obtaining the RP service token.
  • Proof strategy: The authorization proof handles both user-bound resources, protected by access-token secrecy, and anonymous resources, protected by client-secret secrecy.Both cases lead to a contradiction of the assumption that the attacker learned the protected resource.

I.4. Proof of Authorization

The authorization proof assumes an attacker has learned a protected resource and derives contradictions from the secrecy of access tokens and client secrets. The session-integrity argument separately tracks state and connected OAuth events.

  • Authorization proof: The authorization proof assumes a protected resource is attacker-derivable while the IdP and relevant parties remain honest.The contradiction is established separately for user-bound and anonymous resources.
  • Authorization proof: The attacker cannot learn an RP secret because it is sent only through HTTPS to the intended IdP and is not exposed by IdP processing.The same reasoning covers client password transmissions in the modeled flows.
  • Authorization proof: For anonymous resources, learning the resource requires client credentials and an access token, but the attacker cannot obtain the necessary client secret or token.This yields a contradiction for the anonymous-resource case.
  • Authorization proof: For user-bound resources, Lemma 6 prevents the attacker from learning the access token needed to request the resource.Thus the attacker cannot send the request that would reveal the resource.
  • Session integrity: Under honest-browser, honest-IdP, and honest-RP assumptions, third parties cannot learn the login state value.The proof tracks creation and use of the login session and state across browser, IdP, and RP processing.

Authorization Code Mode.

The authorization code flow links browser selection, IdP authentication, code issuance, token exchange, and protected-resource access through HTTPS requests and redirects. The proof identifies these linked processing steps as one OAuth session.

  • Authorization Code Mode: The IdP form submits the selected identity’s credentials and OAuth parameters in an HTTPS POST whose origin identifies the IdP.The request body includes client_id and state, and the form script obtains these from its initial state.
  • Authorization Code Mode: The browser begins the authorization-code flow by selecting an IdP identity and sending the RP’s authorization request with fresh state and client identification.The RP’s redirect request carries response_type=code and initializes the IdP form script.
  • Authorization Code Mode: The RP’s protected-resource request and IdP response complete the sequence as an OAuth session ending at the RP.The session starts when the browser initiates the flow and ends when the RP receives the protected resource.
  • Authorization Code Mode: After valid credentials, the IdP creates a fresh authorization code bound to the client, redirect URI, and selected identity.The code is stored in the IdP state and returned only in the authorization response redirect.
  • Authorization Code Mode: The RP sends the authorization code to the IdP token endpoint, which creates a fresh access token when the code binding is valid.The access token is then returned to the RP for subsequent authorization or authentication.
  • Implicit Mode: The implicit mode differs by issuing an access token immediately and returning it in the URI fragment rather than issuing an authorization code.RP JavaScript retrieves the fragment token and relays it to the RP.
  • Security result: The formal analysis concludes session integrity for authentication and, together with other lemmas, proves the main OAuth security theorem.The cited results state the session-integrity lemma and the theorem derivation.
Loading 1601.01229v4…