// SPDX-FileCopyrightText: © 2026 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: CC-BY-NC-ND-4.0
//
// Expected at 1 session(s): c1c0a0e0; 2 session(s): c1c0a0e0. Only the
// transmitted ciphertext is public; a passive attacker cannot substitute the
// keys.

attacker[passive]

principal Alice[
	generates a
	ga = PUBKEY(a)
]

Alice -> Bob: ga

principal Bob[
	knows private m1
	generates b, n1
	gb = PUBKEY(b)
	ss_a = DH_KEX(ga, b)
	e1 = AEAD_ENC(ss_a, n1, m1, gb)
]

Bob -> Alice: gb, n1, e1

principal Alice[
	ss_b = DH_KEX(gb, a)
	e1_dec = AEAD_DEC(ss_b, n1, e1, gb)?
]

queries[
	confidentiality? e1
	confidentiality? m1
	authentication? Bob -> Alice: e1
	equivalence? ss_a, ss_b
]