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. 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. Are you proposing that we take path (1) and delay both drafts? I am strongly opposed to this. (2) is the clear decision here. If you truly believe more modeling is needed, rather than trying to selectively delay only one of two applicable drafts with circuitous discussion, I'd encourage you to apply your formal methods expertise to update those models. Whether the outcome is a updated model that checks out, or a concrete problem with (1) and (2), I think either results would be quite valuable. 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. > 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]
