wiki updates

Signed-off-by: Kamal Tufekcic <kamal@lo.sh>
2026-04-23 08:14:02 +03:00 · 2026-04-23 08:14:02 +03:00 · 65c7bcc8e5
commit 65c7bcc8e5
parent c1ee2b58ef
7 changed files with 366 additions and 17 deletions
--- a/Formal-Verification.md
+++ b/Formal-Verification.md
@ -0,0 +1,311 @@
+# Formal Verification
+
+Machine-checked proofs of all 13 security theorems from the
+[Formal Analysis](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](https://git.lo.sh/lo/libsoliton/src/branch/master/verify.sh).
+
+---
+
+# Tamarin Models
+
+Symbolic formal verification of the Soliton cryptographic protocol using
+[Tamarin Prover](https://tamarin-prover.com/). 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
+
+```bash
+# 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](https://bblanche.gitlabpages.inria.fr/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.cvl` library (ships with CryptoVerif)
+
+## Usage
+
+```bash
+# 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 |
+