(* 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))