[noise] Noise Explorer

Thu May 31 04:46:11 PDT 2018

Hello everyone,
Please disregard for now the section on message D in KX in the previous
email, I believe I have have inaccurately described the issue with replays.
Sorry about that, I'm looking into things more closely.

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

On Thu, May 31, 2018 at 12:19 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> Hello everyone,
>
> This is going to be a somewhat detailed email I discuss some thoughts into
> the security grades currently defined in the Noise specification and used
> to evaluate Noise Handshake patterns.
>
> -------------------------------------------------------------
> SECTION I: Improvements Made to Symbolic Model Generation
> -------------------------------------------------------------
>
> I have made some major improvements to the way that Noise Explorer
> generates symbolic models from Noise Handshake Patterns. Symbolic models
> were always generated to evaluate an unbounded number of Noise protocol
> sessions running in parallel between Alice, Bob and Charlie. However, this
> parallel execution was still imprecise in some areas. The following
> improvements address these imprecisions:
>
> ----
> 1. Stronger Ephemeral Freshness
> Previously: while indeed all participants used fresh ephemerals with
> respect to the other participant, that ephemeral would be in fact the same
> one across the unbounded sessions. That is to say, the ephemeral Alice
> would use with Bob would be different than the one she would use with
> Charlie, but in the unbounded parallel execution of Noise sessions, Alice
> would use that same ephemeral with Bob in all parallel sessions, thereby
> producing a notable loss of precision in the analysis.
>
> Now: a new ephemeral is generated and guaranteed to be fresh for each
> session in the unbounded number of sessions: Alice will use a new ephemeral
> with Bob every time. As you can imagine, this pushes the verification cost
> further up but is, I believe, an important addition.
> ----
> 2. Stronger Session Separation
> Previously: to put it simply, individual message pattern exchanges (such
> as, for example, message B in some Noise Handshake Pattern) between Alice
> and Bob would be, to a large degree, interchangeable between sessions,
> thereby producing a notable loss of precision in the analysis.
>
> Now: session uniqueness is more strongly enforced, and the symbolic models
> are able to reason that, for example, some message B from a session that
> Alice and Bob had *in the past* is being replayed in a session that is
> currently occurring between Alice and Bob over the same Noise Handshake
> Pattern. As you can imagine, this also pushes the verification cost further
> up, but is, I believe, also an important addition.
> ----
> 3. Unbounded Number of Tokenless Messages
> Previously: after the key exchange phase was over, and within each session
> in the unbounded number of sessions, the initiator would only send one
> tokenless message and obtain one response tokenless message.
>
> Now: within the unbounded number of parallel protocol sessions, there is
> also an unbounded number of tokenless messages being sent in either
> direction after the key exchange phase is accomplished.
> ----
>
> -------------------------------------------------------------
> 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. Bob can be led to accept this
> message as originating by Alice and meant for him without issue. Of course,
> this happens without anyone's static keys needing to be compromised --
> Bob's static keys are never used in this pattern anyway -- therefore,
> authenticity grade 2 cannot be met.
>
> Discrepancies occur in other patterns too, including K, KK, KX, XN, etc.
> -- in KX, for example:
>
> KX
>   -> s
>   ...
>   -> e                       0                0
>   <- e, ee, se, s, es        2                3
>   ->                         2                5
>   <-                         2                5
>
> Messages B, C and D are all affected by similar issues, but let's focus on
> message D as an example: during this session, an active attacker can
> man-in-the-middle the ephemerals are replace them with Alice and Bob's
> ephemeral public keys, but from a previous session. This will lead to Alice
> accepting a message D from Bob that was sent in a previous session. This is
> problematic for two reasons:
>
> 1. Message D would be a replay, and yet the confidentiality grade asserts
> that message pattern D is replay-resistant.
> 2. Does a message from Bob from *any session* suffice to authenticate Bob
> for this session, even if the message itself was sent by Bob in a session
> that happened long in the past? Current authenticity grades do not discuss
> this.
>
> I suppose there are other examples that can be given, but I think the two
> above are sufficiently illustrative. As it stands, the current security
> grades are not precise enough, and therefore lead to situations where
> ascribing them to certain message patterns can indeed be misleading. I hope
> this email clarifies my case for this conclusion, and that we can begin
> moving forward on redesigning the security grading system to be based on
> formally specified security qualifications instead of elaborate, but
> nevertheless imprecise, paragraphs. Due to this imprecision, Noise
> Explorer's latest analysis severely downgrades the grading on many Noise
> Handshake Patterns, and I would like for us to establish some more
> appropriate security grades for revision 34 so that we can have a more
> precise way to reason about what each Noise Handshake Pattern accomplishes.
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
>
> On Sat, May 26, 2018 at 12:09 PM Nadim Kobeissi <nadim at symbolic.software>
> wrote:
>
>> Hello everyone,
>> I have two updates that will hopefully be useful:
>>
>> 1. All one-way handshake patterns (K, N, X) are now added to the
>> compendium.
>> 2. Given the growing size of formal verification results, I have added a
>> search function to the top of the compendium page that will allow you to
>> quickly search for a Noise Handshake Pattern by its name:
>> https://noiseexplorer.com/patterns/
>>
>> Have a great weekend,
>>
>> Nadim Kobeissi
>> Symbolic Software • https://symbolic.software
>> Sent from office
>> On Fri, May 25, 2018 at 5:52 PM Trevor Perrin <trevp at trevp.net> wrote:
>>
>> > On Fri, May 25, 2018 at 3:43 PM, Nadim Kobeissi <nadim at symbolic.software
>> >
>> wrote:
>> > > I guess I'm confused, because confidentiality grade 2 does not say
>> anything
>> > > about the *sender's* static key being compromised after the session is
>> > > concluded and how that may lead to decryption. It only discusses the
>> > > recipient's static keys:
>> > >
>> > > "2: Encryption to a known recipient, forward secrecy for sender
>> compromise
>> > > only, vulnerable to replay. This payload is encrypted based only on
>> DHs
>> > > involving the recipient's static key pair. If the recipient's static
>> > > private key is compromised, even at a later date, this payload can be
>> > > decrypted. This message can also be replayed, since there's no
>> ephemeral
>> > > contribution from the recipient."
>>
>> > I was talking about the first and only message (A) in pattern K.
>>
>> > If you're talking about subsequent messages in this pattern, these
>> > messages don't exist.  But even if they existed, it wouldn't be
>> > correct to say "Message contents are sent in cleartext", so not sure
>> > what Noise Explorer was doing there.
>>
>> > > Either way, "tokenless" messages for K have now been removed from the
>> > > analysis. This will be reflected on the website in a few minutes.
>>
>> > Cool, that takes care of it.
>>
>>
>> > Trevor
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20180531/3c745131/attachment.html>