Yesterday's Permission

Take the Ashdown instruction, an invented intake matter that recurs through this book. Ashdown Ltd instructs a firm. The firm's intake agent delegates to a research agent, with a grant to read and summarise a privileged advice note from tick 1 to tick 10. At tick 3 the research agent starts work. At tick 5 the client withdraws consent. The research agent is mid-run.

Every property from Who Gets to Write the Specification? held at tick 3: correctness, validity, authority. None of them has a time argument. This chapter adds one.

A permission is a cached answer to a question whose answer can change. Three claims follow. First, revocation is a race, and the number that matters is the length of the window in which a stale copy still says yes, not whether the system has a revoke function. Second, an enforcement point that cannot reach the issuer must choose between overstaying and refusing, and no design removes that choice; it only prices it. Third, and most contestable: the short-lived credential, on which the certificate and agent-identity communities now lean, solves the smaller half of the problem. A token expires. A summary does not. What the withdrawn fact has already produced is the larger exposure, and the agent-identity texts I have read do not address it.

I build verified AI systems for law firms, so I gain if partners start asking vendors about staleness windows. Read the Thursday section below with that in mind. Nothing here is legal advice.

I also owe three corrections. In When the Hands Run Wild I wrote that grants are "time-bounded and revocable" and that approval "grants the capability with automatic expiration and revocation", as though the adjective finished the job. In Part III of The Soul and the Hands I listed "Capability revocation and its propagation effects?" as an open question and left it there. And in Make the Safe Harbour Compile I wrote: "Staleness is a solved problem in the discipline being borrowed from." That was too quick. Versioning tells you which rule you checked against. It does not tell you what is still standing on the old one.

The theorem stays proved

Lean's kernel is monotonic [adding facts never removes a conclusion]. Once allowed_before is proved, it is proved. The world is not monotonic: withdrawals, repeals and overturned judgments remove things. Those two facts do not contradict each other.

The book's case file contains both of these, and both are kernel-checked:

• allowed_before: the research agent may read the advice at tick 4 under the grant.
• revoked_copy_refuses: under the revoked grant it may not at tick 6.

Each statement names its own tick. In my file, revoke_preserves_past proves the general form: for any grant and any tick before the revocation, the revoked grant and the original give the same answer. The read at tick 4 stays authorised forever. What changes is the standing of everything that relies on that read from tick 5 on.

So a theorem cannot go stale, and a reliance can. If a proof is to be used after its premises may have moved, it must carry what it depends on. The file has a small structure for that, Certified: a proof, plus a declared list of the facts it relied on. proof_stands_certificate_stale shows the three-part state: before withdrawal the certificate is current; after it, not current; and the proposition is still proved throughout. undeclared_stays_green shows the limit: the same proof with its dependency left off the list stays green after withdrawal. The kernel checks the proof. It can check a premise you stated as a hypothesis, but not that you stated every premise the world requires.

Jon Doyle's Truth Maintenance System of 1979 worked by "recording and maintaining the reasons for program beliefs" so that a reasoning program could revise them when an assumption failed (Doyle, 1979). Both halves, recording and revision, have returned to agents in 2026 preprints, discussed under the objections below.

Revocation is a race

OAuth's token revocation RFC says the invalidation "takes place immediately", then in the next sentence: "In practice, there could be a propagation delay, for example, in which some servers know about the invalidation while others do not" (Lodderstedt et al., 2013, RFC 7009). It tells implementers to keep that window small. The working-group draft on agent identity says recipients must not use cached decisions that are no longer valid "after a revocation or risk notification is received" (Kasselman et al., 2026, draft-ietf-wimse-aims-00). It is an Internet-Draft, not a standard. Note where its clock starts: on receipt. The interval between the issuer's decision and receipt is exactly what it leaves open, beyond a duty to enforce "without undue delay".

A copy of a permission held at an enforcement point is a replica. The issuer is the single writer. Revocation is a write. Keeping replicas honest is cache coherence, and Google's Zanzibar paper gives the failure a name, the "new enemy" problem, which "can arise when we fail to respect the ordering between ACL updates or when we apply old ACLs to new content" (Pang et al., 2019). Zanzibar's answer is a token called a zookie, which makes a check no older than the content it guards, on a globally consistent database. That works when one organisation owns the whole store, which a chain of agents crossing firms does not.

