[noise] Noise Explorer

[Trevor Perrin]

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

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