[noise] Noise Explorer

Sat Aug 4 02:36:36 PDT 2018

Hello everyone,
In addition to the 13 PSK patterns added last week, the following five new
PSK patterns have been added today:

https://noiseexplorer.com/patterns/XKpsk3/
https://noiseexplorer.com/patterns/IXpsk2/
https://noiseexplorer.com/patterns/KKpsk0/
https://noiseexplorer.com/patterns/KKpsk2/
https://noiseexplorer.com/patterns/XXpsk3/

Enjoy the weekend,

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

On Tue, Jul 31, 2018 at 9:57 AM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/20180804/2c7807bb/attachment.html>