// SPDX-FileCopyrightText: © 2019-2022 Nadim Kobeissi <nadim@symbolic.software> 
// SPDX-License-Identifier: GPL-3.0-only
// (included in our artifact as a reference model)

attacker[active]

principal Alice[
	knows private alongterm
	galongterm = G^alongterm
]

principal Bob[
	knows private blongterm, bs
	generates bo
	gblongterm = G^blongterm
	gbs = G^bs
	gbo = G^bo
	gbssig = SIGN(blongterm, gbs)
]

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

principal Alice[
	generates ae1
	gae1 = G^ae1
	amaster = HASH(gbs^alongterm, gblongterm^ae1, gbs^ae1, gbo^ae1)
	arkba1, ackba1 = HKDF(amaster, nil, nil)
]

principal Alice[
	generates m1, ae2
	gae2 = G^ae2
	_ = SIGNVERIF(gblongterm, gbs, gbssig)?
	akshared1 = gbs^ae2
	arkab1, ackab1 = HKDF(akshared1, arkba1, nil)
	akenc1, _ = HKDF(MAC(ackab1, nil), nil, nil)
	e1 = AEAD_ENC(akenc1, m1, HASH(galongterm, gblongterm, gae2))
]

Alice -> Bob: [galongterm], gae1, gae2, e1

principal Bob[
	bmaster = HASH(galongterm^bs, gae1^blongterm, gae1^bs, gae1^bo)
	brkba1, bckba1 = HKDF(bmaster, nil, nil)
]

principal Bob[
	bkshared1 = gae2^bs
	brkab1, bckab1 = HKDF(bkshared1, brkba1, nil)
	bkenc1, bkenc2 = HKDF(MAC(bckab1, nil), nil, nil)
	m1_d = AEAD_DEC(bkenc1, e1, HASH(galongterm, gblongterm, gae2))
]

principal Bob[
	generates m2, be
	gbe = G^be
	bkshared2 = gae2^be
	brkba2, bckba2 = HKDF(bkshared2, brkab1, nil)
	bkenc3, bkenc4 = HKDF(MAC(bckba2, nil), nil, nil)
	e2 = AEAD_ENC(bkenc3, m2, HASH(gblongterm, galongterm, gbe))
]

Bob -> Alice: gbe, e2

principal Alice[
	akshared2 = gbe^ae2
	arkba2, ackba2 = HKDF(akshared2, arkab1, nil) 
	akenc3, akenc4 = HKDF(MAC(ackba2, nil), nil, nil)
	m2_d = AEAD_DEC(akenc3, e2, HASH(gblongterm, galongterm, gbe))
]

// principal Alice[
// 	generates m3, ae3
// 	gae3 = G^ae3
// 	akshared3 = gbe^ae3
// 	arkab3, ackab3 = HKDF(akshared3, arkba2, nil)
// 	akenc5, akenc6 = HKDF(MAC(ackab3, nil), nil, nil)
// 	e3 = AEAD_ENC(akenc5, m3, HASH(gblongterm, galongterm, gae3))
// ]

// Alice -> Bob: gae3, e3

// principal Bob[
// 	bkshared3 = gae3^be
// 	brkab3, bckab3 = HKDF(bkshared3, brkba2, nil)
// 	bkenc5, bkenc6 = HKDF(MAC(bckab3, nil), nil, nil)
// 	m3_d = AEAD_DEC(bkenc5, e3, HASH(gblongterm, galongterm, gae3))
// ]

phase[1]

principal Alice[leaks alongterm]
principal Bob[leaks blongterm]

queries[
	confidentiality? m1
	authentication? Alice -> Bob: e1
	confidentiality? m2
	authentication? Bob -> Alice: e2
	// confidentiality? m3
	// authentication? Alice -> Bob: e3
]