mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
abf62ef0d0
Derive the session key K in the responder's Msg2 rule and carry it in state (Msg4 binds K from state, no inline DH recomputation) — clears the global derivation-check timeout. Same fix in lean/ and formal/ trees; all lemmas and semantics unchanged. Co-authored-by: Hanzo Dev <[email protected]>
649 lines
21 KiB
Plaintext
649 lines
21 KiB
Plaintext
/*
|
|
* RNS Hybrid Post-Quantum Handshake Protocol
|
|
* Formal model in Tamarin Prover
|
|
*
|
|
* Protocol source:
|
|
* ~/work/lux/node/network/dialer/rns_link.go
|
|
* ~/work/lux/node/network/dialer/rns_identity_pq.go
|
|
* ~/work/zap/zap/src/crypto.rs
|
|
*
|
|
* Cryptographic suite:
|
|
* Classical: X25519 (ECDH) + Ed25519 (signatures)
|
|
* PQ: ML-KEM-768 (key encapsulation) + ML-DSA-65 (signatures)
|
|
* Symmetric: AES-256-GCM, HKDF-SHA256
|
|
*
|
|
* Wire protocol (from rns_link.go):
|
|
* Msg1 (Initiator -> Responder): LinkRequest
|
|
* dest_A || pk_Ed_A || epk_X_A || sig_Ed(pk_Ed_A || epk_X_A) ||
|
|
* pk_DSA_A || epk_M_A || sig_DSA(dest_A || pk_Ed_A || epk_X_A || sig_Ed || pk_DSA_A || epk_M_A)
|
|
*
|
|
* Msg2 (Responder -> Initiator): LinkAccept
|
|
* dest_B || pk_Ed_B || epk_X_B || sig_Ed(pk_Ed_B || epk_X_B) ||
|
|
* pk_DSA_B || epk_M_B || sig_DSA(dest_B || pk_Ed_B || epk_X_B || sig_Ed || pk_DSA_B || epk_M_B)
|
|
*
|
|
* Key derivation:
|
|
* ss_X = X25519(esk_X_A, epk_X_B) [= X25519(esk_X_B, epk_X_A)]
|
|
* ss_M = SHA256("RNS-MLKEM-Hybrid-v1" || sort(epk_M_A, epk_M_B))
|
|
* combined = ss_X || ss_M
|
|
* session_key = HKDF(combined, salt=sort(dest_A,dest_B), info="rns-hybrid-link-keys")
|
|
*
|
|
* Msg3 (Initiator -> Responder): LinkProof [encrypted]
|
|
* HMAC(session_key, nonce)
|
|
*
|
|
* Msg4 (Responder -> Initiator): LinkComplete [encrypted]
|
|
* HMAC(session_key, nonce)
|
|
*
|
|
* Tamarin abstraction choices:
|
|
* - X25519 DH modeled via Tamarin's built-in 'diffie-hellman'
|
|
* - ML-DSA-65 modeled as abstract sign/verify function symbols
|
|
* - ML-KEM-768 contribution modeled as hash of both public keys
|
|
* (matches the actual protocol in deriveHybridSecret)
|
|
* - Ed25519 modeled via signing builtin
|
|
* - HKDF modeled as a hash function (one-way, collision-resistant)
|
|
* - Key confirmation via senc/sdec (symmetric encryption proxy for HMAC)
|
|
*
|
|
* Copyright (C) 2019-2025, Lux Industries Inc. All rights reserved.
|
|
*/
|
|
|
|
theory RNSHybridHandshake
|
|
begin
|
|
|
|
builtins: diffie-hellman, signing, hashing, symmetric-encryption
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Function symbols for post-quantum primitives
|
|
* ==================================================================
|
|
*/
|
|
|
|
functions:
|
|
/* ML-DSA-65 (post-quantum digital signature) */
|
|
mldsa_sign/2, /* mldsa_sign(message, sk_dsa) -> sigma_dsa */
|
|
mldsa_verify/3, /* mldsa_verify(message, sigma_dsa, pk_dsa) -> true/fail */
|
|
mldsa_pk/1, /* mldsa_pk(sk_dsa) -> pk_dsa */
|
|
|
|
/* ML-KEM-768 public key derivation (for the hash-based contribution) */
|
|
mlkem_pk/1, /* mlkem_pk(sk_kem) -> pk_kem */
|
|
|
|
/* Session key derivation from combined secrets.
|
|
* Models HKDF(ss_x || ss_m, salt, info). One-way (no equations). */
|
|
derive_session/3 /* derive_session(ss_x, ss_m, salt) -> session_key */
|
|
|
|
/* true/0 is provided by the 'signing' builtin */
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Equations
|
|
* ==================================================================
|
|
*/
|
|
|
|
equations:
|
|
/* ML-DSA verification succeeds with matching key */
|
|
mldsa_verify(m, mldsa_sign(m, sk), mldsa_pk(sk)) = true
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Restrictions (honest party behavior)
|
|
* ==================================================================
|
|
*/
|
|
|
|
/* Equality check helper */
|
|
restriction Eq:
|
|
"All x y #i. Eq(x, y) @ i ==> x = y"
|
|
|
|
/* Inequality check helper */
|
|
restriction Neq:
|
|
"All x y #i. Neq(x, y) @ i ==> not(x = y)"
|
|
|
|
/* Each party uses a unique identity -- no identity reuse across sessions */
|
|
restriction OncePerIdentity:
|
|
"All id s1 s2 #i #j. UsedIdentity(id, s1) @ i & UsedIdentity(id, s2) @ j
|
|
==> s1 = s2"
|
|
|
|
/* Hybrid mode requires both parties to have PQ keys */
|
|
restriction HybridNegotiation:
|
|
"All a b sid #i. HybridNegotiated(a, b, sid) @ i
|
|
==> (Ex #j #k. HasPQKey(a) @ j & HasPQKey(b) @ k & j < i & k < i)"
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Key generation rules
|
|
* ==================================================================
|
|
*/
|
|
|
|
/* Generate a hybrid identity (classical + PQ keys) */
|
|
rule Generate_Hybrid_Identity:
|
|
let
|
|
/* Classical: Ed25519 signing key */
|
|
pk_ed = pk(~sk_ed)
|
|
|
|
/* Post-quantum: ML-DSA-65 signing key */
|
|
pk_dsa = mldsa_pk(~sk_dsa)
|
|
|
|
/* Post-quantum: ML-KEM-768 static key (for identity binding) */
|
|
pk_kem = mlkem_pk(~sk_kem)
|
|
|
|
/* Destination hash: H(pk_ed || pk_dsa) */
|
|
dest = h(<pk_ed, pk_dsa>)
|
|
in
|
|
[ Fr(~sk_ed), Fr(~sk_dsa), Fr(~sk_kem) ]
|
|
--[ CreateIdentity($A, dest)
|
|
, HasPQKey($A)
|
|
]->
|
|
[ /* Long-term key state */
|
|
!LTK_Ed($A, ~sk_ed)
|
|
, !LTK_DSA($A, ~sk_dsa)
|
|
, !LTK_KEM($A, ~sk_kem)
|
|
, !PK_Ed($A, pk_ed)
|
|
, !PK_DSA($A, pk_dsa)
|
|
, !PK_KEM($A, pk_kem)
|
|
, !Destination($A, dest)
|
|
/* Publish public keys (attacker can see them) */
|
|
, Out(pk_ed)
|
|
, Out(pk_dsa)
|
|
, Out(pk_kem)
|
|
, Out(dest)
|
|
]
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Long-term key compromise (for forward secrecy analysis)
|
|
* ==================================================================
|
|
*/
|
|
|
|
/* Reveal Ed25519 long-term signing key */
|
|
rule Reveal_LTK_Ed:
|
|
[ !LTK_Ed($A, sk_ed) ]
|
|
--[ RevealEd($A) ]->
|
|
[ Out(sk_ed) ]
|
|
|
|
/* Reveal ML-DSA long-term signing key */
|
|
rule Reveal_LTK_DSA:
|
|
[ !LTK_DSA($A, sk_dsa) ]
|
|
--[ RevealDSA($A) ]->
|
|
[ Out(sk_dsa) ]
|
|
|
|
/* Reveal both long-term keys at once (full compromise) */
|
|
rule Reveal_LTK_Full:
|
|
[ !LTK_Ed($A, sk_ed), !LTK_DSA($A, sk_dsa) ]
|
|
--[ RevealFull($A), RevealEd($A), RevealDSA($A) ]->
|
|
[ Out(sk_ed), Out(sk_dsa) ]
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Hybrid handshake protocol
|
|
* ==================================================================
|
|
*
|
|
* Initiator (A) <-> Responder (B)
|
|
*
|
|
* A generates: esk_X_A (X25519 ephemeral), esk_M_A (ML-KEM ephemeral)
|
|
* B generates: esk_X_B (X25519 ephemeral), esk_M_B (ML-KEM ephemeral)
|
|
*
|
|
* Message 1 (A -> B): LinkRequest
|
|
* dest_A, pk_Ed_A, 'g'^esk_X_A, sig_Ed, pk_DSA_A, mlkem_pk(esk_M_A), sig_DSA
|
|
*
|
|
* Message 2 (B -> A): LinkAccept
|
|
* dest_B, pk_Ed_B, 'g'^esk_X_B, sig_Ed, pk_DSA_B, mlkem_pk(esk_M_B), sig_DSA
|
|
*
|
|
* Both compute:
|
|
* ss_X = 'g'^(esk_X_A * esk_X_B) [X25519 DH]
|
|
* ss_M = h('MLKEM', epk_M_A, epk_M_B) [ML-KEM hash]
|
|
* K = derive_session(ss_X, ss_M, <dest_A, dest_B>)
|
|
*
|
|
* Message 3 (A -> B): LinkProof = senc(proof_A, K)
|
|
* Message 4 (B -> A): LinkComplete = senc(proof_B, K)
|
|
*
|
|
* Both destroy esk_X_A, esk_X_B, esk_M_A, esk_M_B
|
|
*/
|
|
|
|
/* -- Msg1: Initiator sends LinkRequest -- */
|
|
rule Initiator_Send_Request:
|
|
let
|
|
/* Our public keys */
|
|
pk_ed_A = pk(sk_ed_A)
|
|
pk_dsa_A = mldsa_pk(sk_dsa_A)
|
|
dest_A = h(<pk_ed_A, pk_dsa_A>)
|
|
|
|
/* Ephemeral X25519 key pair */
|
|
epk_X_A = 'g'^~esk_X_A
|
|
|
|
/* Ephemeral ML-KEM key pair */
|
|
epk_M_A = mlkem_pk(~esk_M_A)
|
|
|
|
/* Classical portion to sign: pk_ed || epk_X */
|
|
classical_data = <pk_ed_A, epk_X_A>
|
|
|
|
/* Ed25519 signature on classical portion */
|
|
sig_ed_A = sign(classical_data, sk_ed_A)
|
|
|
|
/* Full data for ML-DSA signature (everything except sig_DSA itself) */
|
|
full_data = <dest_A, pk_ed_A, epk_X_A, sig_ed_A, pk_dsa_A, epk_M_A>
|
|
|
|
/* ML-DSA signature over full data */
|
|
sig_dsa_A = mldsa_sign(full_data, sk_dsa_A)
|
|
in
|
|
[ !LTK_Ed($A, sk_ed_A)
|
|
, !LTK_DSA($A, sk_dsa_A)
|
|
, !Destination($A, dest_A)
|
|
, Fr(~esk_X_A)
|
|
, Fr(~esk_M_A)
|
|
, Fr(~sid)
|
|
]
|
|
--[ InitiatorRequest($A, ~sid)
|
|
, UsedIdentity($A, ~sid)
|
|
]->
|
|
[ /* Send Msg1 */
|
|
Out(<'LinkRequest', dest_A, pk_ed_A, epk_X_A, sig_ed_A,
|
|
pk_dsa_A, epk_M_A, sig_dsa_A>)
|
|
, /* Store initiator state for Msg2 processing */
|
|
St_Init_1($A, ~sid, sk_ed_A, sk_dsa_A, ~esk_X_A, ~esk_M_A,
|
|
dest_A, pk_ed_A, epk_X_A, epk_M_A)
|
|
]
|
|
|
|
/* -- Msg2: Responder receives LinkRequest, sends LinkAccept -- */
|
|
rule Responder_Recv_Request_Send_Accept:
|
|
let
|
|
/* -- Parse incoming LinkRequest -- */
|
|
classical_data_A = <pk_ed_A, epk_X_A>
|
|
full_data_A = <dest_A, pk_ed_A, epk_X_A, sig_ed_A, pk_dsa_A, epk_M_A>
|
|
|
|
/* -- Our keys -- */
|
|
pk_ed_B = pk(sk_ed_B)
|
|
pk_dsa_B = mldsa_pk(sk_dsa_B)
|
|
dest_B = h(<pk_ed_B, pk_dsa_B>)
|
|
|
|
/* Ephemeral X25519 key pair */
|
|
epk_X_B = 'g'^~esk_X_B
|
|
|
|
/* Ephemeral ML-KEM key pair */
|
|
epk_M_B = mlkem_pk(~esk_M_B)
|
|
|
|
/* Classical portion to sign */
|
|
classical_data_B = <pk_ed_B, epk_X_B>
|
|
|
|
/* Ed25519 signature */
|
|
sig_ed_B = sign(classical_data_B, sk_ed_B)
|
|
|
|
/* Full data for ML-DSA signature */
|
|
full_data_B = <dest_B, pk_ed_B, epk_X_B, sig_ed_B, pk_dsa_B, epk_M_B>
|
|
|
|
/* ML-DSA signature */
|
|
sig_dsa_B = mldsa_sign(full_data_B, sk_dsa_B)
|
|
|
|
/* -- Derive the hybrid session key now --
|
|
* The responder already holds everything the key derivation needs:
|
|
* its own X25519 ephemeral secret (~esk_X_B), the initiator's X25519
|
|
* ephemeral public (epk_X_A from Msg1), and both ML-KEM ephemeral
|
|
* publics. So it computes K here (matching deriveHybridSecret in
|
|
* rns_link.go, which derives the key as soon as both shares are known)
|
|
* and carries it in its state, rather than reconstructing the DH
|
|
* product again in Msg4.
|
|
*/
|
|
ss_X = epk_X_A^~esk_X_B
|
|
ss_M = h(<'MLKEM', epk_M_A, epk_M_B>)
|
|
K = derive_session(ss_X, ss_M, <dest_A, dest_B>)
|
|
in
|
|
[ /* Receive Msg1 */
|
|
In(<'LinkRequest', dest_A, pk_ed_A, epk_X_A, sig_ed_A,
|
|
pk_dsa_A, epk_M_A, sig_dsa_A>)
|
|
, !LTK_Ed($B, sk_ed_B)
|
|
, !LTK_DSA($B, sk_dsa_B)
|
|
, !Destination($B, dest_B)
|
|
, /* Bind $A to the party that owns pk_ed_A */
|
|
!PK_Ed($A, pk_ed_A)
|
|
, Fr(~esk_X_B)
|
|
, Fr(~esk_M_B)
|
|
, Fr(~sid)
|
|
]
|
|
--[ /* Verify Ed25519 signature on classical portion */
|
|
Eq(verify(sig_ed_A, classical_data_A, pk_ed_A), true)
|
|
/* Verify ML-DSA signature on full data */
|
|
, Eq(mldsa_verify(full_data_A, sig_dsa_A, pk_dsa_A), true)
|
|
/* Protocol events */
|
|
, ResponderAccept($B, ~sid, dest_A)
|
|
, HybridNegotiated($B, $A, ~sid)
|
|
, UsedIdentity($B, ~sid)
|
|
]->
|
|
[ /* Send Msg2 */
|
|
Out(<'LinkAccept', dest_B, pk_ed_B, epk_X_B, sig_ed_B,
|
|
pk_dsa_B, epk_M_B, sig_dsa_B>)
|
|
, /* Store responder state (includes $A for authentication claims
|
|
* and the derived session key K) */
|
|
St_Resp_1($B, ~sid, sk_ed_B, sk_dsa_B, ~esk_X_B, ~esk_M_B,
|
|
dest_B, pk_ed_B, epk_X_B, epk_M_B,
|
|
dest_A, pk_ed_A, epk_X_A, epk_M_A, $A, K)
|
|
]
|
|
|
|
/* -- Msg3: Initiator receives LinkAccept, derives keys, sends LinkProof -- */
|
|
rule Initiator_Recv_Accept_Send_Proof:
|
|
let
|
|
/* -- Our public values: reused from St_Init_1 (the values we
|
|
* generated and stored in Msg1), not recomputed. pk_ed_A,
|
|
* pk_dsa_A, epk_X_A, epk_M_A are bound directly by the St_Init_1
|
|
* state fact below. -- */
|
|
|
|
/* -- Parse incoming LinkAccept -- */
|
|
classical_data_B = <pk_ed_B, epk_X_B>
|
|
full_data_B = <dest_B, pk_ed_B, epk_X_B, sig_ed_B, pk_dsa_B, epk_M_B>
|
|
|
|
/* -- Derive session key -- */
|
|
/* X25519 DH: g^(esk_X_A * esk_X_B) */
|
|
ss_X = epk_X_B^esk_X_A
|
|
|
|
/* ML-KEM contribution: commutative hash of both ephemeral ML-KEM public keys */
|
|
ss_M = h(<'MLKEM', epk_M_A, epk_M_B>)
|
|
|
|
/* Session key via HKDF */
|
|
salt = <dest_A, dest_B>
|
|
K = derive_session(ss_X, ss_M, salt)
|
|
in
|
|
[ /* Our state from Msg1 */
|
|
St_Init_1($A, sid, sk_ed_A, sk_dsa_A, esk_X_A, esk_M_A,
|
|
dest_A, pk_ed_A, epk_X_A, epk_M_A)
|
|
, /* Receive Msg2 */
|
|
In(<'LinkAccept', dest_B, pk_ed_B, epk_X_B, sig_ed_B,
|
|
pk_dsa_B, epk_M_B, sig_dsa_B>)
|
|
, /* Bind $B to the party that owns pk_ed_B */
|
|
!PK_Ed($B, pk_ed_B)
|
|
, Fr(~proof_A)
|
|
]
|
|
--[ /* Verify Ed25519 signature */
|
|
Eq(verify(sig_ed_B, classical_data_B, pk_ed_B), true)
|
|
/* Verify ML-DSA signature */
|
|
, Eq(mldsa_verify(full_data_B, sig_dsa_B, pk_dsa_B), true)
|
|
/* Protocol events */
|
|
, InitiatorDeriveKey($A, sid, K)
|
|
, HybridNegotiated($A, $B, sid)
|
|
/* Ephemeral key destruction (forward secrecy) */
|
|
, EphemeralDestroyed($A, sid, esk_X_A, esk_M_A)
|
|
]->
|
|
[ /* Send Msg3: encrypted proof */
|
|
Out(senc(<'LinkProof', ~proof_A>, K))
|
|
, /* Store state for Msg4 */
|
|
St_Init_2($A, sid, K, dest_A, dest_B, pk_ed_B, pk_dsa_B, $B)
|
|
]
|
|
|
|
/* -- Msg4: Responder receives LinkProof, confirms key, sends LinkComplete --
|
|
*
|
|
* The session key K was derived in Msg2 and is carried in St_Resp_1, so it
|
|
* is bound here directly from the responder's own state (no recomputation of
|
|
* the Diffie-Hellman shared secret in this rule). Receiving a LinkProof that
|
|
* decrypts under K is the responder's key-confirmation step.
|
|
*/
|
|
rule Responder_Recv_Proof_Send_Complete:
|
|
[ /* Our state from Msg2 (includes $A binding and the derived key K) */
|
|
St_Resp_1($B, sid, sk_ed_B, sk_dsa_B, esk_X_B, esk_M_B,
|
|
dest_B, pk_ed_B, epk_X_B, epk_M_B,
|
|
dest_A, pk_ed_A, epk_X_A, epk_M_A, $A, K)
|
|
, /* Receive Msg3: encrypted proof */
|
|
In(senc(<'LinkProof', proof_A>, K))
|
|
, Fr(~proof_B)
|
|
]
|
|
--[ /* Key confirmation: we could decrypt the proof */
|
|
ResponderDeriveKey($B, sid, K)
|
|
, KeyConfirmed($B, sid, K)
|
|
/* Ephemeral key destruction */
|
|
, EphemeralDestroyed($B, sid, esk_X_B, esk_M_B)
|
|
/* Running claim: B authenticated A and derived key K */
|
|
, RunningResponder($B, $A, sid, K)
|
|
]->
|
|
[ /* Send Msg4: encrypted complete */
|
|
Out(senc(<'LinkComplete', ~proof_B>, K))
|
|
, /* Session established */
|
|
!SessionKey($B, sid, K)
|
|
]
|
|
|
|
/* -- Initiator receives LinkComplete: session established --
|
|
*
|
|
* K is bound from St_Init_2 (stored in Msg3), so no DH reconstruction occurs
|
|
* in this rule.
|
|
*/
|
|
rule Initiator_Recv_Complete:
|
|
[ St_Init_2($A, sid, K, dest_A, dest_B, pk_ed_B, pk_dsa_B, $B)
|
|
, In(senc(<'LinkComplete', proof_B>, K))
|
|
]
|
|
--[ /* Key confirmation: both sides can encrypt/decrypt */
|
|
KeyConfirmed($A, sid, K)
|
|
/* Commit claim: A finished protocol with B */
|
|
, CommitInitiator($A, $B, sid, K)
|
|
/* Session established */
|
|
, SessionEstablished($A, $B, sid, K)
|
|
, Secret(K)
|
|
]->
|
|
[ !SessionKey($A, sid, K) ]
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Classical-only handshake (for downgrade analysis)
|
|
* ==================================================================
|
|
*
|
|
* A party without PQ keys falls back to X25519-only.
|
|
* We model this separately to prove no-downgrade when both have PQ keys.
|
|
*/
|
|
|
|
/* Generate a classical-only identity (no PQ keys) */
|
|
rule Generate_Classical_Identity:
|
|
let
|
|
pk_ed = pk(~sk_ed)
|
|
dest = h(pk_ed)
|
|
in
|
|
[ Fr(~sk_ed) ]
|
|
--[ CreateClassicalIdentity($A, dest)
|
|
/* Note: no HasPQKey action -- this party cannot do hybrid */
|
|
]->
|
|
[ !LTK_Ed_Classical($A, ~sk_ed)
|
|
, !PK_Ed_Classical($A, pk_ed)
|
|
, !Destination_Classical($A, dest)
|
|
, Out(pk_ed)
|
|
, Out(dest)
|
|
]
|
|
|
|
/* Classical-only handshake: no ML-DSA, no ML-KEM */
|
|
rule Classical_Initiator:
|
|
let
|
|
pk_ed_A = pk(sk_ed_A)
|
|
dest_A = h(pk_ed_A)
|
|
epk_X_A = 'g'^~esk_X_A
|
|
classical_data = <pk_ed_A, epk_X_A>
|
|
sig_ed_A = sign(classical_data, sk_ed_A)
|
|
in
|
|
[ !LTK_Ed_Classical($A, sk_ed_A)
|
|
, !Destination_Classical($A, dest_A)
|
|
, Fr(~esk_X_A)
|
|
, Fr(~sid)
|
|
]
|
|
--[ ClassicalInitiator($A, ~sid)
|
|
, IsClassicalSession(~sid)
|
|
]->
|
|
[ Out(<'ClassicalRequest', dest_A, pk_ed_A, epk_X_A, sig_ed_A>)
|
|
, St_Classical_Init($A, ~sid, sk_ed_A, ~esk_X_A, dest_A, pk_ed_A, epk_X_A)
|
|
]
|
|
|
|
rule Classical_Responder:
|
|
let
|
|
classical_data_A = <pk_ed_A, epk_X_A>
|
|
|
|
pk_ed_B = pk(sk_ed_B)
|
|
dest_B = h(pk_ed_B)
|
|
epk_X_B = 'g'^~esk_X_B
|
|
classical_data_B = <pk_ed_B, epk_X_B>
|
|
sig_ed_B = sign(classical_data_B, sk_ed_B)
|
|
|
|
ss_X = epk_X_A^~esk_X_B
|
|
K = derive_session(ss_X, 'no_pq', <dest_A, dest_B>)
|
|
in
|
|
[ In(<'ClassicalRequest', dest_A, pk_ed_A, epk_X_A, sig_ed_A>)
|
|
, !LTK_Ed_Classical($B, sk_ed_B)
|
|
, !Destination_Classical($B, dest_B)
|
|
, Fr(~esk_X_B)
|
|
, Fr(~sid)
|
|
]
|
|
--[ Eq(verify(sig_ed_A, classical_data_A, pk_ed_A), true)
|
|
, ClassicalResponder($B, ~sid, dest_A)
|
|
, ClassicalSessionKey($B, ~sid, K)
|
|
, IsClassicalSession(~sid)
|
|
]->
|
|
[ Out(<'ClassicalAccept', dest_B, pk_ed_B, epk_X_B, sig_ed_B>)
|
|
]
|
|
|
|
/*
|
|
* ==================================================================
|
|
* Security lemmas
|
|
* ==================================================================
|
|
*/
|
|
|
|
/*
|
|
* -- Lemma 1: Executability --
|
|
* The protocol can complete successfully (sanity check).
|
|
*/
|
|
lemma executability:
|
|
exists-trace
|
|
"Ex A B sid K #i.
|
|
SessionEstablished(A, B, sid, K) @ i"
|
|
|
|
/*
|
|
* -- Lemma 2: Session key secrecy --
|
|
* The attacker cannot learn the session key unless they compromise
|
|
* a long-term signing key of one of the participants BEFORE the session.
|
|
*
|
|
* Note: because keys are ephemeral, compromising long-term keys alone
|
|
* is not sufficient to derive the session key. But if the attacker
|
|
* impersonates a party (using their long-term key), they can MITM.
|
|
*/
|
|
lemma session_key_secrecy:
|
|
"All K #i.
|
|
Secret(K) @ i
|
|
==> ( not(Ex #j. K(K) @ j) )
|
|
| ( Ex A #r. RevealFull(A) @ r & r < i )"
|
|
|
|
/*
|
|
* -- Lemma 3: Mutual authentication --
|
|
* If A completes a session believing it talked to B,
|
|
* then B actually participated in a session with A.
|
|
* (Unless one of their signing keys was compromised.)
|
|
*/
|
|
lemma mutual_authentication:
|
|
"All A B sid K #i.
|
|
CommitInitiator(A, B, sid, K) @ i
|
|
==> ( Ex sid2 #j. RunningResponder(B, A, sid2, K) @ j & j < i )
|
|
| ( Ex #r. RevealEd(A) @ r )
|
|
| ( Ex #r. RevealDSA(A) @ r )
|
|
| ( Ex #r. RevealEd(B) @ r )
|
|
| ( Ex #r. RevealDSA(B) @ r )"
|
|
|
|
/*
|
|
* -- Lemma 4: Forward secrecy --
|
|
* Compromising long-term keys AFTER a session completes does NOT
|
|
* reveal the session key. This holds because:
|
|
* (a) X25519 ephemeral keys are destroyed after key derivation
|
|
* (b) ML-KEM ephemeral keys are destroyed after key derivation
|
|
* (c) Session key depends on ephemeral secrets, not long-term secrets
|
|
*/
|
|
lemma forward_secrecy:
|
|
"All A B sid K #i.
|
|
SessionEstablished(A, B, sid, K) @ i
|
|
==> ( not(Ex #j. K(K) @ j) )
|
|
| ( Ex #r. RevealFull(A) @ r & r < i )
|
|
| ( Ex #r. RevealFull(B) @ r & r < i )"
|
|
|
|
/*
|
|
* -- Lemma 5: No downgrade attack --
|
|
* If both parties have PQ keys, the session MUST use hybrid mode.
|
|
* An attacker cannot force a classical-only session between two
|
|
* PQ-capable parties.
|
|
*
|
|
* Proof sketch: classical session rules require !LTK_Ed_Classical
|
|
* facts, which are only produced by Generate_Classical_Identity
|
|
* (which does NOT emit HasPQKey). Hybrid identity rules produce
|
|
* !LTK_Ed (different fact name), so a PQ party cannot participate
|
|
* in classical sessions by construction.
|
|
*
|
|
* We verify this with two sub-lemmas:
|
|
* (a) No classical initiator has PQ keys
|
|
* (b) No classical responder has PQ keys
|
|
*/
|
|
lemma no_downgrade_initiator:
|
|
"All A sid #i.
|
|
ClassicalInitiator(A, sid) @ i
|
|
==> not(Ex #j. HasPQKey(A) @ j)"
|
|
|
|
lemma no_downgrade_responder:
|
|
"All B sid dest #i.
|
|
ClassicalResponder(B, sid, dest) @ i
|
|
==> not(Ex #j. HasPQKey(B) @ j)"
|
|
|
|
/*
|
|
* -- Lemma 6: Key confirmation (injective agreement) --
|
|
* If initiator A completes a session with B deriving key K,
|
|
* then B previously confirmed the same key K in a running session.
|
|
* This is the standard injective agreement pattern and implies
|
|
* both parties derived the same session key.
|
|
*/
|
|
lemma key_confirmation:
|
|
"All A B sid K #i.
|
|
CommitInitiator(A, B, sid, K) @ i
|
|
==> ( Ex sid2 #j. RunningResponder(B, A, sid2, K) @ j
|
|
& KeyConfirmed(B, sid2, K) @ j
|
|
& j < i )
|
|
| ( Ex #r. RevealEd(A) @ r )
|
|
| ( Ex #r. RevealDSA(A) @ r )
|
|
| ( Ex #r. RevealEd(B) @ r )
|
|
| ( Ex #r. RevealDSA(B) @ r )"
|
|
|
|
/*
|
|
* -- Lemma 7: Ephemeral key destruction --
|
|
* After a session is established, ephemeral keys have been destroyed.
|
|
* (Modeled as: the EphemeralDestroyed event occurs before SessionEstablished.)
|
|
*/
|
|
lemma ephemeral_destruction:
|
|
"All A B sid K #i.
|
|
SessionEstablished(A, B, sid, K) @ i
|
|
==> Ex esk_x esk_m #j. EphemeralDestroyed(A, sid, esk_x, esk_m) @ j & j < i"
|
|
|
|
/*
|
|
* -- Lemma 8: Session key uniqueness --
|
|
* Different sessions produce different keys (no key reuse).
|
|
*/
|
|
lemma session_key_uniqueness:
|
|
"All A1 B1 A2 B2 sid1 sid2 K #i #j.
|
|
( SessionEstablished(A1, B1, sid1, K) @ i
|
|
& SessionEstablished(A2, B2, sid2, K) @ j
|
|
)
|
|
==> #i = #j"
|
|
|
|
/*
|
|
* -- Lemma 9: Hybrid security (defense in depth) --
|
|
* The session key depends on BOTH the X25519 DH secret AND the ML-KEM
|
|
* contribution. An attacker who can break classical DH but not lattice
|
|
* problems (or vice versa) cannot derive the session key.
|
|
*
|
|
* This is an implicit property of the derive_session construction:
|
|
* K = derive_session(ss_X, ss_M, salt)
|
|
* where ss_X requires ECDH and ss_M requires knowledge of ML-KEM keys.
|
|
* Tamarin's symbolic model ensures this by construction -- ss_X and ss_M
|
|
* are both required inputs to derive_session, and derive_session is
|
|
* modeled as a one-way function (no reduction equations).
|
|
*
|
|
* We state this as: the attacker cannot learn K without knowing BOTH
|
|
* the X25519 ephemeral secret AND the ML-KEM ephemeral secrets.
|
|
*/
|
|
lemma hybrid_defense_in_depth:
|
|
"All A B sid K #i.
|
|
SessionEstablished(A, B, sid, K) @ i
|
|
==> not(Ex #j. K(K) @ j)
|
|
| ( Ex #r. RevealFull(A) @ r & r < i )
|
|
| ( Ex #r. RevealFull(B) @ r & r < i )"
|
|
|
|
/*
|
|
* -- Lemma 10: Identity binding --
|
|
* The session key is bound to both parties' identities via the
|
|
* destination hashes in the HKDF salt. An attacker cannot redirect
|
|
* a session key to a different pair of identities.
|
|
*/
|
|
lemma identity_binding:
|
|
"All A B sid K #i.
|
|
SessionEstablished(A, B, sid, K) @ i
|
|
==> Ex #j. InitiatorRequest(A, sid) @ j & j < i"
|
|
|
|
end
|