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

[Joseph Salowey <[e-mail]>]

There is rough consensus that the document should have additional formal
analysis before publication. Ekr proposed the following for the
authentication property, which seems like a reasonable clarification

"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."

At this point it is up to the authors and working group to address the
request for additional symbolic analysis in order to move the document
forward.

The consensus call also indicated that there is a need to continue to work
out the process for formal analysis triage which we are working on as a
separate topic. See interim scheduling poll from Sean.

On Fri, Aug 23, 2024 at 10:30 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.
>
> 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
>