Created
December 31, 2019 01:44
-
-
Save nocko/81295813d06ba7b84bf37c00af6666d3 to your computer and use it in GitHub Desktop.
Verifpal model of Salt Channel w/ Cert auth used in Poseidon BLE protocol
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
attacker[active] | |
principal FactoryAuth [ | |
knows private w // "wearable key" | |
gw = G^w | |
] | |
principal FacilityAuth [ | |
knows private f // "facility key" | |
gf = G^f | |
] | |
// Wearable | |
principal Server [ | |
knows public c0 // Unused AD | |
knows private s // Long-term server key | |
gs = G^s // Server public key | |
] | |
// Panel | |
principal Client [ | |
knows public c0 | |
knows private c // Long-term client key | |
gc = G^c // Client public key | |
generates ec // Ephemeral client key | |
m1 = G^ec // Ephemeral client public key | |
] | |
//// Pre-arranged key sharing happens here; assumed that attacker cannot observe | |
// Factory Auth reads/signs wearable public | |
Server -> FactoryAuth: [gs] | |
principal FactoryAuth [ | |
server_cert = SIGN(w, gs) | |
] | |
FactoryAuth -> Server: [server_cert] | |
FactoryAuth -> Client: [gw] // Panel knows Factory Auth public key | |
// Facility Auth reads/signs panel public | |
Client -> FacilityAuth: [gc] | |
principal FacilityAuth [ | |
client_cert = SIGN(f, gc) | |
] | |
FacilityAuth -> Client: [client_cert] | |
FacilityAuth -> Server: [gf] // Wearable knows facility public key | |
//// Door panel exchange starts here - The attacker lives here and all trafic is read/writeable to them | |
Client -> Server: m1 | |
principal Server [ | |
generates es | |
m2 = G^es // This is m2 | |
shared_s = m1^es | |
// M3 Encrypts the server public and | |
m3a = AEAD_ENC(shared_s, gs, c0) | |
m3b = AEAD_ENC(shared_s, SIGN(s, HASH(m1, m2)), c0) | |
] | |
Server -> Client: m2, m3a, m3b | |
principal Client [ | |
shared_c = m2^ec | |
gs_dec = AEAD_DEC(shared_c, m3a, c0)? | |
m3b_dec = AEAD_DEC(shared_c, m3b, c0)? | |
valid_c = SIGNVERIF(gs_dec, HASH(m1, m2), m3b_dec)? | |
m4a = AEAD_ENC(shared_c, gc, c0) | |
m4b = AEAD_ENC(shared_c, SIGN(c, HASH(m1, m2)), c0) | |
] | |
Client -> Server: m4a, m4b | |
principal Server [ | |
gc_dec = AEAD_DEC(shared_s, m4a, c0)? | |
m4b_dec = AEAD_DEC(shared_s, m4b, c0)? | |
valid_s = SIGNVERIF(gc_dec, HASH(m1, m2), m4b_dec)? | |
s_cert_enc = AEAD_ENC(shared_s, server_cert, c0) | |
] | |
Server -> Client: s_cert_enc | |
principal Client [ | |
s_cert = AEAD_DEC(shared_c, s_cert_enc, c0)? | |
valid_s_cert = SIGNVERIF(gw, gs_dec, s_cert)? | |
c_cert_enc = AEAD_ENC(shared_c, client_cert, c0) | |
generates pt1 | |
req = AEAD_ENC(shared_c, pt1, c0) | |
] | |
Client -> Server: c_cert_enc, req | |
principal Server [ | |
c_cert = AEAD_DEC(shared_s, c_cert_enc, c0)? | |
valid_c_cert = SIGNVERIF(gf, gc_dec, c_cert)? | |
pt1_dec = AEAD_DEC(shared_s, req, c0)? | |
generates pt2 | |
resp = AEAD_ENC(shared_s, pt2, c0) | |
] | |
Server -> Client: resp | |
principal Client [ | |
pt2_dec = AEAD_DEC(shared_c, resp, c0)? | |
] | |
queries[ | |
// The long-term private keys aren't revealed | |
confidentiality? s | |
confidentiality? c | |
confidentiality? w | |
confidentiality? f | |
// The M3 only depends on m1 & m2; so only messages m4 and later can be authenticated | |
authentication? Client -> Server: m4a | |
authentication? Client -> Server: m4b | |
authentication? Client -> Server: c_cert_enc | |
authentication? Server -> Client: s_cert_enc | |
authentication? Client -> Server: req | |
authentication? Server -> Client: resp | |
confidentiality? pt1 | |
confidentiality? pt2 | |
] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment