In regard to moving RFC 8773 to standards track the formal analysis triage group has provided input on the need for formal analysis which was posted to the list [1]. The authors have published a revision of the draft [2] to address some of this feedback, however the general sentiment of the triage panel was that there should be some additional symbolic analysis done to verify the security properties of the draft and to verify there is no negative impact on TLS 1.3 security properties.
The formal analysis is to verify the following properties of the proposal in the draft: - The properties of the handshake defined in Appendix E.1 of RFC8446 [3] remain intact if either the external PSK is not compromised or (EC)DH is unbroken. - The public key certificate authentication works as in TLS 1.3, and this extension adds the condition that the party has possession of the external PSK. The details of external PSK distribution are outside the scope of this extension. This is a consensus call for the working group to determine how to proceed between these two options: 1. Require formal analysis in the symbolic model to verify that the proposal in the document does not negatively impact the security properties of base TLS 1.3 and that the additional security properties cited above are met 2. Proceed with publishing the document without additional formal verification Please respond to the list with a brief reason why you think the document requires formal analysis or not. This call will end on September 16, 2024. Thanks Joe, Deirdre, and Sean [1] https://mailarchive.ietf.org/arch/msg/tls/vK2N0vr83W6YlBQMIaVr9TeHzu4/ [2] https://author-tools.ietf.org/iddiff?url1=draft-ietf-tls-8773bis-00&url2=draft-ietf-tls-8773bis-02&difftype=--html [3] https://www.rfc-editor.org/rfc/rfc8446.html#appendix-E.1
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
