<div dir="ltr">Hello everyone,<div><br></div><div>Related news: Noise Explorer's compendium now also has formal verification results IKpsk1!</div><div><br></div><div><a href="https://noiseexplorer.com/patterns/IKpsk1/">https://noiseexplorer.com/patterns/IKpsk1/</a> <br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><br></div><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></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Feb 7, 2019 at 12:50 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hello everyone,<div>I'm excited to be able to say that Noise Explorer finally contains a full analysis of IKpsk2! This is the Noise Handshake Pattern used in WireGuard.</div><div><br></div><div>It took 21 days to run IKpsk2's ProVerif model.</div><div><br></div><div>The results are available here:</div><div><a href="https://noiseexplorer.com/patterns/IKpsk2/" target="_blank">https://noiseexplorer.com/patterns/IKpsk2/</a><br></div><div><br></div><div>For comparison, IK's results are available here:</div><div><a href="https://noiseexplorer.com/patterns/IK/" target="_blank">https://noiseexplorer.com/patterns/IK/</a><br></div><div><br></div><div>The intrepid among you will notice that upon first glance, IKpsk2 seems to obtain security guarantees that are "weaker" than IK. For example, message A in IK has an authentication grade of 1 and a confidentiality grade of 2, whereas in IKpsk2, message A appears to have an authentication grade of 0 and a confidentiality grade of 0. This is misleading and I will explain why.</div><div><br></div><div>Whenever we test for static key compromise in non-PSK Noise Handshake Patterns, the query looks something like this:</div><div>"event(RecvMsg(bob,alice,stagepack_a(sid_b),m)) ==> event(SendMsg(alice,c_1211,stagepack_a(sid_a),m)) || event(LeakS(phase0,alice)) || event(LeakS(phase0,bob))."</div><div><br></div><div>..which translates to: "In this query, we test for sender authentication and message integrity. If Bob receives a valid message from Alice, then Alice must have sent that message to someone, or Alice had their static key compromised before the session began, or Bob had their static key compromised before the session began." <br></div><div><br></div><div>And whenever we test for static key compromise in PSK Noise Handshake Patterns, the query looks something like this: <br></div><div>"event(RecvMsg(bob,alice,stagepack_a(sid_b),m)) ==> event(SendMsg(alice,c_1342,stagepack_a(sid_a),m)) || (event(LeakS(phase0,alice)) && event(LeakPsk(phase0,alice,bob))) || (event(LeakS(phase0,bob)) && event(LeakPsk(phase0,alice,bob)))."</div><div><br></div><div>...which translates to: "In this query, we test for sender authentication and message integrity. If Bob receives a valid message from Alice, then Alice must have sent that message to someone, or Alice had their static key *****<b>and PSK*****</b> compromised before the session began, or Bob had their static key <b>*****</b><b>and PSK</b><b>*****</b>compromised before the session began." (emphasis mine).</div><div><br></div><div>So therefore, notice that in PSK Noise Handshake Patterns, testing for static key compromise across all security queries also comes conjoined with a test for PSK compromise. The security query is modified to test whether the compromise of the party's static key <b>and </b>PSK is necessary.</div><div><br></div><div>Since the PSK in IKpsk2 only appears at message B, its entailed effects or security improvements occur only after that point. The updated security queries are intended to reflect the PSK's before-and-after effect across the entire Noise Handshake Pattern.</div><div><br></div><div>I hope that you find the parameters and queries for this analysis reasonable. Of course, feedback is welcome.</div><div><br></div><div>Don't forget that 18 other PSK pattern analyses are also available:</div><div><a href="https://noiseexplorer.com/patterns/" target="_blank">https://noiseexplorer.com/patterns/</a> (type "psk" in the search bar.)</div><div><br></div><div>Best regards,</div><div><br></div><div><div><div dir="ltr" class="gmail-m_273306159835624435gmail_signature"><div dir="ltr"><div><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></div></div></div></div></div></div></div></div></div></div></div> </blockquote></div>