[Verifpal] Analysing Monokex

[Loup Vaillant David]

Errata: The model was not quite right. I just noticed that the specs
did not match my reference implementation: it has a couple extraneous
hashes when no payload is present. Here is the corrected model.

Loup.




On Sat, 2019-09-14 at 00:37 +0200, Loup Vaillant David wrote:
> Hi,
> 
> Sorry for the long email, but this is one of those where I question
> everything.
> 
> ---
> 
> At last, we are using Verifpal for something practical: the Noise
> inspired authenticated key exchange protocol I've been working on for
> 10 months.
> 
> More specifically, Mike <tankf33der at disroot.org> has given me a model
> for the X pattern, which I have modified a bit (mainly to add the
> queries).
> 
> At a high level, the X pattern is basically the same as Noise X
> pattern: it's a one way pattern, aimed at stuff like file encryption,
> mail encryption, where the only thing we can do is encrypt some
> stuff,
> then send it, without the recipient ever responding, without any
> special infrastructure (not even something like Signal).
> 
> Technical details are provided in the attached model and specs.
> 
> I believe this model will provide interesting tests, mostly because
> security isn't perfect:
> 
> - It is vulnerable to key compromise impersonation
> - It is vulnerable to replay attacks
> - It does not have full forward secrecy
> 
> And there's something more, that is shared by most patterns (both
> Monokex and Noise): the authentication of some data is *delayed*.
> Here's how it works:
> 
> - We start from an initial (public hash)
> - IE mixed into the hash
> - es is computed, and mixed into the hash
> - An encryption key (and a new hash) is extracted from the hash
> - IS is encrypted
> - The encrypted IS is mixed into the hash
> - An authentication tag (and a new hash) is extracted from the hash
> 
> At this point, we have an encrypted and authenticated IS. But so far
> it
> only has been authenticated with IE, which the attacker could have
> sent.
> 
> - ss is computed, and mixed into the hash
> - An authentication tag (and a new hash) is extracted from the hash
> 
> At this point (if my protocol is properly designed) the transcript
> (including IS and IE) have been authenticated. We *know* at this
> point
> that Alice is who she says she is (modulo key compromise or replay).
> 
> - The session key is the last hash
> - The message is sent, using the session key
> - (The message sends a message back, but we shouldn't)
> 
> 
> Now let's question everything.
> 
> As expected, Verifpal didn't catch any serious attack. What's a bit
> surprising is that version 0.6.4 *did* catch that IS and IE weren't
> quite authenticated (they are successfully used at a time they are
> vulnerable to attacker tampering).  Note that 0.6.6 misses that
> attack.
> 
> I wonder, though: should IS and IE be considered not authenticated?
> Because at first, they're decidedly *not*. Their authenticity is only
> confirmed later. And as far as I know, that's okay.
> 
> This illustrates a problem I've had with the way authentication
> queries
> are done for a long time. Unlike confidentiality, we don't care that
> a
> particular piece of message was authenticated. What we actually care
> about is whether the values derived from them are trustworthy, *when*
> they become trustworthy, and the absence of exploitable oracles
> (assuming reasonable implementations).
> 
> Right now, to know which authentication query I have to write, I
> can't
> just pick a constant and query whether it was safely derived. I have
> to
> manually trace back where it comes from exactly, and when one of its
> ancestor is a message from another principal, I query *that*. This is
> error prone, and lacks some granularity.
> 
> In the X pattern summed up above, I don't really care whether the
> initiator's ephemeral key, or even its encrypted static key, are
> authenticated. What I do care about is that by the time the recipient
> has processed everything, the *session key* is trustworthy. That, and
> oracles.
> 
> So yes, the pieces of message I ask the authenticity of, are
> successfully used at a time they aren't authenticated just yet.
> That's
> okay, under (correct me If I'm wrong) exactly two conditions:
> 
> - They *are* authenticated at a later point
> - They don't expose some oracle before that point.
> 
> What then, would count as an oracle? In practice it depends. Mostly,
> that would be variable time primitives. Diffie Hellman key exchanges
> for instance can exit early if the public key is invalid. Libsodium
> for
> instance validates the public key before the actual X25519 scalar
> multiplication. Monocypher however is unconditionally constant time.
> 
> Such an oracle was the death of an earlier version of Monokex. I used
> to omit intermediate authentication tags, and only check the very
> last
> one, at the end of each message. I assumed that every operations
> would
> be constant time, even with input from the attacker. Thus no oracle,
> and no way to leak information.
> 
> With Monocypher or TweetNaCl, I would be correct. Libsodium's X25519
> however exits early when the public key is all zero. So the attacker
> could guess which key was sent, XOR that with the relevant
> ciphertext,
> and see whether the other party responds early. If they did, the
> decrypted key becomes all zero, which is invalid and triggers an
> early
> return, which is detectable through a timing side channel.
> 
> Oops.
> 
> Another thing, is that we can hardly expect the model to model
> everything. Imagine you're doing some protocol, and are using zero
> RTT.
> Problem is, the first message is such that it is vulnerable to
> tampering. On the third message though, we can confirm *after the
> fact*
> that the first message was legit after all (assuming we authenticate
> the whole transcript).
> 
> What's a protocol user to do with this? Well, the zero RTT payload
> may
> be used in a way that doesn't exposes oracles, and then we would have
> to wait for the third message before we fully trust it. Many such use
> cases will be out of Verifpal's scope (and rightly so).
> 
> I would like to query not the authenticity of messages, but the
> trustworthiness of the constants derived from them. I would like to
> query that trustworthiness *at several points* of the protocol. For
> instance:
> 
>     Alice -> Bob : msg, tag
>     principal Bob [
>         query trustworthy? msg  // clearly not
>         _tag = MAC(key, msg)
>         _    = ASSERT(_tag, tag)
>         query trustworthy? msg  // now we should be good
>     ]
> 
> It should work also when the constant is derived from a message. For
> instance:
> 
>     Alice -> Bob : msg, tag
>     principal Bob [
>         digest =
> HASH(msg)
>         query trustworthy? digest  // nope
>         _tag   =
> MAC(key, msg)
>         _      = ASSERT(_tag, tag)
>         query
> trustworthy? digest  // now we should be good
>     ]
> 
> No need to track the authenticity of `msg` specifically, I only care
> about its derived value.
> 
> 
> Then there's the Oracle Problem. Let's take the last example above:
> we
> are hashing `msg` *before* it becomes trustworthy. If the HASH
> primitive happens to expose exploitable oracles, we should be warned
> about.
> 
> Except in practice, most hashes work in constant time, and using them
> on untrustworthy values won't reveal anything. Same goes for modern
> decryption primitives, though I wouldn't bet my life on that. And
> exponentiation can definitely expose an oracle, but not always
> (depends
> on the implementation).
> 
> Here's what I think: we should expand the concept of "guard" to
> values
> inside primitives.  That is, if I write this:
> 
>     digest = HASH(foo, [bar], baz)
> 
> then it's a promise that even if `bar` is attacker controlled,
> directly
> or indirectly, this particular use of HASH will still not leak any
> information. (Typically that's a promise of being constant time, but
> in
> some circumstances, it might be constant energy as well, or even
> constant radiation).
> 
> ---
> 
> To sum it up, we may want to break down authentication into a
> trustworthiness part, and an Oracle susceptibility part.  It would
> make
> authentication queries more transparent, as well as easier to get
> right.
> 
> Confidentiality is the easy one: once the protocol is complete,
> values
> are either known by the attacker, or they're not. It's a global
> property, that holds for any particular constant. Authentication
> however is much more context dependent. They should not be treated
> the
> same way.
> 
> Loup.
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: x-active.vp
Type: text/x-csrc
Size: 2218 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190915/a1d5812a/attachment.c>