On Sun, May 24, 2026 at 4:10 PM Eric Rescorla <[email protected]> wrote:
> 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. > Ah, nice find! I figured this *must* exist by now, but wasn't sure. The draft, by omission, implied there wasn't, but *surely* integrating a key agreement as important as ML-KEM, into a protocol as important as TLS, would have attracted the eye of *some* formal methods enthusiast by now. :-) > 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? > Sure. It *is* conceivable that we: - Are confident that *if X25519 is secure*, TLS 1.3 with X25519MLKEM768 is secure - Are *not* confident that *if ML-KEM-768 is secure,* TLS 1.3 with X25519MLKEM768 is secure But I don't think that situation should be good enough for X25519MLKEM768. I mean, the whole point of X25519MLKEM768 is to incorporate ML-KEM. We're burning a whole kilobyte of ClientHello to do it. If we aren't even satisfied that we integrated ML-KEM correctly, what are we even doing here? The bar for *either* draft-ietf-tls-ecdhe-mlkem or draft-ietf-tls-mlkem should include being satisfied in the ML-KEM integration. (To be clear, I think we solidly meet that bar, so this is all moot. Just that, even if we didn't, it would still not be a reason to artificially separate the drafts.) > 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]
