// SPDX-FileCopyrightText: © 2026 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: CC-BY-NC-ND-4.0
//
// Expected at 1 session(s): c0a0; 2 session(s): c1a0. A cross-role key
// substitution exposes the hybrid secret when another run reaches the shared
// classical-key leak.

attacker[active]

principal Alice[
	knows private alongterm
	galongterm = PUBKEY(alongterm)
]

principal Bob[
	knows public info
	knows private blongterm, bs, dkb
	generates bo
	gblongterm = PUBKEY(blongterm)
	gbs = PUBKEY(bs)
	gbo = PUBKEY(bo)
	ekb = PUBKEY(dkb)
	gbssig = SIGN(blongterm, gbs)
	ekbsig = SIGN(blongterm, ekb)
]

Bob -> Alice: [gblongterm], gbs, gbssig, gbo, ekb, ekbsig

principal Alice[
	generates m1, ae1, r
	gae1 = PUBKEY(ae1)
	valid = SIGNVERIF(gblongterm, gbs, gbssig)?
	kvalid = SIGNVERIF(gblongterm, ekb, ekbsig)?
	ss, ct = KEM_ENCAP(ekb, r)
	akm = HASH(DH_KEX(gbs, alongterm), DH_KEX(gblongterm, ae1), DH_KEX(gbs, ae1), DH_KEX(gbo, ae1), ss)
	amaster = HKDF(nil, akm, info)
	generates n_e1
	e1 = AEAD_ENC(amaster, n_e1, m1, HASH(galongterm, gblongterm, gae1))
]

Alice -> Bob: [galongterm], gae1, ct, n_e1, e1

principal Bob[
	bss = KEM_DECAP(dkb, ct)
	bkm = HASH(DH_KEX(galongterm, bs), DH_KEX(gae1, blongterm), DH_KEX(gae1, bs), DH_KEX(gae1, bo), bss)
	bmaster = HKDF(nil, bkm, info)
	m1_d = AEAD_DEC(bmaster, n_e1, e1, HASH(galongterm, gblongterm, gae1))?
]

phase[1]

principal Alice[
	leaks alongterm, ae1
]

principal Bob[
	leaks blongterm, bs, bo
]

queries[
	confidentiality? m1
	authentication? Alice -> Bob: e1
]