[Verifpal] Analysing Monokex

[Loup Vaillant David]

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: 2134 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190914/88f5ffd7/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: x-spec.md
Type: text/markdown
Size: 1635 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190914/88f5ffd7/attachment.md>