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

[Nadim Kobeissi <[e-mail]>]

You know what? I did my PhD work mostly in ProVerif. I’ll just go and write some new models myself. I’ll keep you all posted, if that’s how you’re going to be.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 28 May 2026, at 10:20 PM, Nadim Kobeissi <[e-mail]> wrote:
> 
> Hi Eric,
> 
> I think this would be reasonable if the discussion had veered off to, say, some kind of high-level ProVerif tutorial, or worse, some eggheaded discussion on esoteric properties of Horn clauses as they apply to ProVerif. But neither of these are true; the discussion was still very much grounded in how to best apply ProVerif to TLS 1.3, and came after I had done hours of work today trying to explain the impact of the three papers you cited on the discussion.
> 
> In that light, the chairs’ decision feels quite stifling.
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
>> On 28 May 2026, at 10:17 PM, Eric Rescorla <[e-mail]> wrote:
>> 
>> I agree with Sean. This is not the right place to debug/refine the formal models. It would be the right place to report on the results of the modelling work/
>> 
>> -Ekr
>> 
>> 
>> On Thu, May 28, 2026 at 12:59 PM Nadim Kobeissi <[e-mail]> wrote:
>>> I did an actual real-life double-take reading this. Discussions formal models of TLS are off-topic for this list?
>>> 
>>> Is this a joke?
>>> 
>>> Also, it’s ProVerif, Sean, not “pro-verify”.
>>> 
>>> Nadim Kobeissi
>>> Symbolic Software • https://symbolic.software <https://symbolic.software/>
>>> 
>>>> On 28 May 2026, at 9:26 PM, Sean Turner <[e-mail] <mailto:[e-mail]>> wrote:
>>>> 
>>>> Please take the detailed discussion about the pro-verify model off list.
>>>> 
>>>> Discussions about the specifics of any formal analysis model are off topic for this mailing list as well as in-person/virtual TLS WG meetings.
>>>> 
>>>> Please note that what is in scope WRT formal analysis is the draft, the claims, and the results of the formal analysis. The specific details about how the formal analysis is arrived at is not on topic.
>>>> 
>>>> Thanks,
>>>> Joe and Sean
>>>> 
>>>>> On May 28, 2026, at 12:05, Muhammad Usama Sardar <[e-mail] <mailto:[e-mail]>> wrote:
>>>>> 
>>>>> Hi Yaakov,
>>>>> 
>>>>> 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.
>>>>> 
>>>>> Kindly let me know if I misunderstood some of your comments:
>>>>> 
>>>>> On 28.05.26 16:06, Yaakov Stein wrote:
>>>>>> 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,
>>>>>> 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.
>>>>> 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.
>>>>>> The real missing element in your code is not the removing of the commutativity artifact,
>>>>>> but rather modeling different failure modes:
>>>>> 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.
>>>>>> There is no CRQC, and neither ECC nor MLKEM are broken (hybrid and pure are proven safe)
>>>>>> There is no CRQC, but someone finds a classical break for MLKEM (in which case hybrids are OK but pure MLKEM is not)
>>>>>> There is a CRQC and thus ECC is broken, but MLKEM withstands all classical and quantum attacks (and pure MLKEM is proven correct),
>>>>>> 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.
>>>>> 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
>>>>> 
>>>>> _______________________________________________
>>>>> TLS mailing list -- [e-mail] <mailto:[e-mail]>
>>>>> To unsubscribe send an email to [e-mail] <mailto:[e-mail]>
>>>> _______________________________________________
>>>> TLS mailing list -- [e-mail] <mailto:[e-mail]>
>>>> To unsubscribe send an email to [e-mail] <mailto:[e-mail]>
>>> 
>>> _______________________________________________
>>> TLS mailing list -- [e-mail] <mailto:[e-mail]>
>>> To unsubscribe send an email to [e-mail] <mailto:[e-mail]>
>