[noise] Noise Explorer

Tue Jul 31 00:57:55 PDT 2018

Things are looking fine now!

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

On Mon, Jul 30, 2018 at 11:32 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> Hold on, these results don't look completely right. Sorry, I think I
> pushed them too early. I'll send another email once I figure things out.
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
>
> On Mon, Jul 30, 2018 at 11:23 PM Nadim Kobeissi <nadim at symbolic.software>
> wrote:
>
>> 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/20180731/9aac8f4d/attachment.html>