193 lines
6.9 KiB
Text
193 lines
6.9 KiB
Text
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(<rk, ss, 'rk'>)
|
|
ek = h(<rk, ss, 'ek'>)
|
|
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(<rk, ss, 'rk'>)
|
|
ek = h(<rk, ss, 'ek'>)
|
|
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(<rk, ss, 'rk'>)
|
|
ek = h(<rk, ss, 'ek'>)
|
|
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(<rk, ss, 'rk'>)
|
|
ek = h(<rk, ss, 'ek'>)
|
|
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(<rk, ss, 'ek'>) → 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
|