Move the pin to the engine's main and regenerate
`.e2e-ref` was at 0e91cf0, which is why doc-pages was red: this branch regenerated security.leaf from a newer SECURITY.md than the pin names, so the gate compared the page against the old source and found a page ahead of it. The pin now names 60f82e6, which carries the moved lattice disclosure with its warning markers removed, the corrected §19.5 and §20.6 Android columns, and the new §19.3 head-signature row. Four pages follow it: audit, engine, security and spec. The spec page has been telling readers since this morning that Android verifies no inclusion proof and pins no head. It does both, in client/Trust.kt. This is what takes that off the page. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 5
parent
2c58a68ab4
commit
e75cdcbcfc
@@ -1 +1 @@
|
||||
0e91cf0d49f2d90da5cd1ced2ca55f2ca740c1dd
|
||||
60f82e6e9dfed8050cf4c951f3037f16d879d025
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
<!-- GENERATED by Scripts/build-doc-pages.sh from flamenet-e2e/docs/AUDIT-SCOPE.md.
|
||||
Edits made HERE are deleted the next time that script runs.
|
||||
Change the markdown source and re-run it.
|
||||
source-sha256: f634dbaa8653b2bf -->
|
||||
source-sha256: 6e389f58eb4bfd00 -->
|
||||
<article class="band doc doc-generated">
|
||||
<div class="wrap wrap-narrow">
|
||||
<h1 id="audit-scope">Audit scope</h1>
|
||||
@@ -97,12 +97,11 @@ what is stored and for how long.</li>
|
||||
records the alternative.</li>
|
||||
<li><strong>Compromised endpoints.</strong> Keys live on devices;
|
||||
malware on one reads plaintext.</li>
|
||||
<li><strong>Peers with no post-quantum identity.</strong> Android
|
||||
shipped §20 in 0.29, so this is now a rollout rather than a platform
|
||||
gap: a device that has not taken the update, or one restored from a
|
||||
backup written before it, publishes no <code>ik_pq</code> and is
|
||||
authenticated classically. §20.2 makes that a supported state rather
|
||||
than an error; it is not a silent downgrade. §20.6.</li>
|
||||
<li><strong>Peers with no post-quantum identity.</strong> A device that
|
||||
has not taken the update, or one restored from a backup written before
|
||||
it, publishes no <code>ik_pq</code> and is authenticated classically.
|
||||
§20.2 makes that a supported state and not an error; it is not a silent
|
||||
downgrade. §20.6.</li>
|
||||
</ul>
|
||||
<h2 id="4-trust-boundaries">4. Trust boundaries</h2>
|
||||
<ul>
|
||||
@@ -113,6 +112,12 @@ is what detects a fork.</li>
|
||||
<li><strong>Issuer ⇄ relay.</strong> The issuer's verification key is
|
||||
<strong>configuration, never fetched</strong>. A relay that fetched it
|
||||
over HTTPS could be handed a key by a compromised issuer.</li>
|
||||
<li><strong>Client ⇄ issuer.</strong> Separate boundary, weaker rule. A
|
||||
client has no configuration channel, so it reads the issuer key from the
|
||||
relay's <code>/.well-known/flamenet/relay</code> once and pins it, as it
|
||||
does the log head. The first read is taken on faith and every head after
|
||||
it is checked, which catches a relay that changes its issuer key and not
|
||||
one that was dishonest from the first contact. §19.3.</li>
|
||||
<li><strong>Device ⇄ device.</strong> Peers authenticate through the
|
||||
ratchet. Identity changes are pinned and surfaced rather than accepted
|
||||
silently.</li>
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
<!-- GENERATED by Scripts/build-doc-pages.sh from flamenet-e2e/README.md.
|
||||
Edits made HERE are deleted the next time that script runs.
|
||||
Change the markdown source and re-run it.
|
||||
source-sha256: f3862932722bdd0f -->
|
||||
source-sha256: dda11c7adf31e254 -->
|
||||
<article class="band doc doc-generated">
|
||||
<div class="wrap wrap-narrow">
|
||||
<h1 id="flamenet-e2e">flamenet-e2e</h1>
|
||||
@@ -110,7 +110,8 @@ src/e2e-client.js REST client + manager, pinning, trust, registration, replen
|
||||
src/e2e-bootstrap.js page wiring
|
||||
src/e2e-vault.js encrypted IndexedDB store for keys and ratchet state
|
||||
vendor/ bundled @noble/post-quantum, MIT, rebuildable via scripts/build-vendor.sh
|
||||
test/ five suites; run them before trusting anything here
|
||||
test/ run them before trusting anything here; the four CI runs need no network,
|
||||
`npm test` adds the ones wanting a live relay and a Swift toolchain
|
||||
docs/SPEC.md the protocol contract, §12 is the post-quantum delta</code></pre>
|
||||
<h2 id="use">Use</h2>
|
||||
<pre class="js"><code>import { DeviceIdentity, E2ESession } from &#("#")39;./src/e2e.js&#("#")39;;
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
<!-- GENERATED by Scripts/build-doc-pages.sh from flamenet-e2e/SECURITY.md.
|
||||
Edits made HERE are deleted the next time that script runs.
|
||||
Change the markdown source and re-run it.
|
||||
source-sha256: 73372e9266389804 -->
|
||||
source-sha256: 756563bdae2de235 -->
|
||||
<article class="band doc doc-generated">
|
||||
<div class="wrap wrap-narrow">
|
||||
<h1 id="security">Security</h1>
|
||||
@@ -62,12 +62,11 @@ one user. Native clients do not have this property. Any deployment
|
||||
making confidentiality claims to users must be explicit about which
|
||||
client those claims apply to.</li>
|
||||
</ul>
|
||||
<h2
|
||||
id="warning-file-labels-the-half-of-the-lattice-that-is-not-enforced">⚠️
|
||||
File labels: the half of the lattice that is not enforced</h2>
|
||||
<h2 id="file-labels-the-half-of-the-lattice-that-is-not-enforced">File
|
||||
labels: the half of the lattice that is not enforced</h2>
|
||||
<p>The Files screen carries classification labels, and a label set is a
|
||||
claim about which rules hold. Only one of the two holds, so the other is
|
||||
named here rather than implied away. See flamenet-messenger ios#("#")65 and
|
||||
named here instead of implied away. See flamenet-messenger ios#("#")65 and
|
||||
android#("#")15.</p>
|
||||
<p><strong>No read up is enforced.</strong> An object your session label
|
||||
does not dominate is not visible, and by default writes happen at
|
||||
@@ -77,16 +76,16 @@ principal cleared to a high label may open a session at a lower one and
|
||||
write there, carrying down what they read above it. No client stops
|
||||
this, because a session label inside a principal's clearance range is a
|
||||
legitimate session.</p>
|
||||
<p>🔴 This is the half the model exists for. No-read-up stops somebody
|
||||
<p>This is the half the model exists for. No-read-up stops somebody
|
||||
reaching material above them, which most systems get right.
|
||||
No-write-down stops the material leaking <em>downward through a person
|
||||
who is allowed to see it</em>, which is the threat a lattice is built to
|
||||
contain.</p>
|
||||
<p>⚠️ Deliberate, and not an oversight: a rule enforced on one client
|
||||
and not the other is worse than the gap, and strict enforcement with no
|
||||
downgrade path produces a workaround culture. Doing it properly means an
|
||||
explicit downgrade action with an audit trail. Until that exists, this
|
||||
is written down.</p>
|
||||
<p>The gap is a decision, not an oversight: a rule enforced on one
|
||||
client and not the other is worse than the gap, and strict enforcement
|
||||
with no downgrade path produces a workaround culture. Doing it properly
|
||||
means an explicit downgrade action with an audit trail. Until that
|
||||
exists, this is written down.</p>
|
||||
<p>So "implements Bell-LaPadula" would be too round a word. What exists
|
||||
is the <strong>simple security property</strong>, not the
|
||||
<strong>★-property</strong>.</p>
|
||||
|
||||
+51
-43
@@ -3,7 +3,7 @@
|
||||
<!-- GENERATED by Scripts/build-doc-pages.sh from flamenet-e2e/docs/SPEC.md.
|
||||
Edits made HERE are deleted the next time that script runs.
|
||||
Change the markdown source and re-run it.
|
||||
source-sha256: 68c16c3f2737c5f7 -->
|
||||
source-sha256: 1e697de7cd21a6e6 -->
|
||||
<article class="band doc doc-generated">
|
||||
<div class="wrap wrap-narrow">
|
||||
<h1 id="flamenet-messenger-end-to-end-encryption-spec">Flamenet
|
||||
@@ -3734,80 +3734,76 @@ record.</p>
|
||||
<td>yes</td>
|
||||
<td><code>src/keylog.js</code></td>
|
||||
<td><code>KeyLog.swift</code></td>
|
||||
<td><code>KeyLog.kt</code>, no call site</td>
|
||||
<td><code>KeyLog.kt</code></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>Client demands a proof before first use</td>
|
||||
<td>n/a</td>
|
||||
<td>automatic</td>
|
||||
<td>automatic</td>
|
||||
<td>no</td>
|
||||
<td>automatic</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>Checks the head signature against a pinned issuer key</td>
|
||||
<td>n/a</td>
|
||||
<td>yes</td>
|
||||
<td>yes</td>
|
||||
<td>yes</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>Refuses a relay that serves no log</td>
|
||||
<td>n/a</td>
|
||||
<td>opt-in</td>
|
||||
<td>opt-in</td>
|
||||
<td>no</td>
|
||||
<td>opt-in</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>A relay that stops answering reads as a fork</td>
|
||||
<td>n/a</td>
|
||||
<td>yes</td>
|
||||
<td>yes</td>
|
||||
<td>no</td>
|
||||
<td>yes</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>Append-only pinning across sessions</td>
|
||||
<td>n/a</td>
|
||||
<td>yes</td>
|
||||
<td>yes</td>
|
||||
<td>no</td>
|
||||
<td>yes</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>§19.4 gossip, consumes a peer's head</td>
|
||||
<td>n/a</td>
|
||||
<td>yes</td>
|
||||
<td>yes</td>
|
||||
<td>no</td>
|
||||
<td>yes</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>§19.4 gossip, sends its own head</td>
|
||||
<td>n/a</td>
|
||||
<td>yes</td>
|
||||
<td>yes</td>
|
||||
<td>no</td>
|
||||
<td>yes</td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>The last row is split from the one above on purpose: a client that
|
||||
only consumes gossip is a client no fork can be detected against, so
|
||||
consuming and sending are recorded separately.</p>
|
||||
<p><strong>The Android column read <code>automatic</code> and
|
||||
<code>yes</code> until 2026-09-21 and was wrong in every row.</strong>
|
||||
<code>KeyLog.kt</code> is real and is checked against the published
|
||||
vectors, but counting production call sites across
|
||||
<code>engine/src/main</code> and <code>app/src/main</code> gives zero
|
||||
for <code>verifyInclusion</code>, <code>verifyConsistency</code>,
|
||||
<code>verifyHead</code>, <code>canonicalLeaf</code>,
|
||||
<code>rootFromInclusion</code> and <code>logSubject</code>. The gossip
|
||||
type <code>kt_head</code> is declared in <code>Content.kt</code> and
|
||||
listed in <code>CONTROL</code>, so an arriving head is classified as
|
||||
traffic not to display, and nothing sends one or acts on one. An Android
|
||||
client today verifies no inclusion proof, pins no head, and gossips
|
||||
nothing.</p>
|
||||
<p>§15 records the opposite error, two Android cells marked not done
|
||||
that were already working, and corrects it the same way this does: by
|
||||
what has been RUN. A cell is evidence about behaviour, not about whether
|
||||
a file exists. The rule that catches both directions is to find the call
|
||||
site, and the iOS column survives it, <code>verifyHead</code> has six
|
||||
callers, <code>verifyConsistency</code> two,
|
||||
<code>verifyInclusion</code> and <code>canonicalLeaf</code> one
|
||||
each.</p>
|
||||
<p>Until those call sites exist, a conversation with an Android device
|
||||
has the property §19 was written to remove: the relay is the sole
|
||||
distributor of that device's bundles and substitution leaves no evidence
|
||||
on that end.</p>
|
||||
<p>The Android call sites are in <code>client/Trust.kt</code>, reached
|
||||
from <code>client/Conversations.kt</code>:
|
||||
<code>enforceKeyLogIfServed</code> per served bundle,
|
||||
<code>verifyLogConsistencyIfDue</code> on a timer,
|
||||
<code>headPayload</code> to send a head and <code>gossip</code> to
|
||||
consume one. The pin and the served flag are per relay host in the
|
||||
vault, so both survive a restart.</p>
|
||||
<p>A cell here is evidence about behaviour, not about whether a file
|
||||
exists, and the check that produces one is to find the call site. It has
|
||||
to be run against every module: this repository's engine is
|
||||
<code>engine/</code>, but its clients live in <code>client/</code>, and
|
||||
a search of <code>engine/</code> and <code>app/</code> alone finds none
|
||||
of the call sites above and reports a working implementation as absent.
|
||||
§15 records the same error made the other way.</p>
|
||||
<p>Verification is checked across engines and against the running relay,
|
||||
not transitively: <code>test/interop.mjs</code> proves the two engines
|
||||
compute the same leaf hash and both reject a reversed audit path, and
|
||||
@@ -3820,6 +3816,17 @@ back its own bytes would otherwise satisfy the check, and refuses with
|
||||
<code>KeyNotLoggedError</code> or <code>KeyLogForkError</code>. The head
|
||||
is pinned on first sight and every later fetch must prove consistency
|
||||
with it.</p>
|
||||
<p>The head signature is a separate row because inclusion and
|
||||
consistency both reduce to <code>root</code>, and <code>root</code>
|
||||
arrives inside the head the relay served. They establish that a log is
|
||||
self-consistent, not that it is the log the issuer vouches for, so a
|
||||
client checking only those two has verified nothing about who it is
|
||||
talking to. The web engine reads the issuer key from
|
||||
<code>/.well-known/flamenet/relay</code>, pins it on first sight next to
|
||||
the head pin, and refuses a head signed by another key, a signature
|
||||
lifted from a different head, or a missing signature from a relay that
|
||||
published a key. A relay publishing no issuer key is left unchecked, on
|
||||
the §19.4 argument about deployments predating a section.</p>
|
||||
<p><strong>Audit-path ordering.</strong> RFC 6962 audit paths are
|
||||
ordered leaf-first. A top-down reading of the same array produces the
|
||||
correct root for any left-spine index, so an implementation that
|
||||
@@ -3927,8 +3934,12 @@ a bundle.</p>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>Android shipped this in <strong>0.29</strong>, published 2026-09-21.
|
||||
The rollout is not the same thing as the release: a device that has not
|
||||
taken the update, or one restored from a backup written before it,
|
||||
Both halves: <code>DeviceIdentity</code> mints and signs, and
|
||||
<code>client/Conversations.kt</code> calls <code>PQIdentity.check</code>
|
||||
from <code>sessionFor</code>, which is the new-session path §20.5 names
|
||||
and the only moment a downgrade can be attempted.</p>
|
||||
<p>The rollout is not the same thing as the release: a device that has
|
||||
not taken the update, or one restored from a backup written before it,
|
||||
publishes no <code>ik_pq</code> and is authenticated classically. §20.2
|
||||
makes that a supported state, so nothing breaks, but a conversation is
|
||||
post-quantum authenticated only where both ends have it and no client
|
||||
@@ -4004,14 +4015,11 @@ and checks it byte for byte against the vector, which is the
|
||||
cross-engine agreement FIPS 204 keygen determinism allows. Signatures
|
||||
are deliberately not pinned in the vectors because ML-DSA signing is
|
||||
randomised; verification is against the public key instead.</p>
|
||||
<p>The paragraph that stood here said "iOS and Android implement none of
|
||||
this", which contradicted the table four lines above it and had been
|
||||
wrong since iOS shipped §20. Corrected 2026-09-21. The lesson is the one
|
||||
§12 and §14 each record: a status that disagrees with itself teaches the
|
||||
reader to distrust the parts that are accurate.</p>
|
||||
<p><strong>Android implements none of it.</strong> A conversation is
|
||||
post-quantum-authenticated only where both ends are web or iOS. Nothing
|
||||
surfaces to either user which one a given conversation got.</p>
|
||||
<p><strong>Android does all of it too</strong>, as of 0.29.
|
||||
<code>PQSign</code> is ML-DSA-65 on BouncyCastle,
|
||||
<code>DeviceIdentity</code> publishes and signs, and
|
||||
<code>Conversations</code> enforces the same three refusals on the
|
||||
new-session path.</p>
|
||||
<h2 id="21-anonymous-sender-credentials">21. Anonymous sender
|
||||
credentials</h2>
|
||||
<h3 id="211-what-exists-and-what-it-does-not-do">21.1 What exists, and
|
||||
|
||||
Reference in New Issue
Block a user