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

[Muhammad Usama Sardar]

Hi Yaakov,






Kindly let me know if I misunderstood some of your comments:

On 28.05.26 16:06, Yaakov Stein wrote:

Thanks for your valuable input. That's indeed very useful. Some quick thoughts inline, since you requested. I will report back more details after carefully and thoroughly double-checking everything. Whenever you have time, I will appreciate a couple of clarifying questions inline. In case it helps, [0] has full details of my ProVerif modeling and its semantics.

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).

Sure, there are several cryptographic proofs for DHKE which are the basis for this property. I will add those references to be clear.

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.

Thanks a lot. Really appreciate your time.

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):

Sure, I'll add comments for easier search. Thanks for your valuable feedback. If some areas of code were hard to understand or need more comments, I'll love to hear that to make it more readable for other authors so that they can extend the models in future.

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.

Please note that gxy,g,x,y etc. are all local variables of Client and Server processes. For simplicity, ignoring transformation 'e2b' and assuming StrongHash and there is no BadElement, Client process will have:

gxy = gy^x

and Server process will have:

gxy = gx^y

These are two separate 'terms' in ProVerif. ProVerif is unable to distinguish between the two. Could you please clarify how without the "equation" they can both be equal? To be clear: is your understanding that even if I remove the 'equation,' the proof should still work as-is? I think it is an essential ingredient in the proof.

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)

To clarify, my understanding is that the client is by definition the endpoint which initiates the connection, consistent with RFC8446bis, Sec. 1.1 [1].

I know that some papers in literature have taken the position that you are mentioning. I do not object to that, but to the best of my knowledge, they haven't found any /real/ additional attacks.

you are just relying on it to prove that the two sides end up with the SAME shared secret

in a single TLS session.

Could you please explain this point? I think this is the main point of confusion. See my clarification of the two 'gxy' above.

Now, KEMs do not build a shared secret from symmetric participation of two sides,

This arises from one side generating the secret (and thus knowing it)



So, you need to model *decap(sk,ct) produces the same shared secret ss*

and drop this in, instead of agreement from commutativity.

but they still end up with the two sides arriving at the same shared secret. and the other side decrypting a public key encrypted version (and thus also learning it).

It didn't work for me. I think at the very least something to replace commutativity is required.

Something like (forgive my not being an expert in ProVerify syntax)

no worries at all. This is still very useful. I think we are largely in sync. Syntax is no problem. Please don't worry about that.

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.

Mind clarifying what do you have 'bitstring' for? That's the only difference I have (using your symbols):

fun encap_ct(kem_pk): kem_ct.

fun encap_ss(kem_pk): kem_ss.

I have followed the NIST FIPS 203: Algorithm 20, p. 37 [2]. It seems that the algorithm takes as input only variable (ek in [2]). Please correct me if I am misunderstanding something or missing something in the FIPS 203 spec.

Now, the last thing I want is for this to produce the result that pure MLKEM is sufficient now.

but rather modeling different failure modes:

The real missing element in your code is not the removing of the commutativity artifact,

Sure, the purpose of both Karthik et al.'s work as well as mine was to study security under non-PQ threat model. I started updating it for the simplest scenario (mode 1 in your proposal). Once the simplest PQ case works out, I will add the four scenarios as per your guidance.

 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 would appreciate hearing from you what you think about both points.

(I left out some less likely cases such as ECC breaking classically and MLKEM not.)

Please feel free to share if more explanation on any of points will be helpful. Would be happy to explain anything unclear.

Kind regards,

-Usama

[0] https://www.researchgate.net/publication/396593308_Perspicuity_of_Attestation_Mechanisms_in_Confidential_Computing_General_Approach

[1] https://www.ietf.org/archive/id/draft-ietf-tls-rfc8446bis-14.html#section-1.1

[2] https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.203.pdf

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
TLS mailing list -- tls@ietf.org
To unsubscribe send an email to tls-le...@ietf.org