103 lines
2.4 KiB
Plaintext
103 lines
2.4 KiB
Plaintext
// 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
|
|
]
|