search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

HSL Receive interface and implementation using reprs #225

Closed aseemr closed 5 years ago

aseemr commented 5 years ago

This pull request contains a sample flight implementation in HSL using the reprs.

The flight implemented in the module is the EE_C_CV_FIN flight. In addition to adding repr modules for each of these flight types, I have also added a repr module for Handshake13 messages (see https://github.com/project-everest/mitls-fstar/pull/225/files#diff-eb42ad423220e534651efcac13928b8c). This repr module provides predicates for specific instances (such as is_ee, is_fin etc.) and functions to obtain specific instance reprs (with corresponding predicates in the precondition), e.g. obtain a EE repr from an HSM13 repr, provides is_ee holds for the HSM13 repr.

The flight types in HSL.Receive are changed to return reprs, instead of indices and ghost messages separately. All the reprs are of type MITLS.Repr.HSM13, with refinements on their "kind" (is_ee etc.). There are additional refinements for stitching together the indices of multiple reprs in the same flight (see https://github.com/project-everest/mitls-fstar/pull/225/files#diff-52d8985a276b9061a526ee72c6b100a7R195).

The (ad-hoc) receive function returns this flight, with s (stateful) valid repr predicate for each of the reprs in the flight (see https://github.com/project-everest/mitls-fstar/pull/225/files#diff-52d8985a276b9061a526ee72c6b100a7R215).

Also some minor changes in MITLS.Repr here: https://github.com/project-everest/mitls-fstar/pull/225/files#diff-bb3be56c5c41c7d3146f3a6a947f1a4d.