<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="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></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">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>