[noise] Formal verification of NoiseIK

Trevor Perrin trevp at trevp.net
Fri Jul 14 09:58:44 PDT 2017

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?


More information about the Noise mailing list