A Comprehensive Formal Security Analysis of OAuth 2.0

1. Introduction

• OAuth 2.0 enables web users to authorize relying parties to access resources at identity providers and is widely used for authentication and SSO.It supports login at millions of relying parties through major identity providers and underpins OpenID Connect.Source: §1 · p. 5
• The study analyzes all four OAuth grant types simultaneously across relying parties and identity providers, including malicious identity providers, relying parties, and browsers.The modeled grant types are authorization code, implicit, resource owner password credentials, and client credentials.Source: §1 · p. 5, Contributions of this Paper · p. 5
• Existing OAuth analyses largely targeted implementations, omitted simultaneous grant types, or lacked a comprehensive formal web model.The paper identifies this gap as important because browser and web-technology interactions can introduce additional security risks.Source: §1 · p. 5

Contributions of this Paper.

• The formal model instantiates the FKS web infrastructure and captures realistic HTTP, browser, iframe, storage, messaging, script, and dynamic-corruption behavior.The OAuth model follows RFC6749, incorporates RFC6819 and additional web-security recommendations, and models configuration options.Source: Contributions of this Paper · pp. 5–6
• The paper formalizes authorization, authentication, and session integrity as OAuth’s three central security properties.Session integrity encompasses both authorization and authentication.Source: Contributions of this Paper · p. 6
• Four practical attacks break OAuth security, including credential forwarding, IdP mix-up impersonation, forced attacker login, and forced use of attacker-controlled resources.The attacks were verified on actual OAuth and OpenID Connect implementations, and the authors propose implementable fixes.Source: Contributions of this Paper · p. 6
• The working groups confirmed the attacks and the need for standard changes; the IdP mix-up attack led to a new RFC draft.The fixes apply to new and existing OAuth and OpenID Connect deployments.Source: Contributions of this Paper · p. 6
• With the fixes and recommended best practices in place, the authors prove OAuth’s authorization, authentication, and session-integrity properties in a comprehensive expressive web model.These guarantees do not directly establish OpenID Connect security because OpenID Connect adds details beyond OAuth; its formal analysis remains future work.Source: Contributions of this Paper · p. 6

Structure of this Paper.

• The paper presents its formal OAuth analysis in Section 5, discusses related work in Section 6, concludes in Section 7, and places additional model, attack, OpenID Connect, and proof details in the appendix.The OAuth section primarily describes authorization-code mode, while the other three grant types are explained briefly and detailed in Appendix A.Source: Structure of this Paper · p. 7, §2 · p. 7

2. OAuth 2.0

• OAuth lets users authorize relying parties to access protected resources at identity providers, and it is also commonly used to authenticate users through unique identifiers.The paper illustrates authorization with IFTTT accessing Facebook data and authentication with Facebook-based login at Pinterest.Source: §2 · p. 7
• OAuth requires relying-party registration with an identity provider, including a client identifier, optionally a client secret, and one or more registered redirection endpoint URIs.The protocol descriptions assume a redirect URI and shared client secret, although OAuth supports multiple options and the analysis considers them more broadly.Source: §2 · p. 7
• In the authorization-code mode, the user authenticates at the identity provider, returns with a code, and the relying party exchanges it with client credentials for an access token.The identity provider checks the code, client binding, client secret, redirect URI, and non-reuse before issuing the token.Source: §2 · p. 7
• The resulting access token lets a relying party access protected resources for authorization or retrieve a user identifier and issue a session cookie for authentication.Authorization may view or manipulate protected resources, while authentication uses the identifier to establish the relying party session.Source: §2 · p. 9
• When supporting multiple identity providers, a relying party tracks user intention either through distinct redirect URIs or by storing the intended provider in a session.The paper names these approaches naïve and explicit user intention tracking and notes that the same issue applies to implicit mode.Source: §2 · p. 9
• The implicit mode parallels authorization-code mode but delivers an access token directly through the browser in a URI fragment, which client-side JavaScript must retrieve.The token can then support authorization or authentication analogously to the authorization-code flow.Source: §2 · p. 9

Resource Owner Password Credentials Mode.

• In the resource owner password credentials mode, users give identity-provider credentials directly to relying parties, which authenticate on their behalf to obtain access tokens.This mode is intended for highly trusted relying parties or situations where browser-based modes cannot be performed.Source: Resource Owner Password Credentials Mode · p. 9

3. Attacks

• The authors identify four OAuth attacks—307 redirect, IdP mix-up, state leak, and naïve RP session integrity—and provide fixes for them.Their formal analysis shows that the fixes suffice to establish OAuth security.Source: §3 · p. 9
• The attacks also apply to OpenID Connect, were verified on actual implementations, and were confirmed by the respective working groups.Figure 2 summarizes where the attacks apply.Source: §3 · p. 10, Figure 2 · p. 10

Assumptions.

• The attack relies on the IdP choosing a 307 redirect immediately after the credential POST, a behavior permitted because OAuth does not specify an exact redirect method.The paper notes that OAuth examples use 302 but permit any user-agent redirect method.Source: Assumptions · p. 10

