@inproceedings{ AAB+24,
  author        = {Jos{\'e} Bacelar Almeida and 
                   Santiago Arranz Olmos and
                   Manuel Barbosa and 
                   Gilles Barthe and 
                   Fran{\,c}ois Dupressoir and
                   Benjamin Gr{\'e}goire and 
                   Vincent Laporte and 
                   Jean-Christophe L{\'e}chenet and 
                   Cameron Low and
                   Tiago Oliveira and 
                   Hugo Pacheco and 
                   Miguel Quaresma and 
                   Peter Schwabe and 
                   Pierre-Yves Strub},
  title         = {Formally verifying {Kyber} -- Episode {V}: Machine-checked {IND-CCA} security and correctness of {ML-KEM} in {EasyCrypt}},
  booktitle     = {Advances in Cryptology -- {CRYPTO 2024}}, 
  editor        = {Leonid Reyzin and Douglas Stebila},
  publisher     = {Springer-Verlag Berlin Heidelberg},
  series        = {Lecture Notes in Computer Science},
  year          = {2024},
  pages         = {to appear},
  note          = {\url{http://cryptojedi.org/papers/\#hakyberv}},
}