When Does Authorization End? Effect Closure at Provider Boundaries
Igor Santos-Grueiro
cs.CR
Sep 2, 2026 · v1
cs.DC
TL;DR
Lean 4 machine-checks the reduction from closure to finite games, certificate soundness, contract-to-game translations, and Kafka Effect Fence invariants.
Abstract
Revocation completion, clean state, or operation success can leave authorized work able to cause an effect the application rejects while the provider stays within its contract. We call the absence of all such paths policy-relative effect closure, or effect closure for short. Thus, a grant is closed when its existing authorizations retain no such path, and it cannot issue any new ones. We present EFFECTBOUND, which uses an evidence-supported finite contract to decide whether an interface can truthfully report closure while required work completes. It reduces this to finite control with hidden state and returns a strategy, an impossibility certificate, or no verdict when evidence is insufficient. Machine-checked proofs establish the reduction and checker soundness; the checker derives closure results and validates certificates. Across GitHub, Kubernetes, NATS, and Kafka, closure fails in three ways: an interface lacks a needed control, clean visible state hides active work, or the model stops before the effect frontier—the last point where the effect can be prevented. The GitHub tool cannot bind a merge to the reviewed commit; a controlled run confirms that it may merge a different commit. NATS can report no stored or pending messages while dispatched work can still publish downstream. In Kafka, all fixed-set brokers had applied the revocation, yet an earlier authorized request could still append. We add a gate that blocks new use of revoked authority and delays return until earlier in-flight work completes. In a fixed-set Kafka 4.3.1 test deployment, this closes the studied synchronous, nontransactional write path without blocking unrelated requests. For a grant, authorization ends only when issuance stops and no earlier authorization can reach an effect the application rejects.
Problem
Revocation completion, clean visible state, or operation success at provider boundaries can still leave previously authorized work able to cause effects the application rejects. The paper asks when an interface can truthfully report that authorization has ended, a property it calls policy-relative effect closure.
Approach
EffectBound builds an evidence-supported finite contract of the provider path from grant to authorization instance, continuation, effect frontier, and effect. It reduces boundary realizability to control of a partially observed discrete-event system, which yields a winning strategy, an impossibility certificate, or abstention when evidence is insufficient. Lean 4 machine-checks the reduction, certificate soundness, the contract-to-game translations, and the closure derivations. Three repair placements (Bind, Re-enter, Fence) are evaluated on GitHub MCP, Kubernetes, NATS, and Kafka.
Results
Six paths fail closure through missing controls, hidden active work, or models that stop before the effect frontier. All repairs reduce forbidden effects to zero while required work still completes. Lean validates all 17 translated game certificates (2 winning, 15 losing), and Kafka's Effect Fence closes the studied synchronous write path without blocking unrelated requests.
| Path | Base | Repair | Repaired | Complete |
|---|
| GitHub MCP-to-REST | 25/25 | Bind SHA | 0/25 | 25/25 |
| NATS redelivery | 10/10 | Bind ID | 0/10 | 10/10 |
| Kubernetes RBAC | 30/30 | Re-enter | 0/30 | 30/30 |
| NATS purge | 30/30 | Tracked Drain | 0/30 | 30/30 |
| Kafka produce | 10/10 | Effect Fence | 0/10 | 10/10 |
Forbidden effects before and after repair