3.1. 307 Redirect Attack

• The 307 redirect attack lets a malicious RP obtain a user’s credentials when an IdP redirects immediately after credential submission using HTTP status 307.The browser forwards the POST body, including credentials, to the RP, enabling user impersonation and breaking authorization and authentication.Source: Attack · p. 10

Attack.

• Requiring HTTP 303 redirects fixes the 307 attack because the HTTP standard unambiguously defines 303 to drop an HTTP POST body.Thus, redirect selection is security-critical rather than merely an implementation detail.Source: Attack · p. 10

3.2. IdP Mix-Up Attack

• The IdP mix-up attack confuses an RP about the user’s selected IdP, causing an honest IdP’s authorization code or access token to reach the attacker.The attacker can then impersonate the user at the RP or access protected resources, breaking authorization and authentication.Source: §3.2 · p. 11
• The IdP mix-up attack applies to authorization-code and implicit modes when an RP tracks user intention explicitly and uses one redirection URI across IdPs.It assumes a network attacker can manipulate the initial user–RP exchange, an RP accepting honest and malicious IdPs, and no need for the user to send secrets over an unencrypted channel.Source: §3.2 · pp. 11–12, Attack on Authorization Code Mode · p. 12
• The formal analysis shows OAuth can remain secure without HTTPS for the initial request when the proposed IdP mix-up fix is applied.This addresses the realistic possibility of network manipulation or TLS stripping during the initial user–RP interaction.Source: §3.2 · p. 12

Attack on Authorization Code Mode.

• The authorization-code IdP mix-up attack leaks an honest user’s code to the attacker, who can then break authorization when client secrets are optional.The attacker redirects the flow between AIdP and HIdP, causing the RP to redeem the code at the wrong IdP.Source: Attack on Authorization Code Mode · p. 13, Related Attacks · p. 13
• The same attack breaks authentication by letting the attacker submit the stolen code in a fresh session and receive an RP session for the honest user’s account.The attacker does not learn an access token, but the RP uses the token obtained from HIdP to identify the honest user.Source: Attack on Authorization Code Mode · p. 13

Variant.

• A variant requires only a web attacker: AIdP redirects the user to HIdP, where the attacker exploits the same mix-up without intercepting network messages.The user’s intended IdP differs from the IdP used in the redirected login, which a vigilant user might detect.Source: Variant · p. 13

Related Attacks.

• The attack generalizes beyond implementation bugs: related cross social-network request forgery requires weaker redirect checks, whereas this attack works even when IdPs strictly check redirect URIs.The authors state that the IETF OAuth Working Group is amending the standard according to their fixes; a related OpenID Connect attack [30] additionally assumes RP-side CSRF.Source: Related Attacks · p. 13
• The fundamental flaw is that OAuth redirects do not reliably identify their originating IdP, even with HTTPS, so the RP cannot validate the redirect’s source.The problem persists because explicit tracking omits the source, while naïve tracking can be spoofed.Source: Related Attacks · pp. 13–14
• The proposed fix adds an attacker-resistant IdP identity parameter to each redirect URI, allowing the RP to verify that the response came from the expected IdP.The authors show this fix mitigates the IdP mix-up attack and the related attacks in [30].Source: Related Attacks · p. 14

3.3. State Leak Attack

• A state leak through the Referer header enables session swapping or login CSRF, allowing attackers to log users in as the attacker or substitute attacker-controlled resources.The authorization-code and implicit modes are affected when redirected pages or IdP login pages load external links, because state is reusable.Source: §3.3 · p. 14, State Leak at IdPs · p. 14

State Leak at IdPs.

• Referrer policies that expose at most the origin, combined with single-use state, prevent state leakage and protect authorization codes; the security proof confirms the fix’s effectiveness.Modern browsers support referrer policies that can suppress or reduce the Referer header; the model permits only the origin for RP/IdP pages.Source: State Leak at IdPs · pp. 14–15

3.4. Naïve RP Session Integrity Attack

• Naïve user-intention tracking breaks RP session integrity by allowing an attacker-controlled IdP to make an RP accept the attacker’s authorization code or token as the user’s login.The proposed fix is to track explicit user intention, because the IdP mix-up fix cannot protect spoofable redirection parameters in this setting.Source: §3.4 · p. 15

3.5. Implications to OpenID Connect

• All four attacks apply to OpenID Connect; the 307 redirect, state leak, and naïve session-integrity attacks transfer directly, while the IdP mix-up attack affects authorization-code and hybrid modes.In hybrid mode, depending on RP implementation details, authorization, authentication, or both can be broken when no client secret is used.Source: §3.5 · p. 15

3.6. Verification and Disclosure

• The researchers verified the attacks across mod_auth_openidc, pyoidc, the Facebook PHP SDK, and nytimes.com, and reported them to working groups and affected developers.The OAuth Working Group confirmed the attacks and prepared an RFC draft mitigating the IdP mix-up attack; fixes for the other attacks remained under discussion.Source: §3.6 · pp. 15–16

