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

[Muhammad Usama Sardar <[e-mail]>]

Dear chairs,

I had a short meeting with Russ today and we don't understand 
/precisely/ what the FATT is worried about and therefore why a formal 
analysis is required at all.

Extending CH and SH to negotiate external PSK follows the best current 
practice for extending TLS. Moreover, external PSK (shared out of band) 
instead of zero in the initial handshake can't make security worse. Even 
if external PSK is leaked, it's not worse than a known constant (zero). 
What could possibly go wrong?

I don't see any liaison announced for this draft. So I don't know whom 
to ask for it. Could you please clarify with the FATT exactly which 
property from Appendix E.1 of RFC8446 it thinks might break with this 
draft?

Thanks,

Usama

On 23.08.24 18:30, Joseph Salowey 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 
> <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 [e-mail]