# Proposal: OIDC and OAuth2

Capability-native abstractions for OpenID Connect identity providers,
OAuth 2.0 clients, issued tokens, workload identity federation, and
the authentication/authorization flows that every modern cloud and
enterprise deployment depends on.


## Why a Separate Proposal

OIDC and OAuth2 are related but distinct from certificates and keys.
Keys ([cryptography-and-key-management-proposal.md](cryptography-and-key-management-proposal.md))
are secret material. Certificates
([certificates-and-tls-proposal.md](certificates-and-tls-proposal.md))
are public assertions of *identity binding* validated against a PKI
trust store. OIDC/OAuth2 is a *delegated authority* protocol family:
tokens are short-lived bearer credentials or proof-of-possession
handles issued by an identity provider after authenticating a subject,
scoped by a set of permissions, and consumed by a relying party or
resource server.

The failure modes barely overlap. Key compromise vs. IdP compromise
vs. CA mis-issuance require different detection and recovery stories.
Revoking a TLS certificate, revoking an access token, and revoking a
KEK are three different operations with three different operational
tempos (manifest update / IdP admin action / KMS grant edit).

Putting this in a separate proposal also matches the cross-cutting
nature of the feature: OIDC/OAuth2 shows up in login
([boot-to-shell-proposal.md](boot-to-shell-proposal.md)), session
state ([user-identity-and-policy-proposal.md](user-identity-and-policy-proposal.md)),
key unlock ([volume-encryption-proposal.md](volume-encryption-proposal.md)),
cloud KMS access ([cryptography-and-key-management-proposal.md](cryptography-and-key-management-proposal.md)
`CloudKmsKeySource`), and service-to-service authentication
([networking-proposal.md](networking-proposal.md)). Threading it
through every touchpoint without a shared definition would be a
silo-per-consumer repeat of the Linux ssh-agent/gpg-agent/keyctl
story.

## Problem

capOS needs to:

- Accept federated authentication for console and web-terminal login
  (corporate IdP, Google, GitHub, Okta, Azure AD, Keycloak, Dex) so
  sessions do not depend on capOS storing or managing primary user
  credentials.
- Run as a cloud workload without baked-in long-lived IAM credentials,
  using the modern workload identity federation pattern (RFC 8693
  token exchange) to obtain short-lived cloud provider credentials
  from an attested instance identity or a local keypair.
- Authenticate service-to-service calls using OAuth2 client
  credentials, `private_key_jwt`, DPoP, or mTLS, chosen by policy
  rather than hard-wired per consumer.
- Consume OAuth2 access tokens from external clients (an HTTP API
  running under capOS verifies bearer tokens against an issuer's
  JWKS) without every service writing its own JWT parser.
- Expose scopes and OIDC claims as policy input to
  `AuthorityBroker` / `PolicyEngine` without letting them act as
  ambient authority.
- Map external subjects to local principals, accounts, sessions,
  policy profiles, and resource profiles through explicit admission
  configuration rather than treating provider claims as local roles.

Without a shared abstraction each consumer would invent its own JWT
parser, JWKS cache, issuer list, discovery-document fetcher, refresh
scheduler, and token storage. That is roughly the OAuth/OIDC mess
already visible in most operating systems and app stacks.

## Scope

In scope:

- Relying-party (RP) role for OIDC. capOS is the RP; the IdP is
  external.
- Client role for OAuth2. capOS acts as confidential client, public
  client (PKCE), or federated workload client.
- Resource-server role for OAuth2. A capOS service can validate
  inbound bearer tokens.
- Token capability objects for ID tokens, access tokens, refresh
  tokens, DPoP proofs, and client assertions.
- Integration with `SessionManager`, `CredentialStore`,
  `AuthorityBroker`, `CloudKmsKeySource`, `EncryptedBlockDevice`
  unlock flows.

Out of scope for v1:

- OAuth2 authorization server / OIDC provider role. capOS does not
  issue tokens to third parties in the first iteration. A
  `LocalIdentityProvider` that issues tokens to other capOS services
  is possible later work; it sits on top of the same primitives.
- SAML. The modern direction is OIDC; a deployment that needs SAML
  can add a second `SessionManager.login` adapter without reshaping
  the model.
- OAuth 1.0a. Dead.
- UMA 2.0. Out until a concrete consumer appears.
- CIBA (Client-Initiated Backchannel Authentication). Useful for
  step-up on mobile devices; revisit once the web shell gateway ships.

## Design Principle: Tokens Are Typed Capabilities

In the OAuth/JWT world a token is a byte string. Possession equals
authority. Every library re-parses, re-validates, and re-caches the
token; every log line risks leaking it; every service that needs to
forward it must hand it over unattenuated. That is the same
architectural failure mode as "a key is a byte string" — the
protection mechanism (TLS in transit, DPoP, audience binding) is
orthogonal to the system's main abstraction.

In capOS, a token is a capability object. Holding an `AccessToken` cap
means "you may present this token for one outbound request, read a
bounded subset of its claims, or exchange it for a more specific
token." The raw token bytes live in the address space of the
OAuth/OIDC service; callers reach them by invoking typed methods.

Consequences mirror the key-cap case:

- **Attenuation by scope.** A caller that only needs to read `sub`
  receives a `TokenClaims` facet that does not expose the raw JWT.
  A caller that only needs to call one resource server receives a
  `BoundToken` that rejects use against other audiences.
- **Revocation is a cap drop plus server-side revocation.** Dropping
  the cap prevents that holder from using the token; revoking the
  token at the IdP prevents any holder from using it. Both paths
  exist; neither requires a kernel mechanism.
- **Audit is intrinsic.** Every token present, every refresh, every
  token exchange flows through the audit cap. Bearer-token leakage
  to logs becomes harder because the raw string is never returned.
- **Composition, not configuration.** An OAuth client is a cap that
  encapsulates client_id, client authentication method, allowed
  grants, scopes, and target IdP. Building one means composing caps,
  not stringifying URLs into config files.
- **Per-consumer issuance by default.** When a service needs a token
  for a downstream call, it asks its `OAuthClient` cap; the OAuth
  service issues a per-consumer down-scoped token. Transfer between
  processes is possible but explicit.

This also gives capOS a natural story for the agent shell's
"agent never sees secrets" rule: the agent holds an `ApprovalGrant`
cap that internally holds the access token; the agent invokes the
wrapped resource server cap; the token never appears as data in
the model's prompt window.

## Schemas

### Identity provider

```capnp
interface OidcIdentityProvider {
    # The stable issuer URL (RFC 8414 / OIDC Discovery).
    issuer            @0 () -> (url :Text);

    # Discovery document (cached; refreshed on a schedule or on
    # signature-verification failure). Returning the parsed metadata,
    # not raw JSON, forces the implementation to validate it once.
    metadata          @1 () -> (meta :OidcProviderMetadata);

    # JWKS fetched from the provider's `jwks_uri`, exposed as a set of
    # PublicKey caps keyed by `kid`. Key rotation is invisible to
    # callers: they ask for a `kid`, they get a current PublicKey or
    # an error.
    jwks              @2 () -> (set :Jwks);

    # Verify an ID token fully — signature against jwks, issuer match,
    # audience match against the registered client, nonce, exp/nbf/iat
    # with clockSkewSeconds from policy, and required `acr`/`amr`
    # predicates if set by the OAuthClient.
    verifyIdToken     @3 (jwt :Data,
                          policy :IdTokenPolicy)
                      -> (claims :IdTokenClaims);
}

struct OidcProviderMetadata {
    issuer                           @0 :Text;
    authorizationEndpoint            @1 :Text;
    tokenEndpoint                    @2 :Text;
    userinfoEndpoint                 @3 :Text;
    jwksUri                          @4 :Text;
    endSessionEndpoint               @5 :Text;
    deviceAuthorizationEndpoint      @6 :Text;
    revocationEndpoint               @7 :Text;
    introspectionEndpoint            @8 :Text;

    responseTypesSupported           @9  :List(Text);
    grantTypesSupported              @10 :List(Text);
    tokenEndpointAuthMethodsSupported @11 :List(Text);
    scopesSupported                  @12 :List(Text);
    idTokenSigningAlgValuesSupported @13 :List(Text);
    codeChallengeMethodsSupported    @14 :List(Text);
    dpopSigningAlgValuesSupported    @15 :List(Text);
    requestObjectSigningAlgValuesSupported @16 :List(Text);
    # Present when the IdP advertises OAuth 2.0 Token Exchange (RFC 8693).
    tokenExchangeSupported           @17 :Bool;
}

struct IdTokenPolicy {
    expectedAudience     @0 :Text;           # registered client_id
    expectedAzp          @1 :Text;           # authorized party, if set
    requiredAcr          @2 :List(Text);     # any-of
    requiredAmr          @3 :List(Text);     # any-of
    maxAgeSeconds        @4 :UInt32;         # per OIDC core `max_age`
    clockSkewSeconds     @5 :UInt32;
    nonceMustMatch       @6 :Data;           # empty = no nonce check
    requireAtHashMatch   @7 :Bool;           # if accessToken present
    requireCHashMatch    @8 :Bool;           # if code present
}

struct IdTokenClaims {
    issuer     @0 :Text;
    subject    @1 :Text;
    audience   @2 :List(Text);
    issuedAt   @3 :Int64;
    expiresAt  @4 :Int64;
    notBefore  @5 :Int64;
    nonce      @6 :Data;

    acr        @7  :Text;
    amr        @8  :List(Text);
    azp        @9  :Text;
    authTime   @10 :Int64;

    email      @11 :Text;
    emailVerified @12 :Bool;
    preferredUsername @13 :Text;
    name       @14 :Text;
    groups     @15 :List(Text);

    # Opaque claim map for everything else (profile-specific fields,
    # custom claims). Values are JSON-encoded bytes.
    additional @16 :List(NamedBlob);
}

struct NamedBlob {
    name  @0 :Text;
    value @1 :Data;
}
```

