[noise] Noise Explorer

Tue Aug 21 02:08:15 PDT 2018

Hello everyone,
A Noise Explorer paper now exists:
https://eprint.iacr.org/2018/766

Your feedback is welcome!

Best regards,

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

On Sat, Aug 4, 2018 at 11:36 AM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/20180821/5057545f/attachment.html>