FKS Model

• The extended FKS model [14] [17] represents browsers, servers, DNS servers, web attackers, and network attackers as communicating processes in a standards-oriented web system.It supports either one network attacker or multiple web attackers; OAuth-specific server and script behavior is defined separately.Source: §4 · pp. 16–17

Communication Model

• Communication proceeds by nondeterministically delivering pooled events to listening processes, whose state transitions produce new derivable events and induce system runs.A system configuration contains all process states, waiting events, and unused nonces.Source: §4 · pp. 16–17
• The symbolic Dolev–Yao representation encodes HTTP(S) requests, addresses, nonces, cryptographic operations, and equational reasoning over formal terms.HTTPS requests include a fresh symmetric key, and the attacker process records received messages and derives every message permitted by the symbolic theory.Source: §4 · pp. 16–17

Web Browsers

• The browser model captures users, credentials, windows, documents, cookies, web storage, JavaScript, navigation, XHRs, postMessages, forms, iframes, DNS, HTTP(S), and browser corruption.Security rules constrain script access and manipulation, while a corrupted browser behaves as an attacker process.Source: §4 · p. 17

5. Analysis

• The analysis formalizes OAuth’s model and security properties, then proves the security of the fixed protocol with full details provided in Appendices F–I.The analyzed version includes the fixes introduced in Section 3.Source: §5 · p. 18

5.1. Model

• The model extends the FKS web model with HTTP Basic Authentication and Referrer Policies, while adhering to RFC 6749 and its security considerations.It is designed to include all OAuth configuration options with as few assumptions as possible.Source: §5.1 · p. 18, Design · p. 18

Design.

• Every relying party and identity provider may run all four OAuth modes simultaneously, while relying parties, identity providers, and browsers may be corrupted at any time.The model also permits flexible or loosely checked redirection URIs, including patterns and origin-only checking, which strengthens the proved guarantees.Source: Design · p. 18
• The design permits clients with or without secrets, HTTP or HTTPS visits without required STS, arbitrary browser navigation and concurrent login flows, and standard cookie-based RP sessions.User authentication at the IdP uses username and password, and RPs may explicitly choose redirection URIs or use previously registered ones.Source: Design · p. 18

Attack Mitigations.

• Honest RPs and IdPs must exclude untrusted third-party JavaScript, open redirectors, and cross-site scripting, because these can expose access tokens or authorization codes.The model combines these requirements with the new-attack fixes and standard mitigations as implementation guidelines.Source: Attack Mitigations · p. 18
• Fresh session-bound state nonces and origin checks protect OAuth entry, password-login, token-posting, and IdP credential-submission endpoints against CSRF attacks.Reusing a state value across login attempts lets a malicious IdP attack session integrity; origin checking also covers endpoints outside OAuth’s scope.Source: Attack Mitigations · pp. 18–19
• HTTPS endpoints, restrictive Referrer Policies, 303 redirects, secure and freshly regenerated session cookies, protected password transmission, client-ID validation, and explicit user-intention tracking prevent token, code, cookie, authentication, and intent-confusion attacks.Protected resources are abstract resources an RP can use at an IdP after successful authorization, closely following RFC 6749.Source: Attack Mitigations · p. 19, Concepts Used in Our Model · p. 19

Concepts Used in Our Model.

• The model represents protected resources, service tokens as RP-issued session cookies, and trusted RPs whose compromise can affect security guarantees.Protected resources may be bound to a user or acquired through client credentials without a user identity; service tokens abstract RP session mechanisms.Source: Concepts Used in Our Model · p. 20

OAuth Web System with a Network Attacker.

• OWS_n models unbounded finite sets of RPs, IdPs, and browsers under a network attacker, with all OAuth modes, mitigations, corruption, and browser scripts represented.RPs manage login and service sessions, IdPs authenticate users, and the implicit-flow script forwards the access token and state to the RP over HTTPS.Source: OAuth Web System with a Network Attacker · p. 20

OAuth Web System with Web Attackers.

• OWS_w replaces the network attacker with an unbounded finite set of web attackers and is used to analyze session integrity.This separates the adversary model used for session-integrity properties from the network-attacker model used for authorization and authentication.Source: OAuth Web System with Web Attackers · pp. 20–21

Limitations of Our OAuth Model.

• The model omits token and session expiration, revocation, logout, refresh-token behavior, scoped resource access, and IdP error messages.It overapproximates refresh tokens by leaving access tokens unexpired and assumes RPs always receive full access to users’ IdP data.Source: Limitations of Our OAuth Model · p. 21

5.2. Security Properties

• The security properties require authorization and authentication failures to imply corruption of the relevant IdP, user browser, or trusted RP.Authorization concerns unauthorized access to protected resources, while authentication concerns obtaining an honest RP’s service token under a user’s identity; client-credentials resources are not user-bound.Source: §5.2 · p. 21

Session Integrity.

