<div dir="ltr"><div>Hello everyone,</div><div>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.<br></div><div><br></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><br><div class="gmail_quote"><div dir="ltr">On Thu, May 31, 2018 at 12:19 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">
Hello everyone,<br><br>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.<br><br>-------------------------------------------------------------<br>SECTION I: Improvements Made to Symbolic Model Generation<br>-------------------------------------------------------------<br><br>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:<br><br>----<br>1. Stronger Ephemeral Freshness<br>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.<br><br>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.<br>----<br>2. Stronger Session Separation<br>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.<br><br>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.<br>
----
<br>3. Unbounded Number of Tokenless Messages<br>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.<br><br>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.<br><div>
----
</div><br>-------------------------------------------------------------<br>SECTION II: Changes Apparent in our Analysis and Thoughts on Security Grades in the Noise Specification<br>-------------------------------------------------------------<br><br>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.<br><br>For example, consider the following pattern:<br><br><span style="font-family:monospace,monospace">IN<br> -> e, s 0 0<br> <- e, ee, se 0 3<br> -> 2 1<br> <- 0 5</span><br><br>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:<br>> "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."<br><br>However, this does not make total sense: as we can now observe in our ProVerif analysis, when we arrive at message C:<br>Alice has executed the following key mixing operations: mixHash(e), mixHash(s), mixHash(re), mixKey(ee), mixKey(se)<br>Bob has executed the following key mixing operations: mixHash(e), 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
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.<br><br>Discrepancies occur in other patterns too, including K, KK, KX, XN, etc. -- in KX, for example:<br><br><span style="font-family:monospace,monospace">KX<br> -> s<br> ...<br> -> e 0 0<br> <- e, ee, se, s, es 2 3<br> -> 2 5<br></span><div><span style="font-family:monospace,monospace"> <- 2 5</span></div><br><div>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:</div><div><br></div><div>1. Message D would be a replay, and yet the confidentiality grade asserts that message pattern D is replay-resistant.</div><div>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.<br></div><div><br></div><div>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.<br></div><div><div><br></div><div><div dir="ltr" class="m_-2611633076876096690gmail_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 Sat, May 26, 2018 at 12:09 PM Nadim Kobeissi <nadim@symbolic.software> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello everyone,<br>
I have two updates that will hopefully be useful:<br>
<br>
1. All one-way handshake patterns (K, N, X) are now added to the compendium.<br>
2. Given the growing size of formal verification results, I have added a<br>
search function to the top of the compendium page that will allow you to<br>
quickly search for a Noise Handshake Pattern by its name:<br>
<a href="https://noiseexplorer.com/patterns/" rel="noreferrer" target="_blank">https://noiseexplorer.com/patterns/</a><br>
<br>
Have a great weekend,<br>
<br>
Nadim Kobeissi<br>
Symbolic Software • <a href="https://symbolic.software" rel="noreferrer" target="_blank">https://symbolic.software</a><br>
Sent from office<br>
On Fri, May 25, 2018 at 5:52 PM Trevor Perrin <<a href="mailto:trevp@trevp.net" target="_blank">trevp@trevp.net</a>> wrote:<br>
<br>
> On Fri, May 25, 2018 at 3:43 PM, Nadim Kobeissi <nadim@symbolic.software><br>
wrote:<br>
> > I guess I'm confused, because confidentiality grade 2 does not say<br>
anything<br>
> > about the *sender's* static key being compromised after the session is<br>
> > concluded and how that may lead to decryption. It only discusses the<br>
> > recipient's static keys:<br>
> ><br>
> > "2: Encryption to a known recipient, forward secrecy for sender<br>
compromise<br>
> > only, vulnerable to replay. This payload is encrypted based only on DHs<br>
> > involving the recipient's static key pair. If the recipient's static<br>
> > private key is compromised, even at a later date, this payload can be<br>
> > decrypted. This message can also be replayed, since there's no ephemeral<br>
> > contribution from the recipient."<br>
<br>
> I was talking about the first and only message (A) in pattern K.<br>
<br>
> If you're talking about subsequent messages in this pattern, these<br>
> messages don't exist. But even if they existed, it wouldn't be<br>
> correct to say "Message contents are sent in cleartext", so not sure<br>
> what Noise Explorer was doing there.<br>
<br>
> > Either way, "tokenless" messages for K have now been removed from the<br>
> > analysis. This will be reflected on the website in a few minutes.<br>
<br>
> Cool, that takes care of it.<br>
<br>
<br>
> Trevor<br>
</blockquote></div>
</blockquote></div>