Hi Ilari,Thank you for your feedback. I don't see how you derived the conclusions from my email because I didn't intend to say any such things. Perhaps my response was not precise. Let me try to clarify the misunderstandings below.
On 09.03.26 15:40, Ilari Liusvaara wrote:
On Sun, Mar 08, 2026 at 11:49:36PM +0100, Muhammad Usama Sardar wrote:Hi John, Thanks for initiating this discussion and sharing your insightful comments. On 08.03.26 10:32, John Mattsson wrote:Any potential problems would be in the composition between MLS and TLS 1.3.It seems clear that formal analysis would be required for this draft.- The security considerations could be expanded.I agree and I will be happy to work with Russ to address this concern, as we worked for 8773bis before. In general, I really appreciate the document structure, in particular the "Motivation and Design Rationale" section.This looks like a massive change to TLS 1.3, and one that would not be a small tweak to existing analysis (like 8773bis or EKU), but require a whole new analysis.
Please note that I did not intend to compare the formal analysis effort required here with the one for 8773bis or EKU at all. I made three points in my email (rephrasing and expanding for clarity below):
1. Formal analysis would be required for this draft to fly. While TLS and MLS are independently verified, their composition may not necessarily be secure. 2. I share John's concern on security considerations and I am offering help to Russ to revise the security considerations and do the formal analysis to get it through FATT. I mentioned 8773bis in the sense that he promptly responded to all my questions, promptly provided all the inputs I requested, and when I found a problem [0], he promptly acknowledged it and merged my PR within a week. That is the ideal author-verifier collaboration model, and I am confident we'll make this one work as well. 3. I appreciated his document structure, which is very close to best practices template that I would like to see. I am looking forward to discussing this in my presentation next week.
Furthermore, I think this mechanism is far too complex for updating shared secrets, with huge amount of accidental complexity. There is absolutely nothing "straightforward" about this.
From #1-3, I am not sure why or how you interpreted my support to Russ as implying the mechanism being "straightforward" or "not complex". Recall that I was not happy with the FATT requesting a formal analysis of 8773bis. So by asserting that the tls-using-mls-handshake draft requires formal analysis in #1, I was actually acknowledging that it is non-trivial one.
I acknowledge your concern about complexity which is a real risk as it might lead to state space explosion. It's hard to say anything until I have a thorough look at the MLS proofs and I have a formal model for composition of MLS with TLS, and I have formalized all the properties to be checked, and I have put them in ProVerif to test. But once done, that would actually mean I would have done all the (several months of) effort for the verification, potentially just to find out that ProVerif cannot solve it in reasonable time. I am not aware of any practical way to know in advance whether it would lead to state space explosion. It's an unfortunate world (of formal methods) I live in. I do understand that not many members live in that world and that's even more unfortunate for me.
I respectfully disagree. I believe the first thing to do is to have a realistic threat model. The discussion of complexity comes next. I see that you agree below that we don't have the predicate satisfied yet.As complex as EKU seems, it is mostly essential complexity.
Furthermore, the threat model seems just as dubious as the one EKU uses,
I don't see a threat model in tls-using-mls-handshake draft. Maybe I missed something. That's one of the things I'm hoping to work with Russ to make it explicit in security considerations (#2).
And thanks for acknowledging that the threat model of EKU is dubious. I think the concern I have been raising [1] needs a serious discussion in the meeting, and the authors need to explain the threat model more precisely. I believe consistently avoiding this question in the meetings is leading us just nowhere. My question will not just suddenly disappear one day. I will raise in each and every meeting until I am provided a satisfactory and believable answer, because key schedule is security-critical function.
and I do not think it is even possible to compose MLS and TLS in any remotely reasonable way. Group messaging and transport are to very different things.
Maybe that's not a good argument. As an example, attestation and transport are also two very different things and we have SEAT WG composing the two. I think what matters is the real-world use cases and their corresponding requirements.
Best regards, -Usama [0] https://mailarchive.ietf.org/arch/msg/tls/6Wk82oBGd61rTK23DgfYb7BmRKM/ [1] https://mailarchive.ietf.org/arch/msg/tls/vM60CqbWgt-rnghnIEDdiHFJHcw/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
