Reference
Claims and limits
A feature can be released while its full security argument remains open. This ledger keeps implementation state separate from the strength and scope of its evidence.
The released protocol
| Property / ledger row | Evidence | Boundary |
|---|---|---|
| C1-original · broad active hybrid claim | Refuted historically | A reproduced trace rejected the earlier v3 claim. It is historical negative evidence, not a fresh attack on cap9 and not something a later feature silently turns into a theorem. |
| C1-M · matching-session confidentiality | Conditional sketch | The narrower argument depends on the named Auris-SK-HCE-Q hidden-component extraction assumption and its matching-session conditions. It is not the general rule “one component survives, therefore the channel is secure.” |
| C2 / C3 · integrity and forward secrecy | Design, regression tests and scoped arguments | AEAD and key deletion mechanisms require correct identity binding, retained-key policy, state management and implementation. They do not prove the complete messenger. |
| C4 · directional PQ healing | Sketch + simulations | Fresh unexposed key material, authenticated incorporation and sufficient delivered conversation are required. No universal message count or wall-clock deadline is claimed. |
| C5 · crash and rollback behavior | Executable models and regression tests | Send-state retirement fixes and random per-message salts reduce specific failure modes. Collisions remain probabilistic; state rollback, replay and retained secrets require separate treatment. |
| Cap9 protected headers | Implemented mechanism; versioned migration logic | Per-run keys reduce exposure compared with a stable session key. Current/retained key compromise, counters, timing and migration grace remain relevant. |
| Hybrid inner transport | Implementation, vectors and tests | Backend authentication is distinct from peer authentication. The deployed custom composition does not inherit the separate v5 proof. |
The historical ledger uses these row names across several protocol revisions. September amendments must be read alongside their versioned specifications, rather than applying every old result to today’s client.
The frozen v5 research candidate
- R2: pre-use root indistinguishability is a conditional, non-mechanized mathematical argument for revision 1.16. It excludes operational use of the root, ratcheting and implementation conformance.
- R3: symbolic pairwise authentication has 34 selected results in the archived evidence: 19 all-traces properties and 15 reachability witnesses. Symbolic primitives and trusted boundary premises are not an implementation audit.
- The earlier Q3 authentication model’s adequacy was rejected. Replaying a prover’s successful verdict did not answer whether its model admitted the relevant attacker.
- Pre-use system lifting retains an explicit failure term for the surrounding system. No argument here establishes that term is negligible for the product.
What is not established
- A complete computational proof of the released handshake, ratchet, storage and call composition.
- A committing-AEAD theorem for the whole salted message construction.
- Global traffic-analysis resistance, identity-free calls, or an operator unable to correlate sockets.
- Human identity established solely by a directory signature or successful message decryption.
- Complete crash, rollback, multi-device and recovery safety from a primitive-level theorem.
- Independent human expert review of the whole app or an independent product audit.
- Overall superiority to another messenger, or a claim of being quantum-proof.
How a claim earns stronger evidence
Name the version, property, attacker, compromise timing, delivery assumptions and leakage. Link the frozen statement and artifacts. Reproduce the result; test whether the model permits the relevant attack; relate its transitions to the implementation; then review the remaining composed system. A failed check or counterexample narrows the claim instead of disappearing from the record.
How to read the evidence explains which sources are public and which remain project-reported. Comparisons applies the same standard to other systems.
Reviewed · Review scope and versions