153 lines
5.2 KiB
Text
153 lines
5.2 KiB
Text
(* 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))
|