Agree that it would be good publish a timely revision clarifying these issues. Doing so improves the current situation.
I don’t think we have to prioritize formal verification versus getting out a timely revision clarifying the issues. We could start formal verification and at the same time publish a revision. If the formal verification later show that more changes are needed, we publish 9147bisbis. John From: Eric Rescorla <e...@rtfm.com> Date: Saturday, 7 December 2024 at 18:56 To: hannes.tschofe...@gmx.net <hannes.tschofe...@gmx.net> Cc: John Mattsson <john.matts...@ericsson.com>, Russ Housley <hous...@vigilsec.com>, Joe Salowey <j...@salowey.net>, IETF TLS <tls@ietf.org> Subject: Re: [TLS] Re: Adoption call for RFC 9147bis FWIW, I generally agree with John that it would be best if everything nontrivial that comes out of TLS WG was formally verified (props to to Muhamed, Arto, Hannes and Thomas for doing that for TLS attestation). I also think it would be helpful to have some kind of formal analysis for 9147-bis and I'd definitely be interested in participating in it. I do think the situation is a little different in this case because we already published DTLS 1.3 and the purpose of the -bis is to fix some known issues, so at the end of the day we may have to prioritize formal verification versus getting out a timely revision clarifying these issues. However, the process will take some time, so we certainly do not have to decide now and the best way to avoid having to is to try to get the analysis moving sooner rather than later. -Ekr On Sat, Dec 7, 2024 at 9:23 AM <hannes.tschofenig=40gmx....@dmarc.ietf.org<mailto:40gmx....@dmarc.ietf.org>> wrote: Have to add a note to this statement: “ Formal verification would likely have caught several of the issues identified by David Benjamin as well as the issues with post-handshake messages when replay protection is turned off identified by me. I hope everything going out the TLS WG in the future will be formally verified. “ When everything goes smoothly, it’s the working group that gets the credit. But when something goes wrong, the blame falls squarely on the authors. I am looking forward to your contributions to the formal analysis since you missed the opportunity last time. Ciao Hannes From: John Mattsson <john.mattsson=40ericsson....@dmarc.ietf.org<mailto:40ericsson....@dmarc.ietf.org>> Sent: Montag, 2. Dezember 2024 19:43 To: Russ Housley <hous...@vigilsec.com<mailto:hous...@vigilsec.com>>; Joe Salowey <j...@salowey.net<mailto:j...@salowey.net>> Cc: IETF TLS <tls@ietf.org<mailto:tls@ietf.org>> Subject: [TLS] Re: Adoption call for RFC 9147bis Hi, I support adoption and just like Russ I look forward to formal verification. Formal verification would likely have caught several of the issues identified by David Benjamin as well as the issues with post-handshake messages when replay protection is turned off identified by me. I hope everything going out the TLS WG in the future will be formally verified. Cheers, John From: Russ Housley <hous...@vigilsec.com<mailto:hous...@vigilsec.com>> Date: Monday, 2 December 2024 at 19:00 To: Joe Salowey <j...@salowey.net<mailto:j...@salowey.net>> Cc: IETF TLS <tls@ietf.org<mailto:tls@ietf.org>> Subject: [TLS] Re: Adoption call for RFC 9147bis I do not object, but I look forward to the FATT review. Russ On Dec 2, 2024, at 12:38 PM, Joseph Salowey <j...@salowey.net<mailto:j...@salowey.net>> wrote: This is a call for adoption of draft-rescorla-tls-rfc9147bis-00[1] as the basis for an RFC9147 bis document. This document is seeded with the content of RFC 9147. If you object to the adoption of this document please respond to this thread by December, 9 2024. Cheers, Joe, Deirdre, and Sean [1] https://datatracker.ietf.org/doc/html/draft-rescorla-tls-rfc9147bis-00 _______________________________________________ TLS mailing list -- tls@ietf.org<mailto:tls@ietf.org> To unsubscribe send an email to tls-le...@ietf.org<mailto:tls-le...@ietf.org> _______________________________________________ TLS mailing list -- tls@ietf.org<mailto:tls@ietf.org> To unsubscribe send an email to tls-le...@ietf.org<mailto:tls-le...@ietf.org>
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