`IdTokenClaims` is intentionally read-only metadata. Possessing a
serialized copy must not grant authority. The durable external subject key is
`subjectHash = hash(providerKind, issuer, tenant, subject)`; admission policy
maps it to a local principal, account, and profiles before a `UserSession` is
minted.

### External identity admission

OIDC authentication produces verified claims. It does not by itself create a
local account, select local roles, or grant capabilities. After
`verifyIdToken` succeeds, `SessionManager` resolves the external subject
through one of the identity proposal's admission sources:

- a manifest-seeded external admission rule for bootstrap, recovery, or
  early console login before durable storage exists;
- a local account-store `ExternalIdentityBinding` that maps
  `hash(providerKind, issuer, tenant, subject)` to an existing local
  principal; or
- an explicit auto-creation rule that creates a pseudonymous or
  tenant-scoped account with named policy and resource profiles.

The binding shape belongs with the account model, but OIDC consumers depend on
its semantics:

```capnp
struct ExternalIdentityBinding {
    bindingId @0 :Data;
    provider @1 :Text;        # OIDC issuer or configured provider name
    subjectHash @2 :Data;     # hash(provider kind, issuer, tenant, subject)
    principalId @3 :Data;     # local or pseudonymous principal
    tenant @4 :Text;
    acceptedClaims @5 :List(Text);
    expiresAtMs @6 :UInt64;
    policyProfile @7 :ProfileRef;
    resourceProfile @8 :ProfileRef;
    schemaVersion @9 :UInt32;
    storeEpoch @10 :UInt64;
    recordVersion @11 :UInt64;
    policyEpoch @12 :UInt64;
    previousHash @13 :Data;
    contentHash @14 :Data;
}
```

OIDC `groups`, `roles`, `acr`, `amr`, tenant IDs, device posture, source
network, and token age are normalized ABAC inputs. A binding rule may map a
provider group to a local role only for a named provider/tenant, expiry, and
policy version. Imported claims are discarded or refreshed when stale, and
roles selected from them remain broker inputs rather than authority.

An external session receives durable storage only when a binding or
auto-creation rule maps it to a local principal and a resource profile. Without
that mapping, the session is guest, anonymous, or one-shot pseudonymous policy
with narrow temporary resources.

### OAuth client

```capnp
interface OAuthClient {
    # Bound configuration.
    info              @0 () -> (meta :OAuthClientMetadata);

    # Authorization Code + PKCE (OAuth 2.1 default). The caller owns
    # the redirect side-channel; this cap drives the token exchange
    # after the code returns.
    startAuthCode     @1 (requested :TokenRequest)
                      -> (authUrl :Text, state :AuthCodeState);
    completeAuthCode  @2 (state :AuthCodeState,
                          code :Data)
                      -> (bundle :TokenBundle);

    # Device Authorization Grant (RFC 8628). Appropriate for serial
    # consoles, embedded displays, and TVs — anywhere the capOS
    # process has no browser.
    startDeviceCode   @3 (requested :TokenRequest)
                      -> (userCode :Text,
                          verificationUri :Text,
                          verificationUriComplete :Text,
                          expiresIn :UInt32,
                          interval :UInt32,
                          state :DeviceCodeState);
    pollDeviceCode    @4 (state :DeviceCodeState)
                      -> (outcome :DeviceCodePoll);

    # Client Credentials (RFC 6749 §4.4). Backend-to-backend; the
    # caller principal is the client itself.
    clientCredentials @5 (requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # Refresh an existing bundle (RFC 6749 §6). Fails if the stored
    # refresh token is expired or revoked.
    refresh           @6 (token :RefreshToken,
                          requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # JWT Bearer (RFC 7523). Caller presents a signed assertion about
    # a subject; issuer returns a token for that subject. Used for
    # service delegation and some IdP federation flows.
    jwtBearer         @7 (assertion :Data,
                          requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # Token Exchange (RFC 8693). Foundation of modern workload
    # identity federation: exchange a subject token (e.g. a signed
    # instance-identity JWT or an attestation report envelope) for
    # an access token at the remote issuer.
    tokenExchange     @8 (subjectToken :Data,
                          subjectTokenType :Text,     # RFC 8693 §2.1
                          actorToken :Data,
                          actorTokenType :Text,
                          requested :TokenRequest)
                      -> (bundle :TokenBundle);

    # Revoke (RFC 7009). Best-effort; not all IdPs honor it.
    revoke            @9 (token :TokenRef, reason :Text) -> ();
}

struct OAuthClientMetadata {
    clientId          @0 :Text;
    issuer            @1 :Text;
    authMethod        @2 :ClientAuthMethod;
    defaultScopes     @3 :List(Text);
    defaultAudience   @4 :Text;
    redirectUris      @5 :List(Text);
    dpopRequired      @6 :Bool;
    pkceRequired      @7 :Bool;     # true for public clients
}

enum ClientAuthMethod {
    none              @0;   # public client with PKCE
    clientSecretBasic @1;   # HTTP Basic; confidential clients
    clientSecretPost  @2;   # form-encoded; legacy
    privateKeyJwt     @3;   # RFC 7523 §2.2 — signed JWT with client's PrivateKey
    tlsClientAuth     @4;   # RFC 8705 — mTLS using TlsClientConfig
    selfSignedTlsClientAuth @5;
}

struct TokenRequest {
    scopes            @0 :List(Text);
    audience          @1 :Text;
    resource          @2 :List(Text);   # RFC 8707
    acrValues         @3 :List(Text);
    maxAgeSeconds     @4 :UInt32;
    prompt            @5 :List(Text);   # "login", "consent", "select_account", "none"
    loginHint         @6 :Text;
    nonce             @7 :Data;         # empty = generate fresh
    requestedExpirySeconds @8 :UInt32;  # hint; IdP has final say
    dpopKey           @9 :PrivateKey;   # optional DPoP binding
    extraParams       @10 :List(NamedBlob);
}

struct AuthCodeState {
    opaque @0 :Data;    # server-held state; PKCE verifier, nonce, etc.
}
struct DeviceCodeState {
    opaque @0 :Data;
}

struct DeviceCodePoll {
    union {
        pending     @0 :Void;
        slowDown    @1 :Void;
        expired     @2 :Void;
        denied      @3 :Void;
        granted     @4 :TokenBundle;
    }
}
```

### Tokens

```capnp
interface AccessToken {
    # Claims view (parsed once; opaque tokens return empty claims and
    # let the IdP's introspection endpoint be the source of truth).
    claims            @0 () -> (claims :TokenClaims);

    # Present the token for a single outbound HTTP request. The token
    # service inserts the Authorization / DPoP headers into the
    # outbound request built by the caller. Raw bytes do not leave
    # the token service through this path.
    authorize         @1 (request :OutboundHttpRequest)
                      -> (prepared :OutboundHttpRequest);

    # Down-scope to a narrower scope set or audience. Fails if the
    # requested scopes are not a subset of the current token's scopes.
    # Implementation can either return a wrapper cap that performs
    # client-side attenuation (for simple bearer tokens) or call the
    # IdP's token-exchange endpoint (for cross-audience narrowing).
    attenuate         @2 (scopes :List(Text),
                          audience :Text)
                      -> (narrower :AccessToken);

    # Explicit export for rare cases where the caller truly needs the
    # raw token (e.g. a capOS HTTP client that has no token-aware
    # stack). Emits an audit event naming the reason. Excluded by
    # default from attenuated caps returned by `attenuate`.
    exportRaw         @3 (reason :Text) -> (bytes :Data);

    # Token reference for revocation, introspection, or logging. Always
    # a hash or opaque ID; never the raw token.
    reference         @4 () -> (ref :TokenRef);

    # Expiry information for client-side backoff and pre-refresh.
    expiry            @5 () -> (notBefore :Int64, notAfter :Int64);
}

interface RefreshToken {
    # Refresh tokens are always longer-lived secrets. They do not
    # expose an `authorize` path — their only use is through
    # OAuthClient.refresh. `reference` and `expiry` match AccessToken.
    reference         @0 () -> (ref :TokenRef);
    expiry            @1 () -> (notBefore :Int64, notAfter :Int64);
    # Export is available but guarded and audited; used for migration
    # between token stores, not for ordinary operation.
    exportRaw         @2 (reason :Text) -> (bytes :Data);
}

interface IdToken {
    claims            @0 () -> (claims :IdTokenClaims);
    raw               @1 (reason :Text) -> (bytes :Data);
}

struct TokenBundle {
    access    @0 :AccessToken;
    refresh   @1 :RefreshToken;   # may be null
    id        @2 :IdToken;        # may be null
    expiresIn @3 :UInt32;
    tokenType @4 :Text;           # "Bearer" or "DPoP"
    scopes    @5 :List(Text);
    resource  @6 :List(Text);
}

struct TokenClaims {
    issuer     @0 :Text;
    subject    @1 :Text;
    audience   @2 :List(Text);
    scope      @3 :List(Text);
    clientId   @4 :Text;
    issuedAt   @5 :Int64;
    expiresAt  @6 :Int64;
    notBefore  @7 :Int64;
    jwtId      @8 :Text;
    # Confirmation (cnf, RFC 7800) for proof-of-possession tokens.
    confirmation @9 :TokenConfirmation;
    additional @10 :List(NamedBlob);
}

struct TokenConfirmation {
    union {
        none     @0 :Void;
        jkt      @1 :Data;        # DPoP: thumbprint of holder public key
        x5tS256  @2 :Data;        # mTLS client cert thumbprint
    }
}

struct TokenRef {
    kind      @0 :TokenRefKind;
    value     @1 :Data;           # hash, jti, or opaque server ref
}

enum TokenRefKind {
    jti       @0;    # JWT `jti`
    sha256    @1;    # SHA-256 of the raw token
    serverId  @2;    # opaque IdP-side identifier
}

struct OutboundHttpRequest {
    method    @0 :Text;
    url       @1 :Text;
    headers   @2 :List(NamedBlob);
    body      @3 :Data;
}
```

