<div dir="ltr">
<div>Hello everyone,<br></div><div><br></div><div>The reason for my silence on
Noise Explorer was that I've been stuck on a very tricky issue with the
formal models for the past two weeks: generating a model that captures an unbounded number of sessions executed in parallel of the Noise Handshake Pattern between the
parties (Alice, Bob and Charlie), with a fresh, distinct new ephemeral
for everyone in every one of these unbounded number of sessions.</div><div><br></div><div>This was very difficult (for me, at least,) because of two reasons:</div><div>
1. Describing this particular scenario, given that Noise does not really contain a notion of session IDs or similar, proved quite difficult to do in the applied pi calculus for reasons that I won't go into here (if you think you know of an easy way, you're wrong, I tried every darn way for 12 days and can assure you that it includes the one you're thinking of!) The difficulty of doing this was what led me to send my previous half-baked analysis -- at some point I got lost in the torrent of output that I was getting from all the
different models I was experimenting with, and was misled by an output that illustrated a result we had already discussed but in a very different way. Thanks, Trevor, for your correction.<br></div><div> 2.
Struggling to ensure that it doesn't result in a performance hit that
makes the verification of even the simplest Handshake Patterns not
terminate.</div><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><br></div><div>According to the results so far, the results currently available in the Noise specification
are again matched result-for-result and there is no longer a perceived
difference, as I misleadingly argued in my previous long email to the
mailing list. However, the tests are still not finished for every model,
but will likely be finished tomorrow (c.f. <a href="https://imgur.com/a/hiAmPpM">https://imgur.com/a/hiAmPpM</a>)<br></div><div><br></div><div>By tomorrow I should
have all the results. I personally expect them to match the ones currently on Noise Explorer (and in the specification on Trevor's website.) But you never know, hence why we're doing this whole thing anyway.</div><div><br></div><div>Working on this project has been incredibly fun and rewarding. Most especially solving this particular issue, which is the most trouble I've ever had with ProVerif!<br></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><br><div class="gmail_quote"><div dir="ltr">On Thu, May 31, 2018 at 8:09 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>Dear Trevor,</div><div><br></div><div>I don't think you're missing something. Your response, I think, is fully correct.</div><div><br></div><div>Indeed, I think that I sent my previous email while in the middle of a thread of thought, under the pretense that I was in fact at the end of it.</div><div><br></div><div>Bear with me as I sort these models out -- it is normal, I suppose, for one to make such an error after a certain very large amount of time is spent staring at generated protocol models.</div><div><br></div><div>I am currently working more on improving the separation between unbounded sessions (which is proving to be nontrivial). I will have more well-formed contributions for you as well as, I hope, a concrete proposal for a new security model in the coming days.</div><div><br></div><div>Thank you for your patience,<br></div><div><br></div><div><div><div dir="ltr" class="m_-4499762689459215101gmail_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 Thu, May 31, 2018 at 7:10 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">Hi Nadim,<br>
<br>
Thanks for digging into this, I'd definitely like to make sure the<br>
spec's description of security properties aligns with Noise Explorer.<br>
<br>
Comments below -<br>
<br>
<br>
On Thu, May 31, 2018 at 10:19 AM, Nadim Kobeissi<br>
<nadim@symbolic.software> wrote:<br>
> -------------------------------------------------------------<br>
> SECTION II: Changes Apparent in our Analysis and Thoughts on Security Grades<br>
> in the Noise Specification<br>
> -------------------------------------------------------------<br>
><br>
> Because of the improvements discussed earlier, it is now easier to<br>
> illustrate, using the formal verification process itself that underlies<br>
> Noise Explorer, why the security grades described in the Noise specification<br>
> are problematic. This is something that was alluded to previously in this<br>
> thread, but I believe was not fully elaborated upon.<br>
><br>
> For example, consider the following pattern:<br>
><br>
> IN<br>
> -> e, s 0 0<br>
> <- e, ee, se 0 3<br>
> -> 2 1<br>
> <- 0 5<br>
><br>
> According to the Noise specification (and indeed to the earlier, less<br>
> precise analysis of Noise Explorer), message C in IN benefits from the<br>
> following level of authenticity:<br>
>> "2: Sender authentication resistant to key-compromise impersonation (KCI).<br>
>> The sender authentication is based on an ephemeral-static DH ("es" or "se")<br>
>> between the sender's static key pair and the recipient's ephemeral key pair.<br>
>> Assuming the corresponding private keys are secure, this authentication<br>
>> cannot be forged."<br>
><br>
> However, this does not make total sense: as we can now observe in our<br>
> ProVerif analysis, when we arrive at message C:<br>
> Alice has executed the following key mixing operations: mixHash(e),<br>
> mixHash(s), mixHash(re), mixKey(ee), mixKey(se)<br>
> Bob has executed the following key mixing operations: mixHash(e),<br>
> mixHash(s), mixHash(re), mixKey(ee), mixKey(se)<br>
><br>
> Based on the above, we can see that an attacker man-in-the-middling the<br>
> ephemerals can then convince Bob that a message that Alice had sent to<br>
> Charlie was indeed meant to be for Bob.<br>
<br>
I don't follow - Bob will only accept Alice's 3rd message if it's<br>
based on his (Bob's) ephemeral. If Charlie is another honest party in<br>
the "Bob" role, the same will be true for Charlie.<br>
<br>
<br>
> Bob can be led to accept this<br>
> message as originating by Alice and meant for him without issue.<br>
<br>
Any 3rd message accepted by Bob will indeed by originated by Alice and<br>
meant for him (in the sense of being based on his - Bob's -<br>
ephemeral). The grade #2 seems like an accurate description of this<br>
property.<br>
<br>
As best as I can tell, you're describing an "attacker" (Charlie?) who<br>
simply functions as a wire, and relays messages without changing them<br>
between Alice and Bob. But this attacker doesn't break the described<br>
security properties, so this just seems like a re-statement of the<br>
security model (message transmission is under the control of the<br>
attacker).<br>
<br>
But maybe I'm missing something?<br>
<br>
Trevor<br>
</blockquote></div>
</blockquote></div>