Unsurprisingly, I am in favor of requiring formal alnalysis (option 1), as I think all nontrivial extensions to TLS should have some formal analysis.
I would note that the main rationale for this specification is as future-proofing for PQ. With the publication of ML-KEM by NIST, PSKs become less attractive for this purpose, which I think makes the case for PS weaker and thus the case for proceeding with PS without analysis also weaker. I would modify the question slightly as below: On Fri, Aug 23, 2024 at 10:32 AM Joseph Salowey <j...@salowey.net> wrote: > 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. > I think the right analysis is one in which the attacker knows the PSK. For instance, say we have a company where everyone shares a PSK (as some kind of post-quantum protection) and you want to make sure employee A cannot impersonate employee B. -Ekr > 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 >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
