[messaging] KCI in X3DH

[Ximin Luo]

Hi Trevor,

On the ART paper near the end it mentions: "we use the X3DH paper [..] extended to include the static-static DH key in order to prevent UKS and KCI attacks".

After some digging we came across this part from [1]: "When [..] Bob’s long-term secret key [..] [and] pre-key is also compromised, ProVerif finds [..] a novel key compromise impersonation attack"

Indeed, in this case the attacker can generate a new fake A-eph "from Alice" and compute X3DH(Alice, Bob) via

Alice[public static] ^ Bob[private prekey] ||
Fake-Alice[public eph] ^ Bob[private static] ||
Fake-Alice[private eph] ^ Bob[public prekey]

The defence is to turn X3DH into "X4DH", with an additional DH(Alice[static], Bob[static]) in there. I know one explicit goal of X3DH was to retain deniability and I think this extra step does not compromise that, so perhaps it is worth updating the X3DH spec [2]?

(Another possible defense is to require Alice to sign each ephemeral key but that would allow passive attackers to confirm that she is the initiator of the session given only the ciphertext.)

I'd guess how most implementations work today is that the static-secret and the prekey-secrets are stored in pretty much the same place, so I think compromising both is roughly as-feasible as compromising just the static-secret. In other words, if we consider that KCI in the latter (only-static) case is worth defending against, then we should also consider defending against KCI in the former case where both are compromised.

OTOH, I'm still uncertain how including the static-static DH key "prevents UKS" which AFAIU is just a rebranded key-identity binding validation attack, that you can't really solve cryptographically but need a proper PKI for. (Various sources suggest hashing in identity-related data into the material being authenticated as an opportunistic but potentially-ineffective countermeasure, which does makes sense.) It would be good if the ART paper authors could comment on this part to clarify.

X

[1] Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach, 
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet

[2] https://signal.org/docs/specifications/x3dh/#key-compromise

-- 
GPG: ed25519/56034877E1F87C35
GPG: rsa4096/1318EFAC5FBBDBCE
https://github.com/infinity0/pubkeys.git