### Token verifier (resource-server side)

```capnp
interface TokenVerifier {
    # Validate an inbound bearer token: signature against the
    # provider's JWKS (or introspection endpoint for opaque tokens),
    # issuer, audience, expiry, required scopes, confirmation claim
    # (DPoP proof or mTLS peer cert).
    verifyAccess      @0 (token :Data,
                          policy :TokenVerificationPolicy,
                          proof :VerificationProof)
                      -> (outcome :TokenVerificationOutcome);
}

struct TokenVerificationPolicy {
    expectedIssuer    @0 :Text;
    expectedAudience  @1 :Text;
    requiredScopes    @2 :List(Text);     # all-of
    anyRequiredScopes @3 :List(Text);     # any-of if non-empty
    clockSkewSeconds  @4 :UInt32;
    requireConfirmation @5 :ConfirmationKind;   # none / dpop / mtls
    allowedAlgorithms @6 :List(SignatureScheme);
    allowIntrospection @7 :Bool;          # opaque token support
}

enum ConfirmationKind {
    none @0;
    dpop @1;
    mtls @2;
}

struct VerificationProof {
    union {
        none      @0 :Void;
        dpopProof @1 :DpopProof;
        peerCert  @2 :Certificate;
    }
}

struct DpopProof {
    jwt       @0 :Data;                   # the DPoP header value
    httpMethod @1 :Text;
    httpUrl   @2 :Text;
    nonce     @3 :Data;                   # server-issued DPoP nonce (RFC 9449 §8)
}

struct TokenVerificationOutcome {
    union {
        valid   @0 :ValidToken;
        invalid @1 :TokenVerificationFailure;
    }
}

struct ValidToken {
    claims     @0 :TokenClaims;
    algorithm  @1 :SignatureScheme;
    keyId      @2 :Text;
}

struct TokenVerificationFailure {
    reason     @0 :TokenFailureReason;
    detail     @1 :Text;
}

enum TokenFailureReason {
    badSignature        @0;
    unknownKeyId        @1;
    unexpectedIssuer    @2;
    audienceMismatch    @3;
    expired             @4;
    notYetValid         @5;
    insufficientScopes  @6;
    missingConfirmation @7;
    dpopMismatch        @8;
    mtlsThumbprintMismatch @9;
    revoked             @10;
    malformed           @11;
    introspectionDenied @12;
    weakAlgorithm       @13;
}
```

### JWKS

```capnp
interface Jwks {
    # Public keys exposed as PublicKey caps keyed by `kid`. Key
    # rotation is invisible to callers: they ask for a `kid`, they
    # get a current PublicKey or `unknownKeyId`.
    keyById    @0 (kid :Text) -> (key :PublicKey);

    # Enumerate keys (for diagnostics and admin). Returns metadata
    # only; PublicKey caps come from keyById.
    listKeyMeta @1 () -> (keys :List(JwkMeta));

    # Monotonic version bumped on every refresh that changes the key
    # set; consumers cache validated signatures by (kid, version).
    version    @2 () -> (n :UInt64);

    # Force a refresh. Audited. Called automatically on
    # verification-time `unknownKeyId`; exposed for admin use.
    refresh    @3 () -> ();
}

struct JwkMeta {
    kid        @0 :Text;
    algorithm  @1 :AsymmetricAlgorithm;
    use        @2 :Text;        # "sig" or "enc"
    scheme     @3 :SignatureScheme;
    createdAt  @4 :Int64;
}
```

### Workload identity federation

```capnp
interface WorkloadIdentityFederation {
    # Produce a fresh remote access token by exchanging a local
    # subject token (instance-identity JWT, attestation report,
    # Kubernetes projected token, GitHub Actions OIDC token, ...)
    # at the remote issuer per RFC 8693.
    exchange   @0 (requested :TokenRequest)
               -> (bundle :TokenBundle);

    info       @1 () -> (meta :WorkloadFederationMeta);
}

struct WorkloadFederationMeta {
    remoteIssuer        @0 :Text;
    audience            @1 :Text;
    subjectSource       @2 :SubjectSource;
    allowedScopes       @3 :List(Text);
    minRefreshInterval  @4 :UInt32;
}

enum SubjectSource {
    instanceIdentityJwt    @0;   # from CloudMetadata.InstanceIdentity
    attestationReport      @1;   # SEV-SNP / TDX / Nitro
    projectedServiceAccount @2;  # e.g. Kubernetes projected token
    githubActionsOidc      @3;   # ci/cd trust anchor
    localPrivateKeyJwt     @4;   # private_key_jwt against remote STS
}
```

### DPoP

DPoP (RFC 9449) binds a token to a client-held key. The binding is
expressed as a `TokenConfirmation.jkt` on the access token plus a
short-lived proof JWT per outbound request.

```capnp
interface DpopSigner {
    # Returns a fresh DPoP proof JWT for an outbound request. The
    # signer holds the PrivateKey; the access token is `jkt`-bound to
    # that key's thumbprint.
    newProof   @0 (method :Text,
                   url :Text,
                   accessTokenHash :Data,
                   serverNonce :Data)
               -> (proofJwt :Data);

    publicKey  @1 () -> (pk :PublicKey);
}
```

A deployment requiring DPoP composes `AccessToken` + `DpopSigner` in
a wrapper cap so ordinary callers just invoke `authorize` and receive
a request with both `Authorization: DPoP ...` and `DPoP:` headers set.

### JWT wrappers over key-management primitives

These live here rather than in the key-management proposal because
JWT is a protocol frame, not a crypto primitive. They are thin
adapters over `PrivateKey` / `PublicKey`.

```capnp
interface JwtSigner {
    # Sign a compact-serialized JWT. The key lives in a KeyVault;
    # JwtSigner is the schema-aware wrapper.
    sign       @0 (header :JwtHeader, claims :Data) -> (jwt :Data);
    publicKey  @1 () -> (pk :PublicKey);
    keyId      @2 () -> (kid :Text);
}

interface JwtVerifier {
    verify     @0 (jwt :Data, policy :JwtVerifyPolicy)
               -> (outcome :JwtVerifyOutcome);
}

struct JwtHeader {
    algorithm  @0 :SignatureScheme;
    keyId      @1 :Text;
    type       @2 :Text;            # "JWT", "at+jwt", "dpop+jwt"
    contentType @3 :Text;
}

struct JwtVerifyPolicy {
    expectedIssuer    @0 :Text;
    expectedAudience  @1 :Text;
    expectedType      @2 :Text;
    allowedAlgorithms @3 :List(SignatureScheme);
    clockSkewSeconds  @4 :UInt32;
    jwksSource        @5 :Jwks;     # preferred
    staticKey         @6 :PublicKey; # for single-signer cases
}

struct JwtVerifyOutcome {
    union {
        valid   @0 :JwtValid;
        invalid @1 :JwtInvalid;
    }
}

struct JwtValid {
    header     @0 :JwtHeader;
    claims     @1 :Data;
}

struct JwtInvalid {
    reason     @0 :TokenFailureReason;
    detail     @1 :Text;
}
```

`SignatureScheme` is reused from the key-management proposal. Adding
`ps256`/`ps384`/`ps512` and `es256`/`es384`/`es512` aliases there
covers the JWT algorithm registry without duplicating the enum.

## Grant Types in Detail

