Research seriesL3algorithms
IND-CCA says an eavesdropper with a decapsulation oracle cannot tell ML-KEM's shared secret from random. It says nothing about which public key or ciphertext that secret is tied to, what happens when someone else generated the key, what a 'formally verified' implementation has actually been checked against, or what HPKE, X-Wing and SSH quietly assume when they wrap the KEM. This series reads each of those gaps at the level of its evidence: the KEM binding notions and re-encapsulation attacks, malicious keys and the seed-versus-expanded format decision, the scope and limits of machine-checked ML-KEM, and the assumptions each protocol construction places on FIPS 203. Every topic is tied to the channels, key stores and model-serving endpoints that AI agents depend on.
IND-CCA keeps ML-KEM's shared secret hidden. It says nothing about which key and ciphertext the secret belongs to, and some protocols quietly depend on that.
ML-KEM's guarantees assume an honest key generator. When a key arrives from somewhere else, the FIPS 203 checks, the key format and its provenance decide what is still true.
Machine-checked ML-KEM exists in several forms. Each proves something different, against its own specification and machine model, and none proves everything a deployment needs.
Three standardized constructions wrap ML-KEM outside the TLS handshake. Each takes different properties from the KEM, supplies others itself, and gives something up.