<div dir="ltr"><div>Dear Trevor,</div><div><br></div><div>Thank you for your interest!<br></div><div><br></div><div>I am committed to keeping Noise Explorer in sync with the latest revision of the Noise specification. Once revision 34 is published, you will within a short time see an update to the Noise Explorer stack targeting revision 34, and the revision 33 stack will be discontinued, taken offline and no longer supported. The same will happen with every revision.</div><div><br></div><div>The deferred patterns in revision 34 are an excellent target for analysis, and their analysis results will be rolled out with the revision 34 update to Noise Explorer.</div><div><br></div><div>Regarding the automation of security result generation: this is already implemented and you yourself can generate the results using the Noise Explorer command-line tool, available on the website.</div><div><br></div><div>The issue, however, is that formal verification with ProVerif can take a very long time when you have an active attacker, three principals (one malicious) and 11 queries for every single message. This is why I actually built my own ProVerif verification rig specifically for this purpose, and it's certainly been breaking a sweat to output these results.<br></div><div><br></div><div>So, while you can certainly obtain the analysis results yourself for a pattern such as NK within 10 minutes using Noise Explorer on your laptop, something like IK took 42 hours even on my dedicated hardware.</div><div><br></div><div>What I can commit to do from my end is to always keep the Noise Explorer website up to date for any pattern that you include in any Noise specification revision, including these recent deferred pattern and any upcoming pattern. You can also personally suggest some arbitrary pattern you think is important, and I will run the tests on my local dedicated verification rig and post on Noise Explorer the ProVerif model and results, as is currently the case with the revision 33 examples.</div><div><br></div><div>With regards to the results we have already, they match the ones in your existing table, but are more nuanced since we added two more authenticity grades (3 and 4), since our security model includes a compromised principal.<br></div><div><br></div><div>Identity hiding is also something that I plan to take a closer look at very soon.<br></div><div><br></div><div><div dir="ltr" class="gmail_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><br><div class="gmail_quote"><div dir="ltr">On Tue, May 22, 2018 at 5:45 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">On Tue, May 22, 2018 at 9:42 AM, Nadim Kobeissi <nadim@symbolic.software> wrote:<br>
> Please access Noise Explorer using this address: <a href="https://noiseexplorer.com" rel="noreferrer" target="_blank">https://noiseexplorer.com</a><br>
><br>
> Regarding the compendium of patterns included on the website, I also request<br>
> that you send me additional Noise Handshake Patterns, so that I can use<br>
> Noise Explorer to generate formal models, pretty HTML results, and then post<br>
> these too in the compendium<br>
<br>
Hey Nadim,<br>
<br>
Looks fascinating, I'm looking forward to spending some time with<br>
this.  We're on the verge of publishing spec revision 34 (I was<br>
supposed to do it last week, but will try to find time this week).<br>
<br>
This introduces 22 new "deferred" patterns, so those would be a<br>
perfect target for more analysis.  We'd like to ensure that the<br>
deferred patterns eventually achieve the same security as the<br>
"fundamental" pattern they're based on, for one thing.<br>
<br>
<a href="https://github.com/noiseprotocol/noise_spec/blob/rev34/output/noise.pdf" rel="noreferrer" target="_blank">https://github.com/noiseprotocol/noise_spec/blob/rev34/output/noise.pdf</a><br>
<br>
I'd also like to double-check these results against the spec's<br>
security properties tables, and see if we can generate similar tables<br>
for the new patterns, it would be great to have that automated.<br>
<br>
And if you were really ambitious, the "identity hiding" properties<br>
would be great to have automated analysis for, but I'm sure that's<br>
more complicated.<br>
<br>
Trevor<br>
</blockquote></div>