Verification Semantics

Verification Semantics

Decision predicate

Let:

• e be the attempted external effect;
• C(e) be the canonical request representation;
• H(C(e)) be the action digest;
• r be the PermitReceipt;
• P_t be current policy state;
• R_t be current revocation/status state; and
• ctx be explicit authorization-critical context.

The intended posture is:

Commit_I(e) occurs only when
Verify(e, r, P_t, R_t, ctx) = ALLOW
and all required downstream checks succeed.

Conceptual verification gates

The exact implementation may short-circuit in a different order, but an ALLOW outcome should establish every required invariant:

1. Input and profile support — the request, receipt, signatures, identifiers, and profile declarations are well formed and supported.
2. Canonicalization — the selected profile deterministically represents every effect-relevant field.
3. Action binding — the computed digest or commitment matches the authorization artifact.
4. Policy binding — the policy digest or epoch is acceptable; mismatch and prohibited rollback are denied.
5. Validity — time or sequence bounds are current under explicit clock and parsing semantics.
6. Scope — effect type, interface, target, tenant, purpose, jurisdiction, audience, identity, operation, budget, and other selected constraints match.
7. Issuer and authenticity — signatures and issuer evidence validate under the configured authority profile.
8. Status and recency — required revocation, issuer, authority, policy, and related evidence is current enough.
9. Anti-replay — nonce, sequence, counter, reservation, or equivalent state is valid and atomically consumed or reserved as required.
10. Domain profile — any non-waivable profile-specific checks pass.
11. Downstream enforcement — when required, derived capability or decision evidence is independently validated at the destination.

Fail-closed pseudocode

function verify(effect, receipt, policy, status, context):
    deny if input is malformed, ambiguous, conflicting, or unsupported

    canonical = canonicalize(effect, receipt.canonicalization_profile)
    deny if digest(canonical) != receipt.action_digest

    deny if policy digest or epoch is unacceptable
    deny if receipt is not currently valid
    deny if any required scope field mismatches
    deny if issuer or signature evidence is unverifiable
    deny if required status or revocation evidence is stale or missing
    deny if anti-replay evidence is absent, invalid, replayed, or raced
    deny if any non-waivable profile check fails

    return ALLOW with evidence digests and an auditable decision record

This is explanatory pseudocode, not a normative API or wire format.

Decision outputs

A useful decision record contains at least:

• ALLOW or DENY;
• machine-readable denial reason when applicable;
• action digest and canonicalization profile;
• policy digest and epoch;
• receipt, issuer, and evidence references or digests;
• validity and status-recency information needed for reproduction;
• anti-replay outcome; and
• the enforcement stage that produced the final outcome.

The record should not expose secrets, production credentials, unnecessary personal data, or sensitive customer material.

Constrained modes

A constrained or degraded mode must be explicitly authorized by policy and must not waive non-waivable checks. “Status service unavailable,” “profile unknown,” or “context ambiguous” must not silently become ALLOW.

Why denial tests matter

An ALLOW demo proves only that one expected path can complete. The stronger interoperability signal is a deterministic set of negative vectors showing that materially different actions, stale state, malformed input, replay, tampering, bypass, unsupported profiles, and missing evidence are denied for the intended reason.

See Evidence and Test Matrix and Security, Privacy, and Limitations.