Re: [TLS] Adoption call for draft-rescorla-tls-ctls

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