[noise] Noise Explorer

[Katriel Cohn-Gordon]

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