<div dir="ltr">Hello everyone,<div>A Noise Explorer paper now exists:</div><div><a href="https://eprint.iacr.org/2018/766">https://eprint.iacr.org/2018/766</a></div><div><br></div><div>Your feedback is welcome!</div><div><br></div><div>Best regards,</div><div><br clear="all"><div><div dir="ltr" class="gmail_signature"><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Sat, Aug 4, 2018 at 11:36 AM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hello everyone,</div><div>In addition to the 13 PSK patterns added last week, the following five new PSK patterns have been added today:</div><div><br></div><div><a href="https://noiseexplorer.com/patterns/XKpsk3/" target="_blank">https://noiseexplorer.com/patterns/XKpsk3/</a></div><div><a href="https://noiseexplorer.com/patterns/IXpsk2/" target="_blank">https://noiseexplorer.com/patterns/IXpsk2/</a></div><div><a href="https://noiseexplorer.com/patterns/KKpsk0/" target="_blank">https://noiseexplorer.com/patterns/KKpsk0/</a></div><div><a href="https://noiseexplorer.com/patterns/KKpsk2/" target="_blank">https://noiseexplorer.com/patterns/KKpsk2/</a></div><div><a href="https://noiseexplorer.com/patterns/XXpsk3/" target="_blank">https://noiseexplorer.com/patterns/XXpsk3/</a></div><div><br></div><div>Enjoy the weekend,<br></div><div><br></div><div><div><div dir="ltr" class="m_1832962632052654871gmail_signature"><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Jul 31, 2018 at 9:57 AM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Things are looking fine now!</div><div><br></div><div><div><div dir="ltr" class="m_1832962632052654871m_1744697882307673134gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 30, 2018 at 11:32 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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.<br></div><div><br></div><div><div><div dir="ltr" class="m_1832962632052654871m_1744697882307673134m_4188073113407555655gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 30, 2018 at 11:23 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hello everyone,</div><div><br></div><div>PSK patterns are starting to enter the Noise Explorer compendium! 13 new patterns have been added, all PSK patterns:</div><div><br></div><div><a href="https://noiseexplorer.com/patterns/Npsk0/" target="_blank">https://noiseexplorer.com/patterns/Npsk0/</a></div><div><a href="https://noiseexplorer.com/patterns/Kpsk0/" target="_blank">https://noiseexplorer.com/patterns/Kpsk0/</a></div><div><a href="https://noiseexplorer.com/patterns/Xpsk1/" target="_blank">https://noiseexplorer.com/patterns/Xpsk1/</a></div><div><a href="https://noiseexplorer.com/patterns/NNpsk0/" target="_blank">https://noiseexplorer.com/patterns/NNpsk0/</a></div><div><a href="https://noiseexplorer.com/patterns/NNpsk2/" target="_blank">https://noiseexplorer.com/patterns/NNpsk2/</a></div><div><a href="https://noiseexplorer.com/patterns/NKpsk0/" target="_blank">https://noiseexplorer.com/patterns/NKpsk0/</a></div><div><a href="https://noiseexplorer.com/patterns/NKpsk2/" target="_blank">https://noiseexplorer.com/patterns/NKpsk2/</a></div><div><a href="https://noiseexplorer.com/patterns/NXpsk2/" target="_blank">https://noiseexplorer.com/patterns/NXpsk2/</a></div><div><a href="https://noiseexplorer.com/patterns/XNpsk3/" target="_blank">https://noiseexplorer.com/patterns/XNpsk3/</a></div><div><a href="https://noiseexplorer.com/patterns/KNpsk0/" target="_blank">https://noiseexplorer.com/patterns/KNpsk0/</a></div><div><a href="https://noiseexplorer.com/patterns/KNpsk2/" target="_blank">https://noiseexplorer.com/patterns/KNpsk2/</a></div><div><a href="https://noiseexplorer.com/patterns/INpsk1/" target="_blank">https://noiseexplorer.com/patterns/INpsk1/</a></div><div><a href="https://noiseexplorer.com/patterns/INpsk2/" target="_blank">https://noiseexplorer.com/patterns/INpsk2/</a><br></div><div><br></div><div>I hope to add more PSK patterns with time.</div><div><br></div><div>Have a great summer, everyone,<br></div><div><br></div><div><div><div dir="ltr" class="m_1832962632052654871m_1744697882307673134m_4188073113407555655m_-3375498491096418805gmail_signature"><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Jul 27, 2018 at 5:48 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hello again everyone,<br>I hope you are all enjoying the summer and not wrestling the proverbial bear that is a Ph.D. thesis draft.<br><br>I am writing to report some new developments with Noise Explorer.<br><br>1. New Validation Rules.<br>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:<br>> 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):<br>> * After an "se" token, the initiator must not send a handshake payload or transport payload unless there has also been an "ee" token.<br>> * After an "ss" token, the initiator must not send a handshake payload or transport payload unless there has also been an "es" token.<br>> * After an "es" token, the responder must not send a handshake payload or transport payload unless there has also been an "ee" token.<br><div>> *After an "ss" token, the responder must not send a handshake payload or transport payload unless there has also been an "se" token.</div><div><br></div><div>These new validation rules, along with some minor fixes to existing rules, have now been implemented in Noise Explorer.<br></div><br><div>2. Download ProVerif Models Directly from Compendium Entry.<br></div><div>You can now go to a compendium entry, for example [1], and immediately generate and download the ProVerif models from there.<br></div><div><br></div><div>3. Bug Fixes and Typos.</div><div>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.<br></div><div><br></div><div>4. All 38 Patterns.<br></div><div>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.</div><div><br></div><div>What a better world we now all share due to these improvements!</div><div><br></div><div>Best regards,<br></div><div><br></div>Nadim Kobeissi<br>Symbolic Software • <a href="https://symbolic.software" target="_blank">https://symbolic.software</a><br><div>Sent from office</div><div><br></div><div> References:<br><div>[0] <a href="https://moderncrypto.org/mail-archive/noise/2018/001722.html" target="_blank">https://moderncrypto.org/mail-archive/noise/2018/001722.html</a></div><div>[1] <a href="https://noiseexplorer.com/patterns/IK/" target="_blank">https://noiseexplorer.com/patterns/IK/</a></div> <br></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Jun 13, 2018 at 11:00 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hello everyone,</div><div><br></div><div>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): <a href="https://noiseexplorer.com/patterns/" target="_blank">https://noiseexplorer.com/patterns/</a><br></div><div><br></div><div>As far as I can see, all results match what is expected. I invite Trevor to check this.</div><div><br></div><div>I am also very pleased to announce a wonderful new feature: Detailed Analysis for Noise Message Patterns.</div><div>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!</div><div><br></div><div>Here's how you can use this feature:</div><div> 1. Access any pattern's results. For example: <a href="https://noiseexplorer.com/patterns/XX1/" target="_blank">https://noiseexplorer.com/patterns/XX1/</a></div><div> 2. In the results description, click on "Show detailed analysis" next to any message.</div><div> 3. For example, if you access the detailed analysis for Message C of the XX1 pattern: <a href="https://noiseexplorer.com/patterns/XX1/C.html" target="_blank">https://noiseexplorer.com/patterns/XX1/C.html</a></div><div><br></div><div>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.<br></div><div><br></div><div>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.</div><div><br></div><div>Best regards,<br></div><div><br></div><div><div><div dir="ltr" class="m_1832962632052654871m_1744697882307673134m_4188073113407555655m_-3375498491096418805m_-5807141320788155178m_-4223277242546640480gmail_signature"><div dir="ltr">Nadim Kobeissi<div>Symbolic Software <span style="color:rgb(84,84,84);font-size:small">• <a href="https://symbolic.software" target="_blank">https://symbolic.software</a></span></div><div><span style="color:rgb(84,84,84);font-size:small">Sent from office</span></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Jun 12, 2018 at 7:38 PM Trevor Perrin <<a href="mailto:trevp@trevp.net" target="_blank">trevp@trevp.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><br></div><div class="gmail_extra"><div class="gmail_quote">On Tue, Jun 12, 2018 at 5:17 PM, Nadim Kobeissi <span dir="ltr"><<a href="mailto:nadim@symbolic.software" target="_blank">nadim@symbolic.software</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"> <div><br></div><div>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.<br></div></div></blockquote><div><br></div><div><div>Nice!, I hope this produces a paper at some point, I'd definitely like to understand more of these nuances and modelling.</div><div><br></div><div>Anyways, of course let us know when this run finishes up, I definitely want to double-check it against the rev34 draft before releasing.</div></div><div><br></div><div>Trevor</div><div><br></div></div></div></div> </blockquote></div> </blockquote></div> </blockquote></div> </blockquote></div> </blockquote></div> </blockquote></div> </blockquote></div>