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

[Muhammad Usama Sardar <[e-mail]>]

Hi Nadim,

Thank you for your valuable input. TL;DR is that none of the three 
papers is /symbolic/ (vs. computational) proof for standalone ML-KEM for 
TLS. The two papers for standalone ML-KEM are computational proofs. Both 
symbolic and computational proofs are complementary and not a substitute 
of each other.

Social media posts are distraction and out of scope of IETF. So let's 
please close that topic.

> 1. Huguenin-Dumittan & Vaudenay (eprint 2021/844). This is a 
> pen-and-paper game-based proof, not automated verification model, 
> which I think is what the FATT is mainly concerned with. The main 
> theorem shows the TLS 1.3 handshake with the DH key exchange replaced 
> by a KEM is secure in the Dowling et al. MultiStage model whenever the 
> KEM is OW-CPA. ML-KEM, being IND-CCA, trivially satisfies this. The 
> authors themselves note the resulting bound is "very much non-tight," 
> and QROM is left as an open problem. Effectively, this is qualitative 
> reassurance for pure-KEM TLS 1.3, not a tight practical bound.
>
> 2. Zhao, Jiang & Zhao (eprint 2024/1360) closes both of those gaps: 
> the paper tightens the ROM bound from O(q^6) to O(q) (O(1) for rigid 
> D-OW-CPA KEMs like NTRU and Classic McEliece), and provides the first 
> QROM proof. CRYSTALS-Kyber (= ML-KEM-PKE) is the named instantiation. 
> This is still pen-and-paper, but this is the closest thing that seems 
> to have been cited so far to a tight, QROM-valid computational 
> analysis of pure-KEM TLS 1.3.
 From my perspective, the key point is that both are computational-level 
proofs using pen-and-paper. None of them is maintainable and easily 
extensible if we were to use ML-KEM as a default in the future.

More importantly, none of these is symbolic proof. ProVerif can be used 
for symbolic proof. It also provides an automated way to update the 
proofs for extensions in the future.

In any case, it is up to the WG if computational proofs are deemed 
sufficient.

Even if they are sufficient, I believe it remains valuable to complement 
those results with an automated proof in ProVerif.

>
> 3. Blanchet & Jacomme (CSF ’24) is actually a mechanized CryptoVerif 
> proof of draft-ietf-tls-hybrid-design-09 (the X25519+MLKEM hybrid 
> draft) under post-quantum sound semantics the authors had to develop 
> for the tool. Theorem 3 establishes forward secrecy of hybrid TLS 1.3 
> against quantum attackers under PQ-IND-CCA2 of the KEM, PQ-PRF for 
> HMAC, PQ-CR for the hash, and classical EUF-CMA for signatures.
Thanks, that is very helpful. By any chance, could you possibly share 
your opinion whether there is any substantive change from -09 to -16 
that might invalidate that proof in CryptoVerif? If there is no such 
substantive change, that should already address the concern of folks.
> So, Eric's framing appears to be correct, as far as I can tell: 
> pure-KEM TLS 1.3 is covered by (1) and (2), and the hybrid is 
> mechanically verified by (3).
As a summary, there is /no/ computerized proof for standalone ML-KEM in 
TLS in the three papers shared, whereas there /is/ computerized 
(computational) proof for draft-ietf-tls-hybrid-design-09 in CryptoVerif.

> Secondly, none of these are ProVerif proofs, which I think is what 
> Muhammad is pushing for.
Exactly, and more broadly computerized proofs at symbolic level which 
can be updated for future extensions.
> Separately from the merits of any specific draft, the broader symbolic 
> verification literature for TLS 1.3 does have a real gap: existing 
> ProVerif models bake DH commutativity equations into the primitive 
> layer, so they cannot speak to KEM-based key exchange, pure or hybrid. 
> Now, of course, you can choose to simply not care about ProVerif 
> models, or, say, prefer Tamarin models, that’s your prerogative! But 
> if you think ProVerif models are worth anything, then updating those 
> models with an idealized-KEM abstraction is legitimate, useful work, 
> and contributions on that front would be welcome from anyone willing 
> to do them.
ProVerif and Tamarin are both acceptable tools. This was already 
clarified by FATT a couple of years ago. In fact, I have exclusively 
used ProVerif for all the drafts so far. AFAIK, Hannes and Chris also 
use ProVerif.

