Skip to content

Instantly share code, notes, and snippets.

@nocko
Created December 31, 2019 01:44
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save nocko/81295813d06ba7b84bf37c00af6666d3 to your computer and use it in GitHub Desktop.
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
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