• Session integrity requires that completed authorization or authentication flows were user-initiated and, with an honest IdP, preserve the identity selected when the flow began.For authorization, completion means the RP obtains a protected resource; for authentication, completion means the user is logged in under the resulting identity.Source: Session Integrity · pp. 21–22
• Session integrity is analyzed against web attackers because network attackers can force login under their own account by changing cookies from non-secure to secure origins, defeating state-based CSRF defenses.The paper notes that stronger solutions using JavaScript and HTML5 features are conceivable but are less common and typically outside the OAuth standard.Source: Session Integrity · p. 22

Main Theorem.

• Theorem 1 establishes authorization and authentication security against network attackers and session integrity for authorization and authentication against web attackers.The result also implies authentication and authorization security when web attackers are considered.Source: Main Theorem · p. 22

7. Conclusion

• With the proposed fixes and required OAuth security recommendations and best practices, OAuth provides strong authorization, authentication, and session-integrity properties; without them, security cannot be guaranteed.The results provide precise implementation guidelines, although individual deployments may fail to satisfy them, such as when relying parties run untrusted JavaScript.Source: §5.3 · p. 22, §7 · pp. 23–24

6. Related Work

• The closest prior formal study, Bansal et al., used applied pi-calculus, WebSpi, and ProVerif mainly to discover implementation attacks, whereas this work uses a more expressive model to prove security.Their positive results relied on a more limited model with restrictions including one identity provider per relying party and honest identity providers.Source: §6 · pp. 22–23, §7 · p. 23
• Empirical work examined deployed OAuth implementations across identity providers, relying parties, and mobile apps, while other work studied SDK assumptions and OpenID Connect attacks.The cited studies include analyses of 3 identity providers and 96 relying parties, 10 identity providers and 60 relying parties, and 4 identity providers and 500 relying parties.Source: §6 · p. 23
• Other formal studies found known OAuth weaknesses or analyzed restricted protocols and modes, but omitted generic web features such as HTTP status codes, cookies, browser windows, documents, iframes, messaging, and origin headers.These studies include Pai et al., Kumar, and Chari, Jutla, and Roy.Source: §6 · p. 23, §7 · p. 23

7. Conclusion

• The paper presents the first extensive formal analysis of OAuth 2.0 using a comprehensive web model covering all grant types and options, malicious relying parties and identity providers, and corrupted browsers or users.The underlying generic web model is described as the most comprehensive web model to date.Source: §7 · p. 23
• The analysis revealed four attacks affecting OAuth and OpenID Connect, verified them, proposed fixes, and reported them to the relevant working groups, which confirmed the attacks.The fixes and recommendations were under discussion or already incorporated into a draft RFC.Source: §7 · p. 23
• Future work identified by the paper is a formal analysis of OpenID Connect building on this OAuth analysis.The authors describe their OAuth model as a starting point for that next step.Source: §7 · p. 24

Further Recommendations and Options.

• The analysis models the OAuth protocol’s endpoint and client options while assuming HTTPS, recommended state-based CSRF defenses, common session cookies, and best practices that avoid known attacks.Scopes are omitted and full access is assumed; the model also covers absent client secrets and redirect-URI patterns.Source: Endpoints · p. 27, §A.2 · p. 28, Further Recommendations and Options · p. 28

Endpoints.

• OAuth registration assigns client identifiers and, when confidentiality is possible, client secrets; public or secretless clients are supported, redirect URIs or patterns are registered, and IdP endpoints are configured.Before redirecting, the RP typically establishes a browser session and uses a state parameter bound to that session to prevent CSRF; the analysis follows this recommendation.Source: Endpoints · p. 27

A.2. OAuth Modes.

• The implicit mode delivers an access token through the browser without authenticating the RP, whereas password credentials and client credentials serve trusted or non-user-centered scenarios.Password mode sends the user’s credentials and client credentials to the IdP; client-credentials tokens are bound to the RP rather than a user.Source: §A.2 · pp. 28–30

B. IdP Mix-Up Attack in the OAuth Implicit Mode

• IdP mix-up in OAuth implicit mode leaks an honest user’s access token and lets the attacker impersonate that user at the RP.The attacker redirects the browser between IdPs, causing the RP to use an HIdP token at AIdP; authentication then fails when the attacker reuses the captured token.Source: B. IdP Mix-Up Attack in the OAuth… · p. 31

Modes and Protocol Flow.

• OpenID Connect extends OAuth with discovery, dynamic client registration, and an id token containing the user identifier, intended RP, and issuer.The hybrid flow discovers IdP metadata, registers the RP, obtains authorization and access tokens, verifies the id token, and retrieves user information.Source: Modes and Protocol Flow · pp. 31, 34

The IdP Mix-Up Attack.

• OpenID Connect’s hybrid mode enables IdP mix-up attacks that break authorization or authentication through stolen tokens, redeemable codes, or forged identity tokens.Without a client secret, an attacker can redeem a stolen authorization code; alternative token selection can leak an HIdP token or enable honest-user impersonation.Source: The IdP Mix-Up Attack · pp. 36–37

C. The FKS Web Model

• The formal analysis proceeds by presenting the FKS web infrastructure model together with specified changes and additions.This passage introduces the modeling framework for the subsequent analysis without stating its later findings.Source: C. The FKS Web Model · p. 38
• The FKS web model extends browser and HTTP abstractions with Authorization and ReferrerPolicy headers and permits multiple stored passwords per origin.The Authorization header models HTTP Basic Authentication, while ReferrerPolicy models a response-delivered referrer policy.Source: C. The FKS Web Model · p. 38

C.1. Communication Model

• The communication model defines a signature of disjoint constants and cryptographic function symbols over terms, messages, placeholders, events, and protoevents.It also specifies equational normalization, pattern matching, variable replacement, and events represented by sender, receiver, and message.Source: §C.1 · p. 38, Terms, Messages and Events · pp. 38–39

Terms, Messages and Events.

• Terms, messages, and events provide the symbolic vocabulary for modeling domains, HTTP methods, encryption, signatures, nonces, wildcard patterns, and event sequences.Ground terms are messages, protomessages may contain process placeholders, and events record receiver, sender, and message values.Source: Terms, Messages and Events · pp. 38–39

Atomic Processes, Systems and Runs.

• Atomic processes map an input event and current state nondeterministically to output events and a new state, while systems execute these transitions through configurations and finite or infinite runs.Each processing step selects a process and waiting event, replaces placeholders with fresh nonces, prepends output events, and updates the selected process state.Source: Atomic Processes, Systems and Runs · pp. 39–41

Atomic Dolev-Yao Processes.

• Atomic Dolev-Yao processes restrict state transitions to messages derivable from the current event and state, using placeholders for variables.The derivation set dV(M) contains terms constructible from messages in M through term composition and substitution.Source: Atomic Dolev-Yao Processes · p. 41

C.2. Scripts

• Scripts model client-side technologies such as JavaScript as derivation-constrained relations that transform browser-provided state into new state and commands.Script variables can be replaced by fresh placeholders and ultimately nonces; the attacker script outputs anything derivable from its input.Source: §C.2 · p. 41

C.3. Web System

• A web system is a tuple containing DY processes, scripts, and initial events, partitioning processes into honest, web-attacker, and network-attacker components.Web attackers cannot listen beyond their own addresses or spoof others, whereas network attackers can listen to and spoof all addresses.Source: §C.3 · p. 42

D. Message and Data Formats; D.1. Notations

• The message-format framework introduces sequence, dictionary, and pointer notation for representing structured protocol data and accessing nested components.Dictionaries use unique keys, support extraction and deletion operations, and treat the empty dictionary as the empty sequence.Source: D. Message and Data Formats · p. 43, §D.1 · p. 43

D.2. URLs; D.3. Origins

• URLs encode plain or secure protocols, hosts, paths, parameters, and optional fragments, while origins pair a domain with either HTTP or HTTPS.An omitted URL fragment is assigned ⊥, and origins are terms ⟨host,protocol⟩.Source: §D.2 · p. 44, §D.3 · p. 44

D.4. Cookies

• Cookies contain names and value records with secure, session, and httpOnly flags that control transport, lifetime, and JavaScript access.Cookies appear in HTTP(S) requests, while responses transfer only cookie names and values.Source: §D.4 · p. 44

D.5. HTTP Messages; Encrypted HTTP Messages..

• HTTP messages include nonces, methods, hosts, paths, status codes, headers, and bodies; HTTPS encrypts requests with a server public key and responses with a client-chosen symmetric key.The nonce maps each response to its corresponding request, and encrypted messages are represented as HTTPSRequests and HTTPSResponses.Source: §D.5 · pp. 44–45, Encrypted HTTP Messages · p. 45

D.6. DNS Messages

• DNS requests resolve domains using nonces, and DNS responses return the resolved IP address while echoing the request nonce for matching.Requests have the form ⟨DNSResolve,domain,n⟩, whereas responses have the form ⟨DNSResolved,domain,result,n⟩.Source: §D.6 · p. 46

D.7. DNS Servers

• The flat DNS model answers each domain query directly with a fixed address from a DNS server’s encoded mapping.The model abstracts from hierarchical resolution, recursion, and caching, which could be modeled separately for attacks on DNS itself.Source: §D.7 · p. 46

E.1. Notation and Terminology (Web Browser State)

• The formal browser state represents windows, active and historical documents, opener relationships, origins, cookies, and nested subwindows.Window references are nonces; documents expose their origin, while inactive documents and cross-origin content are restricted through the model’s state projections.Source: §E.1 · pp. 47–48
• Browser visibility and storage operations enforce web security semantics by restricting cross-origin state, merging cookies with HTTP-only handling, and updating cookies by name.Clean removes inactive documents, limits non-same-origin documents, and clears document headers; CookieMerge and AddCookie follow simplified RFC6265-based rules.Source: §E.1 · pp. 48–49

E.2. Description of the Web Browser Atomic Process

