[Verifpal] Analysing Monokex

Sun Sep 15 12:47:26 CEST 2019

https://source.symbolic.software/verifpal/verifpal/commit/d582c154e26b74f65582c7e04a1fc82cdf695acc

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 15, 2019, at 12:43 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> 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.
>> 
> <x-active.vp>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal