[noise] Noise Explorer

[Nadim Kobeissi]

Dear Trevor,

In general, and especially with recent ProVerif model optimizations, I now
believe that most models won't take very long. However, X1X1 still took
about 30 hours to verify (and was consuming 15+GB RAM at its peak) and just
finished this morning. Last week, IK took 42 hours, so there are some
outliers. In general, though, I think we're in a very good spot now, and
most likely I can verify most things quicker than, say, a few weeks ago,
when I was still optimizing the ProVerif model generation to create more
verification-efficient models and setting up my local verification
hardware. So yes, I think we can be more optimistic about verification
times going forward!

>   * There should be 34 patterns, so I think you've got one typo pattern
(there's a "K").

Regarding K, I decided to add a one-way handshake pattern because why not?
I took it from the original specification. You can see the results here:
https://noiseexplorer.com/patterns/K.noise.html

> You could filter out the tokenless messages if they don't have different
security properties from the previous handshake message.  At least, that's
how the Noise spec presents it.

It's okay, perhaps it's better to display them once a user clicks to access
the full result in Noise Explorer, just for completeness. I am imagining
scenarios where, for example, a telecom agency wants to design a local
protocol to address an internal use case. They open Noise Explorer and,
before, attempting to create their own Noise Handshake Pattern, explore the
compendium to see if they can find a pattern that suits their needs. Once
they find a candidate pattern, most likely they will benefit more from a
verbose description (even if this is less useful in the specification.)

> Our numeric grades are still a little unharmonized, but I'll keep that
discussion in a separate thread.

I tried my best to explain my viewpoint on this in the email I sent
yesterday. I'm happy to discuss this further!

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office
On Fri, May 25, 2018 at 9:27 AM Trevor Perrin <trevp at trevp.net> wrote:

> Very nice!  Give Bruno thanks.  Seems like these runs aren't taking as
> long as we thought?

> Anyways, looks like the deferred patterns end up with the same
> properties as their fundamental pattern, which is a good sanity-check.
> I'll look for better checks, in next day or so.  It will also be easy
> for me to extract this information into a table for the rev34 spec, so
> thanks for that contribution.

> Minor nits:
>   * There should be 34 patterns, so I think you've got one typo pattern
> (there's a "K").
>   * You could filter out the tokenless messages if they don't have
> different security properties from the previous handshake message.  At
> least, that's how the Noise spec presents it.
>   * Our numeric grades are still a little unharmonized, but I'll keep
> that discussion in a separate thread.


> Trevor


> On Fri, May 25, 2018 at 6:50 AM, Nadim Kobeissi <nadim at symbolic.software>
wrote:
> > Hello everyone,
> >
> > Good news: the temporary verification issue has been addressed (with
> > sincere thanks to Bruno Blanchet for his help) -- and now all 35
patterns
> > have two "tokenless" messages in their compendium verification results!
> >
> > To explore these new results, go to the Noise Explorer website and
click on
> > "Explore Patterns" in the navigation menu: https://noiseexplorer.com
> >
> > Nadim Kobeissi
> > Symbolic Software • https://symbolic.software
> > Sent from office
> > On Fri, May 25, 2018 at 8:16 AM Nadim Kobeissi <nadim at symbolic.software>
> > wrote:
> >
> >> Hello everyone,
> >
> >> I'm pleased to announce that Noise Explorer now includes formal
> >> verification results with two "tokenless" messages for 28 of its 35
> >> compendium entries.
> >> Due to some constraints in ProVerif that we are currently investigating
> > and
> >> that we hope to soon remedy, some patterns had to be temporarily
> > restricted
> >> to only one "tokenless" message, while one pattern could not have any
> >> "tokenless" messages at all.
> >
> >>       - Patterns that still have only one "tokenless" message: NK,
K1N, XN,
> >> I1N, NK1, NX (6 in total.)
> >>       - Patterns that do not have any "tokenless" messages: NX1 (1 in
> > total.)
> >>       - Patterns that now have two "tokenless" messages: everything
else
> > (28
> >> in total.)
> >
> >> To explore these new results, go to the Noise Explorer website and
click
> > on
> >> "Explore Patterns" in the navigation menu: https://noiseexplorer.com
> >
> >> Nadim Kobeissi
> >> Symbolic Software • https://symbolic.software
> >> Sent from office
> >
> >> On Thu, May 24, 2018 at 7:30 PM Nadim Kobeissi <nadim at symbolic.software

> >> wrote:
> >
> >> > Dear Trevor,
> >
> >> > Here is the exact text of the grades in question in today's Noise
> >> > specification:
> >
> >> > Authenticity grade 1: "Sender authentication vulnerable to
> > key-compromise
> >> > impersonation (KCI). The sender authentication is based on a
> > static-static
> >> > DH ("ss") involving both parties' static key pairs. If the
recipient's
> >> > long-term private key has been compromised, this authentication can
be
> >> > forged. Note that a future version of Noise might include signatures,
> >> which
> >> > could improve this security property, but brings other trade-offs."
> >
> >> > Authenticity grade 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."
> >
> >> > The issue lies in that the above two paragraphs do not specify
whether
> >> > there is an opening for a malicious principal to mess with things.
> > Observe
> >> > message C in the following two results:
> >
> >> > https://noiseexplorer.com/patterns/KN.noise.html
> >> > https://noiseexplorer.com/patterns/IK.noise.html
> >
> >> > In IK, message C is resistant to key compromise impersonation even if
> > its
> >> > sender (the initiator) negotiates a separate session in parallel
with a
> >> > compromised principal Charlie, who is controlled by the attacker
> >> > unbeknownst to the sender.
> >
> >> > In KN, message C is also resistant to key compromise impersonation,
but
> >> > unlike message C in IK, this property does not hold if Charlie also
> > enters
> >> > the fray in a similar manner.
> >
> >> > In the current Noise specification, both KN and IK are given the
similar
> >> > grade for authenticity. That is the problem and the reason for the
> >> expanded
> >> > authenticity grading system. In Noise Explorer's system, grades 3
and 4
> >> > essentially are short hand for "1 and 2 but with maintained key
> > compromise
> >> > impersonation resistance even when negotiating with a compromised
> >> > principal."
> >
> >> > Now, I understand your suggestion with regards to pairing these
grades
> >> with
> >> > corresponding confidentiality queries, but this raises two questions
in
> > my
> >> > mind:
> >
> >> > 1. The confidentiality queries in question are written and
formalized to
> >> > deal with message secrecy and forward secrecy two properties that do
not
> >> at
> >> > all touch upon authenticity. Shouldn't we strive to therefore
working on
> >> > separating these properties formally?
> >
> >> > 2. There is also the question of reduced precision. Instead of having
> >> > authenticity grades "1, 3-5" and grade "2, 3-5", why not settle for a
> >> > system where we obtain precise grades for authenticity, independently
> > from
> >> > having to look at a confidentiality/message secrecy/forward secrecy
> >> result?
> >
> >> > Nadim Kobeissi
> >> > Symbolic Software • https://symbolic.software
> >> > Sent from office
> >> > On Thu, May 24, 2018 at 6:10 PM Trevor Perrin <trevp at trevp.net>
wrote:
> >
> >> > > On Thu, May 24, 2018 at 12:05 PM, Nadim Kobeissi
> >> > > <nadim at symbolic.software> wrote:
> >> > > > Hello everyone,
> >> > > > I've been following up on all of these discussions very closely,
but
> >> > have
> >> > > > not said anything because I've been working furiously on getting
all
> >> the
> >> > > > formal results for all 22 deferred patterns *with* two
"tokenless"
> >> > messages
> >> > > > out. I'm afraid that with the addition of two "tokenless"
messages
> > to
> >> > every
> >> > > > single model, the cost of verification increases dramatically.
> > Things
> >> > are
> >> > > > still going to take quite a long time -- I wish we weren't
nearing
> >> > June, at
> >> > > > least I'd have a use for the free radiators I now have in my
> > apartment
> >> > due
> >> > > > to this -- quite a lot of finely tuned dedicated hardware is now
> >> dealing
> >> > > > with the formal verification load.
> >> > > >
> >> > > > An important clarification: Trevor says the following:
> >> > > >> Thinking more on rev34, it would probably be irresponsible to
> > publish
> >> > > >> *without* security tables for all the deferred patterns...  So
I'd
> >> > > >> love to work out how to get your output processed into some
tables
> >> > > >> like the current ones (or possibly changed around a bit,
depending
> > on
> >> > > >> that discussion).  Or really: for you to work that out, so I
could
> >> > > >> just copy-and-paste :-)....
> >> > > >
> >> > > > Trevor, the security tables for 20 of the deferred patterns are
> >> already
> >> > > > available on Noise Explorer's website. They simply do not include
> > the
> >> > > > "tokenless" messages. Just a note in the event that you missed
that.
> >> :-)
> >> > > >
> >> > > > Regarding the discussions on security properties, I'm personally
> >> > currently
> >> > > > satisfied with the recognition that any deferred pattern that
opens
> >> up a
> >> > > > potential UKS attack will simply never qualify towards
authenticity
> >> > grades
> >> > > > 3 and 4 (as defined by Noise Explorer) and will always be
restricted
> >> to
> >> > a
> >> > > > maximum of 1 or 2 (as defined by Noise Explorer, see my previous
> > email
> >> > > > where I list a "very quick summary" of the additions to the
> >> authenticity
> >> > > > properties.)
> >
> >> > > Hmm, the way I think about it, no patterns should ever open up a
> >> > > potential UKS attack?  Also, the deferred patterns should end up
with
> >> > > the same properties as their corresponding fundamental pattern,
since
> >> > > they perform the same operations.
> >
> >> > > Looking more closely at your numeric grades, I think your two new
> >> > > authentication grade numbers just correspond to the Noise
> >> > > authentication grades 0-2, except you use 2 new numbers based on
the
> >> > > confidentiality grade it's being paired with:
> >
> >> > > ("NE" for Noise Explorer):
> >
> >> > > NE 0 -> spec(0, 0-2)
> >> > > NE 1 -> spec(1, 0-2)
> >> > > NE 2 -> spec(2, 0-2)
> >> > > NE 3 -> spec(1, 3-5)
> >> > > NE 4 -> spec(2, 3-5)
> >
> >> > > In other words, I don't think these new NE grades encode new
> >> > > information.  So I'm not yet convinced they improve things versus
the
> >> > > Noise spec's system, seems like we could map your 3->1, and your
4->2,
> >> > > and bring things into alignment?
> >
> >> > > Trevor