• The browser atomic process maps input events and states nondeterministically to output protoevents and successor states, using fresh nonce placeholders where required.Its relation Rp is defined by termination of the specified algorithm, and Figure 12 lists the placeholders used by the browser algorithms.Source: §E.2 · pp. 49–50, Figure 12 · p. 50

Functions.

• The browser functions select navigable or same-origin windows, create or preserve opener relationships, cancel pending requests, and navigate backward by switching active documents.GETNAVIGABLEWINDOW can create a new window for _BLANK, while CANCELNAV removes matching pending HTTP and DNS requests.Source: Functions · pp. 50–51
• The SEND function prepares HTTP requests by enforcing HTTPS for strict-transport hosts, adding eligible cookies and origin headers, applying referrer policies, and initiating DNS resolution.It stores the request in pendingDNS until resolution completes and distinguishes window references from XMLHttpRequest references.Source: Functions · pp. 51–52
• The browser executes scripts by selecting a new script and document state, saving it, and interpreting the resulting command.The execution state includes cookies, local and session storage, identifiers, secrets, and script outputs before commands are dispatched.Source: Functions · pp. 52–53
• Script commands generate navigations, form submissions, and XMLHttpRequests with method, body, origin, referrer, and referrer-policy handling.The model restricts form methods to GET and POST and blocks certain XMLHttpRequest methods when a non-null XHR reference is present.Source: Functions · pp. 53–54
• Back/forward navigation restores the complete state of a previously viewed document, although reloads may be triggered nondeterministically.The navigation function updates active documents and cancels the affected navigation before proceeding.Source: Functions · pp. 52, 54
• HTTP response processing stores cookies and HTTPS strict-transport-security state, follows supported redirects, and either creates a document or delivers an XHR response.Redirects preserve or modify request details according to status and method, while XHR redirects are not performed.Source: Functions · pp. 55–56

• The browser collects incoming messages and delegates them to protocol-specific processing before continuing its main event loop.It stores messages in pendingRequests when the browser is not corrupted, invokes dV and IPs, and emits the resulting action and state.Source: Main Algorithm · p. 56
• User-triggered actions can run scripts, create URL requests in new or existing windows, reload documents, or navigate forward.URL requests choose protocol, host, path, fragment, and parameters; reloads use the active document’s location and referrer, while forward navigation calls NAVFORWARD.Source: Main Algorithm · p. 56
• Corruption messages either fully corrupt the browser or close it while retaining only non-session cookies.FULLCORRUPT sets isCorrupted, whereas CLOSECORRUPT clears secrets, windows, DNS and request state, session storage, and session cookies.Source: Main Algorithm · p. 57
• Encrypted HTTP responses are decrypted and accepted only when their nonce matches the pending request; otherwise processing stops.Valid responses are removed from pendingRequests and passed to PROCESSRESPONSE, while nonce mismatches terminate the transition without processing.Source: Main Algorithm · p. 57
• DNS responses are accepted only for pending, IP-valued, domain-matching queries, after which HTTPS requests are encrypted and HTTP requests remain plaintext.The browser removes the completed DNS request, records the resulting pending request, and emits the resolved address, message, and URL.Source: Main Algorithm · pp. 57–58

F.1. Outline

• The OAuth web system comprises a network attacker, finite sets of browsers, relying parties, and identity providers, with scripts and trigger events defining system behavior.DNS servers are subsumed by the network attacker, which can use all addresses for sending and listening.Source: §F.1 · p. 59, F. Formal Model of OAuth with a… · p. 59

F.3. Keys and Secrets

• The model assigns domains, IP addresses, SSL keys, passwords, relying-party secrets, and protected resources to formalize communication and authorization state.Protected resources depend on the identity provider, user identity, and relying party, while resource-owner password flows may access resources not bound to a relying party.Source: §F.3 · p. 60, §F.4 · p. 61

F.4. Identities, Passwords, and Protected Resources

• Identities are username-domain pairs governed by their domains, with mappings specifying owning browsers, trusted relying parties, OAuth client identifiers, and shared secrets.The model also maps identities to owners and assigns relying-party-specific resources and credentials.Source: §F.4 · p. 60

F.7. Network Attackers

• The network attacker can listen to and spoof every available address, and browsers initialize with public SSL keys, attacker-controlled DNS resolution, owned identities, and stored secrets.Browsers maintain empty service-token state initially and expose passwords according to whether origins belong to identity providers or trusted relying parties.Source: §F.7 · p. 62, §F.8 · p. 62

F.5. Corruption

• Browsers store user credentials under identity-provider and trusted-relying-party origins, while relying parties and identity providers can be corrupted and then act like attackers.Corrupted processes collect incoming messages and send messages derivable from their state and inputs.Source: §F.5 · p. 61, Network Attacker · p. 61, §F.8 · p. 62

F.9. Relying Parties

