safing-jess/docs/key_establishment_dh.vp
2020-01-27 16:28:30 +01:00

51 lines
889 B
Text

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
]