[noise] Noise Explorer

Thu May 31 03:19:16 PDT 2018

 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/08dece69/attachment.html>