[noise] Noise Explorer

[Nadim Kobeissi]

Hello everyone,

PSK patterns are starting to enter the Noise Explorer compendium! 13 new
patterns have been added, all PSK patterns:

https://noiseexplorer.com/patterns/Npsk0/
https://noiseexplorer.com/patterns/Kpsk0/
https://noiseexplorer.com/patterns/Xpsk1/
https://noiseexplorer.com/patterns/NNpsk0/
https://noiseexplorer.com/patterns/NNpsk2/
https://noiseexplorer.com/patterns/NKpsk0/
https://noiseexplorer.com/patterns/NKpsk2/
https://noiseexplorer.com/patterns/NXpsk2/
https://noiseexplorer.com/patterns/XNpsk3/
https://noiseexplorer.com/patterns/KNpsk0/
https://noiseexplorer.com/patterns/KNpsk2/
https://noiseexplorer.com/patterns/INpsk1/
https://noiseexplorer.com/patterns/INpsk2/

I hope to add more PSK patterns with time.

Have a great summer, everyone,

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


On Fri, Jul 27, 2018 at 5:48 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/20180730/ccfb5bdd/attachment.html>