Plan for low-level Handshake and HandshakeLog

[aseemr]

Notes from a meeting between @fournet, @ad-l, and @aseemr:

We will work towards an implementation of HS ans HSL consisting of both low-level and high-level components.

On the reading side, HSL will provide a low-level interface, in the same style that we have been working on. On the writing side, HSL.send will still be high-level, and will internally use QD intermediate serializers and bytes-to-buffer conversions. For hashing, on the reading side, HS will send signals to HSL for hashing the messages and adding them to the transcript (where the signals will contain indices in the input buffer, HSL will maintain enough invariants so that HS does not need to pass them on). On the writing side, HSL will automatically hash the messages.

HS implementation will be low-level on the reading side, i.e. it will take buffer indices from HSL and use low-level QD accessors etc. But when it talks to Nego and KS, it will use the QD intermediate parsers to construct high-level messages and then pass them back-and-forth. In other words, Nego and KS, and the related state and invariants in HS will remain high-level. On the writing side, HS will be purely high-level.

We will move to QD datatypes for both high- and low-level (https://github.com/project-everest/mitls-fstar/issues/218).

Towards this plan, we identified following tasks:

• [ ] Switch to QD for HandshakeMessage and Extensions, merge @nikswamy's F* and mitls branches for extraction (@ad-l)

• [ ] Continue work on HS Secret, KDF, Nego in high-level style (@ad-l, @fournet, @s-zanella)

• [ ] Iterate fast on low-level HSL.fsti and implement an HSL.fst that is partially verified but functional (@aseemr, @nikswamy)

• [ ] In Jan., interop with low-level HSL.fst which is partially verified

We discussed some alternate choices for HS and HSL implementation. Will add them as a comment soon.