• Each relying party accepts only HTTPS, stores domains, keys, registrations, session identifiers, and pending requests, and manages login sessions that culminate in service sessions.Service tokens identify service sessions that let users access the relying party’s services.Source: §F.9 · p. 62
• Interactive login selects authorization-code or implicit mode, redirect settings, and fresh session values; the relying party validates returned cookies, identity-provider domains, and state before token processing.Authorization-code flows exchange codes at the token endpoint, whereas implicit flows submit fragment tokens for identity-provider introspection.Source: §F.9 · pp. 63–64
• Non-interactive login forwards user credentials to the identity provider, while client-credentials login sends the relying party’s client credentials after a trigger selects an identity provider.Both flows store prepared requests in pendingDNS before sending DNS queries to the identity provider’s token endpoint.Source: §F.9 · pp. 62–64, Client Credentials Mode · p. 64

Formal description.

• The relying-party state records IdP registrations, service tokens, login sessions, key mappings, SSL keys, pending DNS and HTTP requests, and corruption status.Its initial state maps IdP domains to registration records, leaves corruption unset, and initializes key mappings consistently with the browser model.Source: Formal description · p. 65, , loginSessions ∈ · p. 65

, loginSessions ∈

• The relying-party algorithm validates encrypted responses and DNS results, launches client-credentials requests with client authentication, and supports interactive, implicit, authorization-code, and password flows.Interactive login uses origin checks, fresh state and login-session cookies, while token responses are introspected before authorization or authentication handling.Source: , loginSessions ∈ · pp. 66–68

Client Credentials Mode.

• In client-credentials mode, the relying party requests an access token, introspects it, and stops without issuing a service token.For other introspection flows, it nondeterministically returns the protected resource for authorization or creates a service-token cookie after validating the client identifier and user.Source: Client Credentials Mode · p. 65, , loginSessions ∈ · p. 67

F.10. Identity Providers

• The identity-provider model stores domains, endpoints, users, clients, authorization codes, access tokens, protected resources, and corruption state, and processes authorization, token, and introspection requests.It validates clients and redirect URIs, issues codes or bearer tokens for supported grants, and returns the client ID, user ID, and protected resource for valid introspection tokens.Source: §F.10 · pp. 70–71
• The IdP model validates credentials, CSRF protection, registered redirect URIs, and client authentication before processing OAuth requests.Authorization requests may create authorization codes or bearer access tokens, while invalid credentials, origins, clients, or redirects terminate processing.Source: §F.10 · pp. 72–73
• The authorization endpoint returns codes or bearer tokens bound to the client, redirect URI, user, and supplied state.Authorization codes are stored with client, redirect URI, and username; implicit responses place access tokens and state in the redirect fragment.Source: §F.10 · pp. 72–73
• The token endpoint supports authorization-code, password, and client-credentials grants, issuing bearer tokens after the grant-specific checks succeed.Authorization codes are validated and consumed, password grants verify the user secret, and client-credentials grants require authenticated client credentials.Source: §F.10 · pp. 73–74

G. Formal Model of OAuth with Web Attackers

• The web-attacker model derives from the network-attacker model by using finite web attackers with dedicated IP addresses and domains, while honest parties share an honest DNS server.The resulting system contains honest and web-attacker processes but no network attacker.Source: G. Formal Model of OAuth with Web… · p. 75

G.2. Web Attackers

• The model gives web attackers only their own IP addresses and attacker-controlled domains and keys, while DNS initially resolves domains to addresses owned by their domain owners.These definitions distinguish web attackers from network attackers and specify the initial DNS and attacker states.Source: §G.2 · p. 75, §G.1 · p. 75

H.1. Authorization

• Authorization requires protected resources to remain unavailable unless the IdP, the user’s browser, or a trusted relying party is corrupted.The definition also models attacker access to an IdP service under the victim’s identity, such as posting to a victim’s wall.Source: §H.1 · p. 76

H.2. Authentication

• Authentication requires that an attacker cannot obtain an honest RP service token for a user unless the user’s browser, a trusted RP, or the IdP is corrupted.Being logged in at an RP is represented by obtaining a service token for that identity.Source: §H.2 · p. 76

H.3. Session Integrity for Authorization and Authentication

• Session integrity links OAuth processing steps through direct or browser-mediated causation, defining sessions that preserve user intent and selected identities across authorization flows.OAuth sessions begin with a browser-triggered RP request and end when authorization or login completes, while potentially remaining infinite if completion never occurs.Source: §H.3 · p. 76, Sessions and OAuth Sessions · p. 77

Session Integrity Property for Authorization.

• Session-integrity properties require completed authorization and authentication to follow an honestly initiated OAuth flow and retain the identity selected by the user.For honest identity providers, the formal conditions ensure that the flow does not complete under a different identity.Source: Session Integrity Property for… · p. 78

I.1. Proof Outline

• The proof outline relies on HTTPS and RP invariants: honest RPs protect encrypted messages and keys, preserve pending requests, and never send decryptable requests to other RPs.These properties support the contradiction proofs for authentication and authorization and the event backtracing proof for session integrity.Source: §I.1 · p. 79, §I.2 · pp. 80–81

I. Proof of Authentication

