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 --tls@ietf.org
To unsubscribe send an email totls-le...@ietf.org
_______________________________________________
TLS mailing list -- tls@ietf.org
To unsubscribe send an email to tls-le...@ietf.org
