[noise] Noise Explorer

[Nadim Kobeissi]

Hello again everyone,
I hope you are all enjoying the summer and not wrestling the proverbial
bear that is a Ph.D. thesis draft.

I am writing to report some new developments with Noise Explorer.

1. New Validation Rules.
After the discussion/Gentleman's Disagreement Between Cryptography
Enthusiasts in an earlier thread [0], revision 34 of the Noise
specification was updated with a clarified validation rule in Section 7.3,
rule 4:
> After performing a DH between a remote public key (either static or
ephemeral) and the local static key, the local party must not call
ENCRYPT() unless it has also performed a DH between its local ephemeral key
and the remote public key. In particular, this means that (using canonical
notation):
>     * After an "se" token, the initiator must not send a handshake
payload or transport payload unless there has also been an "ee" token.
>     * After an "ss" token, the initiator must not send a handshake
payload or transport payload unless there has also been an "es" token.
>     * After an "es" token, the responder must not send a handshake
payload or transport payload unless there has also been an "ee" token.
>     *After an "ss" token, the responder must not send a handshake payload
or transport payload unless there has also been an "se" token.

These new validation rules, along with some minor fixes to existing rules,
have now been implemented in Noise Explorer.

2. Download ProVerif Models Directly from Compendium Entry.
You can now go to a compendium entry, for example [1], and immediately
generate and download the ProVerif models from there.

3. Bug Fixes and Typos.
The most misleading fixed typo was that the "detailed analysis" pages
sometimes referred to strong forward secrecy as weak forward secrecy. This,
along with less meaningful typos, were fixed.

4. All 38 Patterns.
Also, Noise Explorer's compendium has had the full results for all 38
patterns for many weeks now, I somehow forgot to announce that here. This
is not new at all, I simply forgot to mention it on this mailing list.

What a better world we now all share due to these improvements!

Best regards,

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

References:
[0] https://moderncrypto.org/mail-archive/noise/2018/001722.html
[1] https://noiseexplorer.com/patterns/IK/


On Wed, Jun 13, 2018 at 11:00 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/20180727/7ae5be43/attachment.html>