[noise] Formal verification of NoiseIK
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:
> 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