[noise] Noise Explorer

Mon Jul 30 14:32:59 PDT 2018

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