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 
> <mailto: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

Reply via email to