[noise] Noise Explorer

[Nadim Kobeissi]

Dear Trevor,

Thank you for your interest!

I am committed to keeping Noise Explorer in sync with the latest revision
of the Noise specification. Once revision 34 is published, you will within
a short time see an update to the Noise Explorer stack targeting revision
34, and the revision 33 stack will be discontinued, taken offline and no
longer supported. The same will happen with every revision.

The deferred patterns in revision 34 are an excellent target for analysis,
and their analysis results will be rolled out with the revision 34 update
to Noise Explorer.

Regarding the automation of security result generation: this is already
implemented and you yourself can generate the results using the Noise
Explorer command-line tool, available on the website.

The issue, however, is that formal verification with ProVerif can take a
very long time when you have an active attacker, three principals (one
malicious) and 11 queries for every single message. This is why I actually
built my own ProVerif verification rig specifically for this purpose, and
it's certainly been breaking a sweat to output these results.

So, while you can certainly obtain the analysis results yourself for a
pattern such as NK within 10 minutes using Noise Explorer on your laptop,
something like IK took 42 hours even on my dedicated hardware.

What I can commit to do from my end is to always keep the Noise Explorer
website up to date for any pattern that you include in any Noise
specification revision, including these recent deferred pattern and any
upcoming pattern. You can also personally suggest some arbitrary pattern
you think is important, and I will run the tests on my local dedicated
verification rig and post on Noise Explorer the ProVerif model and results,
as is currently the case with the revision 33 examples.

With regards to the results we have already, they match the ones in your
existing table, but are more nuanced since we added two more authenticity
grades (3 and 4), since our security model includes a compromised principal.

Identity hiding is also something that I plan to take a closer look at very
soon.

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


On Tue, May 22, 2018 at 5:45 PM Trevor Perrin <trevp at trevp.net> wrote:

> On Tue, May 22, 2018 at 9:42 AM, Nadim Kobeissi <nadim at symbolic.software>
> wrote:
> > Please access Noise Explorer using this address:
> https://noiseexplorer.com
> >
> > Regarding the compendium of patterns included on the website, I also
> request
> > that you send me additional Noise Handshake Patterns, so that I can use
> > Noise Explorer to generate formal models, pretty HTML results, and then
> post
> > these too in the compendium
>
> Hey Nadim,
>
> Looks fascinating, I'm looking forward to spending some time with
> this.  We're on the verge of publishing spec revision 34 (I was
> supposed to do it last week, but will try to find time this week).
>
> This introduces 22 new "deferred" patterns, so those would be a
> perfect target for more analysis.  We'd like to ensure that the
> deferred patterns eventually achieve the same security as the
> "fundamental" pattern they're based on, for one thing.
>
> https://github.com/noiseprotocol/noise_spec/blob/rev34/output/noise.pdf
>
> I'd also like to double-check these results against the spec's
> security properties tables, and see if we can generate similar tables
> for the new patterns, it would be great to have that automated.
>
> And if you were really ambitious, the "identity hiding" properties
> would be great to have automated analysis for, but I'm sure that's
> more complicated.
>
> Trevor
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20180522/103b0ecb/attachment.html>