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