fix(sessions): make ending a session durably cut off access - #138
Conversation
Fresh spec, written from zero after the earlier attempt was discarded. Twelve decisions settled, 35 anchors verified against main at f8d093f. The design hangs the durable boundary on codes.revoked rather than on a session-keyed registry. A rotated refresh token inherits its parent's code_id, so marking the code marks every present and future descendant: gap 2 closes structurally with no race to serialize, and retention needs no defended horizon because the existing code reaper already refuses to delete a code while any refresh token references it. Verification departed from the issue in five places, notably that gap 3's predicate cannot be "no valid session" without breaking the #46 regression guard, and that gap 2's cost estimate assumed a design this document does not adopt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The skill's references gained a four-surface documentation sweep and a
follow-ups section after this agreement was sealed. Running both found work
the first pass missed, so sections 1 to 5 are amended with the corrections
marked rather than absorbed. No sealed decision is reversed and section 3
still has zero open items, so the seal holds.
Two decisions added, both settled with the user:
13. The interactive logout path stays out of scope. Tracing which endpoint
each "End session" button reaches showed that logout_consent.html posts
back with only a csrf field, so the ordinary logout takes the no-hint
branch in HandleAccountLogoutPost: it clears the cookie, audits, and
writes nothing to the database. handleExistingSessionOnLogout is
reachable only with an id_token_hint. The session row therefore survives
an ordinary logout with every client attached. That path performs no
termination at all, so there is nothing for codes.revoked to mark, and
fixing it would settle #109's per-client versus whole-session model from
inside an issue about something else. Drafted onto #109 instead.
14. All three end-session confirmation modals gain a line saying what
termination disconnects, in both catalogs. Three admin console pages
carry the button and all three funnel into the two endpoints decision 5
names, so all three inherit the consequence.
Documentation owed now sits in section 2, with the falsified sentence named:
concepts/tokens.mdx says an offline token keeps working once the browser
session is gone, which stays true of expiry and becomes false of explicit
termination. The earlier pass concluded nothing was falsified and had swept
only the docs site.
Section 9 drafts two follow-ups: the residual serialization window decision
12 accepted, which #134 used to hold before it was closed as moot, and the
interactive logout path as a comment for #109.
Seam 9 now states that the logout pinning tests must drive request shapes
#109 is not rewriting, or they encode its defects as intended behaviour.
Seam 10 records that catalog_hygiene_test.go already guards the six new keys
in both directions, so decision 14 needs no new test code.
37 anchors pass, 14 decisions decided, zero open.
Ending a session has to leave something durable behind, and this is the column that carries it (#129 decision 4). The marker sits on the code rather than on the session because a rotated refresh token inherits its parent's code_id, so marking the code marks every present and future descendant of that grant: a child inserted after the termination committed is born already rejected. A sweep over the rows that happen to exist cannot do that, which is what ruled out every timing-based design. Absence of a session row could not carry the fact instead. The background worker reaps idle and expired sessions as routine housekeeping, and an offline grant is designed to survive exactly that, so termination has to write something positive down. RevokeCodesBySessionIdentifier carries `revoked = false` in its predicate, which is load bearing for the count and not only for idempotence: MySQL reports changed rows rather than matched rows, and the updated_at assignment alone would make an already-revoked row count as changed, so without the term the same call reports 2 on MySQL and 0 on the other three engines. The audit event added in a later stage reports that number. MarkCodeAsUsed gains the same term, so a code revoked between validation and claiming cannot still be claimed. A false return from it now means no row transitioned, whether used, revoked or missing, and the comments there said it meant reuse; they are corrected, including the handler's debug message. Behaviour is unchanged: that branch already answered a generic invalid_grant and deliberately never ran the reuse cascade. Nothing reads the marker yet, so no observable behaviour changes with this commit. Tests: unit green in all three modules; data green on sqlite, mysql, postgres and mssql, each engine run separately, covering the sweep's table, the negative control of an unrelated session, idempotence, the unknown and empty identifiers, enlistment in the caller's transaction, the failure path returning an error rather than a benign zero, the revoked-but-unused claim, the dont-update guard, and the migration's shape, backfill, down and re-apply. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Section 6 is the plan, eight stages, stage 1 in full and the rest sketched. Section 7 opens the run log with the plan review and stage 1. The plan review changed the plan in three places, all of them cases where the first draft had drifted from what the seal already decided. Stage 3 is now an inert helper nobody calls and stage 4 is a single activation commit carrying both endpoints, both handler test files, the integration cases, every documentation page and all three confirmation modals, so no deploy can widen what ending a session revokes while a modal still describes the narrower behaviour. The two in-flight-ceremony sentences are held back to the stages that make them true, since documenting a fail-open path as closed is worse than documenting nothing. Stage 7 is forced to extend DeleteUsedCodesWithoutRefreshTokens rather than adding a second method. Section 6 also reverses the first draft's refusal to create the two handler test files section 1 asked for. Decision 9's contract has no other home: integration can read audit rows but cannot force the termination transaction to fail, so nothing there can prove both events are suppressed on failure. Section 0 gains five rows for the code stage 1 created, below a line marking them as the run's rather than the seal's. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
may-continue.sh parses a step's status from the numbered line itself, so a status on a continuation line reads as an untraced step and refuses the gate. The stage 1 steps now carry a short bold title plus the status on the numbered line, with the detail indented under it, and the stage body gains the as-built note the guard also requires. Same shape for every later stage. The as-built note records the two departures: handler_token.go was edited for comment accuracy although no step listed it, and the code preceded the plan because the case tables had to be executed before being written down. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Stage 1 added the codes.revoked marker and the sweep that writes it, but nothing read it. This makes it mean something at both redemption sites. On the authorization_code path the check reads codeEntity.Revoked and answers a generic invalid_grant. On the refresh_token path it reads refreshToken.Code.Revoked, guarded by !isROPCToken since a ROPC token has code_id NULL and so no grant origin to terminate. Both read data already loaded, so neither adds a query. Placement is the security-relevant part and is deliberate on both paths (decision 7). Neither check joins the user-enabled, generation and expiry block above: that block runs before client authentication and before PKCE, so a check placed there tells a presenter holding a stolen code whether the session was terminated, which is the disclosure #137 exists to close. The code path also sits after the wasReused return, so #77's containment cascade is not pre-empted, reuse being the stronger signal that already revokes everything this check would refuse. The refresh path sits after the client-ownership check. The refresh check precedes the typ switch on purpose. That switch's Offline branch checks only the max lifetime and deliberately never consults the session, because a session merely expiring must leave an offline grant working (decision 2), so this is the only gate that reaches an offline token. It is also what closes gap 2 structurally: a rotated child inherits its parent's code_id, so it is born already rejected rather than caught by a sweep. Tests: TestValidateTokenRequest_RevokedCode, ten subtests over both grant types plus ROPC. Four are ordering rows that each vary one thing from an otherwise valid revoked request and name the gate that must answer instead, so none can pass if the check drifts up into the pre-authentication block. Two positive controls, one per grant type. Unit tier green across all three modules. No data or integration tier: this adds no query and changes no endpoint. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dded Stage 2 and its four steps flip to Done, with an as-built note naming the one departure: ten test rows shipped against a plan that specified nine. Section 7 gains the stage 2 entry. It carries the tiers as re-run at the gate rather than as quoted from the implementation session, both review rounds with their model and effort, and round 1's blocking security finding in full, because the reasoning is the useful part. The planned missing-secret ordering row was refused by a length check running before decryption, so it pinned only that the revoked check sits after the missing-credential return, not that it sits after authentication completes. The finding was demonstrated by mutation rather than argued, and the demonstration is recorded. The entry also records that the stage spanned two driver sessions, and what the second re-verified from disk before trusting the first: the diff hash against .review/before.sha, the verdict's request_id, and the tiers. Section 0 gains three anchor rows below the run's line for the code stage 2 created. check-anchors.sh passes all 45. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
TerminateUserSessionTx performs decision 5's three writes in one transaction it owns and commits: mark every code issued through the session revoked, sweep the refresh tokens that session's grants issued, delete the session row. The first write is the one that survives, and the only one that is a boundary: a refresh token can only descend from a code and a rotated child inherits its parent's code_id, so marking the code rejects every present and future descendant of the grant. The sid-scoped token query is load bearing rather than incidental. It matches codes.session_identifier through a join, and that join is the only thing reaching an offline grant's tokens, because an offline refresh token's own session_identifier is empty. Re-filtering the returned rows by rt.SessionIdentifier would drop exactly the offline tokens decision 2 exists to revoke, which is gap 1. Any error returns the zero result rather than a partially populated one: the code sweep can succeed and the transaction still roll back, and a caller auditing that count would record a revocation that never happened. The audit events stay the caller's job, after a successful return, because AuditLogger.Log takes no transaction. It deliberately does not advance the user's authentication generation. Doing so would invalidate every other device that user has, which is the opposite of what ending one session means, and the reason this issue exists separately from #106. Nothing calls the helper and nothing emits the new terminated_user_session event yet. Stage 4 wires both endpoints and carries every piece of user-facing material about them in one commit, so no deploy can perform the broader security action while a page or a modal still describes the narrower one. Tests: unit tier green, all three modules. Four new test functions over 10 leaf cases in revocation_test.go, plus the six audit event guards with the count at 95. Two mutations confirm the suite has teeth: re-filtering the swept rows by the token's own sid fails three assertions in the offline case, and populating the result as the helper goes fails four of the six failure rows. No data or integration tier: no query added, no endpoint changed. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…n refuted Stage 3's steps flip to Done with the as-built note, and section 7 gains its entry: what landed, the tiers re-run at the gate, the review and its one finding, and the three deviations. Two things the trace has to carry that the code does not. The mutation that populates the result as the helper goes fails four of the six failure rows, not the one the implementation session's mailbox note claimed, so the keep-this row's value is narrower than the plan predicted: it names the property and asserts the count, rather than being the only row with teeth. Step 4's table keeps its original wording, because it is the prediction and editing it would erase the evidence that the prediction was wrong. And the stage stalled between sessions because its trace went to .review/stage3-log.md instead of here. The mailbox does not survive the next gate, so on the skill's own terms the stage had recorded nothing, no session ran to ingest round 1, and the driver re-invoked the reviewer three further times against a byte-identical request. Round 1's verdict was recovered from .review/drive.log and verified against the code before being written up. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both explicit "end this session" endpoints now call TerminateUserSessionTx instead of DeleteUserSession, so ending a session marks the authorization codes issued through it revoked and sweeps the refresh tokens those grants produced, offline ones included, in one transaction. Stages 1 to 3 built the column, the rejections and the helper with nothing calling any of them; this is the commit where the behaviour changes. Each handler emits deleted_user_session with its existing payload untouched and then terminated_user_session with the security detail, both after the transaction commits and neither on the error path, so an audited termination can never describe something that rolled back. The admin handler's not-found gate and the account handler's ownership check still answer before the transaction opens. The user-facing material lands in the same commit rather than in a later docs stage, so no deploy can perform the broader security action while a modal or a page still describes the narrower one: three confirmation modals in both locales, and four documentation pages covering what termination revokes, the distinction from a session merely expiring, and the limit that an offline grant's access token keeps working until it expires because it carries no session identifier to check. Tests: unit green on all three modules, including two new handler test files covering the audit payloads field by field and their suppression when the transaction fails, which no higher tier can force. Integration green on all four engines, adding the headline case at POST /auth/token, its same-user survivor control, the account ownership pairing, and two cases pinning that logout still revokes nothing. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The activation stage's as-built note, its mutation evidence and its tier results were written before the review ran. This adds the review itself: round 1, gpt-5.6-sol at effort high, all three axes reviewed, zero findings and zero follow-ups. A clean verdict is recorded with its scope rather than its conclusion, because zero findings in a narrow scope reads exactly like zero findings in a thorough one. So the entry names what the reviewer executed, what it checked by reading, and why nothing in its unchecked list is something the gate depended on. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Blocking decision: does the
|
Stage 5's code review returned one blocking security finding, confirmed against the code rather than taken on the reviewer's word: AuthenticatedAt has two writers, and handler_auth_otp.go is the second one. So a ceremony that reached OTP by SSO reuse, never touching the password form, satisfies decision 6's gate and recreates the session that was just terminated. For a user without OTP on a level2_mandatory client the enrollment page hands the browser the secret it will be tested on, so a stolen cookie alone reaches it. The sealed text disagrees with itself about this ceremony. Decision 6 names both writers and calls them both real authentication; section 1's departure note says the discriminator is level 1 authentication and that the password handler is its only writer. That is the user's call, not the run's: nothing in authentication or session territory is auto-resolved, and no security finding is settled by the run alone. Recorded as decision 15, Open, with the four options and a recommendation, and escalated on PR #138. Stage 5's code stays uncommitted, since the gate expression is the subject of the open decision. Section 8 is added, empty, because the closing PR comment reports it and an absent section reads the same as a forgotten one. Anchors green, 59 rows. No code changed in this commit. Refs #129
|
Let's go with option A. |
The user chose option A on PR #138: a dedicated level 1 proof on the AuthContext rather than reading AuthenticatedAt, which has two writers. Decision 15 flips to Decided with their words and what B, C and D lost on, and keeps the escalated question so the answer stays reviewable. Stage 5's steps are amended where the answer changed them rather than rewritten, because the run log's first stage 5 entry describes the earlier version: step 1's predicate, step 2's comment work (which the answer reverses), step 3's case table (one row replaced, not added), and a new step 6 for the field and the two assertions that pin who writes it. Four anchor rows added, one re-swept. Section 7 gains the continuation entry: what landed, the tiers re-run in full on the amended tree, and five mutations with disjoint failure sets, including one at the integration tier showing the round 1 gate issues a code and recreates the session while #46's guard stays green. Refs #129
|
Applied. Decision 15 is What landed: Three comments changed rather than two, and one is a reversal of what the first stage 5 pass did: it had Tests: the zero-time Verified on the amended tree: modules green on three modules, integration green on all four engines, The cost you accepted shows up as expected: a user whose session expires while they are on the OTP Stage 5 is still uncommitted, deliberately: the gate changed after round 1 read it, so review round 2 is |
…ssion HandleAuthCompletedGet's no-valid-session branch called StartNewUserSession unconditionally, minting a session from authContext.UserId with no proof that anyone authenticated. So an SSO ceremony whose session was ended mid-flight resumed at /auth/completed and silently recreated the session it was riding, and the code it then issued carried a fresh session identifier that no marker from stages 1 to 4 could reach: those stages mark and reject grants that already exist, and this one does not exist yet when termination runs. The gate is deliberately "this ceremony performed level 1" rather than "no valid session". The second shape is legitimate and already guarded by TestSessionDeletedDuringAuthFlow_LoginSucceeds (#46): a session is deleted, the user starts a fresh ceremony and really does enter a password. Failing that shape would break a case that must keep working. The proof is a dedicated Level1AuthCompleted bool on the AuthContext, written only by the password handler. AuthenticatedAt could not carry it: the OTP handler sets that field too, so a ceremony that stepped up to OTP by reusing a session satisfied it without a password, and for a user enrolling on a level2_mandatory client the browser is handed the secret it will be tested on, making the bypass reachable with a stolen cookie alone. That was found by review and answered by the repository owner on PR #138. AuthenticatedAt keeps its existing job of deciding whether to refresh a live session's AuthTime. An older cookie decodes the absent bool as false, which sends a ceremony already past the password form back to login once, and the legitimate step-up on a live session is untouched because it never reaches this branch. Tests: unit green on all three modules, with the completed-handler suite at 13 subtests where main has 10, covering the terminated-SSO shape, the OTP-only shape, the three positive controls that would fail against a gate keyed on the session alone, and the zero-timestamp row that keeps the neighbouring AuthTime discriminator honest. One assertion each in the password and OTP handler suites pins who writes the new field and who must not. Integration green on all four engines, adding the five-hop OTP step-up ceremony from the review finding, paired with #46's guard still green. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 2 read the tree that decision 15's answer produced and returned one quality finding: the amendment that added the OTP-only row deleted the zero-timestamp row beside it, and the claim that the re-auth subtest still covered userReallyAuthenticated's pre-existing !IsZero() term was false, since that subtest supplies a nonzero timestamp and passes either way. The run's own round 1 mutation evidence had already demonstrated exactly that and the amendment carried the claim forward without re-running it. Resolved inside the stage rather than escalated: the axis is quality, the fix is one test row with no production code, interface, schema, wire format, persisted shape or security property involved, and the reviewer, the code and mutation 2 already agree on what is uncovered, so there was no question left to ask. The reasoning is written out because the verdict asked for a human. Section 0 gains test/completed-authtime-zero, step 3's table gains the row and its amendment note now records the false claim instead of absorbing it, and the stage is Done with both tiers re-run in the foreground on the committed tree: modules green at 13 subtests, integration green on all four engines, 64 anchors resolving. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…fusal Stage 6's round 1 review found one blocking conformance defect and it is confirmed against the code: the new liveness refusal at /auth/issue restarts level 1 unconditionally, so a prompt=none ceremony whose session ends in the redirect hop from handlePromptNone is rendered a password form instead of being returned login_required. HasPromptValue has three production callers and none is on that path, so nothing between /auth/issue and /auth/pwd knows the request forbids UI. Escalated rather than fixed because decision 6 decides this shape rather than omitting it: it names prompt=none as the second sub-case's other entry, says restart level 1, and explicitly rejects login_required. Overriding a sealed rejection in authentication territory is the user's call. Section 3 gains item 16 as Open with four options and a recommendation, the header records the halt, section 7 gains the full round 1 record including what the review found sound, and section 8 is no longer stale. Stage 6's code stays uncommitted, as stage 5's did on decision 15. One bookkeeping fix rode along: middleware/session-identifier was cited three times and declared in no anchor row, so check-anchors now covers it at 72 rows. Refs #129
Blocking decision: for
|
The stage 6 round 1 entry said thirteen files, counting this document alongside the uncommitted stage tree. The tree is twelve, now enumerated so a resuming session can check it without recounting: a count that disagrees with git status reads as a lost file. Refs #129
|
Let's go with option A again. |
The user answered on PR #138: "Let's go with option A again." A prompt=none ceremony whose session ends between handlePromptNone's redirect and /auth/issue is returned login_required rather than restarted into a password form it is forbidden to display; every other ceremony still restarts level 1, so decision 6's rejection of login_required is scoped rather than reversed. Decision 16 flips to Decided carrying the user's words and what B, C and D cost. Stage 6 gains the outcome in step 2, a row in the step 5 and step 7 case tables, a third docs sentence in step 6, two anchor rows, and a run log entry recording the re-run tiers and mutations 7 and 8. Section 3 has zero Open items again. Refs #129
|
Applied. Decision 16 is What landed: one branch at the head of the existing refusal in One judgement inside your answer, recorded rather than made silently. The error description is Tests. One row at Docs. A third sentence in Verified on the amended tree, re-run in full rather than narrowed to the change: modules green on Two mutations, and they are the pair that matters here. Removing the new branch, which is stage 6 Stage 6 is still uncommitted, deliberately: the branch the review found missing is now present, so |
…thing Round 2 found the prompt=none refusal clearing the auth context after redirToClientWithError had already committed the response, so the Set-Cookie carrying the clear was dropped and the browser kept a context in ready_to_issue_code. Confirmed against the source and fixed inside the stage rather than escalated: unlike decision 16, this is not a question the agreement answered the other way, it is decision 16's own answer failing to take effect, and the ordering is forced by the same function's success path. Records the finding, the fix, mutation 9 at both tiers, three new anchor rows, the extended case tables, and the reasoning for a third round. Also drafts follow-up 4: the same inversion sits at seven pre-existing call sites, which is where #129's branch copied it from. The stage tree stays uncommitted pending round 3. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Gap 3's remaining exposure was a ceremony that passed /auth/completed while its session was alive, sat on the consent screen, and reached /auth/issue after the session was ended. The code minted there is brand new, so the marker termination writes onto existing codes cannot reach it. HandleIssueGet now checks liveness after the implicit-flow branch and before creating the code. The shape that case actually arrives in is an EMPTY session identifier, not a stale one: MiddlewareSessionIdentifier puts the identifier in the request context only when the row exists. That is not inert, because grantIsOffline reads an empty identifier as an offline grant on its own, so a code issued here would yield a refresh token good for up to RefreshTokenOfflineMaxLifetimeInSeconds whether or not offline_access was asked for. The refusal has two outcomes. An interactive ceremony restarts level 1, per decision 6. A prompt=none ceremony is returned login_required instead, per decision 16, because /auth/level1 leads to a password form and that request forbids any UI; the description matches handlePromptNone's own wording for this condition, so the client cannot tell the two hops apart. The auth context is cleared before the client response is written, since ClearAuthContext persists through a Set-Cookie and redirToClientWithError commits the response in every mode. RevokeCodeIfSessionGone, new on all four engines, compensates for the read followed by an insert: one statement that marks the code when the session is already gone, refusing an empty identifier or a zero id at entry. Termination marks codes that exist when it sweeps, this marks a code whose session was gone when it landed, and the interleaving escaping both is recorded as a residual rather than closed here. Tests: unit on three modules, data on mysql, postgres, mssql and sqlite, integration on all four engines, all green. Three review rounds, the last clean. Refs #129
Records round 3's clean verdict and what it covered, since a clean verdict is worth only what it checked: an independent scratch reproduction against the real CookieStore showing the clear now commits in all three response modes, the refusal's own behaviour intact, both new assertions biting for the right reason, and follow-up 4 correctly scoped out. Stage 6 flips to Done and the header now describes the committed state, which is the one bookkeeping point the reviewer raised. Also records the red run that preceded the green one: the tier script was piped into head, kept running in the container and held port 19090, so the next run contended with it. Refs #129
Ending a session marks every authorization code of that session revoked. A code revoked while it was still unredeemed has used = false, and the existing reaper filters used = true, so those rows would accumulate forever. That unbounded growth is the defect that moved the marker off a session-keyed registry in the first place, so leaving it would reintroduce what decision 4 rejected. DeleteUsedCodesWithoutRefreshTokens gains a second branch rather than a second method: one statement, one shared created_at cutoff, no interface signature change, no migration. Both classes are bounded by the same cutoff, so stating it once keeps the two copies from drifting. Two things about the predicate are load bearing rather than formatting. The NOT IN subquery stays inside the used branch, because ROPC refresh tokens carry code_id = NULL and x NOT IN (..., NULL) is UNKNOWN: hoisting it beside the cutoff would make the whole predicate UNKNOWN and ship the extension inert on any deployment that has ever issued a ROPC token. And used = false is what keeps the sweep away from a code with a live descendant, where the stake is higher than losing a marker, since fk_refresh_tokens_code is ON DELETE CASCADE and deleting the code would delete the very refresh token the marker exists to reject. Nothing a user can observe changes. A code this reaps was already unredeemable, and redemption answers a code it cannot find with the same generic invalid_grant it answers a revoked one with. Tests: two data-tier tests on all four engines, one carrying the class table and one carrying the ROPC NULL row alone, because a NULL code_id anywhere changes what the used branch can prove. Data green on mysql, postgres, mssql and sqlite; modules green on all three modules. Integration not applicable: no endpoint changes, and these rows are unreachable from any endpoint by the time they are reaped. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 1 came back clean: all three axes reviewed, zero findings, zero follow-ups. The entry records what it ran and what it answered question by question, because zero findings in a narrow scope reads exactly like zero findings in a thorough one. Two things worth the space. The reviewer built the statement independently on all four flavors rather than reading the Go, and this session re-derived it again before committing, since a wrongly grouped subquery is the one failure in this stage that leaves a green suite. And .review/before.sha was stale from stage 5, so the reviewer's no-edit claim rests on file mtimes instead of the usual hash comparison; that substitution is recorded rather than passed over. Stage 7 flips to Done and the header follows. Next: stage 8, gap 2's evidence, the last stage. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sable Gap 2 of #129 is the window inside rotation: the presented refresh token is claimed and its replacement inserted as two separate commits, so a refresh that validated before a termination swept the grant inserts its child after the sweep committed. For an offline grant nothing else invalidates that child, because the Offline branch of ValidateTokenRequest checks only the max lifetime and deliberately never consults the session. Decision 4 closed it structurally in stages 1 and 2 rather than by serializing anything: a rotated child inherits its parent's code_id, so marking the code marks every descendant, and the child is born already rejected because the fact predates its existence. Decision 1 asks for the proof before the issue closes, and this is that proof and no production line. TestToken_Refresh_ChildOfATerminatedGrantIsBornRejected checks the claim both ways round on one offline grant terminated through the real admin DELETE. The child that existed when the sweep ran must be refused by the marker rather than by its own revoked row, which the exact error_description distinguishes, since the marker is read in the validator ahead of the handler's revoked-row branch. Then the same child with its own revoked column cleared, which is byte for byte the row state a child inserted after the sweep has: server-minted JWT, row written by rotation, code marked by the real endpoint, session really gone, and the single cleared column the only thing the interleaving decides. That is the case that would hand out a working token without the marker. TestToken_Refresh_RacingATermination_LeavesNoUsableDescendant drives the window for real, eight presentations and the DELETE released together, and asserts the unconditional invariant: at most one replacement, and every replacement plus the pre-race parent refused afterwards. It claims nothing about which interleaving occurred and logs what it got, so a vacuous run says so. Measured, every engine produced one replacement, and on mssql and sqlite it was still live in storage, which is gap 2's own interleaving reached end to end. Two mutations measured on the real code and reverted. With the marker read dropped, and separately with RevokeCodesBySessionIdentifier dropped from the termination helper, stage 4's headline endpoint case and stage 6's consent ceremony both stayed green and only these two tests failed, answering the live child 200 with a working access token. That is the argument for the stage. Tests: integration green on all four engines, exit 0, 4768 passing test lines, zero FAIL, both new tests passing once per engine. Modules and data not run and not claimed: the one changed file is in a package neither tier compiles. Refs #129
Stage 8 flipped to Done with its review recorded. Round 1 was clean on all three axes with zero findings, zero follow-ups and zero bookkeeping, and the reviewed tree is provably the committed tree: .review/before.sha and git diff | sha256sum both read f51d8c916c26, the hash the request named. The entry records what the reviewer ran rather than that it agreed, its answer to each of the request's five questions, and one honesty note: its captured log truncates 3.5MB in the middle, so the per-engine race reading stands on this run's own measurement, not on the reviewer's agreement with it. What the capture does prove is a run spanning mysql through sqlite with zero FAIL and the harness's All tests completed successfully. Remaining: the closing pass, the full suite across every tier, sections 8 and 9 onto the pull request, and gh pr ready. Refs #129
Deferred decisions: noneThe run deferred nothing, so there is no list of assumptions here to check. That is the first thing to
Decision 15, raised at stage 5's review gate. Decision 6 fixed the gate as Decision 16, raised at stage 6's review gate. Stage 6 refuses to mint a code when the ceremony's Both answers are quoted into section 3 of the agreement with the options that lost, and both are covered Two escalations on a change this size is inside the normal range, and both were the same decision Judgement calls the run did make on its own are not hidden in this comment: each is recorded in its |
Follow-ups the run drafted, four, none filedEach is a real defect verified against the code, each is outside this change under section 2 of the The duplicate searches were re-run just now against the 33 open issues, since the tracker may have moved Full reasoning for each, including what was verified and why it is out of scope, is in section 9 of the 1. A code insert can still land between a termination's
|
The guard answered DONE at stage 8's gate, so this is the run's closing pass written into section 7 rather than left in the terminal. The full suite ran on the committed tree, every tier, exit 0, zero FAIL and zero panics: modules across all three modules, then data and integration each on mysql, postgres, mssql and sqlite. The race's per-engine reading reproduced exactly, the third independent run to agree with the stage 8 table: mysql and postgres land the replacement before the sweep, mssql and sqlite land it still live, which is gap 2's own interleaving. Sections 8 and 9 are posted to PR #138 as two comments, the deferred decisions (none, with what came to the user instead) and the four drafted follow-ups with the gh commands that file them. Their duplicate searches were re-run at the close against the 33 currently open issues and all four still stand. Nothing was filed. The entry also records what the run cost: 13 review rounds, 16 mutations, two blocking escalations both belonging to decision 6. Refs #129
The four drafted follow-ups are filedRe-verified against the code first, since the drafts were written during the run. Three went in as
Duplicates checked against the open and closed tracker. #139 is distinct from #131 and #132, which Still open, and it is yours to call. Section 9 of the agreement still reads |
Stage 5's code review returned one blocking security finding, confirmed against the code rather than taken on the reviewer's word: AuthenticatedAt has two writers, and handler_auth_otp.go is the second one. So a ceremony that reached OTP by SSO reuse, never touching the password form, satisfies decision 6's gate and recreates the session that was just terminated. For a user without OTP on a level2_mandatory client the enrollment page hands the browser the secret it will be tested on, so a stolen cookie alone reaches it. The sealed text disagrees with itself about this ceremony. Decision 6 names both writers and calls them both real authentication; section 1's departure note says the discriminator is level 1 authentication and that the password handler is its only writer. That is the user's call, not the run's: nothing in authentication or session territory is auto-resolved, and no security finding is settled by the run alone. Recorded as decision 15, Open, with the four options and a recommendation, and escalated on PR #138. Stage 5's code stays uncommitted, since the gate expression is the subject of the open decision. Section 8 is added, empty, because the closing PR comment reports it and an absent section reads the same as a forgotten one. Anchors green, 59 rows. No code changed in this commit. Refs #129
The user chose option A on PR #138: a dedicated level 1 proof on the AuthContext rather than reading AuthenticatedAt, which has two writers. Decision 15 flips to Decided with their words and what B, C and D lost on, and keeps the escalated question so the answer stays reviewable. Stage 5's steps are amended where the answer changed them rather than rewritten, because the run log's first stage 5 entry describes the earlier version: step 1's predicate, step 2's comment work (which the answer reverses), step 3's case table (one row replaced, not added), and a new step 6 for the field and the two assertions that pin who writes it. Four anchor rows added, one re-swept. Section 7 gains the continuation entry: what landed, the tiers re-run in full on the amended tree, and five mutations with disjoint failure sets, including one at the integration tier showing the round 1 gate issues a code and recreates the session while #46's guard stays green. Refs #129
…ssion HandleAuthCompletedGet's no-valid-session branch called StartNewUserSession unconditionally, minting a session from authContext.UserId with no proof that anyone authenticated. So an SSO ceremony whose session was ended mid-flight resumed at /auth/completed and silently recreated the session it was riding, and the code it then issued carried a fresh session identifier that no marker from stages 1 to 4 could reach: those stages mark and reject grants that already exist, and this one does not exist yet when termination runs. The gate is deliberately "this ceremony performed level 1" rather than "no valid session". The second shape is legitimate and already guarded by TestSessionDeletedDuringAuthFlow_LoginSucceeds (#46): a session is deleted, the user starts a fresh ceremony and really does enter a password. Failing that shape would break a case that must keep working. The proof is a dedicated Level1AuthCompleted bool on the AuthContext, written only by the password handler. AuthenticatedAt could not carry it: the OTP handler sets that field too, so a ceremony that stepped up to OTP by reusing a session satisfied it without a password, and for a user enrolling on a level2_mandatory client the browser is handed the secret it will be tested on, making the bypass reachable with a stolen cookie alone. That was found by review and answered by the repository owner on PR #138. AuthenticatedAt keeps its existing job of deciding whether to refresh a live session's AuthTime. An older cookie decodes the absent bool as false, which sends a ceremony already past the password form back to login once, and the legitimate step-up on a live session is untouched because it never reaches this branch. Tests: unit green on all three modules, with the completed-handler suite at 13 subtests where main has 10, covering the terminated-SSO shape, the OTP-only shape, the three positive controls that would fail against a gate keyed on the session alone, and the zero-timestamp row that keeps the neighbouring AuthTime discriminator honest. One assertion each in the password and OTP handler suites pins who writes the new field and who must not. Integration green on all four engines, adding the five-hop OTP step-up ceremony from the review finding, paired with #46's guard still green. Refs #129 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The user answered on PR #138: "Let's go with option A again." A prompt=none ceremony whose session ends between handlePromptNone's redirect and /auth/issue is returned login_required rather than restarted into a password form it is forbidden to display; every other ceremony still restarts level 1, so decision 6's rejection of login_required is scoped rather than reversed. Decision 16 flips to Decided carrying the user's words and what B, C and D cost. Stage 6 gains the outcome in step 2, a row in the step 5 and step 7 case tables, a third docs sentence in step 6, two anchor rows, and a run log entry recording the re-run tiers and mutations 7 and 8. Section 3 has zero Open items again. Refs #129
1 participant
Closes #129. Built by
/leo-runfrom the sealed agreement, eight stages, each reviewed by a secondagent before it was committed.
Issue: #129, ending a user session does not durably cut off access (
bug,security)Agreement:
docs/issue-129-durable-session-termination.mdRead first: the deferred decisions comment
(nothing was deferred, and it says what came to you instead), then
the follow-ups comment
(four drafted issues, since reviewed and filed as #139, #140, #141 and a comment on #109, see
"Follow-ups filed" at the bottom).
What the change does
Ending a session at either explicit "end session" endpoint becomes a security action with a durable
consequence. Three gaps closed, all of which failed open, meaning they preserved access somebody
believed they had removed:
codes.revokednow carries the boundary: terminating asession marks every authorization code that session issued, in one transaction with the sid-scoped
refresh-token sweep and the session delete. Redemption rejects a revoked code, and so does any
refresh token descended from one.
than by serializing anything: a rotated refresh token inherits its parent's
code_id, so marking thecode marks every present and future descendant. The racing child is born already rejected, because
the fact predates its existence.
/auth/completednow requires that thisceremony performed level 1 authentication before it mints a session, and
/auth/issuerefuses tobind a code to a session that no longer resolves, with a compensating
UPDATEcovering the insertthat lands just after a termination.
A session expiring still leaves an offline grant working, which is what
offline_accessis for. Asession explicitly ended does not. That distinction is the one the whole design rests on, and the
documentation now draws it.
The 16 decisions behind this, including the alternatives that lost and why, are in section 3 of the
agreement. Section 4 states the property that makes it safe; section 1 has the three gaps in full.
What landed, stage by stage
codes.revokedand its sweep: migration 000026 on four engines,RevokeCodesBySessionIdentifier, andAND revoked = falseon the code claim. Inert by construction, nothing reads it yet066d289ValidateTokenRequest, at redemption and at refresh, placed behind client authentication and PKCE per decision 7266615bTerminateUserSessionTx, the three writes in one transaction, plus theterminated_user_sessionaudit event. Still uncalledd19d8b5f964e54/auth/completedgate, on a dedicated level 1 proof rather than onAuthenticatedAt, per decision 155a7c280/auth/issueliveness check, the compensating revoke, andlogin_requiredrather than a login form for aprompt=noneceremony whose session ended, per decision 16422dd8a803f593682d51e26 commits over 60 files, one code commit per stage plus the agreement following it. The agreement's
section 7 is the run log: what landed, which tiers ran, every deviation, every review finding with its
evidence and disposition, and the mutations measured at each gate.
Tests
Full suite at the close, every tier, all four engines, green.
where.sh test --type all, exit 0,zero
FAILand zero panics, "All tests completed successfully". Modules across all three Go modules;the data tier on mysql, postgres, mssql and sqlite; the integration tier on the same four (64.8s, 74.3s,
99.2s, 43.2s), 9022 passing test lines in total.
Per tier, this change adds: migration and data-layer coverage on four engines for both new methods and
for the marker's
dont-updateprotection; unit coverage for both validator rejections including theordering rows that pin them behind client authentication; unit coverage for the termination helper's
transaction threading and its zero result on every failure path; two new handler test files that did not
exist before, covering the audit payloads and that a 403 terminates nothing; and integration coverage of
both endpoints, the three ceremonies that must not recreate a session, the
prompt=nonerefusal, andgap 2 both reconstructed and raced.
The race reaches the window rather than approaching it. In the closing run every engine produced one
replacement token alongside the termination, and on mssql and sqlite that replacement was still live in
storage when it was presented, so the sweep never saw it and the code marker was the only thing between
it and a working grant. On mysql and postgres it landed before the sweep. Both are legitimate and
neither is asserted, so the test logs which happened.
Mutation-tested at every gate, 16 in all, each applied to the real code and reverted. The two for
stage 8 are the argument for that stage existing: with the marker's read removed, and separately with
its write removed, stage 4's headline endpoint case and stage 6's consent ceremony both stayed green,
and only stage 8's two tests failed, answering a terminated grant with a working access token.
Deviations from the plan
Recorded per stage in section 7, and none changed what the change does. The load-bearing ones:
row could not pin what it claimed, because a missing secret is refused by an earlier guard, so a
present-but-wrong secret row was added. Demonstrated by relocating the check and watching the new row
fail while the old one passed.
catch a partially populated result, not one. The prediction was left in place and the measurement
recorded beside it, because editing the prediction would erase the evidence that it was wrong.
OTP alone. Rebuilt on a dedicated level 1 proof after you answered.
prompt=nonecannot be restarted into a loginform), and its round 2 found the new branch clearing the auth context after committing the client
response, so the clear reached nothing. Fixed inside the stage, with assertions that read the
committed response rather than a mock expectation. That defect turned out to exist at seven
pre-existing sites, now ClearAuthContext is called after the client response is committed in seven handlers, so the clear reaches nothing #141.
produced no replacement at all, so the interesting assertions never ran. Every assertion holds at any
value including zero, which is what keeps it a probability knob rather than a synchronization point.
Known limits, stated rather than implied
carries no
sidfor the session middleware to check and termination must not move the user'sgeneration. Decision 11, and the documentation says so rather than letting the credential-change
sentence be read as covering this case too.
UPDATEand itsCOMMIT. Decision 12 accepted it, and it is now Security: a code insert can land between a termination's UPDATE and its COMMIT, escaping both marks #139: closing it needs the same portableorder-a-write-against-a-sweep primitive that Refresh rotation is not coordinated with user-scoped generation changes, so a preserved session can be handed an unusable token #131 and Make refresh-token family containment atomic with rotation #132 want.
decision 13 leaving the interactive path's own defect to RP-Initiated Logout: post_logout_redirect_uri wrongly required, unencoded state, and non-standard sid in the redirect #109, where it is now recorded as a
comment.
Follow-ups filed
The four drafted follow-ups were re-verified against the code after the run closed, then filed. Two
bodies changed on the way in, and both changes narrow a claim rather than widen it.
UPDATE/COMMITwindowbug,security,go)idx_codes_session_identifier, by a blocking READ COMMITTED read, and by writer serialization respectively. Reframed as "correctness rests on three engines' defaults by accident", which is the standard #132's criterion 4 already sets. Without this a reader reproducing on SQLite would conclude the issue is wrongid_token_hintthrough/api/v1/account/logout-requestand lands ondoLogoutWithIdToken, which does tear down. And no first-party UI reaches the no-hint POST at all, since the auth server has no logout link of its own. The reachable callers are an RP omittingid_token_hint, which is conforming, and a direct requestamrbug,security,go)acrstays correct, so the token is internally inconsistent rather than silently over-claiming, and the narrow reachability the draft gave was confirmed, since theAuthMethodscopy sits inside thehasValidUserSessionblock and an idle-expired session therefore leaks nothingClearAuthContextafter the responsebug,security,go)returnafterhttpHelper.InternalServerError, so a failed redirect writes a 500 and falls throughEach was checked for duplicates against the open and closed tracker. #139 is distinct from #131 and
#132 (session-scoped code issuance, versus a user-scoped generation sweep and a family-scoped
containment cascade), and #134 held its previous shape but was closed as moot when decision 4 moved
the marker onto
codes.revoked, so nothing tracked it. Nothing at all tracked #140 or #141.Refs #129