KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM

Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter +4

High-assurance cryptography provides strong guarantees that source implementations are functionally correct and provably secure. In this paper, we demonstrate that the Jasmin compi…