[TLS] Re: New Version Notification for draft-usama-tls-risks-of-mlkem-00.txt

[Yaakov Stein <[e-mail]>]

After reading a bit more of your code, I think this clinches it :

reduc forall sk:kem_sk, r:bitstring;
  decap(sk, encap_ct(pk(sk), r)) = encap_ss(pk(sk), r).

As I said, I don’t know ProVerif syntax and am using copy-and-paste
(in particular, that semicolon mystifies me).

Y(J)S

From: Yaakov Stein <ystein=[e-mail]>
Sent: Thursday, May 28, 2026 5:06 PM
To: Muhammad Usama Sardar <[e-mail]>; [e-mail]
Subject: [EXTERNAL] [TLS] Re: New Version Notification for draft-usama-tls-risks-of-mlkem-00.txt

Muhammad,

The fact that commutativity is blocking your formal correctness proof must be an artifact.
There are many commutative schemes that are not safe (how about adding two partial keys?),
and many non-commutative ones that are (as most informally believe for KEMs).

I am not a ProVerif expert, but I waded through your code,
and think I understand where the issue appears and what to do about it.

As I believe you said (but couldn’t find the email), the commutativity of DH is posited here
(and mentioning “commutativity” or “symmetry” in a comment would make it easier to find):
fun dh_ideal(element,bitstring):element.
equation forall x:bitstring, y:bitstring;
     dh_ideal(dh_ideal(G,x),y) =
     dh_ideal(dh_ideal(G,y),x).

Now, in
fun dh_exp(group,element,bitstring):element
reduc forall g:group, e:element, x:bitstring;
      dh_exp(WeakDH,e,x) = BadElement
otherwise forall g:group, e:element, x:bitstring;
      dh_exp(StrongDH,BadElement,x) = BadElement
otherwise forall g:group, e:element, x:bitstring;
      dh_exp(StrongDH,e,x) = dh_ideal(e,x).

when one side computes:
let gxy = e2b(dh_exp(g,gy,x))
while the other side does:
let gxy = e2b(dh_exp(g,gx,y))
they are provably equal.

So, you are not really using the fact that either side could have initiated the TLS
and we would get the same shared secret (which is not what happens in client-server usage anyway)
you are just relying on it to prove that the two sides end up with the SAME shared secret
in a single TLS session.

Now, KEMs do not build a shared secret from symmetric participation of two sides,
but they still end up with the two sides arriving at the same shared secret.
This arises from one side generating the secret (and thus knowing it)
and the other side decrypting a public key encrypted version (and thus also learning it).

So, you need to model decap(sk,ct) produces the same shared secret ss
and drop this in, instead of agreement from commutativity.

Something like (forgive my not being an expert in ProVerify syntax)
fun pk(kem_sk): kem_pk.

fun encap_ct(kem_pk, bitstring): kem_ct.
fun encap_ss(kem_pk, bitstring): kem_ss.

fun decap(kem_sk, kem_ct): kem_ss.

Now, the last thing I want is for this to produce the result that pure MLKEM is sufficient now.
The real missing element in your code is not the removing of the commutativity artifact,
but rather modeling different failure modes:

  1.  There is no CRQC, and neither ECC nor MLKEM are broken (hybrid and pure are proven safe)
  2.  There is no CRQC, but someone finds a classical break for MLKEM (in which case hybrids are OK but pure MLKEM is not)
  3.  There is a CRQC and thus ECC is broken, but MLKEM withstands all classical and quantum attacks (and pure MLKEM is proven correct),
  4.  There is a CRQC and thus ECC is broken, and someone finds a classical or quantum break for MLKEM (in which case we expect nothing to be safe)
(I left out some less likely cases such as ECC breaking classically and MLKEM not.)

I would appreciate hearing from you what you think about both points.

Y(J)S

This message is intended only for the designated recipient(s). It may contain confidential or proprietary information. If you are not the designated recipient, you may not review, copy or distribute this message. If you have mistakenly received this message, please notify the sender by a reply e-mail and delete this message. Thank you.
This message is intended only for the designated recipient(s). It may contain confidential or proprietary information. If you are not the designated recipient, you may not review, copy or distribute this message. If you have mistakenly received this message, please notify the sender by a reply e-mail and delete this message. Thank you.