I support this effort, and would like to point out that we have recently
published a paper [1] and a collection of tools [2] to automatically
verify the security (non malleability) of binary message formats, which
we successfully applied to all of TLS [3] (which revealed many small
specification errors in published RFCs, and some malleability problems
such as the lack of tag in the CertificateEntry type).
Using this collection of tool, if the new compact format is expressible
in the same syntax as TLS, it may be relatively easy to formally prove
that the compact and full message formats are equivalent (and most of
the proof is automated), by writing the lifting from the compact to the
full specification types. I also recommend to formalize the message
format specification language such that automatic tools like ours can
directly operate over the formats described in the RFC.
[1]
https://www.microsoft.com/en-us/research/uploads/prod/2019/05/20190601everparse.pdf
[2] https://github.com/project-everest/everparse
[3]
https://github.com/project-everest/mitls-fstar/blob/dev/src/parsers/Parsers.rfc
Best,
Antoine
On 2019-11-21 05:36, Sean Turner wrote:
At IETF 105, ekr presented cTLS (Compact TLS) [0][1][2] to both the
TLS WG and the LAKE BOF, which is now a chartered WG [3]. After some
discussions, the ADs suggested [4] that the TLS WG consider whether
this draft be adopted as a TLS WG item. LAKE could then later
specify/refer/adopt/profile it, as appropriate. The authors revised
cTLS and presented the revised draft at IETF 106 [5]. At IETF 106
there was support for adoption of cTLS as a WG item. To confirm this
on the list: if you believe that the TLS WG should not adopt this as a
WG item, then please let the chairs know by posting a message to the
TLS list by 2359 UTC 13 December 2019 (and say why).
NOTE:
: If the consensus is that this draft should be adopted as a WG item,
then this will necessarily result in a WG rechartering discussions.
We would have gotten to this rechartering discussion anyway now that
DTLS 1.3 is progressing out of the WG.
Thanks,
Chris, Joe, and Sean
[0] https://datatracker.ietf.org/doc/slides-105-tls-sessa-ctls/
[1] https://datatracker.ietf.org/doc/draft-rescorla-tls-ctls/
[2] https://github.com/ekr/draft-rescorla-tls-ctls
[3] https://datatracker.ietf.org/doc/draft-rescorla-tls-ctls/
[4]
https://mailarchive.ietf.org/arch/msg/lake/kACwW7PXrmTRa4PvXQ0TA34xCvk
[5]
https://datatracker.ietf.org/meeting/106/materials/slides-106-tls-compact-tls-13-00.pdf
_______________________________________________
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls
_______________________________________________
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls
