[Verifpal] Analysing Monokex

Sat Sep 14 14:32:28 CEST 2019

Dear Loup,

Thank you very much for this exceptionally insightful email (I know I’ve addressed such thanks before, but I mean it every time!)

To start with, I think that the correct result (and the result that 0.6.7 gives) for your model is the following:

 “Result! authentication? I -> R: ie: ie, sent by Attacker and not by I and resolving to G^attacker_0, is successfully
 used in primitive HASH(_h2, ie) in R's state"

If you remove the check on `ASSERT(_T1, T1)`, then you’ll obtain the further result you were looking for:

  "Result! s1, sent by I and resolving to ENC(k1, is), is successfully used in primitive DEC(HASH(HASH(HASH(HASH(HASH(pid, G^r)), G^attacker_0), G^attacker_0^r), one), ENC(HASH(HASH(HASH(HASH(HASH(pid, G^r)), G^attacker_0), G^r^e), one), G^i)) in R's state, despite it being vulnerable to tampering by Attacker”

Unlike 0.6.4, this only happens if the check on `ASSERT(_T1, T1)` is removed, and this is exactly what I’ve been intending since 0.6.4, but I’ve been again and again side-railed by my own bugs and required fixes — hopefully no more:

- 0.6.4 was supposed to give you the second result only if you uncheck`ASSERT(_T1, T1)`, but gave both results always.
- 0.6.6 went too far in the other direction, not giving any result unless you uncheck `ASSERT(_T1, T1)`.
- 0.6.7 I hope fixes things once and for all when it comes to this more nuanced take on authentication queries.

You see, this is how I think we can best and most naturally express your “trustworthiness” property. Here’s what I want to know: is this sufficient for you to get your “trustworthiness” in authentication? From my reading of your email, it should be, and I really hope so because it would mean that I was able to address your use case without making the language more complicated. However your email is quite dense and I suspect that I might not have captured your requirements completely. So, if I’m wrong, please tell me, explain what the current solution misses, and let me know what you would see as a further improvement.

Regarding “oracle exposure”, this would be a really big new thing for Verifpal, and I don’t think we should start looking into it until we are done with things like authentication and forward secrecy giving us expected results. Once we start working on oracles, we start entering computational model territory (i.e. the territory of tools like CryptoVerif); oracles aren’t something that are natural to capture in symbolic model of formal verification. So let’s not go there until we are on solid footing here (at the very least, it deserves a separate email thread from authentication stuff!) But I do agree that this is an excellent direction to investigate and I do want us to look into it soon.

> 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.

Very, very, true. I remain committed to working with you on arriving to the best compromise for illustrating authentication in Verifpal, while keeping to the project’s mission of having a simple language for modeling.

Thanks again Loup for your wonderful contributions.

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

> On Sep 14, 2019, at 12:37 AM, Loup Vaillant David <loup at loup-vaillant.fr> 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><x-spec.md>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal