[noise] Formal verification of NoiseIK

[Trevor Perrin]

On Fri, Jul 14, 2017 at 12:36 AM, Jason A. Donenfeld <Jason at zx2c4.com> wrote:
> Hey guys,
>
> I'll respond in length soon to the explicit nonce thread. I've been
> backed up with the following, but now that this is out of the way I'll
> catch up on the other stuff in the list. But first:
>
> https://www.wireguard.io/formal-verification/
> https://www.wireguard.io/papers/wireguard-formal-verification.pdf
>
> Nice results for NoiseIK: it isn't terrible!

Good to hear!  Looks like there were no surprises, and the properties
you verified match the informal descriptions in the Noise spec.

I should definitely learn Tamarin - the code here looks quite compact
(<400 lines) and at a high level that seems reasonable to work with.

Do you or Kevin have thoughts about generalizing this?

Ideally we'd like a tool that takes any handshake pattern, evaluates
it against all security goals, and then outputs something like our
current security-properties tables.  Perhaps a pre-processor that
generates Tamarin from a handshake pattern, something like that?


Trevor