[noise] Noise Explorer

Tue Jun 12 10:17:33 PDT 2018

 Hello everyone,

The reason for my silence on Noise Explorer was that I've been stuck on a
very tricky issue with the formal models for the past two weeks: generating
a model that captures an unbounded number of sessions executed in parallel
of the Noise Handshake Pattern between the parties (Alice, Bob and
Charlie), with a fresh, distinct new ephemeral for everyone in every one of
these unbounded number of sessions.

This was very difficult (for me, at least,) because of two reasons:
    1. Describing this particular scenario, given that Noise does not
really contain a notion of session IDs or similar, proved quite difficult
to do in the applied pi calculus for reasons that I won't go into here (if
you think you know of an easy way, you're wrong, I tried every darn way for
12 days and can assure you that it includes the one you're thinking of!)
The difficulty of doing this was what led me to send my previous half-baked
analysis -- at some point I got lost in the torrent of output that I was
getting from all the different models I was experimenting with, and was
misled by an output that illustrated a result we had already discussed but
in a very different way. Thanks, Trevor, for your correction.
    2. Struggling to ensure that it doesn't result in a performance hit
that makes the verification of even the simplest Handshake Patterns not
terminate.

After many, many days of effort and testing, I'm very relieved to be able
to tell you now that I've resolved the issue for good. Effectively, the
performance hit is I believe around 30%, and we're back to obtaining sane
security results. Best of all, the models are now really strong: fresh
ephemerals on an unbounded number of sessions! Better handling and modeling
of keys, including PSKs! Better modeling of tokenless messages! And more.

According to the results so far, the results currently available in the
Noise specification are again matched result-for-result and there is no
longer a perceived difference, as I misleadingly argued in my previous long
email to the mailing list. However, the tests are still not finished for
every model, but will likely be finished tomorrow (c.f.
https://imgur.com/a/hiAmPpM)

By tomorrow I should have all the results. I personally expect them to
match the ones currently on Noise Explorer (and in the specification on
Trevor's website.) But you never know, hence why we're doing this whole
thing anyway.

Working on this project has been incredibly fun and rewarding. Most
especially solving this particular issue, which is the most trouble I've
ever had with ProVerif!

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office

On Thu, May 31, 2018 at 8:09 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> Dear Trevor,
>
> I don't think you're missing something. Your response, I think, is fully
> correct.
>
> Indeed, I think that I sent my previous email while in the middle of a
> thread of thought, under the pretense that I was in fact at the end of it.
>
> Bear with me as I sort these models out -- it is normal, I suppose, for
> one to make such an error after a certain very large amount of time is
> spent staring at generated protocol models.
>
> I am currently working more on improving the separation between unbounded
> sessions (which is proving to be nontrivial). I will have more well-formed
> contributions for you as well as, I hope, a concrete proposal for a new
> security model in the coming days.
>
> Thank you for your patience,
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
>
> On Thu, May 31, 2018 at 7:10 PM Trevor Perrin <trevp at trevp.net> wrote:
>
>> Hi Nadim,
>>
>> Thanks for digging into this, I'd definitely like to make sure the
>> spec's description of security properties aligns with Noise Explorer.
>>
>> Comments below -
>>
>>
>> On Thu, May 31, 2018 at 10:19 AM, Nadim Kobeissi
>> <nadim at symbolic.software> wrote:
>> > -------------------------------------------------------------
>> > SECTION II: Changes Apparent in our Analysis and Thoughts on Security
>> Grades
>> > in the Noise Specification
>> > -------------------------------------------------------------
>> >
>> > Because of the improvements discussed earlier, it is now easier to
>> > illustrate, using the formal verification process itself that underlies
>> > Noise Explorer, why the security grades described in the Noise
>> specification
>> > are problematic. This is something that was alluded to previously in
>> this
>> > thread, but I believe was not fully elaborated upon.
>> >
>> > For example, consider the following pattern:
>> >
>> > IN
>> >   -> e, s              0                0
>> >   <- e, ee, se         0                3
>> >   ->                   2                1
>> >   <-                   0                5
>> >
>> > According to the Noise specification (and indeed to the earlier, less
>> > precise analysis of Noise Explorer), message C in IN benefits from the
>> > following level of authenticity:
>> >> "2: Sender authentication resistant to key-compromise impersonation
>> (KCI).
>> >> The sender authentication is based on an ephemeral-static DH ("es" or
>> "se")
>> >> between the sender's static key pair and the recipient's ephemeral key
>> pair.
>> >> Assuming the corresponding private keys are secure, this authentication
>> >> cannot be forged."
>> >
>> > However, this does not make total sense: as we can now observe in our
>> > ProVerif analysis, when we arrive at message C:
>> > Alice has executed the following key mixing operations: mixHash(e),
>> > mixHash(s), mixHash(re), mixKey(ee), mixKey(se)
>> > Bob has executed the following key mixing operations: mixHash(e),
>> > mixHash(s), mixHash(re), mixKey(ee), mixKey(se)
>> >
>> > Based on the above, we can see that an attacker man-in-the-middling the
>> > ephemerals can then convince Bob that a message that Alice had sent to
>> > Charlie was indeed meant to be for Bob.
>>
>> I don't follow - Bob will only accept Alice's 3rd message if it's
>> based on his (Bob's) ephemeral.  If Charlie is another honest party in
>> the "Bob" role, the same will be true for Charlie.
>>
>>
>> > Bob can be led to accept this
>> > message as originating by Alice and meant for him without issue.
>>
>> Any 3rd message accepted by Bob will indeed by originated by Alice and
>> meant for him (in the sense of being based on his - Bob's -
>> ephemeral).  The grade #2 seems like an accurate description of this
>> property.
>>
>> As best as I can tell, you're describing an "attacker" (Charlie?) who
>> simply functions as a wire, and relays messages without changing them
>> between Alice and Bob.  But this attacker doesn't break the described
>> security properties, so this just seems like a re-statement of the
>> security model (message transmission is under the control of the
>> attacker).
>>
>> But maybe I'm missing something?
>>
>> Trevor
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20180612/127bdd7c/attachment.html>