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> 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> > *Sent:* Montag, 2. Dezember 2024 19:43 > *To:* Russ Housley <hous...@vigilsec.com>; Joe Salowey <j...@salowey.net> > *Cc:* IETF TLS <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> > *Date: *Monday, 2 December 2024 at 19:00 > *To: *Joe Salowey <j...@salowey.net> > *Cc: *IETF TLS <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> 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 > 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 >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
