[noise] Noise Explorer

[Trevor Perrin]

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