### Authorization Code + PKCE

Used by the web text shell gateway and any capOS native app with a
browser. PKCE is mandatory (OAuth 2.1); `code_challenge_method = S256`.
The `AuthCodeState.opaque` blob carries the PKCE verifier, nonce, and
original `TokenRequest`; callers do not see or store these
values. Redirect URIs are validated against `OAuthClientMetadata`
exactly, no partial matching.

### Device Authorization Grant (RFC 8628)

Used on serial consoles and other no-browser surfaces. The console
prints `verification_uri` and `user_code`; the user completes the
flow in a separate device's browser; the console polls the token
endpoint. `pollDeviceCode` honors the `slow_down` response and caps
its polling rate at the IdP-advertised `interval`. Expiration is a
hard fail; the console must restart the flow.

This is the primary OIDC path for boot-to-shell on headless hosts and
for interactive cloud-VM serial consoles.

### Client Credentials

Used for backend-to-backend service identity. The calling service
holds an `OAuthClient` cap configured with `privateKeyJwt` or
`tlsClientAuth`. No user is involved; the subject of the issued token
is the client itself.

### Refresh

Used to rotate a short-lived access token without re-authenticating
the user. Refresh tokens are long-lived secrets and live in the
`RefreshToken` cap; they never appear as bytes in session state.
Rotated refresh tokens (IdPs that issue a new refresh token on every
refresh) are installed into the same cap transparently.

### JWT Bearer (RFC 7523)

Used for federation between systems that trust a common signing key.
A capOS service holding a `JwtSigner` can mint an assertion identifying
a subject and exchange it at the IdP for a token acting on behalf of
that subject. Used sparingly; the delegation implication is strong.

### Token Exchange (RFC 8693)

The foundation of modern workload identity federation. Described in
its own subsystem (`WorkloadIdentityFederation`) because the
subject-token source is platform-specific. Concrete mappings:

- **AWS IRSA / IAM OIDC provider**: subject token is a Kubernetes
  projected service-account JWT; IdP is `sts.amazonaws.com`;
  `AssumeRoleWithWebIdentity` returns AWS-scoped credentials.
- **GCP Workload Identity Federation**: subject token is an
  `InstanceIdentity` JWT from the GCE metadata service or a
  Kubernetes projected token; IdP is `sts.googleapis.com`; returned
  token is usable against GCP APIs including Cloud KMS.
- **Azure federated identity credentials**: subject token is an
  OIDC token from a trusted IdP (GitHub, GitLab, Kubernetes,
  another capOS instance); IdP is Azure AD; returned token is a
  standard AAD access token.
- **SEV-SNP / TDX / Nitro attestation**: subject token is the
  attestation report envelope; IdP is the cloud KMS or a standalone
  attestation verifier; returned token authorizes a KMS Decrypt
  against an attestation-policy-gated KEK.

In every case the capOS image contains no long-lived credentials. The
boot path produces a local `InstanceIdentity` cap, passes it to a
`WorkloadIdentityFederation` configured for the target cloud, and
receives short-lived tokens that KMS and other services accept.

## Trust Bootstrap

An `OidcIdentityProvider` cap is created by a trusted service (the
OAuth service) from a provider configuration record. The record
includes:

- The canonical issuer URL.
- One of:
  - a fixed JWKS snapshot baked into the manifest (for air-gapped or
    hermetic deployments), or
  - the discovery URL plus one or more pinned root certs / SPKI
    hashes for the TLS connection that fetches discovery and JWKS
    (via `TlsClientConfig` and `PinSet` from the certificates
    proposal).
- Acceptable algorithms (`allowedAlgorithms` in policy).
- Minimum token lifetime and maximum clock skew.
- Whether the IdP advertises token exchange, DPoP, and PAR (pushed
  authorization requests).
- Client registrations allowed to use this IdP.

The trust root for OIDC verification is ultimately the TLS trust
chain back to a certificate authority plus the discovery document's
signing policy. `OidcIdentityProvider` therefore depends on a
`TlsClientConfig` from the certificates proposal, not on raw sockets.
Issuer URL mismatches and JWKS failures are hard errors; neither
falls back to unauthenticated HTTP.

For enterprise IdPs that rotate signing keys frequently, `Jwks`
caches keys with a short TTL and refreshes on verification-time
`unknownKeyId`. A deployment that wants to forbid automatic refresh
(to pin a specific key set) configures `Jwks` with refresh disabled;
key rotation then requires a manifest update.

## Authentication Strength Mapping

`SessionInfo.authStrength` from user-identity uses X.1254 LoA tiers.
OIDC `acr`/`amr` claims map as follows (deployment-configurable):

- `loa1` — self-asserted, `amr` includes `pwd` only, `acr` absent or
  low.
- `loa2` — single-factor, `amr` includes `pwd`, `pin`, or
  `email`-link style.
- `loa3` — multi-factor with a hardware-backed credential: `amr`
  contains `hwk`, `swk` with device attestation, `face`+`pwd`,
  `fpt`+`pwd`, or equivalent; `acr` typically names a named MFA
  policy.
- `loa4` — high-assurance, typically requires identity proofing plus
  tamper-resistant hardware: `amr` contains `pop` with attested
  device, `hwk` plus `face`, in-person proofing claims, or vendor-
  specific high-assurance `acr` values.

The mapping table lives in `OAuthClientMetadata` policy, not hard-
coded. `loa0` (anonymous) is capOS-specific and has no matching OIDC
claim; anonymous sessions do not use OIDC.

## Consumers

| Consumer                         | Uses                                                             |
|----------------------------------|------------------------------------------------------------------|
| Console login (device code)      | `OAuthClient.startDeviceCode` + `verifyIdToken`                  |
| Web text shell login             | `OAuthClient.startAuthCode` + `verifyIdToken`; TLS from certs    |
| Cloud KMS access (no baked creds)| `WorkloadIdentityFederation.exchange` → `AccessToken.authorize`  |
| `CloudKmsKeySource` unlock       | Wraps `AccessToken.authorize`; no ambient cloud credentials      |
| Service-to-service outbound HTTP | `OAuthClient.clientCredentials` + `AccessToken.authorize`        |
| Inbound API token validation     | `TokenVerifier.verifyAccess`                                     |
| Per-user `EncryptedNamespace`    | `OidcFederatedKeySource` derives KEK from user's `AccessToken`   |
| Audit / telemetry export         | Service identity via client credentials + DPoP                   |
| CI/CD runtime trust              | `WorkloadIdentityFederation` from GitHub Actions OIDC            |

## Threat Model

Specific to this subsystem:

1. **Token leakage via logs.** The classic OAuth failure mode. Raw
   tokens never leave the OAuth service through claims, references,
   or audit records. `exportRaw` is the only escape hatch and is
   audited with a mandatory reason string.
2. **Refresh token theft.** Refresh tokens are long-lived secrets.
   Mitigations: storage in the same service that holds the cap
   (not in session state, not in cookies readable by shells),
   optional rotation on refresh, revocation on logout.
3. **Replay of bearer tokens.** A stolen bearer token is usable
   until expiry. Mitigations: short TTLs; require DPoP
   (`ConfirmationKind.dpop`) for sensitive resources; mTLS for
   service-to-service. Nonce-bound DPoP proofs (RFC 9449 §8) with
   server-issued nonces where the resource server supports them.
4. **Mixed-IdP confusion.** A token issued by IdP A is presented to
   a verifier expecting IdP B. Mitigations: strict `expectedIssuer`
   match; audience binding; IdP-specific `OAuthClient` caps so
   services cannot confuse two OIDC providers; RFC 9207 `iss`
   parameter on authorization responses verified before the token
   exchange.
5. **Discovery-document tampering.** An attacker on the TLS path
   returns a forged discovery document or JWKS. Mitigations: pinned
   TLS roots or SPKI hashes per IdP; JWKS fetched over the same
   pinned TLS client; signature algorithm allow-list rejects
   downgrades; manifest-defined acceptable discovery URL prevents
   runtime redirect to attacker IdP.
6. **PKCE downgrade.** A public client accepts a token without
   proving possession of the code verifier. Mitigations: PKCE is
   mandatory (`pkceRequired = true` is not a bit the caller can
   clear from a derived cap); `code_challenge_method = S256` only.
7. **Authorization code replay.** A leaked code is redeemed by an
   attacker. Mitigations: PKCE binds the code to the verifier the
   browser holds; codes are single-use; redirect URI exact match.
8. **Open redirector via redirect URI.** Mitigations:
   exact-match redirect URIs per registration; no substring
   matching; validated at both `startAuthCode` and
   `completeAuthCode`.
9. **Cross-site request forgery on the authorization request.**
   Mitigations: `state` parameter generated from
   `EntropySource`, stored in `AuthCodeState.opaque`, checked on
   completion; PKCE adds a second CSRF-resistant binding.
10. **OIDC `nonce` omission.** Missing `nonce` on the ID token
    allows replay of an ID token from another session. Mitigations:
    `IdTokenPolicy.nonceMustMatch` is mandatory for interactive
    logins; `verifyIdToken` refuses an ID token whose `nonce` does
    not match the one baked into `AuthCodeState.opaque`.
