[noise] Noise Explorer

[Trevor Perrin]

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