• The authentication proof proceeds by contradiction, showing attackers cannot obtain user passwords, relevant authorization codes, access tokens, or service tokens.The argument concludes that no other route to the service token exists, so the authentication property holds.Source: §I.1 · p. 79, §I.3 · p. 82

I.3. Proof of Authentication

• The proof’s authorization-code lemma rules out attacker knowledge because valid codes require password-authenticated requests and are forwarded only to the honest IdP.Redirect restrictions, HTTPS, Referrer Policy, and IdP validation prevent the code from reaching attacker-controlled parties.Source: §I.3 · pp. 83–84
• Attackers cannot learn users’ passwords, authorization codes, or access tokens in the modeled OAuth system.The proof shows that these values are transmitted only over HTTPS to honest parties, validated, and then discarded without leaking.Source: §I.3 · pp. 82–84
• The proof’s access-token lemma rules out attacker knowledge because tokens are issued only after authenticated flows and are checked by the honest IdP without disclosure.The argument covers authorization-code, implicit, and password grant paths, ensuring tokens are forwarded to the intended IdP and discarded after validation.Source: §I.3 · pp. 84–86
• Lemma 7 derives a contradiction: every request that could create the attacker-known service token must originate from an honest browser, so the token never leaks.The argument covers requests carrying authorization codes, passwords, or access tokens and relies on the absence of honest scripts that use XMLHttpRequest.Source: §I.3 · pp. 86–87

I.4. Proof of Authorization

• Authorization follows because attackers cannot learn RP secrets or the access tokens needed to obtain either anonymous or user-protected resources.The proof derives a contradiction from the assumption that an attacker can derive a protected resource, using HTTPS protection, secret confidentiality, and separate anonymous-resource and user-resource cases.Source: §I.4 · pp. 87–88

I.5. Proof of Session Integrity

• For honest browsers, IdPs, and RPs, third parties cannot learn the OAuth state value; redirects, cookies, fragments, HTTPS, and restrictive Referrer Policy prevent leakage.The proof tracks state from session creation through authorization and callback handling, showing that it remains known only to the browser, IdP, and RP.Source: §I.5 · pp. 88–89
• The resulting OAuth web system is secure with respect to session integrity for authorization.Lemma 11 establishes the corresponding event relationships for password, authorization-code, and implicit modes, while Lemma 12 states the security conclusion.Source: §I.5 · pp. 90–91
• The proof considers every OAuth web-system run, processing step, honest browser and relying party, identity provider, identity, and protected resource satisfying the session-integrity condition.The argument begins from the condition endsOA(Qends,b,r,i,t) and analyzes the resulting processing step.Source: §I.5 · p. 92
• For an honest identity provider, the proof connects the endpoint processing step to the session and shows that the required logical equivalence follows from the event relations in Lemma 11.Because the identity provider and DNS servers are honest, processing steps emitting related events in Figure 15 are connected; the proof then derives the corresponding events in Figure 16.Source: §I.5 · p. 92, Authorization Code Mode · p. 92, Figure 16
• Lemma 11 and Definition 51 imply that receiving an authorization response and emitting authentication establish an OAuth Session for the browser, relying party, and identity provider.The proof applies Lemma 11 when the relying party receives eresp_intr from the identity provider and emits eresp_auth to the browser.Source: §I.5 · p. 92

Authorization Code Mode.

• In authorization-code mode, the redirect carries freshly selected state and client identifiers, while the IdP form script receives these values under the IdP origin.The resulting POST contains the RP client identifier and state, and the form submission supplies the selected identity’s credentials.Source: Authorization Code Mode · p. 93
• The authorization-code analysis identifies OAuth sessions whose endpoints are tied to RP redirects, IdP form submissions, authorization codes, and subsequently issued access tokens.Fresh state values and HTTPS requests constrain the event sequence to the intended RP–IdP interaction.Source: Authorization Code Mode · pp. 93–94
• Authorization-code processing creates a fresh authorization code, exchanges it for a fresh access token, and requires the RP to present that token at the IdP introspection endpoint.The token is accepted only when IdP state contains the corresponding token-to-client-and-identity association.Source: Authorization Code Mode · pp. 93–94

Implicit Mode.

• Implicit mode follows the same session reasoning, but uses response_type token and places the access token and state in the redirect URI fragment.The RP’s implicit-grant script extracts the fragment values and relays the access token to the RP through an HTTPS POST.Source: Implicit Mode · p. 94
• Implicit-mode sessions send the access token to the IdP introspection endpoint, where it is accepted only if the IdP stores the corresponding token, client, and identity association.The IdP creates the access-token entry with a freshly chosen nonce before returning the token to the RP.Source: Implicit Mode · p. 95
• Lemma 13 establishes that every OAuth web system with web attackers is secure with respect to session integrity for authentication.The proof combines authorization session integrity with the behavior of honest IdP introspection endpoints.Source: Implicit Mode · p. 95
• Lemmas 7, 9, 12, and 13 together establish Theorem 1 for the analyzed OAuth web system.This final result depends on the preceding authorization and authentication session-integrity arguments.Source: Implicit Mode · p. 95