docs(auth): what the third reading found, and Proton's rule (ADR 0017)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Tizian 「ティツィアーン」 <raisondetredev@pm.me>

apps/learn/AGENTS.md

@@ -74,12 +74,12 @@ A spaced-repetition learning app: studysets of flashcards, reviewed on an FSRS s
 
 - **Authentication**: server-side sessions (`ServerSideSessionsConfigFromPasswords`), not JWT, for immediate revocation. Scopes are copied onto the session row, so changing a person's scopes means updating their session rows too.
 - **Identity**: `AuthUser` is the person; identity providers (anonymous, GitHub, an email address with a password) attach to it. Content references `AuthUser`, never a provider account. A person may sign in with GitHub and with an address and password, one of each (`account.signInWays`, which also says whether they have a password and a confirmed authenticator); the Profile tab lists their ways in, adds GitHub where offered, and holds halkyon_app's `AccountSecuritySection` (setting up a password, the authenticators, changing it).
-  - **A password and an authenticator** (ADR 0017, built 2026-10-20 for build 22; halkyon_base's and halkyon_app's READMEs): the only way an identified person signs in besides GitHub, which is deprecated. The address, a password that never leaves the device (SRP-6a, `passwordSignIn.begin` and `complete`, the verifier and the account's wrapped keys on the register) and a code from an authenticator app (TOTP, mandatory) or a recovery code. An address nobody has is answered as an account's would be (decoys from `signInDecoyKey`), and every wrong credential is refused alike (`wrongCredentials`). Lost authenticator: the password and a mailed code (or the recovery phrase) turn it off 72 hours later, a mail at the start, a sign-in with a code calling it off; lost password: the recovery phrase's signature and a code set a new one, keys kept, or without the phrase a mailed code resets the whole account (new keys) after the same 72 hours. An account with a password and a confirmed authenticator no longer signs in by a mailed code or GitHub (`usePassword`); where passwords are offered, no new GitHub account is linked (`deprecated`), and from `GITHUB_SIGN_IN_ENDS` on GitHub signs nobody in and pruning forgets every GitHub ID (D2). Password sign-in is on only where the passwords hold `totpKey`, `recoveryCodeKey` and `signInDecoyKey` (`TOTP_KEY`, `RECOVERY_CODE_KEY`, `SIGN_IN_DECOY_KEY` in `deploy/.env`) and email sign-in is set up (`passwordSignIn` in `instance.basics()`). On the device (halkyon_app): signing up shows the recovery phrase once and checks three of its words before anything reaches the instance; signing in checks SRP's M2 and opens the keys before the session is put in place; an authenticator still to set up is set up with the session held back; the unlocked keys stay in the system's keyring per instance and person, gone once another person signs in or nobody. A change of password ends the account's other sessions and a reset all of them, on every service of the instance (`sessions_ended_notice`).
+  - **A password and an authenticator** (ADR 0017, built 2026-10-20 for build 22; halkyon_base's and halkyon_app's READMEs): the only way an identified person signs in besides GitHub, which is deprecated. The address, a password that never leaves the device (SRP-6a, `passwordSignIn.begin` and `complete`, the verifier and the account's wrapped keys on the register) and a code from an authenticator app (TOTP, mandatory) or a recovery code. An address nobody has is answered as an account's would be (decoys from `signInDecoyKey`), and every wrong credential is refused alike (`wrongCredentials`). Lost authenticator: the password and a mailed code (or the recovery phrase) turn it off 72 hours later, a mail at the start, a sign-in with a code calling it off; lost password: the recovery phrase's signature and a code set a new one, keys kept, or without the phrase a mailed code resets the whole account (new keys) after the same 72 hours. An account with a password and a confirmed authenticator no longer signs in by a mailed code or GitHub (`usePassword`); where passwords are offered, no new GitHub account is linked (`deprecated`), and from `GITHUB_SIGN_IN_ENDS` on GitHub signs nobody in and pruning forgets every GitHub ID (D2). Password sign-in is on only where the passwords hold `totpKey`, `recoveryCodeKey` and `signInDecoyKey` (`TOTP_KEY`, `RECOVERY_CODE_KEY`, `SIGN_IN_DECOY_KEY` in `deploy/.env`) and email sign-in is set up (`passwordSignIn` in `instance.basics()`). On the device (halkyon_app): signing up shows the recovery phrase once and checks three of its words before anything reaches the instance; signing in checks SRP's M2 and opens the keys before the session is put in place; an authenticator still to set up is set up with the session held back; the unlocked keys stay in the system's keyring per instance and person, gone once another person signs in or nobody. A session alone never gets a code checked (ADR 0017's third reading, as Proton has it): every signed-in change of how the account is secured (adding an authenticator once one is confirmed, removing a confirmed one, new recovery codes, a new phrase, a new password, deleting) takes the password and a code (`OwnerProof`), each sheet asking for both; a session's wrong proofs count for it alone and the tenth in a row ends it, never making the account's codes wait. A change of password ends the account's other sessions and a reset all of them, on every service of the instance (`sessions_ended_notice`).
   - **One account across the instance** (ADR 0016, decided 2026-10-19; halkyon_base's README): Learn's server holds the instance's register, so its tables keep every service's ways in, handles and profiles, and an account's ID is the `AuthUser` ID in every service. The instance's other services (Todo) are its members: they ask it over its web server (`/halkyon-base/register/…`, `addInstanceRoutes` in `server.dart`, never forwarded by Caddy) with the secret the services share (`instanceSecret`, `INSTANCE_SECRET` in `deploy/.env`), and a member's anonymous person adding a way in becomes an account here under the same ID. Deleting an account (here, or a member passing it on) keeps a notice per member in the same transaction (`account_deletion_notice`), told at once and hourly until each confirms (`tellMembersOfDeletions`). Learn's endpoints and code go through the module as on any register; nothing changes for Learn's apps.
   - **GitHub keeps only the numeric GitHub ID**: our own slim login (halkyon_base's `github.dart`) on Serverpod's GitHub helpers; Serverpod's stock GitHub login endpoint, which stores name, email and avatar, is never exposed. GitHub sign-in is on only where the passwords hold `githubClientId` and `githubClientSecret` (in production `GITHUB_CLIENT_ID`/`GITHUB_CLIENT_SECRET` in `deploy/.env`); the app asks halkyon_base's `instance.basics()`.
   - **Linking keeps the person** (`GitHubUpgradeEndpoint`, `requireLogin`): the GitHub ID joins the signed-in anonymous person, who becomes identified and loses the anonymous identity, in one transaction. **Signing in** (`GitHubSignInEndpoint`) only reaches people who have a GitHub account already, and only without a session: Serverpod refuses to issue another person's session inside a signed-in call. Refusals are `GitHubSignInRefusedException` with a reason.
   - **Switching devices' person** (halkyon_app's `switchToGitHub` and `useSession`, on whether the device holds content as Learn counts it, `PersonDependencies.holdsContent`: its studysets, Recently deleted's too): swap the session directly, never through "signed out" (which would leave the device asking how to start), then delete the account left behind if it was anonymous (nobody could sign into it again), never an identified one. Someone identified is never offered a switch: an address or GitHub account that is another account's is said to be so.
-  - **Email keeps only a keyed hash of the address** (ADR 0010, decided 2026-10-15): our own slim login (halkyon_base's `email.dart`) on Serverpod's code challenges and rate limiter, as Serverpod's email sign-in keeps the address in plain text and passwords. `email_identity` holds HMAC-SHA256 of the address in lower case, keyed with `emailSignInPepper`; the instance mails only an address someone has just typed, and the device remembers the address it signed in with (`SignInAddresses`, `sign_in.json` in the person's folder). A code by mail signs nobody in since ADR 0017 (build 22): it proves an address for a password's setup, a sign-up, a setup never finished, the resets and deleting an account whose second factor doesn't work, each code asked for one of those purposes (`EmailCodePurpose`), taken by it alone, its mail saying what it would do and to type it only in the app on this instance. Eight Crockford characters (halkyon_base's `short_code.dart`, shared with connect codes), 15 minutes, 3 tries, up to 3 valid at once for an address (a fourth voids the oldest); at most 3 codes an hour per address and network, 10 per address from every network and 10 per network. `emailCode.sendCode` (without a session) answers alike for every address. Refusals are `EmailSignInRefusedException` with a reason. Codes go by mail over SMTP (halkyon_base's `code_mail.dart`, naming the app the host configures, pub.dev's `mailer`, TLS only), through the service the passwords name (`emailSmtpHost`, `emailSmtpPort`, `emailSmtpUser`, `emailSmtpPassword`, `emailFrom`; in production `EMAIL_SMTP_…` and `EMAIL_FROM` in `deploy/.env`; learn.halkyon.eu's is Proton's), as plain text with the code in the subject; without one, into the server's log in development, and elsewhere there is no email sign-in (`emailSignIn` in halkyon_base's `instance.basics()`, which the app asks). Nothing logs an address or a code (a failed mail logs its error's type), and never attach a handler to `package:logging`'s root logger, through which `mailer` would.
+  - **Email keeps only a keyed hash of the address** (ADR 0010, decided 2026-10-15): our own slim login (halkyon_base's `email.dart`) on Serverpod's code challenges and rate limiter, as Serverpod's email sign-in keeps the address in plain text and passwords. `email_identity` holds HMAC-SHA256 of the address in lower case, keyed with `emailSignInPepper`; the instance mails only an address someone has just typed, and the device remembers the address it signed in with (`SignInAddresses`, `sign_in.json` in the person's folder). A code by mail signs nobody in since ADR 0017 (build 22): it proves an address for a password's setup, a sign-up, a setup never finished, the resets and deleting an account whose second factor doesn't work, each code asked for one of those purposes (`EmailCodePurpose`), taken by it alone, its mail saying what it would do and to type it only in the app on this instance. Eight Crockford characters (halkyon_base's `short_code.dart`, shared with connect codes), 15 minutes, 3 tries, up to 3 valid at once for an address (a fourth voids the oldest); at most 3 codes an hour per address and network, 10 per address from every network and 10 per network. `emailCode.sendCode` (without a session) answers alike for every address. Refusals are `EmailSignInRefusedException` with a reason. Codes go by mail over SMTP (halkyon_base's `code_mail.dart`, naming the app the host configures, pub.dev's `mailer`, TLS only), through the service the passwords name (`emailSmtpHost`, `emailSmtpPort`, `emailSmtpUser`, `emailSmtpPassword`, `emailFrom`; in production `EMAIL_SMTP_…` and `EMAIL_FROM` in `deploy/.env`; learn.halkyon.eu's is Proton's), as plain text with the code and what it is for in the subject; without one, into the server's log in development, and elsewhere there is no email sign-in (`emailSignIn` in halkyon_base's `instance.basics()`, which the app asks). Nothing logs an address or a code (a failed mail logs its error's type), and never attach a handler to `package:logging`'s root logger, through which `mailer` would.
   - **On Linux and Windows the browser half is the app's own** (`LoopbackWebAuth`, halkyon_app): the system browser and a loopback address (RFC 8252), put in place of flutter_web_auth_2's own implementation (checked with v5.1.0) before each sign-in. The package's front ends every pending sign-in when the app is resumed, and on the desktop the window regaining focus resumes it, so its loopback server closed before GitHub answered. Ours waits for GitHub, the profile's Cancel (shown only there), choosing another tab, a change of person, or 5 minutes; the regression test drives the package's front through a focus change. Remove it once the package stops ending sign-ins on focus there. Serverpod (v4.0.3) reports every cancelled browser round trip as an unknown error, so the gateway knows a cancel only by having asked for it; a cancel on GitHub's own page, or leaving the browser on Android, still shows "Couldn't sign in with GitHub."
 - **Authorization lives in endpoint code**; Serverpod has no row-level security. Load content filtered by the session's `authUserId`, never by an owner ID the client sends. A row another person owns must be indistinguishable from a missing one. Features involving other people require the `identified` scope, declared via `requiredScopes`, never checked ad hoc.
   - **The reference is `DevicesEndpoint`** (`apps/learn/halkyon_learn_server/lib/src/auth/`) with its tests: the owner check sits in the same query (`WHERE "id" = $1 AND "authUserId" = $2`), zero rows means `NotFoundException` (shared, `lib/src/common/`), and every rule has a test that asserts the refusal. Each query carries its SQL as a comment.

docs/adr/0017-password-totp-and-keys.md

@@ -338,6 +338,57 @@ these; all but the ninth were fixed (the developer's choice):
     unavailable**, which the app read as "no password sign-in here": it has its own
     refusal now (`passwordChanged`), saying to sign in again with the new password.
 
+### Third reading (21 Oct 2026)
+
+A third independent reading, of the re-reading's fixes (`1383640..a45842f`), found its
+items 1, 2, 4, 6, 7 and 10 fixed and 5 and 8 holding but for the points below. The first
+finding was a regression of item 3, so rather than count once more, the developer chose
+Proton's rule (21 Oct 2026):
+
+- **A session alone never gets a code checked.** Every signed-in change of how an
+  account is secured takes the owner's proof (`OwnerProof`): the password's SRP proof
+  for a change's challenge (`password.beginChange`, the person checked) and then a TOTP
+  or recovery code. That is adding an authenticator once one is confirmed, removing a
+  confirmed one, new recovery codes, a new phrase, a new password and deleting. Only the
+  first authenticator (none confirmed, after a reset carried out too) is confirmed with
+  its own code alone, and removing one never confirmed takes nothing. A proof given where
+  none is taken is refused, and a confirmed authenticator's code is never checked again
+  for a session (confirming it again is refused as unknown), so no success passes a
+  proof unchecked. `wrongExistingCode` goes: a wrong code from another authenticator is
+  a wrong proof.
+- **A session's proofs count for it alone** (`asOwnerProofTry`, table
+  `session_code_failures`, where the session is, on a member too): each counted before
+  it is checked, cleared only by one accepted, the tenth wrong in a row ending the
+  session. They never count toward the account's waits nor wait for them, and a new
+  password forgets those waits.
+
+The findings, and what was done:
+
+1. **A stolen session guessed codes without end** (high): nine wrong codes for new
+   recovery codes, then removing an unconfirmed authenticator of its own, a success that
+   cleared the count, and again. Closed by the rule: no code is checked for a session
+   without the password first, and only a proof accepted clears the count.
+2. **Whoever knew the password held a signed-in owner out of changing it**: ten wrong
+   codes at sign-in made the account's codes wait, and the owner's change waited too.
+   Signed-in proofs no longer wait for the account's waits, and the change forgets them.
+3. **A stolen session spent the ten changes an account begins an hour**, holding its
+   owner out of changing the password, a new phrase and deleting. Beginning counts
+   nothing against the account: at most 30 an hour per session, a bound on the work one
+   session asks for that holds back no other; only failed proofs count, per session.
+4. **Deleting, with the authenticators' reset taken effect but not carried out**, was
+   offered a code field (the app read "an authenticator was confirmed") which the
+   instance refused (it read "no second factor works"). The instance takes a TOTP or
+   recovery code wherever an authenticator is confirmed, a code by mail where no second
+   factor works, and tells the app which (`SignInWays.secondFactorWorks`).
+5. **A device that didn't know the account's address couldn't change the password, set a
+   new phrase or delete** (`addressUnknown`). Signed-in calls take no address any more:
+   nothing there mails, the account's waits being the sign-in's. Deleting by mail asks
+   for the address where the device doesn't know it, as the code goes there; the
+   instance takes the code only for the account's own address.
+6. **The code mail's subject hid its purpose**, which a notification shows alone. The
+   subject names it ("K7QX-M2PD: your Halkyon Learn code to delete your account"), and the
+   sign-up mail says it also gives a password to an account with that address and none.
+
 ## Consequences
 
 - People keep a password, an authenticator app and a recovery phrase: more to keep than a

packages/halkyon_app/README.md

@@ -69,7 +69,11 @@ Written as the apps are: Dart 3.13's primary constructors, Material from
   screens: the start screen's Sign in and Create an account,
   `showPasswordSignInSheet`, `showAccountSetupSheet`,
   `showAccountRecoverySheet`, and `AccountSecuritySection` for an app's
-  account part. Anonymous people get no keys until something is encrypted
+  account part. Every change of how the account is secured asks for the
+  password with the code, one answer per sheet (`OwnerAnswer`, the owner's
+  proof: a session alone gets no code checked); deleting by a code by mail
+  follows `secondFactorWorks`, as the instance tells it, and asks for the
+  address only where the device doesn't know it. Anonymous people get no keys until something is encrypted
   (step 4). Every build of an app needs a C compiler and make: sodium's build
   hook compiles libsodium.
 - **Files** (`FileSaver`, `PlatformFileSaver`): keeping a file the app made

packages/halkyon_base_server/README.md

@@ -191,8 +191,9 @@ Built on the three parts above, on the register (members forward every step thro
   account without a working second factor. Each is asked for a purpose
   (`EmailCodePurpose`: `signUp`, `finishSetup`, `authenticatorReset`, `accountReset`,
   `deletion`; `email_code_request.purpose`), only that purpose takes it (any other is
-  refused as no longer valid and leaves it unused), and its mail says what it would do
+  refused as no longer valid and leaves it unused), and its mail says what it would do,
-  and to type it only in the app on that instance. Since step 3
+  in its subject too (a notification shows the subject alone), and to type it only in
+  the app on that instance. Since step 3
   nothing turns a code into a session (`emailCode.verifyCode`, `emailSignIn.signIn` and
   the switch token went with build 22, `minimumAppBuild` 22 in Learn).
 - **Signing up** (`passwordSignIn.signUp(request, code, setup)`, without a session): an
@@ -222,30 +223,40 @@ Built on the three parts above, on the register (members forward every step thro
   get no more checked; an address nobody has alike), past which no proof is checked and
   nothing begins for it anywhere until the hour has passed: so whoever knows an address
   and fills its count from one network holds no other back, and guessing from many
-  makes at most 30 guesses an hour. A change's proofs (a `change` challenge) count per
+  makes at most 30 guesses an hour. A signed-in owner's proofs (a `change` challenge,
-  account instead, 10 begun an hour, never toward the address, and no sign-in takes one.
+  below) never count toward the address, and no sign-in takes one. A sign-in or the
-  Every call carrying a code after the password or phrase proved (sign-in, the phrase's
+  phrase's reset carrying a code takes the account's `address` and `language`, refused
-  reset, a change, a new phrase, deletion) takes the account's `address` and `language`,
+  (`wrongCredentials`) before any code is checked when it isn't theirs.
-  refused (`wrongCredentials`) before any code is checked when it isn't theirs.
+- **The owner's proof** (`OwnerProof`, ADR 0017's third reading, as Proton has it): a
+  session alone never gets a code checked. Every signed-in change of how an account is
+  secured (adding an authenticator once one is confirmed, removing a confirmed one, new
+  recovery codes, a new phrase, a new password, deleting) takes the password's SRP proof
+  for a challenge `password.beginChange` gave (30 begun an hour per session, holding
+  back no other) and then a TOTP or recovery code (`proveOwner`, `ownersCode`). A proof
+  given where none is taken is refused, so none passes unchecked. Each proof counts for
+  its session alone (`owner_proof_tries.dart`, `asOwnerProofTry`, table
+  `session_code_failures`, kept where the session is, on a member too), before it is
+  checked; the tenth wrong in a row ends the session (`sessionEnded`), only a proof
+  accepted clears the count, and a try that checked none is taken back. Never toward the
+  account's waits, nor waiting for them: whoever knows the password holds no signed-in
+  owner out of changing it, and a new password forgets those waits.
 - **Authenticators:** a secret made on the register, shown once as an `otpauth://` URI
-  (issuer: the account domain); confirmed by a code; while the account has a confirmed
+  (issuer: the account domain); confirmed by a code from it; while the account has a
-  one, another counts only with a code from that one too (`wrongExistingCode`), so a
+  confirmed one, another counts only with the owner's proof too, so a session alone adds
-  session alone adds no second factor; the first confirmed brings ten recovery codes; at
+  no second factor; confirming one confirmed already is refused as unknown (its code is
-  most 10 per account; the last confirmed one stays; removing a confirmed one, or new
+  never checked for a session); the first confirmed brings ten recovery codes; at most
-  recovery codes, takes a code. Each step's code is accepted once, by a conditional
+  10 per account; the last confirmed one stays; removing a confirmed one, or new recovery
-  update of `lastStep`. A signed-in session's codes here count for that session alone
+  codes, takes the owner's proof, removing one never confirmed nothing. Each step's code
-  (`session_code_tries.dart`, table `session_code_failures`, kept where the session is,
+  is accepted once, by a conditional update of `lastStep`.
-  on a member too), each counted before it is checked; the tenth wrong in a row ends the
-  session (`sessionEnded`), a code accepted clears the count, a try that checked no code
-  is taken back; never toward the account's waits, so a stolen session holds nobody out.
 - **Codes tried in a row** (`second_factor_waits.dart`, table
   `second_factor_failures`): every code tried against an account's second factor after
-  a right password or phrase (sign-in, the phrase's reset, a change, a new phrase,
+  a right password or phrase at sign-in or in the phrase's reset (never the owner's
-  deletion) counts, per account, from every network, before it is checked, one at a time
+  proofs while signed in) counts, per account, from every network, before it is checked, one at a time
   per account (an advisory lock), so codes sent at once get no more checked; every tenth
   in a row begins a wait as it is counted (`codesWait`, with when), an hour, then twice
   as long each time, a day at the most, and every wait mails the account's address
-  (which those calls take); a code accepted, and either reset carried out, clears it.
+  (which those calls take); a code accepted, either reset carried out, and a new
+  password clear it.
 - **Resets:** a lost authenticator: SRP's proof plus a mailed code or the recovery
   phrase's signature asks for it; it takes effect 72 hours later, a mail tells the
   address at once, and signing in with a code calls it off; then the password alone
@@ -256,18 +267,21 @@ Built on the three parts above, on the register (members forward every step thro
   password, the keys staying. A lost password without it: a mailed code asks, 72 hours
   pass (a mail at the start, a sign-in calls it off), a new code carries it out: new
   password, new keys, no authenticators.
-- **Changing while signed in:** `password.beginChange` and `password.change` take the old
+- **Changing while signed in:** `password.change` takes the owner's proof (the old
-  password's SRP proof, a TOTP or recovery code and the same keys wrapped under the new
+  password's SRP proof for a `password.beginChange` challenge, and a TOTP or recovery
-  password; `password.setRecoveryKeys` replaces the phrase's wrapping with the same
+  code) and the same keys wrapped under the new password; `password.setRecoveryKeys`
-  proof and code (a phrase of one's own would otherwise set a new password through the
+  replaces the phrase's wrapping with the same proof (a phrase of one's own would
-  phrase's reset). A session alone changes neither, nor a session and a code.
+  otherwise set a new password through the phrase's reset). A session alone changes
+  neither, nor a session and a code.
 - **Deleting an account with a password** (`account.delete(proof:)`, a `DeletionProof`)
-  takes the same: the password's proof for a `beginChange` challenge, the account's
+  takes the same: the password's proof for a `beginChange` challenge and a code, bound
-  address and a code, bound to the host the device addressed (`requireOwnerToDelete`; a
+  to the host the device addressed (`requireOwnerToDelete`; a member passes the proof on
-  member passes the proof on and the register checks it). Where no second factor works
+  and the register checks it), counted for the session as every owner's proof is. The
-  (a setup never finished, or the authenticators' reset taken effect) the code is one by
+  code is a TOTP or recovery code wherever an authenticator is confirmed; where no second
-  mail asked for deleting (`request`, `code`). An account without a password deletes
+  factor works (a setup never finished, or the authenticators' reset taken effect;
-  with its session, as before.
+  `SignInWays.secondFactorWorks` tells the app) it may be one by mail asked for deleting
+  (`request`, `code`), to the account's own address. An account without a password
+  deletes with its session, as before.
 - **Sessions end everywhere:** a change of password ends every other session of the
   account; a reset of the password or the account ends all. The register ends its own
   and keeps a `sessions_ended_notice` per member (told at once and hourly until it