11. **Mis-issued `sub` claim.** An IdP reuses a `sub` across tenants
    or rebinds it. Mitigations: the external subject key includes
    provider kind, issuer, normalized tenant, and subject; it is never
    `sub` alone. Tenant-scoped IdPs (Azure AD per-tenant, Google
    Workspace) still record the tenant explicitly before hashing.
12. **JWKS flooding.** An attacker forces repeated `unknownKeyId`
    failures to trigger JWKS refreshes. Mitigations: refresh rate-
    limited per `Jwks` cap; audit events recorded; repeated failures
    fail closed rather than refresh-in-loop.
13. **Token exchange policy evasion.** An attacker with a narrow
    subject token exchanges it for a broader one. Mitigations: the
    remote issuer enforces its own policy on token exchange; capOS
    cannot prevent a misconfigured STS. Defense is to pin
    `WorkloadFederationMeta.remoteIssuer` and inspect returned
    scopes against `allowedScopes`.
14. **Clock skew attacks.** Old tokens accepted, new tokens
    rejected. Mitigations: `clockSkewSeconds` is small by default;
    consumers that require hard bounds use an attested time source.

## Security Verification in ITU-T and GOST Terms

OIDC and OAuth2 are IETF/OpenID protocols, but capOS's broader
security vocabulary is ITU-T/ISO-IEC plus, where a deployment
requires it, GOST. The same verification surface this proposal
defines (signature checks on JWTs, discovery and JWKS integrity,
token binding, claim validation, scope enforcement, auth strength,
logout semantics) maps onto those frameworks cleanly; it does not
require a parallel vocabulary.

### ITU-T X.805 security dimensions

X.805 ("Security architecture for systems providing end-to-end
communications") decomposes security into eight dimensions. The
relevant mapping for the OIDC subsystem:

| X.805 dimension        | Where it lives                                                                               |
|------------------------|----------------------------------------------------------------------------------------------|
| Access control         | `AuthorityBroker` + `CapObject::call` (ADF/AEF per X.812); scopes/claims as ABAC input       |
| Authentication         | `OidcIdentityProvider.verifyIdToken`; `TokenVerifier.verifyAccess`                           |
| Non-repudiation        | Signed JWTs + audit records of `verifyIdToken`, issuance, exchange, revocation               |
| Data confidentiality   | TLS for every IdP call; encrypted audit payloads where applicable                            |
| Communication security | `TlsClientConfig` from the certificates proposal; issuer-pinned roots; HSTS-equivalent pins  |
| Data integrity         | JWT signature verification against `Jwks`; `kid` rotation handled without trust decay        |
| Availability           | Failure semantics defined for JWKS refresh, device-code expiry, introspection outage         |
| Privacy                | `IdTokenClaims` exposes only claims the client actually requires; scope minimization         |

Each cell is a discrete thing to verify, test, and review. Keeping
the dimensions explicit makes gaps visible: for example, "what is our
availability story if the IdP's JWKS endpoint is down for 2 hours"
is a concrete X.805 question; the answer is `Jwks` cache TTL +
refresh audit + fail-closed behavior on unknown `kid`.

### ITU-T X.812 ADF/AEF

Already inherited from `user-identity-and-policy-proposal.md`. The
OIDC-specific instances:

- **AEF** (enforcement point): `CapObject::call` and wrapper caps
  (`AccessToken.authorize`, `TokenVerifier.verifyAccess`). Bypass
  requires subverting the cap graph, not forging a claim.
- **ADF** (decision point): the OAuth service when issuing a token,
  `AuthorityBroker` when returning scoped caps, `TokenVerifier` when
  accepting a bearer. A decision returns a capability (or denial);
  it does not return a boolean that downstream code might ignore.

### ITU-T X.1254 / ISO/IEC 29115 LoA

Already built into the mapping: `IdTokenClaims.acr`/`amr` →
`AuthStrength` enum (loa1..loa4). The mapping table lives in
`OAuthClientMetadata` so each deployment can specify which IdP
`acr`/`amr` values count as each tier. `SealPolicy.tokenExchange`
carries `minAuthStrength` so unlock policy can say "require LoA 3+"
without knowing any specific IdP's `acr` taxonomy.

### ITU-T X.1252 identity management terms

X.1252 defines `identity`, `credential`, `entity`, `enrolment`,
`identity provider`, `relying party`, and `identity assurance`. The
proposal's entities map directly:

| X.1252 term            | capOS realization                                                              |
|------------------------|--------------------------------------------------------------------------------|
| Identity provider      | `OidcIdentityProvider`                                                         |
| Relying party          | Any service holding an `OAuthClient` cap                                       |
| Credential             | Bearer, DPoP-bound, or mTLS-bound `AccessToken`; `IdToken`; `RefreshToken`     |
| Enrolment              | `CredentialStore` bootstrap of IdP trust records + subject allow-list          |
| Assurance level        | `AuthStrength` (= X.1254 LoA)                                                  |
| Attribute authority    | IdP via claims; optionally `PolicyEngine` for derived ABAC attributes          |
| Identity binding       | Canonical `subjectHash` mapped to a local `PrincipalInfo.id`; never `sub` alone |

### ITU-T X.1255 and federated-identity discovery

X.1255 is the discovery framework for federated identity. The closest
IETF analog is OIDC Discovery (RFC 8414 + OpenID Discovery 1.0).
`OidcIdentityProvider.metadata` is the capOS surface for both. The
manifest-declared discovery URL + pinned TLS root closes the
"federated discovery must be trustworthy" requirement that X.1255
leaves to deployment.

### ITU-T X.813 / ISO/IEC 10181-4 non-repudiation

Non-repudiation of *authentication* comes from the IdP's signed ID
token. Non-repudiation of *authorization decisions* comes from
`AuditLog` records that include the decision inputs (claim
summaries, policy IDs, outcome). The framework deliberately does
not promise non-repudiation of *shell commands* — the agent shell
is a planner, not a signer of operator intent.

### IETF OAuth security BCPs

For completeness, the proposal tracks:

- **RFC 6819** — OAuth 2.0 Threat Model and Security Considerations.
  Covered by the threat-model section above.
- **RFC 9700** — OAuth 2.0 Security Best Current Practice. The
  "PKCE mandatory", "exact redirect URI match", "mix-up defense
  via `iss` parameter", "no implicit grant", and "rotate refresh
  tokens" items are all baked in rather than opt-in.
- **FAPI 2.0 (OpenID Foundation)** — financial-grade API profile.
  Useful as a pre-packaged high-assurance profile: DPoP or mTLS
  sender-constrained tokens, PAR, signed authorization requests,
  strict algorithms. `OAuthClientMetadata` is deliberately shaped
  so a "FAPI profile" is a set of required fields, not a separate
  interface.

### GOST MAC/MIC (ГОСТ Р 59383-2021, ГОСТ Р 59453.1-2021)

capOS's mandatory-access-control and mandatory-integrity-control
story is described at two levels in
[user-identity-and-policy-proposal.md](user-identity-and-policy-proposal.md)
and [formal-mac-mic-proposal.md](formal-mac-mic-proposal.md):

- a **pragmatic** level where userspace brokers and wrapper caps
  enforce labels at grant paths, and
- a **formal** level where an abstract automaton (subjects,
  objects, containers, hold edges, rights, accesses, information
  flows) carries explicit safety predicates and proof obligations
  in the shape ГОСТ Р 59453.1-2021 requires.

OIDC integration must fit both levels without introducing a second
authority channel. Concretely:

#### Federated principals and subjects

An OIDC-authenticated `UserSession` creates a subject in the
formal automaton with:

- `subjectHash = hash(providerKind, iss, tenant, sub)` — the durable external
  subject key, not reusable across IdPs or tenants. The local session principal
  may be a pseudonymous principal created for this external key or the local
  principal named by an `ExternalIdentityBinding`.
- `confidentiality_label` and `integrity_label` resolved by
  `LabelAuthority` from the policy profile plus optional
  claim-derived refinement (e.g. `groups = ["ops"]` narrows to a
  specific compartment). Claims **influence** labels at mint time;
  they are not authority downstream.
- `authStrength` from `acr`/`amr`, already folded into LoA tiers.

The `create_session` transition in the formal automaton therefore
has one additional precondition when the login method is OIDC:

```text
create_session(principal, policy_profile, resource_profile, oidc_proof):
  pre:
    verify_id_token(oidc_proof) succeeds with IdTokenPolicy
    IdP trust record in CredentialStore permits (subjectHash, policy_profile)
    manifest seed or AccountStore admission permits the binding
    acr/amr satisfy policy_profile's minimum AuthStrength
    subject allow-list or ExternalIdentityBinding admits subjectHash
  effect:
    new subject s with labels derived from policy_profile + claims
    Hold(s, session_bundle) per AuthorityBroker(
        session,
        policy_profile,
        resource_profile,
    )
```

This is the same precondition shape as password and passkey login —
the safety proof does not branch on authentication method. It only
requires that `verify_id_token` is modeled as a trusted verifier
that rejects inputs failing the IdP's published policy.

#### Integrity labels on IdP trust

IdP trust records carry an integrity level. An IdP configured as
the corporate operator IdP can mint sessions with higher integrity
than an IdP configured for guest/partner access. `LabelAuthority`
encodes this in the trust-record metadata; `SessionManager` refuses
to mint a session whose policy profile claims higher integrity than the
admitting IdP's integrity level.

The formal invariant:

```text
integrity(session) <= integrity(admitting_IdP_trust_record)
```

This closes the federated analog of "any trusted login path can
mint a maximally trusted session" — a gap that is easy to
introduce by accident when enterprises add a second, looser IdP.

#### Flow classes for token capabilities

Each method on the typed token interfaces needs a flow class per
the `formal-mac-mic-proposal.md` table. Proposed classifications:

```text
OidcIdentityProvider.verifyIdToken    ReadLike + NoFlow   (pure verification)
OidcIdentityProvider.metadata         ObserveLike
Jwks.keyById                          ObserveLike
Jwks.refresh                          ControlLike         (on the Jwks object)

OAuthClient.startAuthCode             ObserveLike         (emits a URL; no subject-bearing data crosses)
OAuthClient.completeAuthCode          TransferLike        (materializes new authority as a token cap)
OAuthClient.startDeviceCode           ObserveLike
OAuthClient.pollDeviceCode            TransferLike        (on "granted")
OAuthClient.clientCredentials         TransferLike
OAuthClient.refresh                   TransferLike
OAuthClient.jwtBearer                 TransferLike + ControlLike  (delegation)
OAuthClient.tokenExchange             TransferLike        (see narrowing below)
OAuthClient.revoke                    ControlLike

AccessToken.claims                    ReadLike            (claims are metadata of the token object)
AccessToken.authorize                 WriteLike           (outbound side-effect under the token's authority)
AccessToken.attenuate                 TransferLike        (narrower cap minted)
AccessToken.exportRaw                 Declassify          (trusted, audited, restricted)
AccessToken.reference/expiry          ObserveLike

RefreshToken.*                        as above; exportRaw is Declassify
IdToken.raw                           Declassify
IdToken.claims                        ReadLike

TokenVerifier.verifyAccess            ReadLike + NoFlow
DpopSigner.newProof                   WriteLike           (produces a short-lived authenticator bound to a request)
WorkloadIdentityFederation.exchange   TransferLike
```

The key formal-level consequences:

- `AccessToken.exportRaw`, `RefreshToken.exportRaw`, and
  `IdToken.raw` are `Declassify` transitions. They must be
  modeled as trusted transitions with explicit audit. Excluding
  them by default from attenuated caps is consistent with the
  formal model's requirement that declassification go through
  explicit trusted subjects.
- `OAuthClient.tokenExchange` and `AccessToken.attenuate` are
  `TransferLike`; they cannot widen authority. The safety
  predicate is "issued-token scope ⊆ input-token scope ∩ policy
  permits" — exactly the wrapper-narrowing rule from
  `user-identity-and-policy-proposal.md`. The proof obligation is
  a scope-monotonicity lemma on the server side; capOS verifies
  the result by comparing `TokenClaims` before accepting the
  returned cap.
- `AccessToken.authorize` is `WriteLike` against the external
  resource. In the formal model this is an outbound information
  flow from the subject to an object whose label is the label of
  the downstream service the broker wired into the request.
  Deployments needing a MIC proof must ensure the broker refuses
  to bind a low-integrity session's token into a request against
  a high-integrity service — the `integrity(src) >= integrity(dst)`
  rule applied through the broker.

#### Token attenuation as the wrapper-cap discipline

ГОСТ Р 59453.1 requires that every transfer either preserves or
narrows rights; capability attenuation is the capOS mechanism for
that. OIDC's `scope` is a list of strings; treating scope narrowing
as cap attenuation means the verifier at issuance time must reject
any `attenuate` / `tokenExchange` result whose claimed scope is
not a subset of the source token's scope. This is already the
spec's behavior — the point is that the capOS implementation must
enforce it locally as well, because a misbehaving STS would
otherwise be a covert widening channel.

#### Subject-controls-subject and delegation

`OAuthClient.jwtBearer` (RFC 7523) lets a client speak on behalf of
another principal. That is a `ControlLike` transition in the
formal model: the invoking subject is exercising control over the
minted subject. The safety predicate is:

```text
supervise_allowed(invoker, delegated):
  integrity(invoker) >= integrity(delegated)
  and invoker holds a delegation capability for the target IdP
  and confidentiality/compartment labels are compatible
```

This is the formal reason a `jwtBearer` cap is not a default
session authority — it must come from a broker that checks the
control relation.

#### Endpoint declarations

`formal-mac-mic-proposal.md` requires every endpoint to declare
its flow policy. For OIDC-facing services that is:

- `OidcIdentityProvider` endpoints declare `ObserveLike` on
  metadata calls and `ReadLike` on verification.
- `OAuthClient` endpoints declare the flow classes above and bind
  the output token's label to `min(session.label, target_audience.label)`.
- `TokenVerifier` endpoints declare `ReadLike` and bind the
  verified claims to the caller's object label (the claims flow
  into an object owned by the calling service).

