<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/">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/">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">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="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 Tue, Jun 12, 2018 at 7:38 PM Trevor Perrin <<a href="mailto:trevp@trevp.net">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>