Yes, but the question is whether the protocol actually *provides* the property that authentication is based on certificates. The point of the analysis is to determine that.
-Ekr On Mon, Sep 23, 2024 at 3:55 PM Russ Housley <hous...@vigilsec.com> wrote: > I agree, and I think the Security Considerations already cover this point: > > If the external PSK is known to any party other than the client and > the server, then the external PSK MUST NOT be the sole basis for > authentication. The reasoning is explained in Section 4.2 of > [K2016]. When this extension is used, authentication is based on > certificates, not the external PSK. > > Russ > > On Sep 23, 2024, at 4:49 PM, Joseph Salowey <j...@salowey.net> wrote: > > 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 <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. >> >> 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 >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
