attacker[active]

principal Client[
	generates e1
	ge1 = G^e1
]

principal Server[
	knows private s
	generates se
	gse = G^se
	gs = G^s
	gseSignature = SIGN(s, gse)
]

Server -> Client: [gs], gse, gseSignature

principal Client[
	_ = SIGNVERIF(gs, gse, gseSignature)?
	knows private msg1
	s1c = gse^e1
	enc1 = AEAD_ENC(s1c, msg1, HASH(gs, gse, ge1))
]

Client -> Server: ge1, enc1

principal Server[
	s1s = ge1^se
	dec1 = AEAD_DEC(s1s, enc1, HASH(gs, gse, ge1))?
	generates e2
	s2s = ge1^e2
	ge2 = G^e2
	s3s = HKDF(s1s, s2s, nil)
	knows private msg2
	enc2 = AEAD_ENC(s3s, msg2, HASH(gs, gse, ge1, ge2))
]

Server -> Client: ge2, enc2

principal Client[
	s2c = ge2^e1
	s3c = HKDF(s1c, s2c, nil)
	dec2 = AEAD_DEC(s3c, enc2, HASH(gs, gse, ge1, ge2))?
]

queries[
	confidentiality? msg1
	confidentiality? msg2
	authentication? Client -> Server: enc1
	authentication? Server -> Client: enc2 
]