Subject: [MLS] Authentication vulnerability in mls-03; better framing to the rescue

From: Richard Barnes <[email-masked]>
Date: Mon, 18 Feb 2019 17:22:28 -0500

Hey all,

Over the weekend, I drafted a proposed common framing layer that would
entail some changes to how authentication is done.  To make sure this
wasn't harmful, I build some Tamarin models this morning of the two-party
scenario in -03 and my proposed -04.  The bad news is that Tamarin pointed
out a weakness in -03; the good news is that the proposed -04 structure
fixes it, at least in the two-party case.

The vulnerability in -03 unfolds as follows [2]:

- Client A posts an InitKey
- Client B downloads the InitKey and constructs a Welcome and Add messages
- Attacker intercepts Welcome and Add
- Attacker creates a new Welcome message with his own InitKey, and replaces
the MAC on the Add message with one derived from his InitKey
- As a result:
  - Client B will encrypt messages to the attacker thinking they are
encrypting to Client A
  - Client B will never successfully receive a message, because the
attacker doesn't have Client A's private key, and Client A doesn't have the
encryption key.

This vulnerability arises because the Welcome message is too loosely
coupled to the Add message, allowing the init_key to be sent by someone
other than the sender of the Add.  There are two approaches to improving
this binding that seem to solve the problem (as verified by Tamarin):

a) Moving the confirmation MAC under the message signature [3]
b) Including a hash of the WelcomeInfo in the Add message [4]

(The former prevents the attacker from replacing the MAC; the latter the
Welcome message.) Option (a) was already included in PR#120; in addition to
fixing this problem, it makes for better parallelism between Application
and Handshake messages.  Option (b) also seems worth doing, since it gets
the Welcome into the transcript, and allows other participants to verify
that it was correct.

I've updated PR#120 to also include (b).  If folks have other thoughts on
that PR or this analysis, they would be helpful. Likewise, if anyone wanted
to take the Tamarin models linked below and extend them to larger cases (3
or 4 parties shouldn't be crazy), that would help give more confidence in
this change.

Thanks,
--Richard

[1] https://github.com/mlswg/mls-protocol/pull/120
[2] https://github.com/bifurcation/tamarin-ake/blob/master/mls-03.spthy
[3] https://github.com/bifurcation/tamarin-ake/blob/master/mls-04a.spthy
[4] https://github.com/bifurcation/tamarin-ake/blob/master/mls-04b.spthy