Declaring these up-front lets the `formal-mac-mic-proposal.md`
review gate apply without a separate OIDC-specific checker.

#### ГОСТ Р 58833-2020 — identification and authentication

Beyond MAC/MIC, ГОСТ Р 58833-2020 defines organizational and
technical requirements for identification and authentication.
OIDC integration satisfies its technical baseline:

- Identifiers use `subjectHash = hash(providerKind, issuer, tenant, subject)`;
  subject reuse across IdPs or tenants is disallowed by construction.
- Credentials (tokens, refresh tokens, DPoP keys) are held inside
  the OAuth service; raw material does not reach the model, the
  shell, or audit.
- Issuance and revocation (`OAuthClient.startAuthCode/
  startDeviceCode/clientCredentials/...`, `revoke`,
  `SessionManager.logout`) are audited.
- Credential-strength policy is selectable per resource via
  `minAuthStrength` on seal policies and broker decisions,
  aligned to X.1254 / ISO/IEC 29115 LoA.

Organizational measures (credential lifecycle, incident response,
operator training) remain a deployment responsibility the OS
cannot enforce alone.

#### Proof-obligation checklist

A deployment aiming for a GOST-style MAC/MIC claim with OIDC
federation must add these obligations to the
`formal-mac-mic-proposal.md` proof. The checklist is explicit so
reviewers can point at individual items, and so each obligation
maps to one of the tools listed in the next subsection.

1. **`verify_id_token` totality and policy soundness.** Modeled as
   a trusted total function. Accepts only well-formed tokens under
   the configured `IdTokenPolicy` (issuer, audience, `acr`/`amr`,
   `exp`/`nbf`/`iat` with bounded skew, `nonce`, `at_hash` /
   `c_hash` when applicable). Returns `IdTokenClaims` or a failure
   reason; never silently downgrades.
2. **PKCE binding.** No `completeAuthCode(state, code)` succeeds
   unless `state` was produced by a prior `startAuthCode` and the
   PKCE verifier stored in `AuthCodeState.opaque` hashes to the
   `code_challenge` the IdP recorded for `code`.
3. **Nonce binding.** `verifyIdToken` accepts an ID token only if
   `claims.nonce` equals the nonce stored in `AuthCodeState.opaque`
   for the matching `state`. Missing-nonce ID tokens on
   interactive logins are rejected.
4. **`state` binding.** The authorization response's `state`
   matches the one minted from `EntropySource` at `startAuthCode`.
5. **Scope monotonicity.** Every `TransferLike` token transition
   (`AccessToken.attenuate`, `OAuthClient.tokenExchange`,
   `OAuthClient.refresh`, `OAuthClient.jwtBearer`) produces a
   result whose scope is a subset of the input scope intersected
   with the broker/IdP-permitted set. No transition widens scope.
6. **JWKS live-set invariant.** A token signed under `kid = k` is
   accepted iff `k` was present in `Jwks` at some time `t` with
   `iat - clockSkew ≤ t ≤ now`. Rotation that removes `k` does
   not retroactively invalidate tokens already verified under it;
   rotation that adds `k` does not accept tokens older than its
   introduction.
7. **Device-code polling discipline.** `pollDeviceCode` honors the
   IdP-issued `interval`; `slow_down` responses monotonically
   increase the local backoff; `expired` and `denied` are
   terminal.
8. **Refresh rotation invariant.** A successful
   `OAuthClient.refresh` that rotates the refresh token marks the
   prior `RefreshToken` cap broken; any subsequent use returns
   `revoked` (no parallel use of two generations of the same
   refresh-token family).
9. **Session-creation MAC/MIC predicate.** `create_session` with
   an OIDC proof establishes `integrity(session) ≤
   integrity(admitting_IdP_trust_record)` and
   `confidentiality(session) ⊑ confidentiality_ceiling(policy_profile,
   claims)`.
