[noise] Noise Explorer

[Nadim Kobeissi]

On Fri, May 25, 2018 at 10:14 AM Trevor Perrin <trevp at trevp.net> wrote:

> On Fri, May 25, 2018 at 7:45 AM, Nadim Kobeissi <nadim at symbolic.software>
wrote:
> > 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.

> That's wild, that such tiny protocols can contain that much complexity...


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

> Oh, OK.  It threw me off that there weren't other one-way patterns.

> With one-way patterns there will never be additional messages, so you
> shouldn't list the tokenless messages (and the security properties
> being claimed for those messages don't make sense - e.g. it says the
> "response" message would be in cleartext, but I'm not sure why).

ProVerif is detecting that the post-session compromise of the responder's
static key (the sender of message B) would lead to message B being
decryptable. Should this still satisfy confidentiality grade 1 in your view?


> If you're going to do K, maybe also do the other two?  N and X are
> probably the more useful one-way patterns (e.g. in NLS, which is our
> attempt at a more user-friendly set of "profiles", NoiseAnonBox uses N
> and NoiseAuthBox uses X).

> Trevor