[noise] Noise Explorer

[Nadim Kobeissi]

Hello everyone,

I am pleased to announce that we now have 26 of the 38 patterns in the
compendium available with the new analysis (the rest are on the way):
https://noiseexplorer.com/patterns/

As far as I can see, all results match what is expected. I invite Trevor to
check this.

I am also very pleased to announce a wonderful new feature: Detailed
Analysis for Noise Message Patterns.
In addition to producing pleasant and pedagogical renders of formal
verification results for Noise Handshake Patterns, Noise Explorer can now
do the same for individual Message Patterns within these handshake patterns!

Here's how you can use this feature:
    1. Access any pattern's results. For example:
https://noiseexplorer.com/patterns/XX1/
    2. In the results description, click on "Show detailed analysis" next
to any message.
    3. For example, if you access the detailed analysis for Message C of
the XX1 pattern: https://noiseexplorer.com/patterns/XX1/C.html

I am very excited about this feature, as I think it begins to demonstrate
the true pedagogical potential that I believe Noise Explorer has. This is
the direction I've intended for Noise Explorer since the beginning: look at
the valuable insight and learning that we can automatically generate from
formal verification results, themselves automatically generated from formal
models, themselves automatically generated from the Noise Handshake
Patterns! I believe that the next generation of cryptography students will
surely benefit from Noise Explorer specifically due to this sort of
direction.

I look forward for your feedback on this new feature. It's possible you may
spot some inaccuracies or typos: please let me know if you do.

Best regards,

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


On Tue, Jun 12, 2018 at 7:38 PM Trevor Perrin <trevp at trevp.net> wrote:

>
> On Tue, Jun 12, 2018 at 5:17 PM, Nadim Kobeissi <nadim at symbolic.software>
> wrote:
>
>>
>> After many, many days of effort and testing, I'm very relieved to be able
>> to tell you now that I've resolved the issue for good. Effectively, the
>> performance hit is I believe around 30%, and we're back to obtaining sane
>> security results. Best of all, the models are now really strong: fresh
>> ephemerals on an unbounded number of sessions! Better handling and modeling
>> of keys, including PSKs! Better modeling of tokenless messages! And more.
>>
>
> Nice!, I hope this produces a paper at some point, I'd definitely like to
> understand more of these nuances and modelling.
>
> Anyways, of course let us know when this run finishes up, I definitely
> want to double-check it against the rev34 draft before releasing.
>
> Trevor
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20180613/cb6ace77/attachment.html>