[noise] Noise Explorer

[Nadim Kobeissi]

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."

Either way, "tokenless" messages for K have now been removed from the
analysis. This will be reflected on the website in a few minutes.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office
On Fri, May 25, 2018 at 5:32 PM Trevor Perrin <trevp at trevp.net> wrote:

> On Fri, May 25, 2018 at 11:54 AM, Nadim Kobeissi
> <nadim at symbolic.software> wrote:
> >
> >> With one-way patterns there will never be additional messages, so you
> >> shouldn't list the tokenless messages (and the security properties
> >> being claimed for those messages don't make sense - e.g. it says the
> >> "response" message would be in cleartext, but I'm not sure why).
> >
> > ProVerif is detecting that the post-session compromise of the
responder's
> > static key (the sender of message B) would lead to message B being
> > decryptable. Should this still satisfy confidentiality grade 1 in your
view?

> No, it's confidentiality grade 2 - both the Noise spec and Noise
> Explorer correctly list the single message in the K pattern as (1,2).
> But Noise Explorer shouldn't list additional messages for this
> pattern.

> Trevor