[TLS]Re: Consensus call for RFC8773bis Formal Analysis Requirement

[Eric Rescorla <[e-mail]>]

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 <[e-mail]> 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 -- [e-mail]
> To unsubscribe send an email to [e-mail]
>