diff --git a/README.md b/README.md index d307870925..5f23c654d6 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,8 @@ Pure-Rust post-quantum cryptographic library. Provides composite identity keys ( | [Abstract.md](Abstract.md) | Security analysis specification — adversary model, theorems, and verification targets for formal modeling | | [Specification.md](Specification.md) | Full cryptographic specification (v1) | | [CHEATSHEET.md](CHEATSHEET.md) | API quick reference with types, sizes, and signatures | +| [tamarin/README.md](tamarin/README.md) | Symbolic formal verification — 8 Tamarin models, 55 lemmas (Theorems 1–13) | +| [cryptoverif/README.md](cryptoverif/README.md) | Computational formal verification — 5 CryptoVerif models with concrete security bounds | ## Crate Layout diff --git a/Specification.md b/Specification.md index 704ac51a39..69cf1cc963 100644 --- a/Specification.md +++ b/Specification.md @@ -2770,7 +2770,7 @@ All CAPI functions with output buffer parameters zero the output upfront (after - `soliton_stream_encrypt_init(key, key_len, caller_aad, aad_len, compress, out)` — init encryptor (generates random base nonce). `key_len` MUST be exactly 32; any other value returns `InvalidLength`. Unlike `header_len` (lenient — extra bytes accepted), `key_len` is strict — the key is always exactly 32 bytes for XChaCha20-Poly1305. - `soliton_stream_encrypt_header(enc, out, out_len)` — copy 26-byte header into caller-allocated buffer; `out_len` MUST be ≥ 26 (lenient: extra buffer space is accepted) - `soliton_stream_encrypt_chunk(enc, plaintext, ..., is_last, out)` — encrypt one chunk; `out_len` MUST be ≥ `STREAM_ENCRYPT_MAX` (1,048,849 bytes) — returns `InvalidLength` for smaller buffers (parallel to the `out_len < STREAM_CHUNK_SIZE → InvalidLength` rule for decrypt chunk) -- `soliton_stream_encrypt_chunk_at(enc: *const, index, plaintext, ..., is_last, out)` — encrypt at explicit index (stateless, random-access); uses `*const SolitonStreamEncryptor` (not `*mut`) to reflect the `&self` Rust contract — see §15.11 for the `*const` caveat. Same `out_len` ≥ `STREAM_ENCRYPT_MAX` requirement as the sequential variant. `index` MUST be unique per call — calling with the same `index` and different plaintexts produces nonce reuse (§15.12). Does not advance `next_index`. Not interchangeable with the sequential variant; see §15.11 for mixed-mode use. **Absent from `soliton.h`**: this function is implemented and exported (`#[unsafe(no_mangle)]`) but has no declaration in the C header — its decrypt counterpart `soliton_stream_decrypt_chunk_at` is declared in the header. Binding authors (C, C++, Go cgo, C#, Dart) must supply a manual `extern` declaration matching the signature above until the header is updated. +- `soliton_stream_encrypt_chunk_at(enc: *const, index, plaintext, ..., is_last, out)` — encrypt at explicit index (stateless, random-access); uses `*const SolitonStreamEncryptor` (not `*mut`) to reflect the `&self` Rust contract — see §15.11 for the `*const` caveat. Same `out_len` ≥ `STREAM_ENCRYPT_MAX` requirement as the sequential variant. `index` MUST be unique per call — calling with the same `index` and different plaintexts produces nonce reuse (§15.12). Does not advance `next_index`. Not interchangeable with the sequential variant; see §15.11 for mixed-mode use. Declared in `soliton.h` (lines 1926–1962) with full documentation. - `soliton_stream_encrypt_is_finalized(enc, out: *mut bool)` — write finalized state to `out` - `soliton_stream_encrypt_free(enc)` — free encryptor (zeroizes key). Returns `int32_t`: 0 on success, `NullPointer` (-13) if outer pointer null, 0 (safe no-op) if inner pointer null (null inner pointer means the handle was already freed or never initialized — matches the double-free behavior of `soliton_ratchet_free` / `soliton_keyring_free`; does NOT return `NullPointer` for inner-null), `ConcurrentAccess` (-18) if in use, `InvalidData` (-17) if type discriminant wrong @@ -2784,13 +2784,7 @@ All CAPI functions with output buffer parameters zero the output upfront (after - `soliton_stream_decrypt_expected_index(dec, out: *mut u64)` — write next expected sequential index to `out` - `soliton_stream_decrypt_free(dec)` — free decryptor (zeroizes key). Returns `int32_t`: 0 on success, `NullPointer` (-13) if outer pointer null, 0 (safe no-op) if inner pointer null (null inner pointer means already-freed or never-initialized — does NOT return `NullPointer` for inner-null, consistent with `soliton_ratchet_free` / `soliton_keyring_free`), `ConcurrentAccess` (-18) if in use, `InvalidData` (-17) if type discriminant wrong -**`SOLITON_STREAM_ENCRYPT_MAX` and `SOLITON_STREAM_CHUNK_SIZE` are NOT defined as `#define` constants in `soliton.h`**: The header references these names in documentation comments but does not provide `#define` or `constexpr` entries. Binding authors who write `out_len = SOLITON_STREAM_ENCRYPT_MAX` get a compile error. The values must be embedded as integer literals in bindings: `STREAM_ENCRYPT_MAX = 1,048,849` (encrypt output buffer, see Appendix A) and `STREAM_CHUNK_SIZE = 1,048,576` (decrypt output buffer, see Appendix A). Language-idiomatic constant definitions are recommended: -```c -// C/C++ — add to binding wrapper or generated header -#define SOLITON_STREAM_ENCRYPT_MAX 1048849UL -#define SOLITON_STREAM_CHUNK_SIZE 1048576UL -``` -These values are stable and will not change without a major version bump. +`SOLITON_STREAM_ENCRYPT_MAX` (1,048,849) and `SOLITON_STREAM_CHUNK_SIZE` (1,048,576) are defined as `#define` constants in `soliton.h` (lines 53–54). Binding authors can use these names directly. These values are stable and will not change without a major version bump. **Streaming decrypt output buffer minimum — `STREAM_CHUNK_SIZE` (1,048,576 bytes)**: Both `soliton_stream_decrypt_chunk` and `soliton_stream_decrypt_chunk_at` require the output buffer to be at least `STREAM_CHUNK_SIZE` bytes regardless of the expected plaintext size. This is because the buffer size cannot be known before decryption completes (for compressed streams, the decompressed size is variable and determined post-AEAD; for uncompressed streams, the plaintext size equals the ciphertext minus the 16-byte AEAD tag, which requires parsing the ciphertext first). The library therefore mandates a worst-case buffer that can hold any valid decrypted chunk. **This is asymmetric with the encrypt side**: the encrypt output buffer uses `STREAM_ENCRYPT_MAX` (1,048,849 bytes), which is larger than `STREAM_CHUNK_SIZE` to accommodate compression overhead and the tag_byte. The decrypt minimum is the raw `STREAM_CHUNK_SIZE` because decrypt outputs plaintext (no tag_byte, no compression overhead). Binding authors who size the output buffer to the expected plaintext for a small final chunk (e.g., a 100-byte final chunk with a 100-byte output buffer) will receive `InvalidLength` with no diagnostic in the error message indicating that buffer size is the cause. See Appendix A for the constant value. diff --git a/cryptoverif/LO_Auth.cv b/cryptoverif/LO_Auth.cv new file mode 100644 index 0000000000..4200501930 --- /dev/null +++ b/cryptoverif/LO_Auth.cv @@ -0,0 +1,121 @@ +(* LO-Auth: Key Possession Proof (Theorem 6) + * + * Protocol (§6): + * Server → Client: c, where (c, ss) ← XWing.Encaps(pk_IK_client[XWing]) + * Client → Server: proof = MAC(key=ss, data="lo-auth-v1") + * Server: accept iff proof = token, where token = MAC(key=ss, data="lo-auth-v1") + * + * Security claims: + * 1. Correspondence: ServerAccepts ==> ClientResponds (Theorem 6) + * 2. Injective correspondence: each acceptance maps to a distinct client + * response (single-use, matching Tamarin's Auth_Single_Use) + * + * Reduces to: X-Wing IND-CCA2 + HMAC-SHA3-256 SUF-CMA. + * + * Decaps oracle (§8.3 compositional note): In the Tamarin model, an explicit + * DecapsOracle rule models the adversary's ability to submit arbitrary + * ciphertexts and observe MAC(Decaps(sk_IK, c), "lo-auth-v1"). In CryptoVerif, + * this is subsumed by the IND-CCA2 KEM assumption, which already provides the + * adversary with a raw decapsulation oracle returning ss directly — strictly + * more powerful than the MAC-wrapped output. The Nc parameter counts all + * client-side decapsulation queries (both legitimate responses and adversarial + * oracle use); the IND-CCA2 advantage bound P_kem(time, 1, Ns, Nc) accounts + * for all such queries. + *) + +(* Session counts *) +param Ns. (* Server challenge sessions *) +param Nc. (* Client response sessions (includes §8.3 Decaps oracle queries) *) + +(* ---------- Type declarations ---------- *) + +type kem_keyseed [large, fixed]. +type kem_pkey [bounded]. +type kem_skey [bounded]. +type kem_secret [large, fixed]. +type kem_ciphertext [bounded]. +type kem_encapoutput [bounded]. + +type macres [fixed]. +type label [fixed]. + +(* ---------- X-Wing KEM (IND-CCA2) ---------- *) + +proba P_kem. +proba P_kem_keycoll. +proba P_kem_ctxtcoll. + +expand IND_CCA2_KEM( + kem_keyseed, kem_pkey, kem_skey, + kem_secret, kem_ciphertext, kem_encapoutput, + kem_pkgen, kem_skgen, kem_encap, kem_pair, kem_decap, + injbot_kem, P_kem, P_kem_keycoll, P_kem_ctxtcoll +). + +(* ---------- HMAC-SHA3-256 as SUF-CMA deterministic MAC ---------- *) + +proba P_mac. + +expand SUF_CMA_det_mac(kem_secret, label, macres, mac_auth, mac_check, P_mac). + +const lo_auth_label: label. + +(* ---------- Events ---------- *) + +event ServerAccepts(kem_pkey, kem_ciphertext). +event ClientResponds(kem_pkey, kem_ciphertext). + +(* ---------- Security queries ---------- *) + +(* Theorem 6 (Key Possession): If the server accepts for a challenge + * ciphertext ct, then the client responded to that same ct. *) +query pk: kem_pkey, ct: kem_ciphertext; + event(ServerAccepts(pk, ct)) ==> event(ClientResponds(pk, ct)). + +(* Single-use (Tamarin: Auth_Single_Use): Each server acceptance maps to + * a distinct client response — no replay of a single client response can + * satisfy two server sessions. *) +query pk: kem_pkey, ct: kem_ciphertext; + inj-event(ServerAccepts(pk, ct)) ==> inj-event(ClientResponds(pk, ct)). + +(* ---------- Channels ---------- *) + +channel c_start, c_srv_start, c_srv_out, c_srv_recv, + c_cli_in, c_cli_out, c_pub. + +(* ---------- Server process ---------- *) + +let Server(pk_client: kem_pkey) = + foreach i_s <= Ns do + in(c_srv_start, ()); + let kem_pair(ss: kem_secret, ct: kem_ciphertext) = kem_encap(pk_client) in + let token: macres = mac_auth(lo_auth_label, ss) in + out(c_srv_out, ct); + in(c_srv_recv, p: macres); + if p = token then ( + event ServerAccepts(pk_client, ct) + ). + +(* ---------- Client process ---------- *) + +let Client(sk_client: kem_skey, pk_client: kem_pkey) = + foreach i_c <= Nc do + in(c_cli_in, ct: kem_ciphertext); + let injbot_kem(ss: kem_secret) = kem_decap(ct, sk_client) in + let tag: macres = mac_auth(lo_auth_label, ss) in + event ClientResponds(pk_client, ct); + out(c_cli_out, tag). + +(* ---------- Main process ---------- *) + +process + in(c_start, ()); + new kem_seed: kem_keyseed; + let pk_client = kem_pkgen(kem_seed) in + let sk_client = kem_skgen(kem_seed) in + out(c_pub, pk_client); + (Server(pk_client) | Client(sk_client, pk_client)) + +(* EXPECTED +All queries proved. +END *) diff --git a/cryptoverif/LO_KEX.cv b/cryptoverif/LO_KEX.cv new file mode 100644 index 0000000000..79d4ea895b --- /dev/null +++ b/cryptoverif/LO_KEX.cv @@ -0,0 +1,231 @@ +(* LO-KEX: Session Establishment (Theorems 1, 2b) + * + * Protocol (§4): + * Bob publishes bundle with σ_SPK = Sign(sk_IK_B, label ‖ pk_SPK_B) + * Alice verifies bundle, encapsulates to IK_B/SPK_B/OPK_B + * Alice signs SI: σ_SI = Sign(sk_IK_A, label ‖ SI) + * Bob verifies σ_SI, decapsulates, derives same (rk, ek) + * + * Simplifications: + * - HybridSig → single EUF-CMA scheme (§2.2: "may be treated as single") + * - Three X-Wing KEMs → three independent IND-CCA2 KEMs + * - HKDF → PRF keyed by ss_IK with (ss_SPK, ss_OPK, pks) as input + * - First-message AEAD omitted (Theorem 1 is about session key, not message) + * - σ_SPK signed by Bob's signing key (same as IK in the hybrid scheme) + * - Alice uses a SEPARATE signing key (models the distinct sk_IK_A[Ed25519+ML-DSA]) + *) + +proof { + crypto uf_cma(sigA_sign); + simplify; + success +} + +param N_A. +param N_B. + +(* ---------- Types ---------- *) + +type kem_keyseed [large, fixed]. +type kem_pkey [bounded]. +type kem_skey [bounded]. +type kem_secret [large, fixed]. +type kem_ciphertext [bounded]. +type kem_encapoutput [bounded]. + +type spk_keyseed [large, fixed]. +type spk_pkey [bounded]. +type spk_skey [bounded]. +type spk_secret [large, fixed]. +type spk_ciphertext [bounded]. +type spk_encapoutput [bounded]. + +type opk_keyseed [large, fixed]. +type opk_pkey [bounded]. +type opk_skey [bounded]. +type opk_secret [large, fixed]. +type opk_ciphertext [bounded]. +type opk_encapoutput [bounded]. + +type sig_keyseed [large, fixed]. +type sig_pkey [bounded]. +type sig_skey [bounded]. +type sig_signature [bounded]. + +type sessionkey [large, fixed]. + +(* ---------- IK KEM (IND-CCA2) ---------- *) + +proba P_kem_ik. +proba P_kem_ik_keycoll. +proba P_kem_ik_ctxtcoll. + +expand IND_CCA2_KEM( + kem_keyseed, kem_pkey, kem_skey, + kem_secret, kem_ciphertext, kem_encapoutput, + ik_pkgen, ik_skgen, ik_encap, ik_pair, ik_decap, + injbot_ik, P_kem_ik, P_kem_ik_keycoll, P_kem_ik_ctxtcoll +). + +(* ---------- SPK KEM (IND-CCA2) ---------- *) + +proba P_kem_spk. +proba P_kem_spk_keycoll. +proba P_kem_spk_ctxtcoll. + +expand IND_CCA2_KEM( + spk_keyseed, spk_pkey, spk_skey, + spk_secret, spk_ciphertext, spk_encapoutput, + spk_pkgen, spk_skgen, spk_encap, spk_pair, spk_decap, + injbot_spk, P_kem_spk, P_kem_spk_keycoll, P_kem_spk_ctxtcoll +). + +(* ---------- OPK KEM (IND-CCA2) ---------- *) + +proba P_kem_opk. +proba P_kem_opk_keycoll. +proba P_kem_opk_ctxtcoll. + +expand IND_CCA2_KEM( + opk_keyseed, opk_pkey, opk_skey, + opk_secret, opk_ciphertext, opk_encapoutput, + opk_pkgen, opk_skgen, opk_encap, opk_pair, opk_decap, + injbot_opk, P_kem_opk, P_kem_opk_keycoll, P_kem_opk_ctxtcoll +). + +(* ---------- Bob's signature (EUF-CMA) — signs SPK bundle ---------- *) + +proba P_sig_B. +proba P_sig_B_keycoll. + +expand UF_CMA_proba_signature( + sig_keyseed, sig_pkey, sig_skey, bitstring, sig_signature, + sigB_skgen, sigB_pkgen, sigB_sign, sigB_verify, + P_sig_B, P_sig_B_keycoll +). + +(* ---------- Alice's signature (EUF-CMA) — signs SessionInit ---------- *) + +type sigA_keyseed [large, fixed]. +type sigA_pkey [bounded]. +type sigA_skey [bounded]. +type sigA_signature [bounded]. + +proba P_sig_A. +proba P_sig_A_keycoll. + +expand UF_CMA_proba_signature( + sigA_keyseed, sigA_pkey, sigA_skey, bitstring, sigA_signature, + sigA_skgen, sigA_pkgen, sigA_sign, sigA_verify, + P_sig_A, P_sig_A_keycoll +). + +(* ---------- HKDF as PRF ---------- *) + +proba P_prf. + +expand PRF_large(kem_secret, bitstring, sessionkey, kdf_kex, P_prf). + +(* ---------- Domain separation constants ---------- *) + +const lo_spk_sig_label: bitstring. +const lo_kex_init_sig_label: bitstring. + +(* ---------- Events ---------- *) + +(* Events bound on the signed session init content — what the signature + * directly authenticates. rk is derived from this, but the correspondence + * is over the authenticated payload. *) +event Alice_Init(sigA_pkey, sig_pkey, kem_ciphertext, spk_ciphertext, opk_ciphertext). +event Bob_Accept(sigA_pkey, sig_pkey, kem_ciphertext, spk_ciphertext, opk_ciphertext). + +(* ---------- Security queries ---------- *) + +(* Theorem 2b: Initiator authentication — if Bob accepts SI, Alice signed it *) +query pkA: sigA_pkey, pkB: sig_pkey, + cik: kem_ciphertext, cspk: spk_ciphertext, copk: opk_ciphertext; + event(Bob_Accept(pkA, pkB, cik, cspk, copk)) + ==> event(Alice_Init(pkA, pkB, cik, cspk, copk)). + +(* Note: Injective variant not claimed — session-init replay is application-layer + * (§7.5 A4). Alice may reuse the same bundle, producing identical SI contents. + * Replay prevention is a caller obligation, not a cryptographic guarantee. *) + +(* ---------- Channels ---------- *) + +channel c_start, c_pub, c_alice_start, c_alice_out, c_bob_in. + +(* ---------- Alice (Initiator) ---------- *) + +let Alice(sk_sig_A: sigA_skey, pk_sig_A: sigA_pkey, + pk_sig_B: sig_pkey, pk_ik_B: kem_pkey, + pk_spk_B: spk_pkey, pk_opk_B: opk_pkey, + sig_spk: sig_signature) = + foreach i_a <= N_A do + in(c_alice_start, ()); + (* §4.2: Verify Bob's SPK signature *) + if sigB_verify((lo_spk_sig_label, pk_spk_B), pk_sig_B, sig_spk) = true then ( + (* §4.3 Step 2: Encapsulate to IK, SPK, OPK *) + let ik_pair(ss_ik: kem_secret, c_ik: kem_ciphertext) = ik_encap(pk_ik_B) in + let spk_pair(ss_spk: spk_secret, c_spk: spk_ciphertext) = spk_encap(pk_spk_B) in + let opk_pair(ss_opk: opk_secret, c_opk: opk_ciphertext) = opk_encap(pk_opk_B) in + (* §4.3 Step 3: Derive session key *) + let rk: sessionkey = kdf_kex(ss_ik, (ss_spk, ss_opk, pk_sig_A, pk_sig_B)) in + (* §4.3 Step 5: Sign session init *) + let si: bitstring = (pk_sig_A, pk_sig_B, c_ik, c_spk, c_opk) in + let sig_si: sigA_signature = sigA_sign((lo_kex_init_sig_label, si), sk_sig_A) in + event Alice_Init(pk_sig_A, pk_sig_B, c_ik, c_spk, c_opk); + out(c_alice_out, (si, sig_si, c_ik, c_spk, c_opk)) + ). + +(* ---------- Bob (Responder) ---------- *) + +let Bob(sk_ik_B: kem_skey, sk_spk_B: spk_skey, sk_opk_B: opk_skey, + pk_sig_A: sigA_pkey, pk_sig_B: sig_pkey) = + foreach i_b <= N_B do + in(c_bob_in, (sig_si: sigA_signature, + c_ik: kem_ciphertext, c_spk: spk_ciphertext, + c_opk: opk_ciphertext)); + (* Bob reconstructs SI from the received components *) + let si: bitstring = (pk_sig_A, pk_sig_B, c_ik, c_spk, c_opk) in + (* §4.4 Step 2: Verify Alice's signature *) + if sigA_verify((lo_kex_init_sig_label, si), pk_sig_A, sig_si) = true then ( + (* §4.4 Step 5: Decapsulate *) + let injbot_ik(ss_ik: kem_secret) = ik_decap(c_ik, sk_ik_B) in + let injbot_spk(ss_spk: spk_secret) = spk_decap(c_spk, sk_spk_B) in + let injbot_opk(ss_opk: opk_secret) = opk_decap(c_opk, sk_opk_B) in + (* §4.4 Step 7: Derive session key *) + let rk: sessionkey = kdf_kex(ss_ik, (ss_spk, ss_opk, pk_sig_A, pk_sig_B)) in + event Bob_Accept(pk_sig_A, pk_sig_B, c_ik, c_spk, c_opk) + ). + +(* ---------- Main process ---------- *) + +process + in(c_start, ()); + (* Bob: IK KEM key *) + new ik_seed: kem_keyseed; + let pk_ik_B = ik_pkgen(ik_seed) in + let sk_ik_B = ik_skgen(ik_seed) in + (* Bob: SPK *) + new spk_seed: spk_keyseed; + let pk_spk_B = spk_pkgen(spk_seed) in + let sk_spk_B = spk_skgen(spk_seed) in + (* Bob: OPK *) + new opk_seed: opk_keyseed; + let pk_opk_B = opk_pkgen(opk_seed) in + let sk_opk_B = opk_skgen(opk_seed) in + (* Bob: signing key (signs SPK bundle) *) + new sigB_seed: sig_keyseed; + let pk_sig_B = sigB_pkgen(sigB_seed) in + let sk_sig_B = sigB_skgen(sigB_seed) in + (* Alice: signing key (signs SessionInit) *) + new sigA_seed: sigA_keyseed; + let pk_sig_A = sigA_pkgen(sigA_seed) in + let sk_sig_A = sigA_skgen(sigA_seed) in + (* Bob signs SPK *) + let sig_spk: sig_signature = sigB_sign((lo_spk_sig_label, pk_spk_B), sk_sig_B) in + (* Publish everything *) + out(c_pub, (pk_ik_B, pk_spk_B, pk_opk_B, pk_sig_B, pk_sig_A, sig_spk)); + (Alice(sk_sig_A, pk_sig_A, pk_sig_B, pk_ik_B, pk_spk_B, pk_opk_B, sig_spk) + | Bob(sk_ik_B, sk_spk_B, sk_opk_B, pk_sig_A, pk_sig_B)) diff --git a/cryptoverif/LO_KEX_Secrecy.cv b/cryptoverif/LO_KEX_Secrecy.cv new file mode 100644 index 0000000000..ce34004326 --- /dev/null +++ b/cryptoverif/LO_KEX_Secrecy.cv @@ -0,0 +1,153 @@ +(* LO-KEX: Session Key Secrecy (Theorem 1) + * + * The session key (rk) is computationally indistinguishable from random + * to any adversary that has not corrupted all of Bob's keys AND Alice's RNG. + * + * Model: Alice encapsulates to Bob's IK/SPK/OPK, derives rk via HKDF-as-PRF. + * Bob decapsulates and derives the same rk. The adversary sees all public + * values (pk_IK_B, pk_SPK_B, pk_OPK_B, ciphertexts, signatures) but not + * the shared secrets or the derived key. + * + * The `secret` query tests whether rk_A (Alice's derived key) is + * indistinguishable from a uniformly random sessionkey. + * + * Reduces to: 3× IND-CCA2 KEM + HKDF PRF. + * + * Simplifications: + * - Signatures omitted: Theorem 1 (key secrecy) does not depend on + * authentication. Bundle integrity (SPK not substituted) is implicit + * in the process structure (Alice receives authentic pk_spk_B). + * - KDF info field simplified: uses (ss_spk, ss_opk, pk_ik_B) rather + * than the full spec info (pk_IK_A, pk_IK_B, pk_EK, crypto_version). + * The PRF proof holds regardless of info content. + * - X-Wing as black-box IND-CCA2: the spec (§2.1) recommends opening + * the combiner for CryptoVerif. The black-box assumption is stronger; + * the bound is in terms of P_kem rather than component advantages. + * - No corruption oracles: the proof covers the no-corruption case. + * Corruption-parameterized secrecy is verified by Tamarin (LO_KEX.spthy). + *) + +param N_A. +param N_B. + +(* ---------- Types ---------- *) + +type kem_keyseed [large, fixed]. +type kem_pkey [bounded]. +type kem_skey [bounded]. +type kem_secret [large, fixed]. +type kem_ciphertext [bounded]. +type kem_encapoutput [bounded]. + +type spk_keyseed [large, fixed]. +type spk_pkey [bounded]. +type spk_skey [bounded]. +type spk_secret [large, fixed]. +type spk_ciphertext [bounded]. +type spk_encapoutput [bounded]. + +type opk_keyseed [large, fixed]. +type opk_pkey [bounded]. +type opk_skey [bounded]. +type opk_secret [large, fixed]. +type opk_ciphertext [bounded]. +type opk_encapoutput [bounded]. + +type sessionkey [large, fixed]. + +(* ---------- Three IND-CCA2 KEMs ---------- *) + +proba P_kem_ik. +proba P_kem_ik_keycoll. +proba P_kem_ik_ctxtcoll. + +expand IND_CCA2_KEM( + kem_keyseed, kem_pkey, kem_skey, + kem_secret, kem_ciphertext, kem_encapoutput, + ik_pkgen, ik_skgen, ik_encap, ik_pair, ik_decap, + injbot_ik, P_kem_ik, P_kem_ik_keycoll, P_kem_ik_ctxtcoll +). + +proba P_kem_spk. +proba P_kem_spk_keycoll. +proba P_kem_spk_ctxtcoll. + +expand IND_CCA2_KEM( + spk_keyseed, spk_pkey, spk_skey, + spk_secret, spk_ciphertext, spk_encapoutput, + spk_pkgen, spk_skgen, spk_encap, spk_pair, spk_decap, + injbot_spk, P_kem_spk, P_kem_spk_keycoll, P_kem_spk_ctxtcoll +). + +proba P_kem_opk. +proba P_kem_opk_keycoll. +proba P_kem_opk_ctxtcoll. + +expand IND_CCA2_KEM( + opk_keyseed, opk_pkey, opk_skey, + opk_secret, opk_ciphertext, opk_encapoutput, + opk_pkgen, opk_skgen, opk_encap, opk_pair, opk_decap, + injbot_opk, P_kem_opk, P_kem_opk_keycoll, P_kem_opk_ctxtcoll +). + +(* ---------- HKDF as PRF keyed by ss_ik ---------- *) + +proba P_prf. + +expand PRF_large(kem_secret, bitstring, sessionkey, kdf_kex, P_prf). + +(* ---------- Security query ---------- *) + +(* Theorem 1: rk_A is indistinguishable from random. + * cv_onesession: secrecy for a single tested session (standard model). *) +query secret rk_A [cv_onesession]. + +(* ---------- Channels ---------- *) + +channel c_start, c_pub, c_alice_start, c_alice_out, c_bob_in, c_bob_done. + +(* ---------- Alice (Initiator) ---------- *) + +let Alice(pk_ik_B: kem_pkey, pk_spk_B: spk_pkey, pk_opk_B: opk_pkey) = + foreach i_a <= N_A do + in(c_alice_start, ()); + (* §4.3 Step 2: Encapsulate to IK, SPK, OPK *) + let ik_pair(ss_ik: kem_secret, c_ik: kem_ciphertext) = ik_encap(pk_ik_B) in + let spk_pair(ss_spk: spk_secret, c_spk: spk_ciphertext) = spk_encap(pk_spk_B) in + let opk_pair(ss_opk: opk_secret, c_opk: opk_ciphertext) = opk_encap(pk_opk_B) in + (* §4.3 Step 3: Derive session key *) + let rk_A: sessionkey = kdf_kex(ss_ik, (ss_spk, ss_opk, pk_ik_B)) in + out(c_alice_out, (c_ik, c_spk, c_opk)). + +(* ---------- Bob (Responder) ---------- *) +(* Bob decapsulates — models the CCA2 decapsulation oracle *) + +let Bob(sk_ik_B: kem_skey, sk_spk_B: spk_skey, sk_opk_B: opk_skey, + pk_ik_B: kem_pkey) = + foreach i_b <= N_B do + in(c_bob_in, (c_ik: kem_ciphertext, c_spk: spk_ciphertext, + c_opk: opk_ciphertext)); + let injbot_ik(ss_ik: kem_secret) = ik_decap(c_ik, sk_ik_B) in + let injbot_spk(ss_spk: spk_secret) = spk_decap(c_spk, sk_spk_B) in + let injbot_opk(ss_opk: opk_secret) = opk_decap(c_opk, sk_opk_B) in + let rk_B: sessionkey = kdf_kex(ss_ik, (ss_spk, ss_opk, pk_ik_B)) in + out(c_bob_done, ()). + +(* ---------- Main process ---------- *) + +process + in(c_start, ()); + (* Bob's KEM keys *) + new ik_seed: kem_keyseed; + let pk_ik_B = ik_pkgen(ik_seed) in + let sk_ik_B = ik_skgen(ik_seed) in + new spk_seed: spk_keyseed; + let pk_spk_B = spk_pkgen(spk_seed) in + let sk_spk_B = spk_skgen(spk_seed) in + new opk_seed: opk_keyseed; + let pk_opk_B = opk_pkgen(opk_seed) in + let sk_opk_B = opk_skgen(opk_seed) in + (* Publish public keys *) + out(c_pub, (pk_ik_B, pk_spk_B, pk_opk_B)); + (Alice(pk_ik_B, pk_spk_B, pk_opk_B) + | Bob(sk_ik_B, sk_spk_B, sk_opk_B, pk_ik_B)) diff --git a/cryptoverif/LO_Ratchet_MsgSecrecy.cv b/cryptoverif/LO_Ratchet_MsgSecrecy.cv new file mode 100644 index 0000000000..3e7c813045 --- /dev/null +++ b/cryptoverif/LO_Ratchet_MsgSecrecy.cv @@ -0,0 +1,44 @@ +(* LO-Ratchet: Message Key Secrecy (Theorem 3) + * + * Given a fresh epoch key ek (from Theorem 1 + KDF_Root), proves that + * message keys mk = KDF_MsgKey(ek, counter) are indistinguishable from + * random. Combined with AEAD security under random keys (standard + * composition via [BN00]), this gives full message secrecy. + * + * Reduces to: HMAC-SHA3-256 PRF. + *) + +param N_msg. + +(* ---------- Types ---------- *) + +type epoch_key [large, fixed]. +type msg_key [large, fixed]. +type counter [fixed]. + +(* ---------- KDF_MsgKey as PRF ---------- *) + +proba P_prf. + +expand PRF_large(epoch_key, counter, msg_key, kdf_msgkey, P_prf). + +(* ---------- Security query ---------- *) + +query secret test_mk [cv_onesession]. + +(* ---------- Channels ---------- *) + +channel c_start, c_ready, c_test_in, c_test_out. + +(* ---------- Process ---------- *) +(* Single derivation: ek is fresh, derive mk at one counter. + * The PRF transformation replaces kdf_msgkey(ek, ctr) with a random value. + * No oracle needed — the PRF_large game handles multi-query internally. *) + +process + in(c_start, ()); + new ek: epoch_key; + out(c_ready, ()); + in(c_test_in, ctr: counter); + let test_mk: msg_key = kdf_msgkey(ek, ctr) in + out(c_test_out, ()) diff --git a/cryptoverif/LO_Stream_Secrecy.cv b/cryptoverif/LO_Stream_Secrecy.cv new file mode 100644 index 0000000000..0aa108f37e --- /dev/null +++ b/cryptoverif/LO_Stream_Secrecy.cv @@ -0,0 +1,116 @@ +(* LO-Stream: Chunk Confidentiality + Integrity (Theorem 13, P1+P2) + * + * Adapted from CryptoVerif's TLS 1.3 Record Protocol example. + * + * IND-CPA: Bit-guessing game — adversary submits two equal-length plaintexts, + * receives encryption of one based on secret bit b0. Advantage = Pr[guess b0]. + * + * INT-CTXT: Injective correspondence — if decryption succeeds at (count, msg), + * encryption must have produced (count, msg). + * + * Nonce uniqueness enforced via table lookup (nonce-respecting adversary, §9.11(f)). + * Nonce derivation: chunk_nonce = xor(base_nonce, count) with injectivity equation. + * + * Reduces to: XChaCha20-Poly1305 IND-CPA + INT-CTXT. + *) + +type key [fixed, large]. +type seqn [fixed]. +type nonce_t [fixed, large]. +type add_data [bounded]. + +param N_enc, N_dec. + +(* ---------- Nonce derivation with injectivity ---------- *) +(* §15.2: chunk_nonce = base_nonce XOR mask(index, tag_byte) + * Modeled as xor(iv, count) per TLS 1.3 record protocol pattern. + * CryptoVerif needs the explicit injectivity equation. *) + +fun xor(key, seqn): nonce_t. + +equation forall k: key, n: seqn, n': seqn; + (xor(k, n) = xor(k, n')) = (n = n'). + +(* ---------- AEAD (IND-CPA + INT-CTXT under unique nonces) ---------- *) + +proba P_cpa. +proba P_ctxt. + +expand AEAD_nonce(key, bitstring, bitstring, add_data, nonce_t, + enc, dec, injbot, Z, P_cpa, P_ctxt). + +(* Per-chunk AAD includes base_nonce + count (§15.4) *) +fun derive_aad(key, seqn): add_data [data]. + +letfun stream_encrypt(k: key, n: nonce_t, m: bitstring, aad: add_data) = + enc(m, aad, k, n). +letfun stream_decrypt(k: key, n: nonce_t, c: bitstring, aad: add_data) = + dec(c, aad, k, n). + +(* ---------- Tables for nonce uniqueness (§9.11(f) game hypothesis) ---------- *) + +table table_enc_nonce(seqn). +table table_dec_nonce(seqn). + +(* ---------- Security queries ---------- *) + +(* P1 (IND-CPA): secret bit indistinguishable *) +query secret b0 [cv_bit]. + +(* P2 (INT-CTXT): injective correspondence *) +event Sent(seqn, bitstring). +event Received(seqn, bitstring). + +query count: seqn, msg: bitstring; + inj-event(Received(count, msg)) ==> inj-event(Sent(count, msg)) + public_vars b0. + +(* ---------- Channels ---------- *) + +channel c_start, c_ready, c_enc_in, c_enc_out, c_dec_in, c_dec_out. + +(* ---------- Encrypt oracle ---------- *) +(* Adversary submits (m0, m1, count). Oracle encrypts m_b where b = b0. + * Count must not have been used before (nonce-respecting). *) + +let Encrypt(k: key, iv: key, b: bool) = + !N_enc + in(c_enc_in, (clear1: bitstring, clear2: bitstring, count: seqn)); + (* Nonce-respecting: reject reused counter *) + get table_enc_nonce(=count) in yield else + insert table_enc_nonce(count); + (* Equal-length requirement for IND-CPA *) + if Z(clear1) = Z(clear2) then + let clear = if_fun(b, clear1, clear2) in + let aad: add_data = derive_aad(iv, count) in + let nonce = xor(iv, count) in + event Sent(count, clear); + let cipher = stream_encrypt(k, nonce, clear, aad) in + out(c_enc_out, cipher). + +(* ---------- Decrypt oracle ---------- *) +(* Adversary submits (ciphertext, count). Must not reuse count. *) + +let Decrypt(k: key, iv: key) = + !N_dec + in(c_dec_in, (cipher: bitstring, count: seqn)); + get table_dec_nonce(=count) in yield else + insert table_dec_nonce(count); + let aad: add_data = derive_aad(iv, count) in + let nonce = xor(iv, count) in + let injbot(clear) = stream_decrypt(k, nonce, cipher, aad) in + event Received(count, clear). + +(* ---------- Main process ---------- *) + +process + in(c_start, ()); + new b0: bool; + new k: key; + new iv: key; (* base_nonce — public *) + out(c_ready, iv); + (Encrypt(k, iv, b0) | Decrypt(k, iv)) + +(* EXPECTED +All queries proved. +END *) diff --git a/cryptoverif/README.md b/cryptoverif/README.md new file mode 100644 index 0000000000..3730a97f50 --- /dev/null +++ b/cryptoverif/README.md @@ -0,0 +1,112 @@ +# 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 | diff --git a/tamarin/LO_AntiReflection.spthy b/tamarin/LO_AntiReflection.spthy new file mode 100644 index 0000000000..b845c829a2 --- /dev/null +++ b/tamarin/LO_AntiReflection.spthy @@ -0,0 +1,108 @@ +theory LO_AntiReflection +begin + +/* + * LO-Ratchet Anti-Reflection (Theorem 12) + * ======================================== + * + * A message encrypted by A for B cannot be reflected back to A as if + * it were from B. The AAD uses direction-dependent fingerprint ordering: + * A→B: AAD = "lo-dm-v1" ‖ fp_A ‖ fp_B ‖ Encode(H) + * B→A: AAD = "lo-dm-v1" ‖ fp_B ‖ fp_A ‖ Encode(H) + * + * Since fp_A ≠ fp_B (invariant h), the AAD differs between directions, + * and AEAD tag verification fails on reflected messages. + * + * §9.9 known pitfall: a model using canonical (sorted) fingerprint + * ordering would NOT detect reflection — the AAD would be identical + * in both directions. This model preserves sender-first ordering. + * + * EXPECTED RESULTS: + * Reflection_Sanity: VERIFIED + * Theorem12_Anti_Reflection: VERIFIED + */ + +builtins: hashing + +// AEAD abstraction +functions: aead_enc/4, aead_verify/4, accept/0 +equations: + aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept() + +// Constant-time equality +restriction Eq: + "All x y #i. Eq(x,y) @i ==> x = y" + +// §5.1 invariant (h): local_fp ≠ remote_fp +restriction Neq: + "All x y #i. Neq(x,y) @i ==> not (x = y)" + + +/* ================= SESSION SETUP ================= */ + +rule Session_Setup: + [ Fr(~mk), Fr(~n) ] + --[ SessionSetup($A, $B, ~mk), + Neq($A, $B) ]-> + [ !SessionKey($A, $B, ~mk), + SendState($A, $B, ~mk, ~n) ] + + +/* ================= SEND / RECEIVE (sender-first AAD ordering) ================= */ + +// A encrypts a message for B +// AAD = fp_sender ‖ fp_recipient ‖ header +rule Send_A_to_B: + let + aad = <'lo-dm-v1', $A, $B, ~header> + c = aead_enc(mk, n, ~m, aad) + in + [ SendState($A, $B, mk, n), Fr(~m), Fr(~header) ] + --[ Sent($A, $B, c, n) ]-> + [ Out() ] + +// B decrypts a message from A +// B reconstructs AAD with sender=A, recipient=B +rule Recv_B_from_A: + let + aad = <'lo-dm-v1', $A, $B, header> + in + [ !SessionKey($A, $B, mk), In() ] + --[ Eq(aead_verify(mk, n, aad, c), accept()), + Received($B, $A, c) ]-> + [ ] + +// A decrypts a "message from B" (potential reflection target) +// A reconstructs AAD with sender=B, recipient=A — REVERSED order +rule Recv_A_from_B: + let + aad = <'lo-dm-v1', $B, $A, header> + in + [ !SessionKey($A, $B, mk), In() ] + --[ Eq(aead_verify(mk, n, aad, c), accept()), + Received($A, $B, c) ]-> + [ ] + + +/* ================= LEMMAS ================= */ + +// Sanity: honest A→B message exchange works +lemma Reflection_Sanity: + exists-trace + "Ex A B c n #i #j. + Sent(A, B, c, n) @i & + Received(B, A, c) @j" + +// Theorem 12: A message sent by A→B cannot be accepted by A as B→A. +// The adversary captures A's ciphertext and replays it to A's receive +// rule. AEAD verification fails because the AAD differs: +// Sent: AAD = <"lo-dm-v1", A, B, header> +// Received: AAD = <"lo-dm-v1", B, A, header> +// Since A ≠ B (invariant h), these are distinct terms. +lemma Theorem12_Anti_Reflection: + "All A B c n #i #j. + Sent(A, B, c, n) @i & + Received(A, B, c) @j + ==> F" + +end diff --git a/tamarin/LO_Auth.spthy b/tamarin/LO_Auth.spthy new file mode 100644 index 0000000000..b2ae364856 --- /dev/null +++ b/tamarin/LO_Auth.spthy @@ -0,0 +1,189 @@ +theory LO_Auth +begin + +/* + * 1. CRYPTOGRAPHIC PRIMITIVES (Abstracted per §2) + */ + +builtins: signing, hashing + +// Hybrid KEM (X-Wing) abstraction per §2.1 +// We treat it as a single IND-CCA2 KEM. +// kem_decaps recovers the encapsulation randomness r (a subterm of the +// ciphertext), and both sides derive the shared secret via kem_ss(pk, r). +// This formulation is subterm-convergent: the RHS `r` is a subterm of the LHS. +functions: kem_pk/1, kem_c/2, kem_ss/2, kem_decaps/2 +equations: kem_decaps(sk, kem_c(kem_pk(sk), r)) = r + +// MAC (HMAC-SHA3-256) per §2.3 +// Modeled as an opaque function. +functions: mac/2 + +// Constant-time equality check helper +restriction Eq: + "All x y #i. Eq(x,y) @i ==> x = y" + +/* + * 2. ADVERSARY MODEL & PKI (§8.2) + */ + +// Generate Identity Keys (IK) +rule Generate_IK: + [ Fr(~sk_IK) ] + --[ LtkGen($P, ~sk_IK) ]->[ !Ltk($P, ~sk_IK), !Pk($P, kem_pk(~sk_IK)), Out(kem_pk(~sk_IK)) ] + +// Corrupt IK (§8.2: Corrupt(IK, P)) +rule Corrupt_IK:[ !Ltk($P, sk_IK) ] + --[ CorruptIK($P) ]->[ Out(sk_IK) ] + +// Corrupt RNG (§8.2: Corrupt(RNG, P, t)) +// We model this by allowing the adversary to learn the randomness `~r` used in a specific step. +rule Corrupt_RNG: + [ !RNG_State($P, ~r) ] + --[ CorruptRNG($P, ~r) ]-> + [ Out(~r) ] + +/* + * 3. LO-Auth PROTOCOL (§6) + */ + +// Server -> Client: Challenge +rule LO_Auth_Challenge: + let + c = kem_c(pk_IK_client, ~r) + ss = kem_ss(pk_IK_client, ~r) + token = mac(ss, 'lo-auth-v1') + in[ !Pk($Client, pk_IK_client), Fr(~r) ] + --[ + AuthChallenge($Server, $Client, ~r, token) + ]->[ + Out( c ), + // §8.3: Linear fact to enforce single-use challenge + AuthPending($Server, $Client, token), + // Expose RNG state for potential corruption + !RNG_State($Server, ~r) + ] + +// Client -> Server: Proof Generation +rule LO_Auth_Client_Response: + let + r = kem_decaps(sk_IK_client, c) + ss = kem_ss(kem_pk(sk_IK_client), r) + proof = mac(ss, 'lo-auth-v1') + in[ !Ltk($Client, sk_IK_client), In( c ) ] + --[ + AuthResponse($Client, c, proof) + ]-> + [ + Out( proof ) + ] + +// Server: Verify +// Consumes AuthPending ensuring the challenge cannot be replayed successfully +rule LO_Auth_Verify_Success: + [ AuthPending($Server, $Client, token), In( proof ) ] + --[ + Eq(token, proof), // Represents constant-time accept + AuthAccepted($Server, $Client, token) + ]-> + [ ] + +// (Optional) Server: Timeout +// §8.3: AuthTimeout consumes the pending state without producing AuthAccepted +rule LO_Auth_Timeout:[ AuthPending($Server, $Client, token) ] + --[ AuthTimeout($Server, $Client, token) ]-> + [ ] + +/* + * 3b. CCA2 DECAPSULATION ORACLE (§8.3 compositional note) + * + * In the composed setting where LO-Auth and LO-KEX share sk_IK[XWing], + * each LO-Auth session gives the adversary an interactive Decaps oracle: + * submit arbitrary c, receive MAC(Decaps(sk_IK, c), 'lo-auth-v1'). + * This accounts for the CCA2 queries in Theorem 1's advantage bound. + */ +// kem_decaps returns r (subterm-convergent), then kem_ss(pk, r) gives ss. +rule LO_Auth_Decaps_Oracle: + let + r_adv = kem_decaps(sk_IK_client, c_adv) + ss_adv = kem_ss(kem_pk(sk_IK_client), r_adv) + in + [ !Ltk($Client, sk_IK_client), In( c_adv ) ] + --[ DecapsOracle($Client, c_adv) ]-> + [ Out( mac(ss_adv, 'lo-auth-v1') ) ] + + +/* + * 4. LEMMAS (§8.6) + */ + +// Sanity: Can the protocol run to completion? +lemma Auth_Exists: + exists-trace + "Ex S C token #i. AuthAccepted(S, C, token) @ i" + +// Sanity: Challenge temporally precedes acceptance. +lemma Auth_Ordering: + "All S C r token #chal #verify. + AuthChallenge(S, C, r, token) @ chal & + AuthAccepted(S, C, token) @ verify + ==> + chal < verify + " + +// §8.3 single-use: AuthPending is linear, so a given token is accepted at most once. +lemma Auth_Single_Use: + "All S C token #i #j. + AuthAccepted(S, C, token) @ i & + AuthAccepted(S, C, token) @ j + ==> + #i = #j + " + +// §8.3: If the challenge timed out, acceptance is impossible (AuthPending was consumed). +lemma Auth_No_Accept_After_Timeout: + "All S C token #t #a. + AuthTimeout(S, C, token) @ t & + AuthAccepted(S, C, token) @ a + ==> + F + " + +// Each Fr(~r) is unique, so distinct challenges produce distinct tokens. +lemma Auth_Unique_Challenge: + "All S1 S2 C1 C2 r token1 token2 #i #j. + AuthChallenge(S1, C1, r, token1) @ i & + AuthChallenge(S2, C2, r, token2) @ j + ==> + #i = #j + " + +// Theorem 6 (LO-Auth Key Possession): +// If the server accepts, then either the adversary corrupted the client's IK, +// corrupted the server's RNG for this challenge, used the Decaps oracle +// (which yields a valid MAC for any ciphertext), or the client responded. +lemma Theorem6_Key_Possession: + "All S C r token #chal #verify. + AuthChallenge(S, C, r, token) @ chal & + AuthAccepted(S, C, token) @ verify + ==> + (Ex #j. CorruptIK(C) @ j) | + (Ex #j. CorruptRNG(S, r) @ j) | + (Ex c_adv #j. DecapsOracle(C, c_adv) @ j) | + (Ex c #resp. AuthResponse(C, c, token) @ resp) + " + +// Theorem 6, strengthened: under an honest client, honest RNG, and no +// oracle use, the adversary cannot forge a proof. +lemma Theorem6_No_Oracle: + "All S C r token #chal #verify. + AuthChallenge(S, C, r, token) @ chal & + AuthAccepted(S, C, token) @ verify & + not (Ex #j. CorruptIK(C) @ j) & + not (Ex #j. CorruptRNG(S, r) @ j) & + not (Ex c_adv #j. DecapsOracle(C, c_adv) @ j) + ==> + (Ex c #resp. AuthResponse(C, c, token) @ resp) + " + +end \ No newline at end of file diff --git a/tamarin/LO_Call.spthy b/tamarin/LO_Call.spthy new file mode 100644 index 0000000000..9b7f7c4a9d --- /dev/null +++ b/tamarin/LO_Call.spthy @@ -0,0 +1,214 @@ +theory LO_Call +begin + +/* + * LO-Call: Call Key Derivation (Theorems 8-11) + * ============================================= + * + * Models call setup (§5.7). Signaling messages (call_id, pk_eph, c_eph) + * are delivered via authenticated channel (direct facts), modeling the + * INT-CTXT guarantee from Theorem 3 — the adversary can observe (Out) + * but cannot modify signaling in transit. + * + * EXPECTED RESULTS: + * Call_Exists: VERIFIED + * Call_Key_Agreement: VERIFIED + * Theorem8_Call_Key_Secrecy: VERIFIED + * Theorem9_Intra_Call_FS: VERIFIED + * Theorem10_Call_Ratchet_Ind: VERIFIED + * Theorem11_Concurrent_Ind: VERIFIED + */ + +builtins: hashing + +// X-Wing KEM (subterm-convergent) +functions: kem_pk/1, kem_c/2, kem_ss/2, kem_decaps/2 +equations: kem_decaps(sk, kem_c(kem_pk(sk), r)) = r + +// KDF_Call: (key_a, key_b, ck_call) from (rk, ss_eph, call_id) +functions: kdf_call_a/3, kdf_call_b/3, kdf_call_ck/3 + +// KDF_CallChain: one-way chain advance +functions: chain_a/1, chain_b/1, chain_ck/1 + + +/* ================= SESSION (abstracted from LO-KEX) ================= */ + +// §5.1 invariant (h): local_fp ≠ remote_fp (self-messaging rejected) +restriction No_Self_Session: + "All I R rk #i. SessionEstablished(I, R, rk) @i ==> not (I = R)" + +rule Establish_Session: + [ Fr(~rk) ] + --[ SessionEstablished($I, $R, ~rk) ]-> + [ !SessionRK($I, $R, ~rk) ] + + +/* ================= CORRUPTION ================= */ + +rule Corrupt_RatchetState: + [ !SessionRK($I, $R, rk) ] + --[ CorruptRatchet($I, $R) ]-> + [ Out(rk) ] + +rule Corrupt_RNG: + [ !RNG_Call($P, r) ] + --[ CorruptRNG($P, r) ]-> + [ Out(r) ] + +// Corrupt current call state — linear, consumes the state. +// Per §8.2: reveals CURRENT (key_a, key_b, ck_call), not initial. +rule Corrupt_CallState: + [ CallState($P, call_id, key_a, key_b, ck, step) ] + --[ CorruptCall($P, call_id, key_a, key_b, ck) ]-> + [ Out() ] + + +/* ================= LO-CALL PROTOCOL (§5.7) ================= */ + +// Step 1: Initiator generates call_id, ephemeral keypair +// Sends (call_id, pk_eph) via authenticated channel (CallOffer fact) +rule Call_Initiate: + let pk_eph = kem_pk(~sk_eph) + in + [ !SessionRK($I, $R, rk), Fr(~call_id), Fr(~sk_eph) ] + --[ CallInitiate($I, $R, ~call_id) ]-> + [ CallPending($I, $R, rk, ~call_id, ~sk_eph), + CallOffer($I, $R, ~call_id, pk_eph, rk), + Out(<~call_id, pk_eph>), + !RNG_Call($I, ~sk_eph) ] + +// Step 2: Peer encapsulates to pk_eph, derives call keys +// Receives via authenticated channel; sends c_eph back via CallAnswer. +rule Call_Respond: + let + c_eph = kem_c(pk_eph, ~r_eph) + ss_eph = kem_ss(pk_eph, ~r_eph) + key_a = kdf_call_a(rk, ss_eph, call_id) + key_b = kdf_call_b(rk, ss_eph, call_id) + ck = kdf_call_ck(rk, ss_eph, call_id) + in + [ !SessionRK($I, $R, rk), + CallOffer($I, $R, call_id, pk_eph, rk), + Fr(~r_eph) ] + --[ CallDerived($R, $I, call_id, key_a, key_b, ck) ]-> + [ CallAnswer($I, $R, call_id, c_eph), + CallState($R, call_id, key_a, key_b, ck, '0'), + Out(c_eph), + !RNG_Call($R, ~r_eph) ] + +// Step 3: Initiator decapsulates, derives call keys +rule Call_Complete: + let + r_eph = kem_decaps(sk_eph, c_eph) + ss_eph = kem_ss(kem_pk(sk_eph), r_eph) + key_a = kdf_call_a(rk, ss_eph, call_id) + key_b = kdf_call_b(rk, ss_eph, call_id) + ck = kdf_call_ck(rk, ss_eph, call_id) + in + [ CallPending($I, $R, rk, call_id, sk_eph), + CallAnswer($I, $R, call_id, c_eph) ] + --[ CallDerived($I, $R, call_id, key_a, key_b, ck) ]-> + [ CallState($I, call_id, key_a, key_b, ck, '0') ] + + +/* ================= INTRA-CALL REKEYING (§5.7) ================= */ + +// Chain advance: linear CallState consumed, new state produced. +// Old keys are zeroized (consumed by the linear fact mechanism). +// Bounded to 3 steps to prevent Tamarin non-termination. + +rule Chain_Bounds: + [ ] --> [ !CB('0', '1'), !CB('1', '2'), !CB('2', '3') ] + +rule Call_Chain_Step: + let + key_a_new = chain_a(ck) + key_b_new = chain_b(ck) + ck_new = chain_ck(ck) + in + [ CallState($P, call_id, key_a, key_b, ck, step), !CB(step, next_step) ] + --[ ChainAdvance($P, call_id, ck, ck_new, step) ]-> + [ CallState($P, call_id, key_a_new, key_b_new, ck_new, next_step) ] + + +/* ================= LEMMAS ================= */ + +// Sanity: full call setup can complete +lemma Call_Exists: + exists-trace + "Ex I R cid ka kb ck #i #j. + CallDerived(I, R, cid, ka, kb, ck) @i & + CallDerived(R, I, cid, ka, kb, ck) @j" + +// Key agreement: both parties derive the same keys (under authenticated signaling) +lemma Call_Key_Agreement: + "All I R cid ka1 kb1 ck1 ka2 kb2 ck2 #i #j. + CallDerived(I, R, cid, ka1, kb1, ck1) @i & + CallDerived(R, I, cid, ka2, kb2, ck2) @j + ==> + ka1 = ka2 & kb1 = kb2 & ck1 = ck2 + " + +// Theorem 8 (Call Key Secrecy): key_a is secret unless: +// - call state directly corrupted, OR +// - ratchet state (rk) AND ephemeral RNG (ss_eph) both compromised +lemma Theorem8_Call_Key_Secrecy: + "All P Q cid ka kb ck #i. + CallDerived(P, Q, cid, ka, kb, ck) @i + ==> + not (Ex #j. K(ka) @j) + | (Ex ka2 kb2 ck2 #j. CorruptCall(P, cid, ka2, kb2, ck2) @j) + | (Ex ka2 kb2 ck2 #j. CorruptCall(Q, cid, ka2, kb2, ck2) @j) + | (Ex r #j1 #j2. CorruptRatchet(P, Q) @j1 & CorruptRNG(P, r) @j2) + | (Ex r #j1 #j2. CorruptRatchet(P, Q) @j1 & CorruptRNG(Q, r) @j2) + | (Ex r #j1 #j2. CorruptRatchet(Q, P) @j1 & CorruptRNG(P, r) @j2) + | (Ex r #j1 #j2. CorruptRatchet(Q, P) @j1 & CorruptRNG(Q, r) @j2) + " + +// Theorem 9 (Intra-Call FS): After chain advance, corruption of P's later +// chain state does not reveal P's prior chain keys. +// Preconditions: +// - Call keys are fresh (no ratchet/RNG corruption) per Theorem 8 +// - Only P's call state is corrupted (the other party Q is not corrupted +// for this call_id — Q may still hold ck_old in their unadvanced state) +// chain_ck is one-way: knowing ck_new = chain_ck(ck_old) does not yield ck_old. +lemma Theorem9_Intra_Call_FS: + "All P cid ck_old ck_new step ka kb ck_cur #adv #c. + ChainAdvance(P, cid, ck_old, ck_new, step) @adv & + CorruptCall(P, cid, ka, kb, ck_cur) @c & + adv < c & + not (Ex A B #j. CorruptRatchet(A, B) @j) & + not (Ex Q r #j. CorruptRNG(Q, r) @j) & + (All Q ka2 kb2 ck2 #j. CorruptCall(Q, cid, ka2, kb2, ck2) @j ==> Q = P) + ==> not (Ex #r. K(ck_old) @r)" + +// Theorem 10 (Call/Ratchet Independence): corrupting call keys does not +// reveal the root key. rk is secret unless ratchet state is corrupted. +lemma Theorem10_Call_Ratchet_Ind: + "All I R rk #i. + SessionEstablished(I, R, rk) @i + ==> + not (Ex #j. K(rk) @j) + | (Ex #j. CorruptRatchet(I, R) @j) + | (Ex #j. CorruptRatchet(R, I) @j) + " + +// Theorem 11 (Concurrent Call Independence): corrupting one call does +// not reveal keys from a concurrent call with a different call_id. +lemma Theorem11_Concurrent_Ind: + "All P Q cid1 cid2 ka1 kb1 ck1 ka2 kb2 ck2 #i #j. + CallDerived(P, Q, cid1, ka1, kb1, ck1) @i & + CallDerived(P, Q, cid2, ka2, kb2, ck2) @j & + not (cid1 = cid2) + ==> + not (Ex #k. K(ka2) @k) + | (Ex ka kb ck #k. CorruptCall(P, cid2, ka, kb, ck) @k) + | (Ex ka kb ck #k. CorruptCall(Q, cid2, ka, kb, ck) @k) + | (Ex r #j1 #j2. CorruptRatchet(P, Q) @j1 & CorruptRNG(P, r) @j2) + | (Ex r #j1 #j2. CorruptRatchet(P, Q) @j1 & CorruptRNG(Q, r) @j2) + | (Ex r #j1 #j2. CorruptRatchet(Q, P) @j1 & CorruptRNG(P, r) @j2) + | (Ex r #j1 #j2. CorruptRatchet(Q, P) @j1 & CorruptRNG(Q, r) @j2) + " + +end diff --git a/tamarin/LO_KEX.spthy b/tamarin/LO_KEX.spthy new file mode 100644 index 0000000000..d4f68c9b73 --- /dev/null +++ b/tamarin/LO_KEX.spthy @@ -0,0 +1,266 @@ +theory LO_KEX +begin + +/* + * LO-KEX: Session Establishment (Theorems 1, 2a, 2b) + * + * SCOPE: This model covers the OPK-PRESENT case only. All three KEM + * encapsulations (IK, SPK, OPK) are unconditional. + * + * The code (kex/mod.rs) supports OPK-absent sessions where IKM = ss_IK ‖ ss_SPK + * (2 shared secrets instead of 3). For those sessions, corruption of IK + SPK + * alone suffices to derive the session key — the Theorem 1 lemmas' requirement + * of all-three-corrupted does not apply. The OPK-absent case has strictly + * weaker security (2-key threshold vs 3-key) and is not modeled here. + * + * This is NOT a soundness issue: the proofs are correct for the OPK-present + * case they model. The OPK-absent case would need separate rules with 2-KEM + * IKM and adjusted secrecy lemmas requiring only IK+SPK corruption. + */ + +/* + * 1. CRYPTOGRAPHIC PRIMITIVES + */ +builtins: asymmetric-encryption, signing, hashing + +// AEAD Abstraction +functions: aead_enc/4, aead_dec/4, aead_verify/4, accept/0 +equations: + aead_dec(k, n, aad, aead_enc(k, n, m, aad)) = m, + aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept() + +// Constant-time equality check helper +restriction Eq: + "All x y #i. Eq(x,y) @i ==> x = y" + +/* + * 2. ADVERSARY MODEL & PKI (§8.2) + */ + +rule Generate_IK: + [ Fr(~sk) ] --[ LtkGen($P, ~sk) ]->[ !Ltk($P, ~sk), !Pk($P, pk(~sk)), Out(pk(~sk)) ] + +rule Corrupt_IK: + [ !Ltk($P, sk) ] --[ CorruptIK($P) ]-> [ Out(sk) ] + +rule Corrupt_SPK: + [ !SPK_Secret($P, id, sk) ] --[ CorruptSPK($P, id) ]-> [ Out(sk) ] + +rule Corrupt_OPK:[ !OPK_Secret($P, id, sk) ] --[ CorruptOPK($P, id) ]-> [ Out(sk) ] + +rule Corrupt_RNG_KEX:[ !RNG_KEX($P, r_IK, r_SPK, r_OPK) ] --[ CorruptRNG_KEX($P) ]->[ Out() ] + + +/* + * 3. LO-KEX PROTOCOL (§4) + */ + +// §4.1: Pre-Key Bundle Generation (Bob) +rule LO_KEX_Publish_Bundle: + let + pk_SPK = pk(~sk_SPK) + pk_OPK = pk(~sk_OPK) + pk_IK = pk(~sk_IK) + sig_SPK = sign(<'lo-spk-sig-v1', pk_SPK>, ~sk_IK) + bundle = <'lo-crypto-v1', pk_IK, pk_SPK, ~id_SPK, sig_SPK, pk_OPK, ~id_OPK> + in[ !Ltk($B, ~sk_IK), Fr(~sk_SPK), Fr(~sk_OPK), Fr(~id_SPK), Fr(~id_OPK) ] + --[ PublishBundle($B, ~id_SPK, ~id_OPK) ]->[ + !SPK_Secret($B, ~id_SPK, ~sk_SPK), !SPK_Pk($B, ~id_SPK, pk_SPK), + !OPK_Secret($B, ~id_OPK, ~sk_OPK), !OPK_Pk($B, ~id_OPK, pk_OPK), + // OPK_Available is a LINEAR fact per §4.4 Step 6 + OPK_Available($B, ~id_OPK), + Out(bundle) + ] + +// §4.3: Session Initiation (Alice) +rule LO_KEX_Alice_Init: + let + pk_IK_A = pk(~sk_IK_A) + + // KEM using standard PKE (ss = ~r, c = aenc(~r, pk)) + c_IK = aenc(~r_IK, pk_IK_B) + ss_IK = ~r_IK + + c_SPK = aenc(~r_SPK, pk_SPK_B) + ss_SPK = ~r_SPK + + c_OPK = aenc(~r_OPK, pk_OPK_B) + ss_OPK = ~r_OPK + + // HKDF derivation using built-in hashing + ikm = + pk_EK = pk(~sk_EK) + info = <'lo-kex-v1', 'lo-crypto-v1', pk_IK_A, pk_IK_B, pk_EK> + + rk = h() + ek = h() + + fp_IK_A = h(pk_IK_A) + fp_IK_B = h(pk_IK_B) + SI = <'lo-crypto-v1', fp_IK_A, fp_IK_B, pk_EK, c_IK, c_SPK, id_SPK, c_OPK, id_OPK> + sig_SI = sign(<'lo-kex-init-sig-v1', SI>, ~sk_IK_A) + + mk0 = h() + aad0 = <'lo-dm-v1', fp_IK_A, fp_IK_B, SI> + c0 = aead_enc(mk0, ~n0, ~m0, aad0) + in[ + !Ltk($A, ~sk_IK_A), + !Pk($B, pk_IK_B), + !SPK_Pk($B, id_SPK, pk_SPK_B), + !OPK_Pk($B, id_OPK, pk_OPK_B), + In(sig_SPK), + Fr(~sk_EK), Fr(~r_IK), Fr(~r_SPK), Fr(~r_OPK), Fr(~n0), Fr(~m0) + ] + --[ + Eq(verify(sig_SPK, <'lo-spk-sig-v1', pk_SPK_B>, pk_IK_B), true), + Init_A($A, $B, rk, ek, id_SPK, id_OPK) + ]->[ + Out(), + !RNG_KEX($A, ~r_IK, ~r_SPK, ~r_OPK) + ] + +// §4.4: Session Reception (Bob) +rule LO_KEX_Bob_Recv: + let + pk_IK_B = pk(~sk_IK_B) + pk_SPK_B = pk(~sk_SPK_B) + pk_OPK_B = pk(~sk_OPK_B) + + fp_IK_A = h(pk_IK_A) + fp_IK_B = h(pk_IK_B) + SI = <'lo-crypto-v1', fp_IK_A, fp_IK_B, pk_EK, c_IK, c_SPK, id_SPK, c_OPK, id_OPK> + + // Decapsulate + ss_IK = adec(c_IK, ~sk_IK_B) + ss_SPK = adec(c_SPK, ~sk_SPK_B) + ss_OPK = adec(c_OPK, ~sk_OPK_B) + + // HKDF derivation using built-in hashing + ikm = + info = <'lo-kex-v1', 'lo-crypto-v1', pk_IK_A, pk_IK_B, pk_EK> + + rk = h() + ek = h() + + mk0 = h() + aad0 = <'lo-dm-v1', fp_IK_A, fp_IK_B, SI> + in[ + !Ltk($B, ~sk_IK_B), + !Pk($A, pk_IK_A), + !SPK_Secret($B, id_SPK, ~sk_SPK_B), + !OPK_Secret($B, id_OPK, ~sk_OPK_B), + OPK_Available($B, id_OPK), + In() + ] + --[ + Eq(verify(sig_SI, <'lo-kex-init-sig-v1', SI>, pk_IK_A), true), + Eq(aead_verify(mk0, n0, aad0, c0), accept()), + Init_B($B, $A, rk, ek, id_SPK, id_OPK) + ]-> + [ ] + +/* + * 4. LEMMAS (§8.6) + */ + +// Sanity check +lemma KEX_Exists: + exists-trace + "Ex A B rk ek id_S id_O #i #j. + Init_A(A, B, rk, ek, id_S, id_O) @ i & + Init_B(B, A, rk, ek, id_S, id_O) @ j" + +// Theorem 1 (A's perspective): Session Key Secrecy +// The root key is secret UNLESS Adv corrupts Alice's RNG, OR ALL of Bob's keys. +lemma Theorem1_Session_Key_Secrecy_A: + "All A B rk ek id_S id_O #i. + Init_A(A, B, rk, ek, id_S, id_O) @ i + ==> + not (Ex #j. K(rk) @ j) + | (Ex #j. CorruptRNG_KEX(A) @ j) + | ( (Ex #j1. CorruptIK(B) @ j1) & (Ex #j2. CorruptSPK(B, id_S) @ j2) & (Ex #j3. CorruptOPK(B, id_O) @ j3) ) + " + +// Theorem 1 (B's perspective): Session Key Secrecy +// If Bob accepts, the key is secret UNLESS Adv impersonated Alice (CorruptIK(A)) +// OR Adv corrupted ALL of Bob's keys. +lemma Theorem1_Session_Key_Secrecy_B: + "All B A rk ek id_S id_O #i. + Init_B(B, A, rk, ek, id_S, id_O) @ i + ==> + not (Ex #j. K(rk) @ j) + | (Ex #j. CorruptIK(A) @ j) + | (Ex #j. CorruptRNG_KEX(A) @ j) // <--- THE MISSING PREDICATE! + | ( (Ex #j1. CorruptIK(B) @ j1) & (Ex #j2. CorruptSPK(B, id_S) @ j2) & (Ex #j3. CorruptOPK(B, id_O) @ j3) ) + " + +// Theorem 1 (A's perspective): Epoch Key Secrecy +// Same structure as rk — ek is derived from the same IKM via a distinct KDF label. +lemma Theorem1_EK_Secrecy_A: + "All A B rk ek id_S id_O #i. + Init_A(A, B, rk, ek, id_S, id_O) @ i + ==> + not (Ex #j. K(ek) @ j) + | (Ex #j. CorruptRNG_KEX(A) @ j) + | ( (Ex #j1. CorruptIK(B) @ j1) & (Ex #j2. CorruptSPK(B, id_S) @ j2) & (Ex #j3. CorruptOPK(B, id_O) @ j3) ) + " + +// Theorem 1 (B's perspective): Epoch Key Secrecy +lemma Theorem1_EK_Secrecy_B: + "All B A rk ek id_S id_O #i. + Init_B(B, A, rk, ek, id_S, id_O) @ i + ==> + not (Ex #j. K(ek) @ j) + | (Ex #j. CorruptIK(A) @ j) + | (Ex #j. CorruptRNG_KEX(A) @ j) + | ( (Ex #j1. CorruptIK(B) @ j1) & (Ex #j2. CorruptSPK(B, id_S) @ j2) & (Ex #j3. CorruptOPK(B, id_O) @ j3) ) + " + +// Theorem 2(a): Recipient Binding +// If Alice initiates with B and Bob accepts the same session, then Alice +// and Bob agree on each other's identity. This is explicit binding: +// fp_IK_B = H(pk_IK_B) is embedded in SI, which Alice signs as σ_SI, +// and Bob verifies σ_SI against pk_IK_A. If both Init_A and Init_B fire +// for the same (rk, ek), the session names both parties correctly. +// (No corruption exclusion needed — this is a structural property of the +// signature + fingerprint binding, not a secrecy claim.) +lemma Theorem2a_Recipient_Binding: + "All A B rk ek id_S id_O #i #j. + Init_A(A, B, rk, ek, id_S, id_O) @i & + Init_B(B, A, rk, ek, id_S, id_O) @j + ==> + i < j + " + +// Theorem 2(b): Initiator Authentication +// If Bob verifies the session init, Alice actually generated it, +// UNLESS the adversary corrupted Alice's Identity Key. +lemma Theorem2b_Initiator_Authentication: + "All B A rk ek id_S id_O #i. + Init_B(B, A, rk, ek, id_S, id_O) @ i + ==> + (Ex #j. Init_A(A, B, rk, ek, id_S, id_O) @ j & j < i) + | (Ex #j. CorruptIK(A) @ j) + " + +// §4.4 Step 6: OPK single-use — the linear OPK_Available fact ensures a given +// OPK id is consumed by at most one session reception. +lemma OPK_Single_Use: + "All B A1 A2 rk1 rk2 ek1 ek2 id_S1 id_S2 id_O #i #j. + Init_B(B, A1, rk1, ek1, id_S1, id_O) @ i & + Init_B(B, A2, rk2, ek2, id_S2, id_O) @ j + ==> + #i = #j + " + +// Key uniqueness: distinct Init_A events (with fresh KEM randomness) produce +// distinct root keys. Two sessions sharing the same rk must be the same event. +lemma Key_Uniqueness: + "All A1 A2 B1 B2 rk ek1 ek2 id_S1 id_S2 id_O1 id_O2 #i #j. + Init_A(A1, B1, rk, ek1, id_S1, id_O1) @ i & + Init_A(A2, B2, rk, ek2, id_S2, id_O2) @ j + ==> + #i = #j + " + +end \ No newline at end of file diff --git a/tamarin/LO_NegativeTests.spthy b/tamarin/LO_NegativeTests.spthy new file mode 100644 index 0000000000..11ae2f5c61 --- /dev/null +++ b/tamarin/LO_NegativeTests.spthy @@ -0,0 +1,350 @@ +theory LO_NegativeTests +begin + +/* + * Negative Tests (Expected Falsifications) + * ========================================= + * + * Each lemma SHOULD be falsified. If any verifies, the model is + * over-constraining the adversary or making incorrect assumptions. + * These confirm the model correctly represents attack paths. + * + * ALL EXPECTED: FALSIFIED + * + * neg_auth_ik_corrupt: IK corruption → auth forged + * neg_auth_rng_corrupt: RNG corruption → auth forged + * neg_ratchet_no_fs_0step: Corrupt immediately → current ek revealed + * neg_ratchet_recv_1step: 1-step recv FS fails (prev_ek_r retains) + * neg_call_rk_plus_rng: rk + RNG corruption → call key derivable + * neg_stream_key_corrupt: Key corruption → forgery possible + * neg_reflect_self_session: Self-session → reflection succeeds + */ + +builtins: hashing, signing, asymmetric-encryption + +functions: kem_pk/1, kem_c/2, kem_ss/2, kem_decaps/2, mac/2 +equations: kem_decaps(sk, kem_c(kem_pk(sk), r)) = r + +functions: aead_enc/4, aead_verify/4, accept/0 +equations: aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept() + +functions: kdf_call_a/3 + +restriction Eq: + "All x y #i. Eq(x,y) @i ==> x = y" + + +/* =========== NEG 1-2: LO-Auth corruption =========== */ + +rule NAuth_GenIK: + [ Fr(~sk) ] --[ NAuthGen($P) ]-> + [ !NAuthLtk($P, ~sk), !NAuthPk($P, kem_pk(~sk)), Out(kem_pk(~sk)) ] + +rule NAuth_CorruptIK: + [ !NAuthLtk($P, sk) ] --[ NAuthCorruptIK($P) ]-> [ Out(sk) ] + +rule NAuth_CorruptRNG: + [ !NAuthRNG($S, r) ] --[ NAuthCorruptRNG($S, r) ]-> [ Out(r) ] + +rule NAuth_Challenge: + let c = kem_c(pk_c, ~r) + ss = kem_ss(pk_c, ~r) + token = mac(ss, 'lo-auth-v1') + in + [ !NAuthPk($C, pk_c), Fr(~r) ] + --[ NAuthChallenge($S, $C, ~r, token) ]-> + [ NAuthPending($S, $C, token), Out(c), !NAuthRNG($S, ~r) ] + +rule NAuth_Verify: + [ NAuthPending($S, $C, token), In(proof) ] + --[ Eq(token, proof), NAuthAccepted($S, $C) ]-> + [ ] + +// NEG 1: IK corruption defeats auth +lemma neg_auth_ik_corrupt: + "All S C #v. + NAuthAccepted(S, C) @v + ==> not (Ex #j. NAuthCorruptIK(C) @j)" + +// NEG 2: RNG corruption defeats auth +lemma neg_auth_rng_corrupt: + "All S C r token #ch #v. + NAuthChallenge(S, C, r, token) @ch & + NAuthAccepted(S, C) @v + ==> not (Ex #j. NAuthCorruptRNG(S, r) @j)" + + +/* =========== NEG 3-4: LO-Ratchet FS boundaries =========== */ + +restriction NRatchetOnce: + "All #i #j. NRInit() @i & NRInit() @j ==> #i = #j" + +rule NR_Init: + [ Fr(~ek) ] --[ NRInit() ]-> [ NR1(~ek, 'nil') ] + +rule NR_Recv1: + [ NR1(ek_r, prev), Fr(~ek) ] --[ NRRecv(~ek) ]-> [ NR2(~ek, ek_r) ] + +rule NR_Adv1: + [ NR2(ek_r, prev) ] --> [ NR3(ek_r, prev) ] + +rule NR_Recv2: + [ NR3(ek_r, prev), Fr(~ek) ] --[ NRRecv(~ek) ]-> [ NR4(~ek, ek_r) ] + +rule NR_Corrupt: + [ NR1(ek, p) ] --[ NRCorrupt(), NRRevealed(ek) ]-> [ ] + +rule NR_Corrupt2: + [ NR2(ek, p) ] --[ NRCorrupt(), NRRevealed(ek), NRRevealed(p) ]-> [ ] + +rule NR_Corrupt3: + [ NR3(ek, p) ] --[ NRCorrupt(), NRRevealed(ek), NRRevealed(p) ]-> [ ] + +rule NR_Corrupt4: + [ NR4(ek, p) ] --[ NRCorrupt(), NRRevealed(ek), NRRevealed(p) ]-> [ ] + +// NEG 3: Corrupt with 0 subsequent recvs → current ek revealed +lemma neg_ratchet_no_fs_0step: + "All ek #r #c. + NRRecv(ek) @r & NRCorrupt() @c & r < c + ==> not (Ex #rev. NRRevealed(ek) @rev)" + +// NEG 4: Same as recv_fs_1step — 1 subsequent recv, ek still in prev +lemma neg_ratchet_recv_1step: + "All ek ek2 #i #j #c. + NRRecv(ek) @i & NRRecv(ek2) @j & NRCorrupt() @c & + i < j & j < c + ==> not (Ex #r. NRRevealed(ek) @r)" + + +/* =========== NEG 5: LO-Call rk+RNG corruption =========== */ + +restriction NCallNeq: + "All I R rk #i. NCallSetup(I, R, rk) @i ==> not (I = R)" + +rule NCall_Setup: + [ Fr(~rk) ] --[ NCallSetup($I, $R, ~rk) ]-> [ !NCallRK($I, $R, ~rk) ] + +rule NCall_CorruptRK: + [ !NCallRK($I, $R, rk) ] --[ NCallCorruptRK($I, $R) ]-> [ Out(rk) ] + +rule NCall_CorruptRNG: + [ !NCallRNG($P, r) ] --[ NCallCorruptRNG($P, r) ]-> [ Out(r) ] + +// Step 1: initiator generates pk_eph (public), sk_eph +// Step 2: peer encapsulates to pk_eph with randomness r_eph +// Corrupt(RNG, initiator, t1) reveals sk_eph +// Corrupt(RNG, peer, t2) reveals r_eph +rule NCall_Derive: + let pk_eph = kem_pk(~sk_eph) + ss = kem_ss(pk_eph, ~r_eph) + ka = kdf_call_a(rk, ss, ~cid) + in + [ !NCallRK($I, $R, rk), Fr(~sk_eph), Fr(~r_eph), Fr(~cid) ] + --[ NCallDerived($R, ka) ]-> + [ Out(pk_eph), + Out(~cid), + Out(kem_c(pk_eph, ~r_eph)), + !NCallRNG($I, ~sk_eph), + !NCallRNG($R, ~r_eph) ] + +// NEG 5: Both rk and ephemeral RNG corrupted → call key derivable +lemma neg_call_rk_plus_rng: + "All R ka #d. + NCallDerived(R, ka) @d + ==> not (Ex #k. K(ka) @k)" + + +/* =========== NEG 6: LO-Stream key corruption =========== */ + +functions: nonce_n/2, aad_n/2 + +rule NS_Init: + [ Fr(~key), Fr(~bn) ] + --[ NSInit(~key, ~bn) ]-> + [ !NSSP(~key, ~bn), NSEnc(~key, ~bn, '0'), Out(~bn) ] + +rule NS_CorruptKey: + [ !NSSP(key, bn) ] --[ NSCorrupt(key) ]-> [ Out(key) ] + +rule NS_Enc: + let n = nonce_n(bn, idx) + aad = aad_n(bn, idx) + c = aead_enc(key, n, ~m, aad) + in + [ NSEnc(key, bn, idx), Fr(~m) ] + --[ NSEncrypted(bn, idx, c) ]-> + [ Out() ] + +// Adversary decrypts with corrupted key +rule NS_Dec_Adversary: + let n = nonce_n(bn, idx) + aad = aad_n(bn, idx) + in + [ !NSSP(key, bn), In() ] + --[ Eq(aead_verify(key, n, aad, c), accept()), + NSDecrypted(bn, idx) ]-> + [ ] + +// NEG 6: Key corruption → adversary can get ciphertext accepted +// (trivially true since adversary holds key and can replay honest ciphertexts) +lemma neg_stream_key_corrupt: + "All bn idx #d. + NSDecrypted(bn, idx) @d + ==> not (Ex #j key. NSCorrupt(key) @j)" + + +/* =========== NEG 7: Anti-reflection without invariant (h) =========== */ + +rule NRefl_Setup: + [ Fr(~mk), Fr(~n) ] + --[ NReflSetup($A, $B, ~mk) ]-> + [ !NReflKey($A, $B, ~mk), NReflSend($A, $B, ~mk, ~n) ] + +// NOTE: No Neq restriction — self-sessions allowed! + +rule NRefl_Send: + let aad = <'lo-dm-v1', $A, $B, ~hdr> + c = aead_enc(mk, n, ~m, aad) + in + [ NReflSend($A, $B, mk, n), Fr(~m), Fr(~hdr) ] + --[ NReflSent($A, $B, c) ]-> + [ Out() ] + +rule NRefl_RecvReflected: + let aad = <'lo-dm-v1', $B, $A, header> + in + [ !NReflKey($A, $B, mk), In() ] + --[ Eq(aead_verify(mk, n, aad, c), accept()), + NReflAccepted($A, $B, c) ]-> + [ ] + +// NEG 7: Without invariant (h), self-session allows reflection +// A sends to A, reflected back — AAD matches because fp order is same +lemma neg_reflect_self_session: + "All A c #i #j. + NReflSent(A, A, c) @i & + NReflAccepted(A, A, c) @j + ==> F" + + +/* ========================================================= + * 8. LO-KEX: OPK-absent weakens secrecy threshold (2-key) + * ========================================================= */ + +// KEX without OPK: IKM = ss_IK ‖ ss_SPK only. +// Corruption of IK + SPK alone suffices to derive rk. + +// Reuse KEX IK generation (produces !KEXLtk and !KEXPk for NKEX2 rules) +rule NKEX2_GenIK: + [ Fr(~sk) ] --[ NKEX2_GenIK($P, ~sk) ]-> + [ !KEXLtk($P, ~sk), !KEXPk($P, pk(~sk)), Out(pk(~sk)) ] + +rule NKEX2_Publish: + let pk_SPK = pk(~sk_SPK) + pk_IK = pk(~sk_IK) + sig_SPK = sign(<'lo-spk-sig-v1', pk_SPK>, ~sk_IK) + in + [ !KEXLtk($B, ~sk_IK), Fr(~sk_SPK), Fr(~id_SPK) ] + --[ NKEX2_Publish($B, ~id_SPK) ]-> + [ !NKEX2_SPK_Secret($B, ~id_SPK, ~sk_SPK), + !NKEX2_SPK_Pk($B, ~id_SPK, pk_SPK), + Out() ] + +rule NKEX2_CorruptSPK: + [ !NKEX2_SPK_Secret($P, id, sk) ] --[ NKEX2_CorruptSPK($P, id) ]-> [ Out(sk) ] + +rule NKEX2_Alice_NoOPK: + let pk_IK_A = pk(~sk_IK_A) + c_IK = aenc(~r_IK, pk_IK_B) + c_SPK = aenc(~r_SPK, pk_SPK_B) + ikm = <~r_IK, ~r_SPK> + rk = h() + in + [ !KEXLtk($A, ~sk_IK_A), !KEXPk($B, pk_IK_B), + !NKEX2_SPK_Pk($B, id_SPK, pk_SPK_B), + In(sig_SPK), Fr(~r_IK), Fr(~r_SPK) ] + --[ Eq(verify(sig_SPK, <'lo-spk-sig-v1', pk_SPK_B>, pk_IK_B), true), + NKEX2_Init($A, $B, rk, id_SPK) ]-> + [ Out() ] + +rule NKEX2_CorruptIK: + [ !KEXLtk($P, sk) ] --[ NKEX2_CorruptIK($P) ]-> [ Out(sk) ] + +// NEG 8: OPK-absent — IK + SPK corruption alone → adversary derives rk +lemma neg_kex_no_opk: + "All A B rk id_S #i. + NKEX2_Init(A, B, rk, id_S) @i + ==> not (Ex #k. K(rk) @k)" + + +/* ========================================================= + * 9. Ratchet: Duplicate message without recv_seen + * ========================================================= */ + +// Minimal ratchet with message counter but NO duplicate detection. +// An adversary replays a valid ciphertext → accepted twice. + +rule NRDup_Init: + [ Fr(~ek) ] --[ NRDupInit() ]-> [ !NRDupKey(~ek) ] + +restriction NRDupOnce: + "All #i #j. NRDupInit() @i & NRDupInit() @j ==> #i = #j" + +functions: kdf_msg/2, nonce_dup/1 + +rule NRDup_Enc: + let mk = kdf_msg(ek, ~ctr) + n = nonce_dup(~ctr) + c = aead_enc(mk, n, ~m, 'aad') + in + [ !NRDupKey(ek), Fr(~ctr), Fr(~m) ] + --[ NRDupSent(~ctr, c) ]-> + [ Out() ] + +// Decrypt WITHOUT recv_seen — always accepts if AEAD passes +rule NRDup_Dec: + let mk = kdf_msg(ek, ctr) + n = nonce_dup(ctr) + in + [ !NRDupKey(ek), In() ] + --[ Eq(aead_verify(mk, n, 'aad', c), accept()), + NRDupAccepted(ctr, c) ]-> + [ ] + +// NEG 9: Without recv_seen, same ciphertext accepted twice +lemma neg_ratchet_duplicate: + "All ctr c #i #j. + NRDupAccepted(ctr, c) @i & + NRDupAccepted(ctr, c) @j + ==> #i = #j" + + +/* ========================================================= + * 10. Call: Self-session collapses role assignment + * ========================================================= */ + +// Without the local_fp != remote_fp guard, both parties get the +// same role — send/recv key separation collapses. + +rule NCallSelf_Setup: + [ Fr(~rk) ] --[ NCallSelfSetup($A, $A, ~rk) ]-> + [ !NCallSelfRK($A, $A, ~rk) ] + +rule NCallSelf_Derive: + let ss = kem_ss(kem_pk(~sk_eph), ~r_eph) + // With fp_lo = fp_hi (same party), canonical ordering produces + // identical role assignment for both sides + ka = kdf_call_a(rk, ss, ~cid) + in + [ !NCallSelfRK($A, $A, rk), Fr(~sk_eph), Fr(~r_eph), Fr(~cid) ] + --[ NCallSelfDerived($A, ka) ]-> + [ Out(kem_pk(~sk_eph)), Out(~cid), Out(kem_c(kem_pk(~sk_eph), ~r_eph)) ] + +// NEG 10: Self-session is reachable (no guard prevents it) +// This confirms the guard is necessary — without it, A initiates a call with itself +lemma neg_call_self_session: + exists-trace + "Ex A ka #i. NCallSelfDerived(A, ka) @i" + +end diff --git a/tamarin/LO_Ratchet.spthy b/tamarin/LO_Ratchet.spthy new file mode 100644 index 0000000000..659bcbe088 --- /dev/null +++ b/tamarin/LO_Ratchet.spthy @@ -0,0 +1,215 @@ +theory LO_Ratchet +begin + +/* + * LO-Ratchet: Forward Secrecy (Theorem 4) and Post-Compromise Security (Theorem 5) + * ================================================================================= + * + * Abstract model: epoch keys are Fr() (fresh names), not KDF-derived. + * This proves FS and PCS are STRUCTURAL properties of the state machine, + * independent of KDF/KEM security. Send and recv are modeled as separate + * sections to avoid Tamarin non-termination on combined state machines. + * + * Corruption comes in two flavors: + * - Consuming (Corrupt_S/R): reveals state, terminates session → used for FS + * - Non-consuming (Observe_S/R): reveals state, session continues → used for PCS + * + * LIMITATIONS: This abstraction does NOT capture: + * - KEM-level PCS (compromised sk_s means compromised ss for one step) + * - Message key derivation (mk = KDF_MsgKey(ek, n)) or Theorem 3 + * - Message counters, skip handling, or replay detection + * + * EXPECTED RESULTS: + * send_sanity: VERIFIED + * send_fs: VERIFIED (Theorem 4a) + * send_corrupt_terminates: VERIFIED + * send_pcs: VERIFIED (Theorem 5, send) + * recv_sanity: VERIFIED + * recv_fs_1step: FALSIFIED (Theorem 4b, 1-step counterexample) + * recv_fs_2step: VERIFIED (Theorem 4b, 2-step FS) + * recv_corrupt_terminates: VERIFIED + * recv_pcs: VERIFIED (Theorem 5, recv) + */ + + +/* ================= SEND SIDE (unchanged — already works) ================= */ + +restriction Once_S: + "All #i #j. InitS() @i & InitS() @j ==> #i = #j" + +rule Bounds_S: + [ ] --> [ !BS('1','2'), !BS('2','3'), !BS('3','4') ] + +rule Init_S: + [ Fr(~ek) ] + --[ InitS() ]-> + [ S('1', ~ek, 'pending') ] + +rule KEM_Send: + [ S(step, ek_s, 'pending'), !BS(step, next), Fr(~ek2) ] + --[ Send(~ek2) ]-> + [ S(next, ~ek2, 'idle') ] + +rule Advance_S: + [ S(step, ek_s, 'idle'), !BS(step, next) ] + --> + [ S(next, ek_s, 'pending') ] + +// Consuming corruption: reveals epoch key, terminates session (for FS proofs) +rule Corrupt_S: + [ S(step, ek_s, status) ] + --[ CorruptS(), RevealedS(ek_s) ]-> + [ ] + +// Non-consuming observation: reveals epoch key, session continues (for PCS proofs) +rule Observe_S: + [ S(step, ek_s, status) ] + --[ ObserveS(), ObservedS(ek_s) ]-> + [ S(step, ek_s, status) ] + +restriction Once_ObserveS: + "All #i #j. ObserveS() @i & ObserveS() @j ==> #i = #j" + +lemma send_sanity: + exists-trace + "Ex ek1 ek2 #i #j. Send(ek1) @i & Send(ek2) @j & i < j" + +lemma send_fs: + "All ek ek2 #i #j #c. + Send(ek) @i & Send(ek2) @j & CorruptS() @c & + i < j & j < c + ==> not (Ex #r. RevealedS(ek) @r)" + +// Consuming corruption terminates the session: no Send can follow CorruptS. +lemma send_corrupt_terminates: + "All ek #s #c. Send(ek) @s & CorruptS() @c ==> s < c" + +// Theorem 5 (PCS, send side): after non-consuming observation, one fresh +// KEM ratchet step produces an epoch key the adversary never observed. +// (Structurally trivial in this abstraction — Fr() is always fresh — but +// documents that the state machine permits recovery from compromise.) +lemma send_pcs: + "All ek_new #obs #send. + ObserveS() @obs & + Send(ek_new) @send & obs < send + ==> not (Ex #r. ObservedS(ek_new) @r)" + + +/* ================= RECV SIDE (unrolled) ================= */ + +/* + * State machine (each node is a distinct fact): + * + * Init → R1(ek_r, prev) "idle" + * ↓ Recv1 + * R2(ek_r, prev) "pending" + * ↓ Adv1 + * R3(ek_r, prev) "idle" + * ↓ Recv2 + * R4(ek_r, prev) "pending" + * ↓ Adv2 + * R5(ek_r, prev) "idle" + * ↓ Recv3 + * R6(ek_r, prev) "pending" + * + * Corrupt can consume any R1..R6. + * + * Each R_i fact has EXACTLY ONE source rule. + * Source analysis: zero branching. Proof search: linear. + */ + +restriction Once_R: + "All #i #j. InitR() @i & InitR() @j ==> #i = #j" + +/* Init: ek_r from KEX, no previous epoch key */ +rule Init_R: + [ Fr(~ek) ] + --[ InitR() ]-> + [ R1(~ek, 'nil') ] + +/* Recv steps: new ek_r, old ek_r → prev */ +rule Recv1: + [ R1(ek_r, prev), Fr(~ek) ] + --[ Recv(~ek) ]-> + [ R2(~ek, ek_r) ] + +rule Adv1: + [ R2(ek_r, prev) ] + --[ Adv() ]-> + [ R3(ek_r, prev) ] + +rule Recv2: + [ R3(ek_r, prev), Fr(~ek) ] + --[ Recv(~ek) ]-> + [ R4(~ek, ek_r) ] + +rule Adv2: + [ R4(ek_r, prev) ] + --[ Adv() ]-> + [ R5(ek_r, prev) ] + +rule Recv3: + [ R5(ek_r, prev), Fr(~ek) ] + --[ Recv(~ek) ]-> + [ R6(~ek, ek_r) ] + +/* Consuming corruption: reveals ek_r and prev, terminates session */ +rule Corrupt_R1: [ R1(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ] +rule Corrupt_R2: [ R2(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ] +rule Corrupt_R3: [ R3(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ] +rule Corrupt_R4: [ R4(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ] +rule Corrupt_R5: [ R5(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ] +rule Corrupt_R6: [ R6(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ] + +/* Non-consuming observation: reveals ek_r and prev, session continues (PCS) */ +rule Observe_R1: [ R1(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R1(ek,p) ] +rule Observe_R2: [ R2(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R2(ek,p) ] +rule Observe_R3: [ R3(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R3(ek,p) ] +rule Observe_R4: [ R4(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R4(ek,p) ] +rule Observe_R5: [ R5(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R5(ek,p) ] +rule Observe_R6: [ R6(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R6(ek,p) ] + +restriction Once_ObserveR: + "All #i #j. ObserveR() @i & ObserveR() @j ==> #i = #j" + + +/* Recv lemmas */ + +lemma recv_sanity: + exists-trace + "Ex ek1 ek2 #i #j. Recv(ek1) @i & Recv(ek2) @j & i < j" + +/* Theorem 4b part 1 (1 step): FALSIFIED + * After 1 subsequent Recv, old ek_r is in prev — revealed on corrupt. */ +lemma recv_fs_1step: + "All ek ek2 #i #j #c. + Recv(ek) @i & Recv(ek2) @j & CorruptR() @c & + i < j & j < c + ==> not (Ex #r. RevealedR(ek) @r)" + +/* Theorem 4b part 2 (2 steps): VERIFIED + * After 2 subsequent Recvs, prev has been overwritten — old ek_r gone. */ +lemma recv_fs_2step: + "All ek ek2 ek3 #i #j #k #c. + Recv(ek) @i & Recv(ek2) @j & Recv(ek3) @k & CorruptR() @c & + i < j & j < k & k < c + ==> not (Ex #r. RevealedR(ek) @r)" + +// Consuming corruption terminates the session: no Recv can follow CorruptR. +lemma recv_corrupt_terminates: + "All ek #r #c. Recv(ek) @r & CorruptR() @c ==> r < c" + +// PCS (recv side, ABSTRACT MODEL ONLY): after non-consuming observation, +// one fresh recv step produces an epoch key the adversary never observed. +// NOTE: This is an artifact of the Fr()-based abstraction, NOT a Theorem 5 +// result. In the real protocol (see LO_Ratchet_PCS.spthy), recv-only PCS +// is NOT achieved — the adversary holds sk_s from the compromise and can +// derive ss from the peer's ciphertext. Real PCS requires a direction +// change (send after recv). See §9.2 worked trace. +lemma recv_pcs: + "All ek_new #obs #recv. + ObserveR() @obs & + Recv(ek_new) @recv & obs < recv + ==> not (Ex #r. ObservedR(ek_new) @r)" + +end diff --git a/tamarin/LO_Ratchet_PCS.spthy b/tamarin/LO_Ratchet_PCS.spthy new file mode 100644 index 0000000000..95aa5ac951 --- /dev/null +++ b/tamarin/LO_Ratchet_PCS.spthy @@ -0,0 +1,193 @@ +theory LO_Ratchet_PCS +begin + +/* + * LO-Ratchet: KEM-Level Post-Compromise Security (Theorem 5) + * =========================================================== + * + * Unlike LO_Ratchet.spthy (which uses abstract Fr() epoch keys), this model + * uses actual KEM encapsulation and KDF derivation to capture the KEM-level + * PCS recovery latency: + * + * - After compromise + RECV: NOT recovered — adversary knows sk_own from + * the compromised state and can decapsulate the peer's ciphertext, + * deriving ss and the new epoch key. + * + * - After compromise + RECV + SEND: RECOVERED — fresh sk_own' is unknown + * to the adversary, and the send encapsulates to the honest peer's pk, + * producing ss that requires sk_peer to derive. + * + * - After compromise + RECV + SEND + RECV: STILL RECOVERED — the peer + * now encapsulates to pk(sk_own'), which the adversary cannot decapsulate. + * + * This matches §8.6 Theorem 5: one direction change (send after recv) is + * sufficient for PCS recovery, assuming the peer is honest and the fresh + * keygen uses uncorrupted RNG (F4). + * + * LIMITATIONS (inherent to symbolic models): + * - IND-CCA2 vs IND-CPA: The symbolic KEM does not distinguish these; + * §8.2/§8.6 require IND-CCA2 for the Theorem 5 reduction. + * - Adversarial injection: Only honest-peer message flow is modeled, + * not the §9.2 chain-injection extension where the adversary + * substitutes pk_s* to extend compromise indefinitely. + * + * The model is fully unrolled (P0→P1→P2→P3→P4) with unique fact names + * to avoid Tamarin non-termination. + * + * EXPECTED RESULTS: + * pcs_sanity: VERIFIED + * pcs_no_recovery_after_recv: FALSIFIED (adversary derives ek) + * pcs_recovery_after_send: VERIFIED + * pcs_recovery_sustained: VERIFIED + * pcs_f4_violated: VERIFIED (F4 defeats the NEXT recv, not this send) + */ + +builtins: hashing + +// X-Wing KEM abstraction (subterm-convergent, per LO_Auth.spthy) +functions: kem_pk/1, kem_c/2, kem_ss/2, kem_decaps/2 +equations: kem_decaps(sk, kem_c(kem_pk(sk), r)) = r + +restriction Once: + "All #i #j. Init() @i & Init() @j ==> #i = #j" + +restriction OncePeer: + "All #i #j. PeerSetup() @i & PeerSetup() @j ==> #i = #j" + +restriction OnceObserve: + "All #i #j. Observe() @i & Observe() @j ==> #i = #j" + + +/* ================= SETUP ================= */ + +// Honest peer: sk_peer never output, pk_peer is public +rule PeerSetup: + [ Fr(~sk_peer) ] + --[ PeerSetup() ]-> + [ !PeerPk(kem_pk(~sk_peer)), Out(kem_pk(~sk_peer)) ] + +// Init: establish ratchet state after KEX +// State = (rk, sk_own, pk_peer) +// pk_own is published (peer needs it to encapsulate to us) +rule Init: + let pk_own = kem_pk(~sk_own) in + [ Fr(~rk), Fr(~sk_own), !PeerPk(pk_peer) ] + --[ Init() ]-> + [ P0(~rk, ~sk_own, pk_peer), Out(pk_own) ] + + +/* ================= OBSERVE (non-consuming compromise) ================= */ + +// Adversary learns rk and sk_own — models Corrupt(RatchetState, P, t_c) +rule Observe: + [ P0(rk, sk_own, pk_peer) ] + --[ Observe() ]-> + [ P1(rk, sk_own, pk_peer), Out(rk), Out(sk_own) ] + + +/* ================= RATCHET STEPS (unrolled) ================= */ + +// Recv1: peer honestly encapsulates to pk(sk_own) +// sk_own is COMPROMISED — adversary has it from Observe, can decapsulate +// c to recover r_peer, compute ss, then derive rk' and ek. +rule Recv1: + let + c = kem_c(kem_pk(sk_own), ~r_peer) + ss = kem_ss(kem_pk(sk_own), ~r_peer) + rk_new = h() + ek = h() + in + [ P1(rk, sk_own, pk_peer), Fr(~r_peer) ] + --[ Recv1_Act(), DerivedEK_R1(ek) ]-> + [ P2(rk_new, sk_own, pk_peer), Out(c) ] + +// Send1: generate fresh keypair, encapsulate to honest peer's pk +// Adversary sees c but cannot derive ss — would need sk_peer (never +// output) or the encapsulation randomness ~r (fresh, never output). +// Fresh ~sk_new replaces compromised sk_own: this is the recovery point. +rule Send1: + let + c = kem_c(pk_peer, ~r) + ss = kem_ss(pk_peer, ~r) + rk_new = h() + ek = h() + pk_own_new = kem_pk(~sk_new) + in + [ P2(rk, sk_own, pk_peer), Fr(~sk_new), Fr(~r) ] + --[ Send1_Act(), DerivedEK_S1(ek) ]-> + [ P3(rk_new, ~sk_new, pk_peer), Out(c), Out(pk_own_new) ] + +// F4 violation: adversary corrupts the RNG at Send1's keygen epoch, +// learning sk_new. The send step still executes (RNG corruption doesn't +// prevent keygen), but the adversary can now decapsulate future messages +// to pk(sk_new). This models Corrupt(RNG, decapsulator, t_keygen) per §8.3 F4. +rule Send1_F4_Violated: + let + c = kem_c(pk_peer, ~r) + ss = kem_ss(pk_peer, ~r) + rk_new = h() + ek = h() + pk_own_new = kem_pk(~sk_new) + in + [ P2(rk, sk_own, pk_peer), Fr(~sk_new), Fr(~r) ] + --[ Send1_F4(), DerivedEK_S1_F4(ek) ]-> + [ P3(rk_new, ~sk_new, pk_peer), Out(c), Out(pk_own_new), + Out(~sk_new) ] // F4 violated: adversary learns sk_new + +// Recv2: peer encapsulates to pk(sk_new) — UNCOMPROMISED key +// Adversary sees c but cannot decapsulate: sk_new was generated fresh +// in Send1 and never output. PCS recovery is sustained. +rule Recv2: + let + c = kem_c(kem_pk(sk_new), ~r_peer) + ss = kem_ss(kem_pk(sk_new), ~r_peer) + rk_new = h() + ek = h() + in + [ P3(rk, sk_new, pk_peer), Fr(~r_peer) ] + --[ Recv2_Act(), DerivedEK_R2(ek) ]-> + [ P4(rk_new, sk_new, pk_peer), Out(c) ] + + +/* ================= LEMMAS ================= */ + +// Sanity: full sequence can execute +lemma pcs_sanity: + exists-trace + "Ex #i. Recv2_Act() @i" + +// After observe + recv1: adversary CAN derive ek (non-recovery). +// Expected: FALSIFIED — adversary has sk_own, decaps c → r_peer, +// computes kem_ss(pk(sk_own), r_peer) → ss, then h() → ek. +lemma pcs_no_recovery_after_recv: + "All ek #r. + DerivedEK_R1(ek) @r + ==> not (Ex #k. K(ek) @k)" + +// After observe + recv1 + send1: ek from send is NOT derivable (recovery). +// Expected: VERIFIED — ss requires sk_peer or ~r, adversary has neither. +lemma pcs_recovery_after_send: + "All ek #s. + DerivedEK_S1(ek) @s + ==> not (Ex #k. K(ek) @k)" + +// After observe + recv1 + send1 + recv2: ek still NOT derivable. +// Expected: VERIFIED — peer encapsulates to pk(sk_new), adversary +// cannot decapsulate without sk_new (fresh, never output). +lemma pcs_recovery_sustained: + "All ek #r. + DerivedEK_R2(ek) @r + ==> not (Ex #k. K(ek) @k)" + +// §8.3 F4 violation: The adversary corrupts the RNG at the recovery +// step's keygen, learning sk_new. However, the Send1 step's ek is +// derived from ss = kem_ss(pk_peer, ~r) where ~r is fresh and sk_peer +// is unknown — F4 leaking sk_new does not help derive THIS step's ek. +// F4 defeats the NEXT recv step (peer encapsulates to pk(sk_new)). +// Expected: VERIFIED — Send1 ek is still protected. +lemma pcs_f4_violated: + "All ek #s. + DerivedEK_S1_F4(ek) @s + ==> not (Ex #k. K(ek) @k)" + +end diff --git a/tamarin/LO_Stream.spthy b/tamarin/LO_Stream.spthy new file mode 100644 index 0000000000..b3c7fa4ea5 --- /dev/null +++ b/tamarin/LO_Stream.spthy @@ -0,0 +1,251 @@ +theory LO_Stream +begin + +/* + * LO-Stream: Streaming AEAD (Theorem 13) + * ======================================= + * + * Chunked AEAD with counter-derived nonces over XChaCha20-Poly1305. + * Each stream uses a caller-provided key and a random base_nonce. + * + * State partition (§15.3): + * Linear (sequential only): next_index, finalized + * Persistent (both interfaces): key, base_nonce, caller_aad + * + * Nonce: nonce(base_nonce, index, tag_byte) — free constructor, + * injectivity by construction (§15.2). + * AAD: stream_aad(base_nonce, index, tag_byte, caller_aad) — free + * constructor, injectivity by construction (§15.4). + * + * Properties: + * P2: Integrity (INT-CTXT) — no forgery without key + * P3: Ordering — chunk accepted at position j only if encrypted at j + * P4: Truncation resistance — finalized only via genuine final chunk + * P5: Cross-stream isolation — chunk from stream A rejected by stream B + * + * Bounded to 3 sequential chunks (indices 0, 1, 2) for termination. + * + * EXPECTED RESULTS: + * Stream_Sanity: VERIFIED + * Stream_Sanity_Finalize: VERIFIED + * Theorem13_P2_Integrity: VERIFIED + * Theorem13_P3_Ordering: VERIFIED + * Theorem13_P4_No_False_Final: VERIFIED + * Theorem13_P5_Cross_Stream: VERIFIED + * Theorem13_Key_Secrecy: VERIFIED + */ + +builtins: hashing + +// AEAD +functions: aead_enc/4, aead_verify/4, accept/0 +equations: aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept() + +// Nonce and AAD constructors (free → injective) +functions: nonce/3, stream_aad/4 + +// Tag bytes +functions: nonfinal/0, final/0 + +// Bounded indices +functions: s/1 + +restriction Eq: + "All x y #i. Eq(x,y) @i ==> x = y" + +rule Index_Bounds: + [ ] --> [ !CB('0', s('0')), !CB(s('0'), s(s('0'))) ] + + +/* ================= STREAM SETUP ================= */ + +rule Stream_Init: + [ Fr(~key), Fr(~bn), Fr(~cid) ] + --[ StreamInit($O, ~key, ~bn, ~cid) ]-> + [ !SP($O, ~key, ~bn, ~cid), + EncSt($O, ~bn, '0', 'false'), + DecSt($O, ~bn, '0', 'false'), + Out(~bn) ] + + +/* ================= CORRUPTION ================= */ + +rule Corrupt_StreamKey: + [ !SP($O, key, bn, cid) ] + --[ CorruptStream($O, key) ]-> + [ Out(key) ] + + +/* ================= SEQUENTIAL ENCRYPTION ================= */ + +// Non-final chunk +rule Enc_Chunk: + let + n = nonce(bn, idx, nonfinal) + aad = stream_aad(bn, idx, nonfinal, cid) + c = aead_enc(key, n, ~m, aad) + in + [ EncSt($O, bn, idx, 'false'), !SP($O, key, bn, cid), + !CB(idx, next), Fr(~m) ] + --[ Encrypted($O, bn, idx, nonfinal, c) ]-> + [ EncSt($O, bn, next, 'false'), Out() ] + +// Final chunk — consumes EncSt without replacement (finalized) +rule Enc_Final: + let + n = nonce(bn, idx, final) + aad = stream_aad(bn, idx, final, cid) + c = aead_enc(key, n, ~m, aad) + in + [ EncSt($O, bn, idx, 'false'), !SP($O, key, bn, cid), Fr(~m) ] + --[ Encrypted($O, bn, idx, final, c), EncFinalized($O, bn, idx) ]-> + [ Out() ] + + +/* ================= SEQUENTIAL DECRYPTION ================= */ + +// Non-final chunk — decryptor advances index +rule Dec_Chunk: + let + n = nonce(bn, idx, nonfinal) + aad = stream_aad(bn, idx, nonfinal, cid) + in + [ DecSt($O, bn, idx, 'false'), !SP($O, key, bn, cid), + !CB(idx, next), In() ] + --[ Eq(aead_verify(key, n, aad, c), accept()), + SeqDec($O, bn, idx, nonfinal, c) ]-> + [ DecSt($O, bn, next, 'false') ] + +// Final chunk — consumes DecSt without replacement (finalized) +rule Dec_Final: + let + n = nonce(bn, idx, final) + aad = stream_aad(bn, idx, final, cid) + in + [ DecSt($O, bn, idx, 'false'), !SP($O, key, bn, cid), + In() ] + --[ Eq(aead_verify(key, n, aad, c), accept()), + SeqDec($O, bn, idx, final, c), DecFinalized($O, bn, idx) ]-> + [ ] + + +/* ================= RANDOM-ACCESS DECRYPTION ================= */ + +// Stateless — reads only persistent state +rule Dec_At: + let + n = nonce(bn, idx, tag) + aad = stream_aad(bn, idx, tag, cid) + in + [ !SP($O, key, bn, cid), In() ] + --[ Eq(aead_verify(key, n, aad, c), accept()), + RaDec($O, bn, idx, tag) ]-> + [ ] + + +/* ================= SECOND STREAM (cross-stream isolation) ================= */ + +// Same key, different base_nonce +rule Stream_Init_B: + [ !SP($O, key, bn_a, cid_a), Fr(~bn_b), Fr(~cid_b) ] + --[ StreamInitB($O, ~bn_b) ]-> + [ !SPB($O, key, ~bn_b, ~cid_b), + DecStB($O, ~bn_b, '0', 'false'), + Out(~bn_b) ] + +// Stream B sequential decrypt +rule Dec_Chunk_B: + let + n = nonce(bn_b, idx, tag) + aad = stream_aad(bn_b, idx, tag, cid_b) + in + [ DecStB($O, bn_b, idx, 'false'), !SPB($O, key, bn_b, cid_b), + !CB(idx, next), In() ] + --[ Eq(aead_verify(key, n, aad, c), accept()), + DecB($O, bn_b, idx, tag) ]-> + [ DecStB($O, bn_b, next, 'false') ] + +// Stream B random-access decrypt +rule Dec_At_B: + let + n = nonce(bn_b, idx, tag) + aad = stream_aad(bn_b, idx, tag, cid_b) + in + [ !SPB($O, key, bn_b, cid_b), In() ] + --[ Eq(aead_verify(key, n, aad, c), accept()), + DecB($O, bn_b, idx, tag) ]-> + [ ] + + +/* ================= LEMMAS ================= */ + +// Sanity: encrypt + decrypt a non-final chunk +lemma Stream_Sanity: + exists-trace + "Ex O bn idx c #i #j. + Encrypted(O, bn, idx, nonfinal, c) @i & + SeqDec(O, bn, idx, nonfinal, c) @j" + +// Sanity: encrypt final + reach DecFinalized +lemma Stream_Sanity_Finalize: + exists-trace + "Ex O bn idx #i #j. + EncFinalized(O, bn, idx) @i & + DecFinalized(O, bn, idx) @j" + +// P2 (Integrity): Sequential decryptor accepts only genuine ciphertexts. +// If SeqDec fires at (bn, idx, tag), the encryptor produced a chunk +// at that exact (bn, idx, tag) — or the key was corrupted. +lemma Theorem13_P2_Integrity: + "All O bn idx tag c #j. + SeqDec(O, bn, idx, tag, c) @j + ==> + (Ex #i. Encrypted(O, bn, idx, tag, c) @i) + | (Ex key #k. CorruptStream(O, key) @k) + " + +// P3 (Ordering): Implicit in P2 for the symbolic model — the sequential +// decryptor's index is part of the nonce/AAD, so accepting at index j +// requires a ciphertext produced at index j. Stated separately per §9.11(b). +// The adversary captures a chunk encrypted at index i and presents it at +// position j. The nonce/AAD mismatch prevents acceptance. +// P3 (Ordering): The SAME ciphertext c encrypted at index idx1 cannot +// be accepted by the sequential decryptor at a different index idx2. +// The nonce/AAD include the index, so mismatch causes AEAD failure. +lemma Theorem13_P3_Ordering: + "All O bn idx1 idx2 tag c #i #j. + Encrypted(O, bn, idx1, tag, c) @i & + SeqDec(O, bn, idx2, tag, c) @j & + not (idx1 = idx2) + ==> (Ex key #k. CorruptStream(O, key) @k)" + +// P4 (Truncation Resistance): DecFinalized only reachable via a genuine +// final-chunk ciphertext (tag_byte=final) from the encryptor. +lemma Theorem13_P4_No_False_Final: + "All O bn idx #j. + DecFinalized(O, bn, idx) @j + ==> + (Ex c #i. Encrypted(O, bn, idx, final, c) @i) + | (Ex key #k. CorruptStream(O, key) @k) + " + +// P5 (Cross-Stream Isolation): A chunk encrypted on stream A cannot be +// accepted by stream B's decryptor (different base_nonce, same key). +// Covers both sequential (DecB) and random-access (DecB) decryption. +lemma Theorem13_P5_Cross_Stream: + "All O bn_a bn_b idx tag c #i #j. + Encrypted(O, bn_a, idx, tag, c) @i & + DecB(O, bn_b, idx, tag) @j & + not (bn_a = bn_b) + ==> (Ex key #k. CorruptStream(O, key) @k)" + +// Key secrecy: stream key secret unless directly corrupted +lemma Theorem13_Key_Secrecy: + "All O key bn cid #i. + StreamInit(O, key, bn, cid) @i + ==> + not (Ex #j. K(key) @j) + | (Ex #j. CorruptStream(O, key) @j) + " + +end diff --git a/tamarin/README.md b/tamarin/README.md new file mode 100644 index 0000000000..478b4e3c69 --- /dev/null +++ b/tamarin/README.md @@ -0,0 +1,176 @@ +# 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 | diff --git a/verify.sh b/verify.sh new file mode 100755 index 0000000000..67d4578d4f --- /dev/null +++ b/verify.sh @@ -0,0 +1,182 @@ +#!/bin/bash +# Formal verification runner for libsoliton. +# Run after editing any .spthy or .cv file. Results should match the +# expected outcomes in tamarin/README.md and cryptoverif/README.md. +# +# Requirements: +# tamarin-prover 1.12.0+ with maude 3.5.1+ on PATH +# cryptoverif 2.12+ on PATH +# +# Usage: +# ./verify.sh # run everything +# ./verify.sh tamarin # tamarin only +# ./verify.sh cryptoverif # cryptoverif only +# ./verify.sh tamarin/LO_Auth.spthy # single file +# +# Environment: +# CV_LIB Path to CryptoVerif pq library (without .cvl extension). +# Example: CV_LIB=/usr/share/cryptoverif/pq ./verify.sh + +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +TAMARIN_DIR="$SCRIPT_DIR/tamarin" +CV_DIR="$SCRIPT_DIR/cryptoverif" +CV_LIB="${CV_LIB:-}" + +if [ -t 1 ]; then + GREEN='\033[0;32m'; RED='\033[0;31m'; YELLOW='\033[0;33m' + BOLD='\033[1m'; RESET='\033[0m' +else + GREEN=''; RED=''; YELLOW=''; BOLD=''; RESET='' +fi + +# Global counters +T_VERIFIED=0; T_FALSIFIED=0; T_ERRORS=0; T_FILES=0 +CV_PROVED=0; CV_FAILED=0; CV_FILES=0 + +print_header() { + echo "" + echo -e "${BOLD}=== $1 ===${RESET}" + echo "" +} + +run_tamarin() { + local file="$1" + local name + name="$(basename "$file" .spthy)" + T_FILES=$((T_FILES + 1)) + + echo -e "${BOLD}--- $name ---${RESET}" + + local output + if ! output=$(tamarin-prover "$file" --prove 2>&1); then + echo -e " ${RED}ERROR: tamarin-prover failed${RESET}" + echo "$output" | tail -5 | sed 's/^/ /' + T_ERRORS=$((T_ERRORS + 1)) + return + fi + + # Check for wellformedness warnings + if echo "$output" | grep -q "WARNING"; then + echo -e " ${RED}WARNING: wellformedness check failed${RESET}" + T_ERRORS=$((T_ERRORS + 1)) + fi + + local time + time=$(echo "$output" | grep "processing time:" | sed 's/.*processing time: //') + + # Parse each result line — avoid subshell pipe by using process substitution + while IFS= read -r line; do + local lemma steps + lemma=$(echo "$line" | sed 's/ (.*//') + steps=$(echo "$line" | grep -oP '\d+ steps' || echo "? steps") + + if echo "$line" | grep -q "verified"; then + echo -e " ${GREEN}PASS${RESET} $lemma ($steps)" + T_VERIFIED=$((T_VERIFIED + 1)) + elif echo "$line" | grep -q "falsified"; then + echo -e " ${YELLOW}FALSE${RESET} $lemma ($steps)" + T_FALSIFIED=$((T_FALSIFIED + 1)) + fi + done < <(echo "$output" | grep -E "verified|falsified") + + echo " ($time)" +} + +run_cryptoverif() { + local file="$1" + local name + name="$(basename "$file" .cv)" + CV_FILES=$((CV_FILES + 1)) + + echo -e "${BOLD}--- $name ---${RESET}" + + if [ -z "$CV_LIB" ]; then + echo -e " ${YELLOW}SKIP${RESET} CV_LIB not set. Run: CV_LIB=/path/to/pq $0 cryptoverif" + CV_FILES=$((CV_FILES - 1)) + return + fi + + local output + output=$(cryptoverif -lib "$CV_LIB" "$file" 2>&1) || true + + if echo "$output" | grep -q "^File.*Error:"; then + echo -e " ${RED}ERROR${RESET}" + echo "$output" | grep "Error:" | sed 's/^/ /' + CV_FAILED=$((CV_FAILED + 1)) + return + fi + + while IFS= read -r line; do + if echo "$line" | grep -q "Proved"; then + local prop bound + prop=$(echo "$line" | sed 's/RESULT Proved //' | sed 's/ up to.*//') + bound=$(echo "$line" | grep -oP 'up to probability .*' || echo "") + echo -e " ${GREEN}PROVED${RESET} $prop" + [ -n "$bound" ] && echo " $bound" + CV_PROVED=$((CV_PROVED + 1)) + elif echo "$line" | grep -q "Could not prove"; then + local prop + prop=$(echo "$line" | sed 's/RESULT Could not prove //') + echo -e " ${RED}FAILED${RESET} $prop" + CV_FAILED=$((CV_FAILED + 1)) + fi + done < <(echo "$output" | grep "^RESULT" | grep -v "^RESULT time") + + if echo "$output" | grep -q "All queries proved"; then + echo -e " ${GREEN}All queries proved.${RESET}" + fi +} + +run_all_tamarin() { + print_header "Tamarin Prover" + for f in "$TAMARIN_DIR"/*.spthy; do + run_tamarin "$f" + echo "" + done +} + +run_all_cryptoverif() { + print_header "CryptoVerif" + for f in "$CV_DIR"/*.cv; do + run_cryptoverif "$f" + echo "" + done +} + +case "${1:-all}" in + tamarin) run_all_tamarin ;; + cryptoverif) run_all_cryptoverif ;; + *.spthy) run_tamarin "$1" ;; + *.cv) run_cryptoverif "$1" ;; + all) run_all_tamarin; run_all_cryptoverif ;; + *) echo "Usage: $0 [all|tamarin|cryptoverif|]"; exit 1 ;; +esac + +# Summary +echo "" +echo -e "${BOLD}=== Summary ===${RESET}" + +T_TOTAL=$((T_VERIFIED + T_FALSIFIED)) +if [ "$T_FILES" -gt 0 ]; then + echo -e " Tamarin: ${T_FILES} files, ${T_TOTAL} lemmas (${T_VERIFIED} verified, ${T_FALSIFIED} falsified, ${T_ERRORS} errors)" +fi + +CV_TOTAL=$((CV_PROVED + CV_FAILED)) +if [ "$CV_FILES" -gt 0 ]; then + echo -e " CryptoVerif: ${CV_FILES} files, ${CV_TOTAL} queries (${CV_PROVED} proved, ${CV_FAILED} failed)" +fi + +GRAND_TOTAL=$((T_TOTAL + CV_TOTAL)) +GRAND_PASS=$((T_VERIFIED + T_FALSIFIED + CV_PROVED)) +GRAND_FAIL=$((T_ERRORS + CV_FAILED)) + +echo -e " Total: ${GRAND_TOTAL} checks, ${GRAND_FAIL} failures" + +if [ "$GRAND_FAIL" -gt 0 ]; then + echo -e " ${RED}Some checks failed.${RESET}" + exit 1 +else + echo -e " ${GREEN}All checks passed.${RESET}" +fi