12 KiB
Formal Verification
Machine-checked proofs of all 13 security theorems from the Formal Analysis specification, using two independent tools: Tamarin Prover (symbolic) and CryptoVerif (computational).
These models were authored by the protocol designers and have not undergone independent peer review. They are published for transparency and to facilitate third-party verification. All results are machine-checkable and reproducible.
Totals: 8 Tamarin models (55 lemmas) + 5 CryptoVerif models (7 queries) = 62 machine-checked results, 0 failures.
Run verify.sh from the repository root to reproduce all results. See
source.
Tamarin Models
Symbolic formal verification of the Soliton cryptographic protocol using Tamarin Prover. 8 models, 55 lemmas.
These models were authored by the protocol designers and have not undergone independent peer review. They are published for transparency and to facilitate third-party verification. All results are machine-checkable and reproducible.
Requirements
- tamarin-prover 1.12.0+
- maude 3.5.1+
Usage
# All models
../verify.sh tamarin
# Single model
tamarin-prover LO_Auth.spthy --prove
Resource Usage
All 8 models complete in under 90 seconds total with under 2 GB peak RAM. No special hardware or overnight runs required — a laptop is sufficient.
This is achieved through bounded unrolling (3–4 steps for ratchet and chain models) and unique fact names per state (eliminating branching during source analysis).
Results
Verified with Tamarin 1.12.0, Maude 3.5.1.
LO_Auth.spthy — Theorem 6 (Key Possession)
| Lemma | Result | Steps |
|---|---|---|
| Auth_Exists | verified | 5 |
| Auth_Ordering | verified | 2 |
| Auth_Single_Use | verified | 8 |
| Auth_No_Accept_After_Timeout | verified | 3 |
| Auth_Unique_Challenge | verified | 2 |
| Theorem6_Key_Possession | verified | 11 |
| Theorem6_No_Oracle | verified | 11 |
LO_KEX.spthy — Theorems 1, 2a, 2b (Session Key Secrecy, Authentication)
OPK-present case only. See header comment for OPK-absent scope note.
| Lemma | Result | Steps |
|---|---|---|
| KEX_Exists | verified | 27 |
| Theorem1_Session_Key_Secrecy_A | verified | 70 |
| Theorem1_Session_Key_Secrecy_B | verified | 136 |
| Theorem1_EK_Secrecy_A | verified | 70 |
| Theorem1_EK_Secrecy_B | verified | 136 |
| Theorem2a_Recipient_Binding | verified | 2 |
| Theorem2b_Initiator_Authentication | verified | 10 |
| OPK_Single_Use | verified | 24 |
| Key_Uniqueness | verified | 2 |
LO_Ratchet.spthy — Theorems 4, 5 (Forward Secrecy, PCS — structural)
Abstract model using Fr() epoch keys. Proves FS and PCS are structural properties of the state machine, independent of KDF/KEM security.
| Lemma | Result | Steps | Notes |
|---|---|---|---|
| send_sanity | verified | 7 | |
| send_fs | verified | 2818 | Theorem 4a |
| send_corrupt_terminates | verified | 193 | |
| send_pcs | verified | 2 | Abstract model only |
| recv_sanity | verified | 6 | |
| recv_fs_1step | falsified | 11 | Expected — prev_ek_r retains old key |
| recv_fs_2step | verified | 9132 | Theorem 4b |
| recv_corrupt_terminates | verified | 273 | |
| recv_pcs | verified | 107 | Abstract model only (see comment) |
LO_Ratchet_PCS.spthy — Theorem 5 (PCS — KEM-level)
KEM-level model proving the 1-step non-recovery / 1-direction-change recovery that the abstract Fr() model cannot distinguish.
| Lemma | Result | Steps | Notes |
|---|---|---|---|
| pcs_sanity | verified | 3 | |
| pcs_no_recovery_after_recv | falsified | 9 | Expected — adversary holds sk_own |
| pcs_recovery_after_send | verified | 7 | |
| pcs_recovery_sustained | verified | 15 | |
| pcs_f4_violated | verified | 7 | F4 defeats next recv, not this send |
LO_Call.spthy — Theorems 8–11 (Call Key Security)
| Lemma | Result | Steps |
|---|---|---|
| Call_Exists | verified | 6 |
| Call_Key_Agreement | verified | 56 |
| Theorem8_Call_Key_Secrecy | verified | 24 |
| Theorem9_Intra_Call_FS | verified | 193 |
| Theorem10_Call_Ratchet_Ind | verified | 3 |
| Theorem11_Concurrent_Ind | verified | 52 |
LO_AntiReflection.spthy — Theorem 12 (Anti-Reflection)
| Lemma | Result | Steps |
|---|---|---|
| Reflection_Sanity | verified | 8 |
| Theorem12_Anti_Reflection | verified | 5 |
LO_Stream.spthy — Theorem 13, Properties 2–5 (Streaming AEAD)
| Lemma | Result | Steps |
|---|---|---|
| Stream_Sanity | verified | 11 |
| Stream_Sanity_Finalize | verified | 7 |
| Theorem13_P2_Integrity | verified | 28 |
| Theorem13_P3_Ordering | verified | 18 |
| Theorem13_P4_No_False_Final | verified | 17 |
| Theorem13_P5_Cross_Stream | verified | 55 |
| Theorem13_Key_Secrecy | verified | 3 |
LO_NegativeTests.spthy — Expected Falsifications
Each lemma confirms a known attack path works in the model. All should be falsified (or verified for exists-trace). If any result flips, the model has a bug.
| Lemma | Result | Steps | Attack path |
|---|---|---|---|
| neg_auth_ik_corrupt | falsified | 8 | IK corruption forges auth |
| neg_auth_rng_corrupt | falsified | 10 | RNG corruption forges auth |
| neg_ratchet_no_fs_0step | falsified | 8 | Corrupt immediately reveals ek |
| neg_ratchet_recv_1step | falsified | 10 | 1-step recv, prev retains ek |
| neg_call_rk_plus_rng | falsified | 9 | rk + RNG derives call key |
| neg_stream_key_corrupt | falsified | 5 | Key corruption enables forgery |
| neg_reflect_self_session | falsified | 7 | Self-session enables reflection |
| neg_kex_no_opk | falsified | 11 | IK+SPK alone breaks OPK-absent |
| neg_ratchet_duplicate | falsified | 7 | No recv_seen → duplicate accepted |
| neg_call_self_session | verified | 3 | Self-call reachable without guard |
Scope and Limitations
- OPK-absent KEX: LO_KEX.spthy models the 3-key (OPK-present) case only. The 2-key OPK-absent case has a weaker secrecy threshold (IK+SPK), validated by neg_kex_no_opk in the negative tests.
- X-Wing as black box: All models treat X-Wing as a single IND-CCA2 KEM without opening the combiner (draft-09 hybrid argument).
- Abstract ratchet: LO_Ratchet.spthy uses Fr() epoch keys (not KDF-derived). KEM-level properties are in LO_Ratchet_PCS.spthy.
- No Theorem 7: Domain separation is vacuously true in Tamarin (string constants are structurally distinct).
- No Theorem 3/13-P1: Message confidentiality (IND-CPA) is computational, covered by the CryptoVerif models.
- Bounded chains: Ratchet and call chain steps are bounded (3–4 steps) to prevent Tamarin non-termination.
Theorem Coverage
| Theorem | Model | Type |
|---|---|---|
| 1 (KEX Key Secrecy) | LO_KEX | Symbolic secrecy |
| 2a (Recipient Auth) | LO_KEX | Structural binding |
| 2b (Initiator Auth) | LO_KEX | Correspondence |
| 4 (Forward Secrecy) | LO_Ratchet | Structural FS |
| 5 (PCS) | LO_Ratchet + LO_Ratchet_PCS | Structural + KEM-level |
| 6 (Auth Key Possession) | LO_Auth | Correspondence |
| 8 (Call Key Secrecy) | LO_Call | Symbolic secrecy |
| 9 (Intra-Call FS) | LO_Call | Chain one-wayness |
| 10 (Call/Ratchet Ind.) | LO_Call | Independence |
| 11 (Concurrent Calls) | LO_Call | Independence |
| 12 (Anti-Reflection) | LO_AntiReflection | AAD direction binding |
| 13 P2–P5 | LO_Stream | Integrity, ordering, truncation, isolation |
CryptoVerif Models
Computational formal verification of the Soliton cryptographic protocol using CryptoVerif.
These models were authored by the protocol designers and have not undergone independent peer review. They are published for transparency and to facilitate third-party verification. All results are machine-checkable and reproducible.
Requirements
- CryptoVerif 2.12+
- The
pq.cvllibrary (ships with CryptoVerif)
Usage
# All models
CV_LIB=/path/to/pq ../verify.sh cryptoverif
# Single model
cryptoverif -lib /path/to/pq LO_Auth.cv
Resource Usage
All 5 models complete in under 5 seconds total with negligible RAM usage. No special hardware required.
Results
Verified with CryptoVerif 2.12.
LO_Auth.cv — Theorem 6 (Key Possession)
| Query | Result | Bound |
|---|---|---|
| event(ServerAccepts) ==> event(ClientResponds) | proved | Ns × P_mac + P_kem |
| inj-event(ServerAccepts) ==> inj-event(ClientResponds) | proved | Ns × P_mac + P_kem |
Primitives: IND-CCA2 KEM (X-Wing), SUF-CMA deterministic MAC (HMAC-SHA3-256).
LO_KEX.cv — Theorem 2b (Initiator Authentication)
| Query | Result | Bound |
|---|---|---|
| event(Bob_Accept) ==> event(Alice_Init) | proved | P_sig_A |
Primitives: EUF-CMA signature (HybridSig). Proof uses only Alice's signature unforgeability. Non-injective (replay is application-layer per §7.5 A4).
LO_KEX_Secrecy.cv — Theorem 1 (Session Key Secrecy)
| Query | Result | Bound |
|---|---|---|
| secret rk_A [cv_onesession] | proved | 2·P_prf + 2·P_kem_ik + 2·P_kem_spk + 2·P_kem_opk + collision terms |
Primitives: 3× IND-CCA2 KEM, PRF (HKDF). Signatures omitted (Theorem 1 is secrecy, not authentication). No corruption oracles (Tamarin covers corruption cases). See header comment for full simplifications list.
LO_Ratchet_MsgSecrecy.cv — Theorem 3 (Message Key Secrecy)
| Query | Result | Bound |
|---|---|---|
| secret test_mk [cv_onesession] | proved | 2 × P_prf |
Precondition: epoch key ek is fresh (from Theorem 1 + KDF_Root output independence). Combined with AEAD IND-CPA+INT-CTXT under random keys (standard [BN00] composition), gives full message secrecy.
LO_Stream_Secrecy.cv — Theorem 13, Properties 1+2 (Streaming AEAD)
| Query | Result | Bound |
|---|---|---|
| secret b0 [cv_bit] (IND-CPA) | proved | 2·P_ctxt + 2·P_cpa(time, N_enc) |
| inj-event(Received) ==> inj-event(Sent) (INT-CTXT) | proved | P_ctxt |
Adapted from CryptoVerif's TLS 1.3 Record Protocol example. Nonce uniqueness enforced via table-based game hypothesis (§9.11(f)). base_nonce is public.
Key properties of the bounds:
- INT-CTXT has no Q-factor — direct forgery reduction
- IND-CPA scales as N_enc × P_cpa — Q-step hybrid argument
Scope and Limitations
- X-Wing as black box: All models treat X-Wing as a monolithic IND-CCA2 KEM. The spec (§2.1) recommends opening the combiner for CryptoVerif. The black-box assumption is stronger; bounds are in terms of P_kem rather than component advantages (P_mlkem + P_x25519 + P_sha3_ro).
- No corruption oracles: The CryptoVerif KEX models prove security for the no-corruption case. Corruption-parameterized secrecy (partial key compromise, RNG corruption) is verified by the Tamarin models.
- Simplified KDF info: LO_KEX_Secrecy.cv binds fewer values in the PRF input than the full HKDF info field. The PRF proof holds regardless of info content; session-binding properties are verified by Tamarin.
- Single-epoch message secrecy: LO_Ratchet_MsgSecrecy.cv assumes a fresh epoch key. The composition chain (Theorem 1 → KDF_Root → fresh ek → PRF → fresh mk → AEAD) is sound but not mechanically verified end-to-end.
- No Theorem 2c/d: Key confirmation requires a combined KEX+Ratchet model.
Theorem Coverage
| Theorem | Model | What's proved |
|---|---|---|
| 1 (KEX Key Secrecy) | LO_KEX_Secrecy | rk indistinguishable from random |
| 2b (Initiator Auth) | LO_KEX | σ_SI authentication via EUF-CMA |
| 3 (Message Secrecy) | LO_Ratchet_MsgSecrecy | mk indistinguishable from random |
| 6 (Auth Key Possession) | LO_Auth | Correspondence + injective |
| 13 P1 (IND-CPA) | LO_Stream_Secrecy | Bit secrecy of challenge bit |
| 13 P2 (INT-CTXT) | LO_Stream_Secrecy | Injective correspondence |