At one enforcement point there are three states. The issuer has not revoked (live), the issuer has revoked and this point has not heard (issuedUnseen), or the point knows (enforced). disagree_iff_unseen says the point and the issuer disagree in exactly one of those. no_delivery_no_enforcement says re-issuing without delivery never moves it. enforced_absorbing follows from a design choice, that the model has no reinstating event: a new grant is a new grant.

With ticks attached, the window has an exact shape, and state_refines_cached proves the timed copy gives the state machine's answer, gated by the grant. The block below is the statement only; the file holding its proof, lean/BuildingInSteel/Revocation.lean, compiles on Lean v4.29.1 with no libraries beyond the book's case file.

theorem window_iff (g : Grant) (r d t : Nat) (p : Principal) (a : Action) :
    cachedPermits g r d p a t ≠ freshPermits g r p a t ↔
      (r ≤ t ∧ t < r + d ∧ g.permits p a t = true) := by

Here d is the propagation delay. The stale copy and the fresh answer differ if and only if the tick is in [r, r + d) and the grant would otherwise have allowed the act. stale_window_bound turns this into a bound: over any horizon, the answers differ on at most d ticks. ashdown_window_tight shows the bound is attained: withdrawal at 5 with a delay of 3 gives ticks 5, 6 and 7. ashdown_lost_notice_runs_to_expiry shows what happens if the notice never arrives: ticks 5 to 9, stopped only by the grant's own expiry at 10.

That gives a precise quantity: the staleness window of an enforcement point is the number of ticks on which its answer differs from the issuer's. Multiply by the rate of action to bound what an agent can do in the window; the rate version is sketched, not proved. I claim no control-theoretic margin or Bode-style conservation law; "window" means a counted set of ticks, and any likeness to dead time in a feedback loop is an analogy I have not formalised.

Checking once

The window assumes the agent asks each time. Agents mid-run often do not. A task that checks its grant at the start and then works is a time-of-check to time-of-use gap, and the theorem I found most useful to write down is check_once_ignores_delivery: with a delivery delay of zero, a run from tick 3 to tick 8 that checked once still reads on ticks 5, 6, 7 and 8. Perfect delivery of the revocation does nothing for it. check_each_zero_delay runs the same task checking every step and gets no post-withdrawal reads at all. check_each_bound proves the general case: checking every step limits post-revocation acts to d, for any grant and any task.

So buying faster revocation signals before changing where agents check is the wrong order. Signal standards such as OpenID's Continuous Access Evaluation Profile (Cappalli and Tulshibagwale, 2025) are useful, and receipt is not enforcement either: on a Keycloak testbed with selective non-delivery injected, 112 of 225 calls (49.78%) were admitted despite successful transport and receiver persistence (Liu et al., 2026). A signal only helps a process that looks.

The bound has a price

Now suppose the issuer cannot be reached. Seth Gilbert and Nancy Lynch's proof sketch of the CAP theorem turns on a server for which "it is impossible for p2 to distinguish" two histories (Gilbert and Lynch, 2012). Permission has the same shape, in miniature. It is not the CAP theorem; it is the same argument. The block below is again the statement only, from the same compiling file.

theorem no_bound_and_availability (pol : LocalPolicy) (f B : Nat) :
    overstays (pol f (f + B)) B (some f) (f + B) = true ∨
    overrefuses (pol f (f + B)) none = true := by

The proof is two cases, because all the content is in the type. pol sees only when the copy was fetched and the time. It does not see whether the grant was revoked, so it must give one answer for two worlds. In one, the grant was revoked at the fetch tick and honouring it overstays the bound. In the other, it was never revoked and refusing is wrong. online_escapes shows the hypothesis is load-bearing: a policy allowed to see the hidden world fails neither way.

Hard-fail refuses when no answer comes back. Soft-fail carries on. Adam Langley's verdict on soft-fail for browsers was that "it's completely useless" against the attacker it is meant to stop, because an attacker who can intercept your traffic can block the check (Langley, 2014). softfail_overstays is the formal form.

