// SPDX-FileCopyrightText: © 2026 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: CC-BY-NC-ND-4.0
//
// Expected at 1 session(s): c0c0c0c0a0a0a0a1a1e0; 2 session(s):
// c0c0c0c0a0a0a0a1a1e1. The private network identifier still blocks an
// attacker-selected hello key.

attacker[active]

principal Alice[
	knows private n
	knows private longterma
	generates ephemerala
	longtermapub = PUBKEY(longterma)
	ephemeralapub = PUBKEY(ephemerala)
]

principal Bob[
	knows private n
	knows private longtermb
	generates ephemeralb
	longtermbpub = PUBKEY(longtermb)
	ephemeralbpub = PUBKEY(ephemeralb)
]

Bob -> Alice: longtermbpub

principal Alice[
	nmacalice = MAC(n, ephemeralapub)
]

Alice -> Bob: ephemeralapub, nmacalice

principal Bob[
	nmacalicevalid = ASSERT(MAC(n, ephemeralapub), nmacalice)?
	nmacbob = MAC(n, ephemeralbpub)
]

Bob -> Alice: ephemeralbpub, nmacbob

principal Alice[
	nmacbobvalid = ASSERT(MAC(n, ephemeralbpub), nmacbob)?
	ephemeralsecretalice = DH_KEX(ephemeralbpub, ephemerala)
	longtermsecretalice = DH_KEX(longtermbpub, ephemerala)
	mastersecret1alice = HASH(n, ephemeralsecretalice, longtermsecretalice)
	sig1alice = SIGN(longterma, HASH(n, longtermbpub, ephemeralsecretalice))
	generates n1, n2
	secretbox1alice = AEAD_ENC(mastersecret1alice, n1, sig1alice, nil)
	secretbox2alice = AEAD_ENC(mastersecret1alice, n2, longtermapub, nil)
	longephemeralsecretalice = DH_KEX(ephemeralbpub, longterma)
	mastersecret2alice = HASH(n, ephemeralsecretalice, longtermsecretalice, longephemeralsecretalice)
]

Alice -> Bob: n1, secretbox1alice, n2, secretbox2alice

principal Bob[
	ephemeralsecretbob = DH_KEX(ephemeralapub, ephemeralb)
	longtermsecretbob = DH_KEX(ephemeralapub, longtermb)
	mastersecret1bob = HASH(n, ephemeralsecretbob, longtermsecretbob)
	sig1bob = AEAD_DEC(mastersecret1bob, n1, secretbox1alice, nil)?
	longtermapub_bob = AEAD_DEC(mastersecret1bob, n2, secretbox2alice, nil)?
	sig1valid = SIGNVERIF(longtermapub_bob, HASH(n, longtermbpub, ephemeralsecretbob), sig1bob)?
	longephemeralsecretbob = DH_KEX(longtermapub_bob, ephemeralb)
]

principal Bob[
	sig2bob = SIGN(longtermb, HASH(n, sig1bob, longtermapub_bob, ephemeralsecretbob))
	mastersecret2bob = HASH(n, ephemeralsecretbob, longtermsecretbob, longephemeralsecretbob)
	generates n3
	secretbox1bob = AEAD_ENC(mastersecret2bob, n3, sig2bob, nil)
]

Bob -> Alice: n3, secretbox1bob

principal Alice[
	knows private m1
	sig2alice = AEAD_DEC(mastersecret2alice, n3, secretbox1bob, nil)?
	sig2valid = SIGNVERIF(longtermbpub, HASH(n, sig1alice, longtermapub, ephemeralsecretalice), sig2alice)?
	generates n4
	secretboxm1alice = AEAD_ENC(mastersecret2alice, n4, m1, nil)
]

Alice -> Bob: n4, secretboxm1alice

principal Bob[
	knows private m2
	m1bob = AEAD_DEC(mastersecret2bob, n4, secretboxm1alice, nil)?
	generates n5
	secretboxm2bob = AEAD_ENC(mastersecret2bob, n5, m2, nil)
]

Bob -> Alice: n5, secretboxm2bob

principal Alice[
	m2alice = AEAD_DEC(mastersecret2alice, n5, secretboxm2bob, nil)?
]

queries[
	confidentiality? n
	confidentiality? m1
	confidentiality? m2
	confidentiality? longtermapub
	authentication? Alice -> Bob: secretbox1alice
	authentication? Alice -> Bob: secretbox2alice
	authentication? Bob -> Alice: secretbox1bob
	authentication? Alice -> Bob: secretboxm1alice
	authentication? Bob -> Alice: secretboxm2bob
	equivalence? mastersecret2alice, mastersecret2bob
]