> To be clear about my own view: Muhammad's advocacy has been argued in 
> a way that conflates "the model no longer applies" with "the protocol 
> is risky," and uses procedural levers (FATT) asymmetrically across the 
> standalone and hybrid drafts, points that David, Ilari, Ekr, Mattsson, 
> and Bas have already addressed at length. But the underlying 
> methodological request, a KEM-aware ProVerif model of TLS 1.3, is 
> independently legitimate, and dismissing this along with the framing 
> is mistaken and illegitimate on its own. What I’m saying is that we 
> can reject the procedural argument while welcoming the modeling work.
I would note that 'no analysis required' is a perfectly valid output of 
FATT review. Moreover, FATT output is subject to approval by the WG.

So FWIW, asking for FATT review is actually harmless.

> [...] The referents are unambiguous: Muhammad, and Bas's earlier 
> message on this thread. [...]
First things first. Social media activity is outside the scope of the 
IETF. Please don't bring anything happening on the social media to the 
IETF lists. If someone has substantial technical feedback, he can join 
the list to post or submit to me by email and I would very much welcome 
that and try my best to address that.

About the text you quoted, TLS WG is not a "cryptography standards 
group." The closest I can think of for that post is CFRG. Moreover, to 
the best of my knowledge, Bas is at Cloudflare and thus not an "academic 
cryptographer." So I believe you are misunderstanding the social media post.

Even if you /were/ right, I believe it's perfectly fine if someone 
somewhere in the world does not like my draft, my formal models, my 
research work and/or my personal opinions. Given how controversial this 
topic is, I am not at all surprised by this. Is there someone here who 
has said something on this topic which has not been refuted? If we were 
to take into account such social media posts, I believe the whole TLS WG 
would be at Whole Foods. 🙂

Since you have mentioned my co-author Bas, there is no conflict between 
the two of us. While we had differences of opinion, we happily worked 
together for draft-westerbaan-tls-keyshare and made the substantive 
change a success. I would take this opportunity to share that yesterday, 
he shared off-list the new plan for the draft and I supported him in 
that, and we will most likely work together to proceed that work in the 
new direction. On the specific issue of ML-KEM, I have added a section 
based on his concern [0]. If anything, the differences of opinions are 
because of:

 1. different backgrounds: he is a cryptographer while I am not. I work
    at the abstraction of symbolic security analysis (ProVerif). Both
    are complementary.
 2. different roles: he is at a company which has a deadline of 2029 for
    PQ and I totally understand where he is coming from when he is
    pushing for certain things. I am at a university where my focus is
    to ensure that we do not miss security flaws in the rush for
    standardization of PQ.

It is on record with one of the chairs that I have appreciated working 
with him. He has been very kind and patient to explain his perspective 
and cryptographic nits to me, and I am trying to understand his 
perspective, and we are converging. As you can very well understand, not 
everything needs to be added in the symbolic model in ProVerif, and 
reasonable choices have to be made to keep it complementary to 
computational proof.

I request that we close this social media topic and keep our focus on 
the technical matters on list. In particular, I would welcome feedback 
on [0]. Thank you!


> Concretely, I would ask the responsible AD to: [...]

I would like to request to withdraw your ask to the AD. Whatever chair 
or other WG participants have liked or commented on social media is 
their personal thing, which has nothing to do with TLS WG. Also, WG 
participants are still giving their feedback on my draft and I am 
addressing their feedback. While the discussion is ongoing, I don't see 
a reason for an escalation to AD.


Best regards,

-Usama

[0] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-hybrid-ml-kem