The third choice is the lease. Cary Gray and David Cheriton proposed in 1989 to give a cache holder rights "for a limited period of time", so that "Non-Byzantine failures affect performance, not correctness" and an unreachable holder delays a write only "until the lease expires" (Gray and Cheriton, 1989); their paper already covers "permission information" among the things to lease. lease_bound proves the benefit: with lease length L, a copy fetched before revocation cannot be honoured at or after r + L, even if every notification is lost. lease_refuses_live_grant shows the cost: a grant nobody revoked is refused once the lease lapses with the issuer unreachable.

The web's certificate system has moved this way. In 2025 the CA/Browser Forum adopted ballot SC-081v3, whose rationale calls certificates "representations of a point in time state of reality" and says "relying solely on revocation is untenable" (CA/Browser Forum, 2025). The maximum validity falls to 200 days from 15/03/2026, 100 days from 15/03/2027 and 47 days from 15/03/2029 (Baseline Requirements, v2.3.1). The agent-identity draft takes the same line: short-lived credentials provide "an alternative to explicit revocation mechanisms".

For access, I agree with them. A lease is the right default for an agent's grant. Publish L, fail closed at expiry, and accept the refusals. What short lifetimes do not touch is the next section.

A token expires. A summary does not.

At tick 4 the research agent wrote a summary of the advice. At tick 5 consent went. The credential that authorised the reading can lapse on schedule. The summary is a file. It has no expiry, it sits in a context window or a vector store, and a drafting agent may use it at tick 12. Neither a lease nor a signal reaches it, because neither is about it. The neighbouring chapter, A Summary Is Not a Permission, deals with a summary that widens a grant. This is the other failure: a faithful summary that outlives one.

Within a single kernel this has been solved for capabilities. seL4, the microkernel with a machine-checked verification (Klein et al., 2014), tracks a capability derivation tree, and its revoke method "removes all capabilities (in all CSpaces) that were derived from a selected capability" (seL4 Reference Manual, v17.0.0). That works because every copy is within the kernel's reach. It also revokes authority, not information: by my reading, what a process has already read is out of the tree's scope.

So the derived state needs its own graph. The Ashdown one is small enough to read: each node has justifications, each justification a list of premises, and a node stands when it is not withdrawn, no defeater stands, and at least one justification is fully supported. ashdown_invalidated computes what withdrawal takes with it. This block is complete as quoted, and compiles against the file's definitions:

theorem ashdown_invalidated :
    ashdown.invalidated [.clientConsent] =
      [.clientConsent, .intakeAuthority, .researchAuthority, .adviceReliance,
       .adviceSummary, .draftParagraph] := by decide

Reachability is the wrong algorithm. The limitation note in the case came from the advice, and it is also in the public filing. limitation_survives says it stands. reachability_over_invalidates says a plain downstream sweep would discard it. Recorded reasons exist for this: a conclusion with a second support survives losing the first. A caution from data protection law keeps this from becoming a loophole: for personal data the EU's EDPB says "the controller cannot swap from consent to other lawful bases", and may not retrospectively use legitimate interest instead (EDPB, 2020, Guidelines 05/2020, para 123). For personal data, a second support counts only if it was declared at the time, and the graph cannot tell you that.

Withdrawal can uncover permission. withdrawal_can_uncover_permission: a disclosure that already had a justification, blocked by a privilege claim, stands once that claim is dropped. So invalidation over defeasible rules is not monotonic. withdraw_more_stands_less proves that withdrawing more never restores anything if there are no defeaters, and the counterexample shows that hypothesis cannot be dropped.