10. **Broker-outbound MAC/MIC predicate.** When the broker binds
    an `AccessToken` to an outbound request, the call site label
    satisfies `integrity(src) ≥ integrity(dst)` and the
    confidentiality flow is permitted. `jwtBearer` delegations
    additionally satisfy `supervise_allowed(invoker, delegated)`.

Additional implicit obligations:

- `Declassify` transitions (`AccessToken.exportRaw`,
  `RefreshToken.exportRaw`, `IdToken.raw`) are restricted to
  trusted subjects and produce audit records with the mandatory
  `reason` argument.
- Endpoint flow declarations for OIDC services cover every
  method in the schemas above; adding a new method without a
  declaration is a review failure.

These are additive to the obligations in
`formal-mac-mic-proposal.md`. None require a new kernel mechanism;
they extend the same wrapper-cap / endpoint-flow-declaration
discipline to OIDC-backed subjects and token-typed capabilities.

#### Tool assignment

| Obligation                                  | Primary tool          | Notes                                                         |
|---------------------------------------------|-----------------------|---------------------------------------------------------------|
| 1. `verify_id_token` totality               | TLA+ + Kani           | TLA+ models the trusted function; Kani proves the Rust impl is total |
| 2. PKCE binding                             | TLA+                  | 3-state machine (started/completed/failed); invariant on state |
| 3. Nonce binding                            | TLA+                  | Joint state with PKCE, same module                            |
| 4. `state` binding                          | TLA+                  | Joint with 2/3; plus Alloy for `EntropySource` uniqueness     |
| 5. Scope monotonicity                       | Alloy + Prusti        | Alloy for the `attenuate`/`exchange` graph; Prusti as post-condition |
| 6. JWKS live-set invariant                  | TLA+                  | Temporal property; Apalache if TLC state-space explodes       |
| 7. Device-code polling discipline           | Z.100 SDL + TLA+      | SDL for state + timer structure; TLA+ for liveness            |
| 8. Refresh rotation invariant               | TLA+                  | Safety + single-generation liveness                           |
| 9. Session-creation MAC/MIC predicate       | Alloy                 | Extends the hold-edge graph model from `formal-mac-mic`       |
| 10. Broker-outbound MAC/MIC predicate       | Alloy                 | Same model; predicate over outbound endpoint declarations     |
| Declassify auditing                         | Kani                  | Rust-level: every `exportRaw` path writes an audit record     |
| Endpoint flow declarations                  | Review gate + Alloy   | Enumerate methods, check coverage relationally                |

Supporting artifacts (useful even before the full proof lands):

- **Z.120 MSC** sequence charts for the three primary flows
  (authorization code + PKCE, device code, token exchange). MSC
  traces from a running capOS are already shaped like the sequence
  dumps `tools/ccs` produces for capability rings, which makes
  property-checking "no RETURN without a matching CALL" a
  straightforward analog to "no token issuance without a matching
  authorization event."
- **Proptest/fuzz harnesses** for the JWT parser, claim validator,
  PKCE verifier hash, DPoP proof parser, and discovery-document
  parser. These are not formal proofs but are the first line of
  defense for obligations 1 and 2. Tracked under the existing
  `security-and-verification-proposal.md` tiered tooling plan.
- **Loom model** for the concurrent `Jwks` refresh path: multiple
  verification requests racing with a refresh triggered by
  `unknownKeyId`. Obligation 6's live-set invariant is the
  correctness condition.

#### Out of scope for the formal track

- The external IdP's own correctness. The model treats the IdP as
  a trusted oracle that emits signed tokens matching its published
  policy; bugs in the IdP itself are not capOS-provable.
- Network-layer adversaries. TLS authentication of the IdP and the
  token endpoint is assumed; that proof lives in the certificates
  proposal's track.
- Timing and microarchitectural side channels on signature
  verification and DPoP checks. Treated as deployment-level
  mitigations (constant-time libraries, cache partitioning) rather
  than modeled flows.
- User behavior. Phishing, social engineering, and operator
  credential sharing are outside the model.
- IdP key compromise. Modeled as an assumption violation; the
  formal proof cannot recover from a signing-key compromise at the
  IdP.

### Note on GOST cryptographic primitives

Separately from MAC/MIC, a deployment may also require GOST
cryptographic algorithms (GOST R 34.10-2012 signatures,
GOST R 34.11-2012 Streebog hashes, GOST R 34.12-2015 symmetric
ciphers) throughout the JWT/JWS and TLS stack. Those are additive
enum extensions in `SignatureScheme`, `HashAlgorithm`,
`AsymmetricAlgorithm`, and `SymmetricAlgorithm` across the key,
certificates, and OIDC proposals plus a certified cryptographic
library. The interface shape does not change; the MAC/MIC analysis
above is independent of the algorithm choice.

### ФСТЭК threat modeling

The threat-model section above enumerates OAuth/OIDC-specific
attacks (leakage, replay, mixed-IdP confusion, discovery
tampering, PKCE downgrade, code replay, redirect hijack, CSRF,
nonce omission, `sub` confusion, JWKS flooding, token-exchange
evasion, clock skew). Mapping that enumeration to ФСТЭК's
"Методика оценки угроз" taxonomy is a deployment-specific
documentation exercise; the raw facts are already here.

### How this combines

A capOS deployment choosing a high-assurance profile selects:

- X.805 dimensions to audit explicitly (all eight for a
  regulated service).
- X.1254 LoA floor per resource (via `minAuthStrength` on seal
  policies and broker bundles).
- A label lattice (confidentiality + integrity) and which IdP
  trust records can mint sessions at which labels.
- Which token transitions are modeled as `Declassify` /
  `Transfer` / `Control` in the MAC/MIC automaton.
- A concrete IdP trust bootstrap (manifest-pinned JWKS snapshot
  vs. discovery with pinned TLS root).
- A concrete audit redaction and retention policy consistent with
  applicable regulation (ITU-T X.816, ФСТЭК guidance, GDPR, or
  sector-specific rules).

No kernel change is required to land any of these. Each choice
narrows the behavior of userspace services — `OAuthClient`,
`OidcIdentityProvider`, `TokenVerifier`, `CredentialStore`,
`SessionManager`, `AuthorityBroker`, `LabelAuthority`,
`AuditLog` — inside the same capability model.

## Interaction with capOS Authority Model

OIDC and OAuth2 decide *which external subject was authenticated* and *which
scopes apply to this call*. Admission policy decides which local principal,
account, policy profile, and resource profile that external subject maps to.
They do not decide *which caps exist in the process*. That remains the job of
`AuthorityBroker`.

Practical flow:

1. User authenticates to capOS via OIDC. `SessionManager.login`
   verifies the ID token and computes
   `subjectHash = hash(providerKind, iss, tenant, sub)`.
2. `SessionManager` resolves `subjectHash` through manifest seed admission,
   a local account-store `ExternalIdentityBinding`, or an explicit
   auto-creation rule. The result is a local or pseudonymous principal plus
   selected policy and resource profiles.
3. `SessionManager` mints a `UserSession` whose `PrincipalInfo.id` is the
   resolved principal and whose `authStrength` derives from `acr`/`amr`.
4. `AuthorityBroker.request` receives the session and any relevant
   access token. Scopes and OIDC claims are inputs to the
   RBAC/ABAC/MAC decision. They are never sufficient authority on
   their own.
5. The broker returns a capability bundle (or denial). The access
   token is delivered inside an `ApprovalGrant` or a wrapper cap
   when the caller needs to invoke an external service; the raw
   bytes remain inside the OAuth service.
6. For outbound calls to an OAuth-protected resource, the capOS
   service holds an `AccessToken` cap; it does not see the token
   string.
7. For inbound calls, a capOS service configured as an OAuth2
   resource server holds a `TokenVerifier` cap plus its
   `AuthorityBroker` cap; verification yields claims, and the
   broker converts claims into narrower caps for the call.

This is the same "decision returns a capability" pattern the
user-identity proposal already uses for Cedar/OPA. OIDC just
provides one more input shape.

## Phases

Phases follow the consumers.

### Phase 1 — IdP and client schemas, JWT verification

- Add the schemas above to `schema/capos.capnp`.
- Implement a RAM-only IdP cache that can load a discovery document
  and JWKS from a static test fixture and verify a sample ID token.
- Implement `JwtVerifier` over `PublicKey` primitives from the key
  proposal using a vetted Rust crate (`jsonwebtoken`, `biscuit`,
  or a purpose-built verifier on top of `rsa` / `ed25519-dalek` /
  `p256`).
- Host tests: signature verification across RS256/ES256/EdDSA,
  issuer/audience/exp checks, clock skew, algorithm allow-list.

### Phase 2 — OAuth client and device code

- `OAuthClient` with `clientCredentials`, `refresh`, and
  `deviceCode` grants.
- Outbound HTTPS via the networking and certificate stacks
  (requires those to be real).
- Console OIDC login proof: QEMU serial starts
  `startDeviceCode`, an operator completes the flow out-of-band,
  `pollDeviceCode` returns a bundle, `verifyIdToken` succeeds, a
  manifest-seeded external admission rule selects policy/resource profiles,
  and a `UserSession` is minted.

### Phase 3 — Authorization code + PKCE

