[noise] Noise Explorer

[Nadim Kobeissi]

Hello everyone,
I've been following up on all of these discussions very closely, but have
not said anything because I've been working furiously on getting all the
formal results for all 22 deferred patterns *with* two "tokenless" messages
out. I'm afraid that with the addition of two "tokenless" messages to every
single model, the cost of verification increases dramatically. Things are
still going to take quite a long time -- I wish we weren't nearing June, at
least I'd have a use for the free radiators I now have in my apartment due
to this -- quite a lot of finely tuned dedicated hardware is now dealing
with the formal verification load.

An important clarification: Trevor says the following:
> Thinking more on rev34, it would probably be irresponsible to publish
> *without* security tables for all the deferred patterns...  So I'd
> love to work out how to get your output processed into some tables
> like the current ones (or possibly changed around a bit, depending on
> that discussion).  Or really: for you to work that out, so I could
> just copy-and-paste :-)....

Trevor, the security tables for 20 of the deferred patterns are already
available on Noise Explorer's website. They simply do not include the
"tokenless" messages. Just a note in the event that you missed that. :-)

Regarding the discussions on security properties, I'm personally currently
satisfied with the recognition that any deferred pattern that opens up a
potential UKS attack will simply never qualify towards authenticity grades
3 and 4 (as defined by Noise Explorer) and will always be restricted to a
maximum of 1 or 2 (as defined by Noise Explorer, see my previous email
where I list a "very quick summary" of the additions to the authenticity
properties.) The rest of the discussion seems to surround properties that
can be inferred from the current queries anyway, so that's fine with me. My
current focus is really to get these 29 "tokenless" message models through
(an extra "tokenless" message was also added to each fundamental pattern
that only had one tokenless message.)

Katriel, thank you for your list of improvements to the parser.

First, I should link to the more recent version of the PEG.js rules, which
is cleaner and applies to revision 34:
https://github.com/SymbolicSoft/noiseexplorer/blob/rev34/src/parser/noiseParser.pegjs
-- I think extracting this into ANTLR will be easier. Any upcoming
publication on Noise Explorer will most certainly include very neat parsing
grammar, as well as translation rules into ProVerif. As you certainly know,
the paper itself is always cleaner than the code (although I am quite
pleased with the cleanliness of the Noise Explorer codebase, which I've
kept to a high standard!)

As discussed off-list, I appreciate the additional syntax checks. Our
original goal with the checks was to ensure that patterns are valid enough
to completely prevent any non-sane ProVerif model generation, but now that
that is achieved, we can surely expand them to ensure that all parsed Noise
Handshake Patterns are as adherent to the specification as possible.
Regarding your suggestions:

> 1a) static keys are only sent if parties are initialised with them
This check already existed. However, as of revision 34, it is no longer
possible to specify the initialization of keys explicitly, and thus this
check has been removed.

> 1b) parties can only send DH values between keys they know or have
received
> - if a party sends an ephemeral key then that ephemeral key is actually
used in a DH value somewhere
> - parties should only use a psk if they are initialised with them
These are good checks to add. A commit will soon appear adding these
checks, and you will be credited for your suggestions, thank you!

> 2) parties can only send their {static,ephemeral} key once per handshake
This check already exists and remains relevant in revision 34.

> 3) parties must not call ENCRYPT in certain cases
> 4) parties must not call ENCRYPT in certain other cases involving a PSK
Hmm. I don't understand what you mean by this "ENCRYPT" operation, and as
you say, it does not seem to be captured in the pattern that is to be
parsed. Could you please elaborate?

> - length restrictions (pattern name < 16 chars, messages contain < 8
tokens, handshakes contain < 8 messages)
> - parties cannot send the same token twice in the same message
> - PSK restrictions: no incorrect modifiers, or modifiers not at the end
of the pattern name, or PSKs in the wrong place, or >1 PSK
> - no tokenless messages except at the end of the pattern
> - message patterns alternate (initiator -> responder, initiator <-
responder) with the first message being sent by the initiator

Yes, these are the checks that exist presently (there might also be others.)

It is very heartening to see such an excellent discussion with regards to
Noise Explorer and the evolution of the security analysis of Noise
protocols. Bear with me as I strive to ensure the provision of all 29
updated formal verification results in the shortest possible delay! I will
continue to monitor the discussion during this time.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office
On Thu, May 24, 2018 at 1:20 PM Katriel Cohn-Gordon <me at katriel.co.uk>
wrote:

> Hi Nadim,

> Great work! you've done a very thorough job and I very much enjoyed using
the website :)

> There are a couple of particular pieces that I think are good standalone
contributions, and I wonder whether it would be possible to extract them
from the Explorer and potentially use them in other tools:



> 1. a grammar for Noise patterns

> Explorer's PEG.js grammar [1] looks good but it's got parsing
instructions mixed in with the grammar, which makes it a bit hard for me to
extract out just the latter. I started writing an ANTLR grammar [2] but
it's duct-tape-and-string, and also I don't really know antlr :)

> It would be super cool if there was a formal grammar in the spec, perhaps
in BNF or similar, that anyone could use to generate their own parser
without having to re-do all the work. I think the IETF has a language for
these but I don't think it really matters which language it is as long as
it's widely understood.



> 2. a list of precisely-defined syntax checks

> This is partially present in the spec [3], which requires that:

>      1a) static keys are only sent if parties are initialised with them
>      1b) parties can only send DH values between keys they know or have
received
>      2) parties can only send their {static,ephemeral} key once per
handshake
>      3) parties must not call ENCRYPT in certain cases
>      4) parties must not call ENCRYPT in certain other cases involving a
PSK

> Of these, I think 3 and 4 are not quite syntax checks because ENCRYPT
doesn't actually appear in the Noise pattern itself, but perhaps there is a
way to phrase them as one (perhaps on the ordering of DH tokens).

> I don't think Explorer checks 3 or 4, but it does also check:

>      - length restrictions (pattern name < 16 chars, messages contain < 8
tokens, handshakes contain < 8 messages)
>      - parties cannot send the same token twice in the same message
>      - PSK restrictions: no incorrect modifiers, or modifiers not at the
end of the pattern name, or PSKs in the wrong place, or >1 PSK
>      - no tokenless messages except at the end of the pattern
>      - message patterns alternate (initiator -> responder, initiator <-
responder) with the first message being sent by the initiator

> and I think it would also be good to add:

>      - if a party sends an ephemeral key then that ephemeral key is
actually used in a DH value somewhere
>      - parties should only use a psk if they are initialised with them

> best,
> Katriel

> [1]
https://github.com/SymbolicSoft/noiseexplorer/blob/master/src/parser/noiseParser.pegjs
> [2] https://github.com/katrielalex/noisy/blob/master/noisy/noisy.g4
> [3] http://noiseprotocol.org/noise.html#pattern-validity
> _______________________________________________
> Noise mailing list
> Noise at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/noise