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

[Eric Rescorla <[e-mail]>]

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