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.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.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.
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.
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.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.
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
