On Sun, May 24, 2026 at 12:43 PM David Benjamin <[email protected]> wrote:
> On Sat, May 23, 2026 at 1:27 PM Ilari Liusvaara <[email protected]> > wrote: > >> 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. >> > > +1. Commutativity may give a correct proof for *this* model of TLS, but > that's not relevant here. The question is whether this model is *useful* > today. > Does it correctly model the scenarios the TLS WG is interested in today? If > it does not, this model is no longer useful because it cannot answer the > questions the WG needs to answer. > > When TLS 1.3 was being developed, with classical cryptography, the answer > was yes. Our key agreement primitives were Diffie-Hellman, so a model that > relied on Diffie-Hellman-specific was useful, and indeed TLS 1.3 got some > mileage out of that work. > > But it is not 2018 anymore. Post-quantum primitives, broadly, do not look > like Diffie-Hellman, so a model that relies on commutativity is clearly no > longer useful to this working group. Such a model *cannot* say anything > about *either* MLKEM1024 *or* X25519MLKEM768. It's not that MLKEM1024 and > X25519MLKEM768 are bad for breaking that model. The model just doesn't > apply anymore. To *usefully* model the impacts of *either* primitive on > TLS, we need a model that starts from an idealized KEM, not an idealized > Diffie-Hellman primitive. > FWIW, it appears to me that we do have some formal verification of TLS 1.3 with MLKEM: Huguenin-Dumittan and Vaudenay (TLS 1.3 with pure ML-KEM) https://eprint.iacr.org/2021/844 Zhao, Jiang, and Zhao (TLS 1.3 with pure ML-KEM) https://eprint.iacr.org/2024/1360 Blanchet and Jacomme (TLS 1.3 with hybrid) https://bblanche.gitlabpages.inria.fr/publications/BlanchetJacommeCSF24.pdf I haven't really read these papers so can't speak to them in detail. I'd be interested in hearing what other WG members think. Now, the WG has two plausible directions to go based on this: > > 1. The WG can decide to defer *both* drafts on someone updating this > particular model to capture a KEM. (Non-commutativity applies equally to > both.) > > 2. The WG can decide that, even though it no longer has the input of *this > model*, it is sufficiently satisfied that MLKEM1024 and X25519MLKEM768 > are valid integrations of their respective primitives into TLS. > This seems mostly right to me. I suppose it's possible we might have an analysis that demonstrated that TLS 1.3 with hybrids no matter what the status of MLKEM, in which case we would have confidence in the absence of a CRQC. I'm not quite sure how one would phrase this, perhaps that the attacker gets to supply both MLKEM shares and the output secret? Keep in mind that *none* of these modeling exercises have anything to do > with the security of ML-KEM as a KEM, or of X25519 as a Diffie-Hellman > primitive. No model of this form will say anything useful about them. They > start by assuming the primitives are correct and checks if TLS used them > right. Questions of *whether* ML-KEM is a secure KEM need to analyze the > primitive itself, such as what was done throughout the NIST process. That > means this entire discussion of formal methods has nothing to do with the > question of whether or hedge ML-KEM with an existing, > known-quantum-vulnerable algorithm. > This seems like the key point. Most of the concerns I have seen raised about pure MLKEM are about the strength of the primitive, not about its TLS integration. -Ekr > >> 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] >> > _______________________________________________ > TLS mailing list -- [email protected] > To unsubscribe send an email to [email protected] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