- Web text shell gateway redirects to the IdP and consumes the
  returned code.
- `startAuthCode` / `completeAuthCode` integrated with the
  gateway's HTTP listener.
- Per-session `nonce`, `state`, and PKCE verifier all live in
  `AuthCodeState.opaque`.

### Phase 4 — Resource server verification

- `TokenVerifier.verifyAccess` with JWKS refresh and
  introspection-endpoint fallback for opaque tokens.
- Policy enforcement: required scopes, audience binding, cnf
  confirmation (DPoP or mTLS).

### Phase 5 — Workload identity federation

- `WorkloadIdentityFederation` with subject sources for GCP and
  AWS.
- Depends on `InstanceIdentity` from cloud-metadata and a working
  outbound TLS client.
- `CloudKmsKeySource` gains a no-baked-credentials unlock path.

### Phase 6 — Private key client auth and DPoP

- `ClientAuthMethod.privateKeyJwt` using `JwtSigner`.
- `DpopSigner` + `ConfirmationKind.dpop` in `TokenVerifier`.
- RFC 9449 nonces when the resource server supports them.

### Phase 7 — mTLS-bound tokens and extended federation

- `ClientAuthMethod.tlsClientAuth` per RFC 8705.
- Attestation-report-backed federation
  (`SubjectSource.attestationReport`) for confidential computing.
- CIBA grant (RFC 9126 + OpenID CIBA) if a deployment needs it for
  step-up on mobile devices.

### Phase 8 — Token exchange as a first-class broker input

- `AuthorityBroker` accepts an `AccessToken` or
  `IdToken` plus scopes as policy input; decisions can return
  narrowed access tokens alongside narrower caps.
- Account-store-backed `ExternalIdentityBinding` records replace
  manifest-only external admission for ordinary federated logins.
  Unknown external subjects are denied unless an explicit auto-creation rule
  names policy and resource profiles.
- Per-user `EncryptedNamespace` unlock via
  `OidcFederatedKeySource` (defined in the key-management proposal)
  using the user's current access token as unlock context.

### Phase 9 — Local IdP (optional, deferred)

- A `LocalIdentityProvider` cap that issues tokens to other capOS
  services on the same host or fleet, signed by a `JwtSigner`
  backed by a `KeyVault`-stored `PrivateKey`. Useful for air-gapped
  deployments and for bootstrapping workload federation between
  two capOS instances. Not in v1.

## Relationship to Other Proposals

- **[cryptography-and-key-management-proposal.md](cryptography-and-key-management-proposal.md)**
  — supplies `PrivateKey` / `PublicKey` / `SignatureScheme` /
  `AsymmetricAlgorithm`. Adds `KeySourceKind.oidcFederated`,
  `SealPolicy.tokenExchange`, `KeyPurpose.oauthClientAssertion`,
  and `KeyPurpose.oidcIdToken` to support this proposal's consumer
  shapes.
- **[certificates-and-tls-proposal.md](certificates-and-tls-proposal.md)**
  — OIDC discovery, JWKS, token endpoint, and IdP admin endpoints
  are all reached over TLS clients built from `TlsClientConfig`.
  IdP pinning composes with `PinSet` from that proposal. mTLS
  client authentication for OAuth reuses `TlsClientConfig`.
- **[boot-to-shell-proposal.md](boot-to-shell-proposal.md)** —
  device code and authorization code grants are
  `SessionManager.login` methods. `CredentialStore` stores IdP
  trust records (issuer URL, JWKS, allowed audiences) alongside
  password verifiers and passkey public credentials.
- **[shell-proposal.md](shell-proposal.md)** — the authority
  broker consumes access tokens as ABAC input; the agent shell
  holds `ApprovalGrant` wrappers, not raw tokens.
- **[user-identity-and-policy-proposal.md](user-identity-and-policy-proposal.md)**
  — federated subjects resolve through manifest seed admission,
  local account-store `ExternalIdentityBinding` records, or explicit
  pseudonymous auto-creation rules; OAuth scopes and OIDC claims are
  ABAC attributes, not authority; `AuthStrength` derives from
  `acr`/`amr`.
- **[volume-encryption-proposal.md](volume-encryption-proposal.md)**
  — OIDC-gated KMS unlock replaces baked IAM credentials; per-user
  `EncryptedNamespace` unlock uses
  `OidcFederatedKeySource`.
- **[cloud-metadata-proposal.md](cloud-metadata-proposal.md)** —
  `InstanceIdentity` is the primary subject token source for
  workload identity federation. The current proposal's own
  `SubjectSource.instanceIdentityJwt` is implemented by that cap.
- **[networking-proposal.md](networking-proposal.md)** —
  outbound OAuth calls use a userspace HTTP/TLS client built over
  the networking stack. Service-to-service OAuth coexists with
  mTLS as two delegation patterns rather than competing ones.
- **[system-monitoring-proposal.md](system-monitoring-proposal.md)**
  — every `verifyIdToken`, token issuance, refresh, exchange,
  and `verifyAccess` flows through the audit cap. Redaction rules
  from the boot-to-shell proposal apply: claim summaries and
  token references, never raw tokens.
- **[security-and-verification-proposal.md](security-and-verification-proposal.md)**
  — JWT/JWS/JWE parsers are classic fuzz targets; PKCE and
  device-code state machines are Loom candidates; token-exchange
  policy evaluation is a Kani candidate.
- **[live-upgrade-proposal.md](live-upgrade-proposal.md)** — the
  OAuth service holds sensitive live state (refresh tokens,
  DPoP private keys, PKCE verifiers). Live upgrade needs a
  state-transfer path that does not leak tokens through shared
  memory.

## Open Questions

1. **Do we ship our own OIDC RP implementation or wrap an existing
   Rust crate?** `openidconnect-rs`, `oauth2-rs`, and `biscuit` are
   candidates. The schema boundary is independent; the implementation
   choice affects TCB size and audit surface.
2. **Opaque access token handling.** Some IdPs issue opaque tokens
   validated only by introspection (RFC 7662). Latency and load on
   the introspection endpoint are operational concerns; caching
   introspection responses is fiddly (when is the cache allowed to
   serve stale "active"?). Probably: support introspection with
   short cache TTL and per-policy opt-in.
3. **PKCE-less legacy clients.** A deployment against an old IdP
   that cannot do PKCE. Do we allow a config escape hatch, or do we
   refuse to boot? Leaning "refuse" given OAuth 2.1 guidance.
4. **DPoP nonce plumbing.** Server-issued nonces (RFC 9449 §8)
   require the caller to retry after the first 401 with the returned
   nonce. Fits naturally in a wrapper cap around `AccessToken`, but
   the retry policy on non-idempotent methods needs a clear rule.
5. **Device code on air-gapped consoles.** Device code presumes the
   user has another device with a browser. Pure-air-gapped hosts
   must fall back to password + passkey; what about console-only
   OIDC without internet? Probably: no-op; offline OIDC is an
   oxymoron, use local auth.
6. **How do tokens transfer across capability boundaries?** Per-
   consumer down-scoped issuance is the default. Should
   `AccessToken.attenuate` be a kernel-level badge, a userspace
   wrapper cap, or both depending on whether attenuation is
   server-side (token exchange) or client-side (scope subset)?
7. **Logout semantics.** OIDC end-session endpoints are
   optional and frequently inconsistent across IdPs. When
   `UserSession.logout` fires, what is the best-effort expectation:
   local session drop + IdP revoke + RP-initiated logout redirect?
   Document a clear failure mode for each step.
8. **Default audiences for `AuthorityBroker` decisions.** When the
   broker down-scopes an access token, what audience does the
   narrower token target — always the resource server the broker
   just returned a cap for? Or a list, for broker decisions that
   return a compound bundle? Probably: one audience per
   `CapRequest`, bundles emitted as multiple broker responses.
9. **External auto-creation policy.** Which OIDC providers may create
   pseudonymous local accounts, which policy/resource profiles may they name,
   and what rollback/recovery record proves the mapping was not replayed from
   stale account-store state?
10. **Support for JAR / PAR / JARM.** Pushed Authorization Requests
   and JWT-Secured Authorization Response Mode are increasingly
   expected by enterprise IdPs. Phase 3 should support PAR; JAR and
   JARM can follow.
11. **Clock source.** OIDC verification depends on a reliable clock.
    Before the Timer capability and a cloud attested-time source
    exist, `verifyIdToken` must either fail closed or consume a
    bootstrap clock from the manifest. Document the first-boot
    behavior.
12. **Key binding for user sessions.** Should a `UserSession` be
    bound to a DPoP key by default (so a leaked session ID is
    useless without the key), or is that overkill for console
    sessions? Probably: yes for web gateway sessions; no for
    direct local console sessions where session state never
    leaves the host.
13. **GOST / jurisdictional OIDC.** Some deployments mandate
    GOST-signed JWTs (GOST R 34.10-2012 on the JWT signature).
    Adding the algorithms to `SignatureScheme` is schema-level;
    validating a GOST-signed discovery document requires matching
    trust-store support in the certificates proposal. Track, do
    not block.