The legal model should not stop here. Guido Governatori and Antonino Rotolo examined whether ideas from belief and base revision can represent legal abrogation and annulment in Defeasible Logic, reached a conclusion they call negative, and proposed a temporal extension instead (Governatori and Rotolo, 2010; abstract read on the author's page). As I read the abstract, my graph is of the family they found wanting. It is dependency tracking with one layer of defeat, adequate for "what must be pulled from the draft", inadequate as a theory of legal change. Their framework aims to represent "many of the subtleties characterizing legal abrogations and annulments". My toy does not.

For personal data, the statute reaches derived state more directly than the standards do. Article 7(3), below, protects the lawfulness of what came before withdrawal, and not continued retention, which is itself processing. UK GDPR Article 17(1)(b) gives erasure where "the data subject withdraws consent ... and where there is no other legal ground for the processing" (UK GDPR, art 17), subject to that article's exceptions, and the EDPB reads the EU text as an active duty: "Controllers have an obligation to delete data that was processed on the basis of consent once that consent is withdrawn, assuming that there is no other purpose justifying the continued retention" (Guidelines 05/2020, para 119). That is "a summary does not expire" in statutory form: someone must go and delete it. Article 19 then requires a controller to communicate that erasure "to each recipient to whom the personal data have been disclosed, unless this proves impossible or involves disproportionate effort" (UK GDPR, art 19). That is one hop of an invalidation graph, in statute, covering recipients and not derived artefacts. Whether a summary is personal data is a legal judgment a graph cannot make. Ashdown Ltd, being a company, is not a data subject at all: its withdrawal is an instruction, and Article 7 does not apply to it. I use the GDPR text for its treatment of timing, not because it governs the invented case.

Two clocks

Statutes are functions of time, and people who work with them know it. The official UK legislation site shows a timeline of changes for each provision (legislation.gov.uk). A rule is not one object. It takes a date, and sometimes a second date.

The law distinguishes how a change reaches back, and a time-indexed permission model must carry the distinction. The UK GDPR text and the two Acts are UK law. The EDPB guidance and the Privacy Shield material are EU sources, not statements of UK law; I use them because they show a regulator and a court handling timing.

Every firm whose transfer register cited Privacy Shield held a stale permission on 16/07/2020, and on the EDPB's stated position the permitted window was zero. Any propagation delay was all exposure.

Two axes are needed to represent this. Temporal database research separated them long ago: Richard Snodgrass and Ilsoo Ahn distinguished valid time from transaction time in 1985 (Snodgrass and Ahn, 1985). Governatori and Rotolo reach two timelines from the legal side, "one internal to a given temporal version of the legal system, and another relative to how the legal system evolves over time". In my file, ex_nunc_keeps_past proves that a withdrawal at tick 5 leaves the answer for any earlier tick unchanged, whenever you ask. ex_tunc_rewrites_past shows an annulment recorded at tick 8: asked at tick 7, the act at tick 4 was permitted; asked at tick 9, it was not. And one_clock_insufficient proves that no function of the acted-at tick alone can reproduce that record. So a table holding one current answer per acted-at tick cannot answer the question a tribunal will ask, which is what you knew and when. You need recording order as well as act time, as a second column or as an append-only log, and order is the first thing the hash chain below provides.

Law allocated the window in 1971

Software standards say minimise the window. English law decided who bears the loss inside it. Section 5 of the Powers of Attorney Act 1971 is the stale-copy problem in statutory language. A donee who acts when the power has been revoked "shall not, by reason of the revocation, incur any liability ... if at that time he did not know that the power had been revoked". A person who deals with the donee "without knowledge of the revocation" gets a transaction "as valid as if the power had then been in existence" (Powers of Attorney Act 1971, s 5).

Read as a specification, that separates three questions: when revocation took effect, who knew, and who carries the consequence. The stale act is not treated as never having happened. Its validity is decided by who knew, an actual state of mind. Section 5 is about powers of attorney, in England and Wales, and I do not claim it applies to software. My claim is about design: the statute treats the window as a fact to allocate, and none of the texts I read here (RFC 7009, the WIMSE draft, CAEP) says who bears a loss inside it. They are about mechanism, which is their job. Allocation needs no number: section 5 turns on knowledge, and the payment rules turn on notice, with the payer, absent fraud, not liable for losses "arising after notification" (Payment Services Regulations 2017, reg 77(4)). What needs a number is pricing the exposure, or telling whether a promised window was kept.

What a hash chain does and does not do

The WIMSE draft requires audit records to be "tamper-evident". The usual construction is a hash chain. When a fact is withdrawn during retention, it does four things, and fails at a fifth. The hash in my Lean file is a toy with no cryptographic properties; it demonstrates structure, and I prove nothing about collision resistance.

Green, against a head someone else kept, means nothing has been altered since it. It does not mean anything recorded is still true. Reading green as current is the error.

The erasure question has a standard engineering answer with a sting. Keep content off the chain, put a commitment on it, and erase the content; erasure_keeps_chain_loses_opening shows the chain still verifies and the content no longer opens. The EDPB's consultation version of its blockchain guidelines accepts commitments and keyed hashes as measures, but warns that "the hash will also be considered personal data", that the conclusion depends on deleting the key or salt, and that unsalted hashes generally fall short (EDPB, 2025, Guidelines 02/2025, v1.1). My model keeps the salt known, so it does not capture that condition. Whether this meets Article 17 on given facts is a legal judgment, and no theorem of mine reaches it. Processors and transfers of a retained log are outside this chapter.

What exists and what does not

Proved generally in lean/BuildingInSteel/Revocation.lean, for every grant, policy, graph or log (no sorry, no declared axioms; #print axioms lists at most propext, Quot.sound and Classical.choice): the state machine results, state_refines_cached, revoke_preserves_past, window_iff, stale_window_bound, check_each_bound, no_bound_and_availability, online_escapes, softfail_overstays, lease_bound, withdraw_more_stands_less, fewer_dependencies_stay_green, seal_append, verify_seal.

Computed on one fixed case or history, each an illustration or a counterexample and not a general result: everything else named here, including check_once_ignores_delivery, ex_nunc_keeps_past, one_clock_insufficient, ashdown_invalidated, reachability_over_invalidates, withdrawal_can_uncover_permission and the other toy-hash results. A single counterexample is enough where the claim is that something does not follow.

Sketched, not proved: exposure as rate times window; any claim with a real hash function.

Assumed, and trusted: that ticks are a shared clock (they are not, and Gray and Cheriton address clock skew); an honest issuer; that d is known; for tamper-evidence, a collision-resistant hash and an earlier head held by someone the rewriter cannot reach, which a deployment must arrange. Nothing here connects to a running system. The model-to-code gap is the subject of The Proof Passed. The Wrong Thing Ran.; the mitigation for this model would be differential testing, replaying a real gate's decision log against window_iff and flagging any answer outside the predicted window.

Does not exist, as far as I have read: an agent-identity standard that sets a maximum staleness figure, or that requires anything of derived artefacts. The Guaranteed Safe AI framework (Dalrymple et al., 2024), whose first author launched ARIA's Safeguarded AI programme, makes the verifier a distinct component, issuing a proof certificate "relative to the world model". That separation of generation from checking is right here too: the gate that checks freshness should be small and outside the generator. But a world model is dated, so its certificate needs the manifest described above.

Objections

"Short-lived credentials make this moot." The certificate evidence supports this. Verdict: right about access, and I adopt it. Wrong about derivation and about tasks that checked once. I would change my mind on seeing a deployed system where expiry of the credential also retires what was produced under it, without a dependency record.

"Information-flow control and agent memory work already do this." The strongest objection to my third claim, and largely right, so I concede most of it. The event is old: Stephen Chong and Andrew Myers wrote in 2005 that systems are "often required not to retain certain information after a specific time or event", and that under an erasure policy "any information derived from it should be erased" (Chong and Myers, 2005). The record has reached agents: CaMeL "maintains a data flow graph" (Debenedetti et al., 2025) and Fides "tracks confidentiality and integrity labels" (Costa et al., 2025). So has the revision, in preprints from this year. Tether "at read time withdraws any verdict whose support has failed anywhere in the store", citing truth maintenance; in its simulated worlds it publishes 0.3% of upstream-failing objects against 62% for a fact memory, rising to 9.4 to 22.1% when relations arrive apart from verdicts (Wang et al., 2026). PolyGraph records "alternative bundles of source evidence, each claimed sufficient on its own", which is my second-support graph at scale (Choudhary, 2026). The measurements favour my claim about the problem: of five agent-memory systems, "no system enforces revocation by default" (Shen et al., 2026).

Verdict: mechanism and event both exist, and this area is under-integrated, not unknown. Three things remain, on my reading. These systems key on a failed source, a retired version or a named datum, while Ashdown's advice stays true and only the authority to use it went. Chong and Myers's conditions could express that inside one program, and "origin binding does not constrain what an authorized record does once its authorization is revoked" (Shen et al.), but I have not read a system that retires artefacts by the grant they were made under. They stop at a boundary: Yao et al., whose motivating cases include a user revoking consent mid-session, exclude "committed side effects" from their guarantee (Yao et al., 2026). And no agent-identity standard I read asks for any of it. I would give up the residue on seeing a system retire artefacts by withdrawn grant, across a store held by another party, or on prediction 1 failing.

"Cache coherence is a metaphor; permissions are not memory." The analogy holds for the window, the single writer, and leases. It fails at the remedy. A stale read in a cache can usually be retried. A disclosure cannot be recalled, and section 5 makes a stale act valid for a third party, which has no cache equivalent. Verdict: keep it for the mechanism, drop it for the consequences. I would drop it altogether if someone showed a revocation design that coherence theory gets wrong.

"Defeasible logic handles this natively; Lean is the wrong tool." On representation, the objection is right. Defeasible logic was built for defeat, and Governatori and Rotolo have extended it to legal change; my graph does not approach that, and I would not use my file as a compliance engine. What Lean adds here is narrow: kernel-checked bounds and computed results over a small model, including the impossibility. Verdict: use the logic for the law and the kernel for the mechanism. I would concede entirely if a temporal defeasible encoding produced the window bound and the indistinguishability result with an equally small checker.

Goodhart, and what formalising loses

A published staleness number is a target, so expect it to be gamed. Vendors will quote the median and not the tail. They will shrink d and leave tasks that check once. Worst, they will shrink the dependency manifest: fewer_dependencies_stay_green proves that a certificate declaring a subset of another's dependencies is current whenever the larger one is, and undeclared_stays_green is the limit case. The defence is to derive the manifest from runtime data flow, as information-flow labels do, and not from self-declaration, and to sample by hand whether drafts trace to what they used.

Formalising also removes something. "Without undue delay" is an open standard, and it lets a tribunal weigh a case. A partner told to stop can still finish the filing that protects the client from a limitation date; a hard gate at r + d cannot tell, and Never Breaks a Rule, Never Finishes deals with that harm. "Did not know" is a question of fact, and ticks have nowhere to put it. Who gains from this? Whoever can afford dependency tracking, and I sell systems that would need it. Keep the standard behind the number: a window should be evidence about reasonable conduct and never a substitute for the test.

What to do on Thursday

If you are a partner, none of this asks you to learn to code or buy anything. It asks for one question, on one live matter, to whoever runs your tools:

If this client withdrew instructions at 10:00, what is the last time any system could still act on them, and what has been produced so far that would have to be pulled?

You want a time, and a list. "Immediately" with no number, or no list, is the finding. An hour of non-billable time, at most. The economics cut against you in places: shorter leases mean more refused actions and more re-authorisation, and a real list means discarding work you may have to write off.

The nearest reason to ask is that the client who withdraws will ask you what happened to their material, and that time and that list are your answer. There is a dated reason too. draft-ietf-wimse-aims-00 was published on 15/09/2026 and is still a draft. What goes into agent identity text gets decided while it is one.

Predictions

1. By 31/12/2027, no RFC or active Internet-Draft from the IETF WIMSE working group will require invalidation of artefacts derived by an agent under a revoked authorisation, as opposed to tokens, sessions and cached decisions. Refuted by any such text with a normative requirement on derived outputs.
2. By 30/06/2028, a public incident report, regulator decision or judgment will attribute harm to an AI agent acting on authority that had already been withdrawn or revoked at the time it acted. Refuted if a search at that date of ICO and EDPB decisions, BAILII and the AI Incident Database finds none, which would suggest either that the window matters less than I claim or that nobody is measuring it.
3. The 100-day certificate step in the Baseline Requirements will take effect on 15/03/2027 as scheduled. Refuted if the CA/Browser Forum delays or withdraws it, which would weaken this chapter's account of the web shifting weight from revocation to shorter lifetimes.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.