[noise] Pattern transformations

[Trevor Perrin]

Alex wrote:
> Would you consider the following statement to be
> in conformity with the definition provided in the spec?:
>
> "If 's' appears after 'ee', 'se', 'es', or 'ss', move it directly
> before the token, and repeat this process until it no longer moves."

I think that's right.



Alex wrote:
> In the linked post you said, "that adds the server's
> static as a pre-message, if it's not one already." If
>  it is already, the pattern never changes. Therefore,
> do we append "+pskresume" even though nothing changed?

Hadn't thought about that, we probably wouldn't bother naming the
pattern if the transformation is a no-op?

> Moreover, the order in which the transformations are composed matters.
>
> (g . f) != (f . g)


Sure, we've discussed notation like NoiseXXhfs+noidh, I guess that
would apply transformations in order: "hfs", then "noidh".

You're right there's more work to be done in defining transformations
and how they interact.

So far I think we've proposed:

 - "noidh" - no identity hiding
 - "hfs" - hybrid forward secrecy
 - "sig" - replace "se" and "es" with signatures
 - ??? -  'add or remove "ss" operations', per Noise spec
 - "pskresume" - bind server static for PSK resumption
 - "semiresume" - bind server static and use semi-ephemerals for resumption

But at some point we'll need to flesh these out, list other
transformations that would be useful, figure out which compositions
make sense, etc.

Probably we'll need better tools for that, e.g. tools that can
automatically work out security properties like Sections 8.4 and 8.5
of the spec.

That might also be a good point to get more crypto / formal methods
researchers involved and apply heavy machinery - Tamarin, EasyCrypt,
F*, Coq, etc.


Trevor