[noise] Noise Explorer

[Nadim Kobeissi]

Dear Trevor,

I don't think you're missing something. Your response, I think, is fully
correct.

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.

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.

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.

Thank you for your patience,

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Thu, May 31, 2018 at 7:10 PM Trevor Perrin <trevp at trevp.net> wrote:

> Hi Nadim,
>
> Thanks for digging into this, I'd definitely like to make sure the
> spec's description of security properties aligns with Noise Explorer.
>
> Comments below -
>
>
> On Thu, May 31, 2018 at 10:19 AM, Nadim Kobeissi
> <nadim at symbolic.software> wrote:
> > -------------------------------------------------------------
> > SECTION II: Changes Apparent in our Analysis and Thoughts on Security
> Grades
> > in the Noise Specification
> > -------------------------------------------------------------
> >
> > Because of the improvements discussed earlier, it is now easier to
> > illustrate, using the formal verification process itself that underlies
> > Noise Explorer, why the security grades described in the Noise
> specification
> > are problematic. This is something that was alluded to previously in this
> > thread, but I believe was not fully elaborated upon.
> >
> > For example, consider the following pattern:
> >
> > IN
> >   -> e, s              0                0
> >   <- e, ee, se         0                3
> >   ->                   2                1
> >   <-                   0                5
> >
> > According to the Noise specification (and indeed to the earlier, less
> > precise analysis of Noise Explorer), message C in IN benefits from the
> > following level of authenticity:
> >> "2: Sender authentication resistant to key-compromise impersonation
> (KCI).
> >> The sender authentication is based on an ephemeral-static DH ("es" or
> "se")
> >> between the sender's static key pair and the recipient's ephemeral key
> pair.
> >> Assuming the corresponding private keys are secure, this authentication
> >> cannot be forged."
> >
> > However, this does not make total sense: as we can now observe in our
> > ProVerif analysis, when we arrive at message C:
> > Alice has executed the following key mixing operations: mixHash(e),
> > mixHash(s), mixHash(re), mixKey(ee), mixKey(se)
> > Bob has executed the following key mixing operations: mixHash(e),
> > mixHash(s), mixHash(re), mixKey(ee), mixKey(se)
> >
> > Based on the above, we can see that an attacker man-in-the-middling the
> > ephemerals can then convince Bob that a message that Alice had sent to
> > Charlie was indeed meant to be for Bob.
>
> I don't follow - Bob will only accept Alice's 3rd message if it's
> based on his (Bob's) ephemeral.  If Charlie is another honest party in
> the "Bob" role, the same will be true for Charlie.
>
>
> > Bob can be led to accept this
> > message as originating by Alice and meant for him without issue.
>
> Any 3rd message accepted by Bob will indeed by originated by Alice and
> meant for him (in the sense of being based on his - Bob's -
> ephemeral).  The grade #2 seems like an accurate description of this
> property.
>
> As best as I can tell, you're describing an "attacker" (Charlie?) who
> simply functions as a wire, and relays messages without changing them
> between Alice and Bob.  But this attacker doesn't break the described
> security properties, so this just seems like a re-statement of the
> security model (message transmission is under the control of the
> attacker).
>
> But maybe I'm missing something?
>
> Trevor
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20180531/83ecad67/attachment.html>