Research · R3
Symbolic authentication
A machine-checked model can establish a precise protocol property under its assumptions. It cannot establish that the model includes every relevant behavior of the app.
The frozen result
The proposed v5 initial handshake has a frozen Tamarin model revision 1.4, an evidence package revision 1.4.1 and a narrowed paper statement revision 1.4.2. Its archived evidence covers 19 all-traces lemmas and 15 existence witnesses across nine checkpoints. These are 34 selected results, not 34 independent audits.
The central pairwise statement says that a modeled pre-commit cryptographic verification has an earlier matching initiator start, unless both modeled device signing keys were previously disclosed. The wire is attacker-controlled, while authorization, selected prekey-generation state and permanent device-ID premises are explicit trusted boundaries. The result is non-injective: replay and durable single acceptance are separate.
Model primitives are symbolic abstractions. Tamarin’s manual explains the distinction between security properties quantified over traces and existence properties used to demonstrate reachable behavior.
What the witnesses actually say
- Honest one-time and last-resort pre-commit verifications can occur. The selected one-time witness uses OT1; forcing the second selectable one-time record was not established by a selected witness.
- Disclosing both signing keys permits an impersonation trace without an honest start. This checks that the attacker can exploit the modeled compromise rather than being excluded by the grammar.
- Redelivering a public transcript can cause two cryptographic verifications. A modeled one-time prekey can support two distinct pre-commit initials. Durable consumption must close that gap elsewhere.
- A session using a selected responder KEM secret compromised before the matching start is reachable. This is an honest reachability witness; it is not an impersonation attack or a root-secrecy result.
- Finite multi-contact examples are reachable. They do not establish arbitrary same-responder concurrency, rotation or recovery.
The accepted-record erratum
The record-provenance lemmas recover an earlier authorization and generation source for selected key tuples. They do not prove equality of every commitment, expiry, ratchet field, one-time root and capability field with the values in the accepted transcript. Revision 1.4.2 narrows the written claim without changing the frozen proof bytes.
Expiry and extension values being included in a transcript does not establish validation of their semantics. The full 44-field symbolic transcript also does not prove injective byte encoding or parser agreement in Swift.
What remains outside
| Boundary | Still needed |
|---|---|
| Concrete cryptography | Computational signature theorem and active-quantum lift |
| Bytes and code | Encoding injectivity, parser agreement, implementation and side-channel conformance |
| Durable state | Single acceptance and one-time consumption across crashes, rollback and concurrency |
| Identity system | Concrete authorization, directory, recovery, transparency, revocation and device-ID discipline |
| Wider protocol | First contact, downgrade, cross-suite/role composition and broader concurrency |
| Independent assessment | Human expert/venue review; no product audit follows from these model results |
How the evidence is checked
The archived package pins the frozen theory by hash and records tool versions, return codes, proof objects and result logs. All-traces proofs require complete trees without unresolved proof leaves. Existence search needs a satisfying trace; unresolved sibling branches do not mean its witness was exhaustive.
This documentation review runs the publication-consistency checker against those saved artifacts. That is not a fresh Tamarin search. The source repository is not public, so readers should treat this package’s result as project-reported until the exact model and evidence are publicly accessible.
An earlier authentication model reproduced its verdicts but failed an adequacy review because its acceptance grammar excluded relevant attacker behavior. The lesson is to inspect what a model permits before treating “verified” as evidence about the intended system.
Reviewed · Review scope and versions