On Fri, May 22, 2026 at 10:16:07PM +0200, Muhammad Usama Sardar wrote: > > Maybe I should have actually cited the original artifacts by Karthik et al. > Specifically, the point under discussion in Sec. 2.1 of -00 can be seen > exactly in their model [1]. Several years ago I basically started with their > model of draft-20 as a baseline and did the following extensions: > > * fixed the key schedule > * updated to the RFC8446bis > * integrated attestation (such as draft-fossati-tls-attestation) > > I have a hard time convincing myself to attest to "shortcomings" in the > proof models. There /may/ be multiple ways to model and they may /all/ be > correct. My position is that this is correct modeling. At least I don't see > why proof via commutativity is wrong.
The problem with commutativity is that it does not work with quantum- safe algorithms[1]. Neither stand-alone nor hybrid algorithms. The latter is because it is not sound to argue that the traditional component makes hybrids secure. For instance, it is possible to prove that both MLKEM1024 and X25519MLKEM768 are sound. However, neither can be proven in the formal model. And with the recent 2029 target, things are already highly critical. > Whether this is the /best/ way to model TLS 1.3 is questionable, and > probably the best person to provide this justification is Karthik because I > /extended/ his models. But then we come back to the point of contacting FATT > [2] because he is in FATT. See above why that way does not cut it anymore. [1] At least outside some really exciting stuff. -Ilari _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
