214 lines
7.6 KiB
Text
214 lines
7.6 KiB
Text
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(<key_a, key_b, ck>) ]
|
|
|
|
|
|
/* ================= 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
|