[noise] Noise Explorer

[Nadim Kobeissi]

Hello everyone,

An update to Noise Explorer is now live: https://noiseexplorer.com/.
Additions and changes:

     1. Noise Explorer now supports revision 34 of the Noise Protocol
Framework specification.
     2. The formal verification of 22 deferred patterns, except for IK1 and
KK1, are now available in the compendium section.
     3. Some minor improvements to the underlying software.

Some notes on the new formal verification results:

First, as noted, two of the 22 deferred patterns do not have their results
posted yet. This is because KK1 and IK1 take more CPU time to verify using
ProVerif. I'll update the compendium once this is done. It is only a
question of time.

Second, unlike the regular patterns, the deferred patterns are not
described in the specification with extra, "tokenless" message arrows
(which indicate protocol messages with no new key exchange or negotiation
operations.) Therefore, they do not appear in the compendium with tokenless
messages either.

If anyone would like me to add one or two "tokenless" message arrows to any
deferred pattern, and to re-run that particular entry in the compendium to
obtain formal verification results for a more comprehensive protocol run,
please let me know and I will do that: everything is fully automated, it
will just take me ten seconds to launch the formal verification job, and
the results will be posted automatically in Noise Explorer once all is
done. However, note that the more tokenless messages you ask me to add, the
longer ProVerif will take to verify the resulting model!

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office
On Tue, May 22, 2018 at 7:28 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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