6. Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Verifiable side-channel security of cryptographic implementations: Constant-time MEE-CBC. In: Peyrin, T. (ed.) FSE 2016. LNCS, vol. 9783, pp. 163–184. Springer, Heidelberg (Mar 2016). https://doi.org/10.1007/978-3-662-52993-5_9 3, 21

7. Almeida, J.B., Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Laporte, V., Oliveira, T., Strub, P.Y.: The last mile: High-assurance and high-speed cryptographic implementations. In: 2020 IEEE Symposium on Security and Privacy. pp. 965–982. IEEE Computer Society Press (May 2020). https://doi.org/10.1109/SP40000.2020.00028 2

8. Almeida, J.B., Barbosa, M., Barthe, G., Grégoire, B., Laporte, V., Léchenet, J.C., Oliveira, T., Pacheco, H., Quaresma, M., Schwabe, P., Séré, A., Strub, P.Y.: Formally verifying kyber episode IV: Implementation correctness. IACR TCHES 2023(3), 164–193 (2023). https://doi.org/10.46586/tches.v2023.i3.164-193 2, 3, 18, 21

9. Almeida, J.B., Baritel-Ruet, C., Barbosa, M., Barthe, G., Dupressoir, F., Grégoire, B., Laporte, V., Oliveira, T., Stoughton, A., Strub, P.Y.: Machine-checked proofs for cryptographic standards: Indifferentiability of sponge and secure high-assurance implementations of SHA-3. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) ACM CCS 2019. pp. 1607–1622. ACM Press (Nov 2019). https://doi.org/10.1145/3319535.3363211 3, 28

10. Avanzi, R., Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J.M., Schwabe, P., Seiler, G., Stehlé, D.: CRYSTALS-KYBER: Algorithm specifications and supporting documentation (version 3.02). Round-3 submission to the NIST PQC standardization project (2021), https://pq-crystals.org/kyber/data/kyber-specification-round3-20210804.pdf 1

11. Barbosa, M., Barthe, G., Bhargavan, K., Blanchet, B., Cremers, C., Liao, K., Parno, B.: SoK: Computer-aided cryptography. In: 2021 IEEE Symposium on Security and Privacy. pp. 777–795. IEEE Computer Society Press (May 2021). https://doi.org/10.1109/SP40001.2021.00008 1, 3

12. Barbosa, M., Barthe, G., Doczkal, C., Don, J., Fehr, S., Grégoire, B., Huang, Y.H., Hülsing, A., Lee, Y., Wu, X.: Fixing and mechanizing the security proof of Fiat-Shamir with aborts and Dilithium. In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part V. LNCS, vol. 14085, pp. 358–389. Springer, Heidelberg (Aug 2023). https://doi.org/10.1007/978-3-031-38554-4_12 3

13. Barbosa, M., Barthe, G., Fan, X., Grégoire, B., Hung, S.H., Katz, J., Strub, P.Y., Wu, X., Zhou, L.: EasyPQC: Verifying post-quantum cryptography. In: Vigna, G., Shi, E. (eds.) ACM CCS 2021. pp. 2564–2586. ACM Press (Nov 2021). https://doi.org/10.1145/3460120.3484567 3

14. Barbosa, M., Dupressoir, F., Grégoire, B., Hülsing, A., Meijers, M., Strub, P.Y.: Machine-checked security for rmXMSS as in RFC 8391 and SPHINCS⁺. In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part V. LNCS, vol. 14085, pp. 421–454. Springer, Heidelberg (Aug 2023). https://doi.org/10.1007/978-3-031-38554-4_14 3

15. Barbosa, M., Hülsing, A.: The security of Kyber’s FO-transform. Cryptology ePrint Archive, Report 2023/755 (2023), https://eprint.iacr.org/2023/755 6

16. Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., Strub, P.Y.: EasyCrypt: A Tutorial, pp. 146–166. Springer (2014), 5

17. Barthe, G., Fan, X., Gancher, J., Grégoire, B., Jacomme, C., Shi, E.: Symbolic proofs for lattice-based cryptography. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) ACM CCS 2018. pp. 538–555. ACM Press (Oct 2018). https://doi.org/10.1145/3243734.3243825 3

18. Barthe, G., Grégoire, B., Heraud, S., Zanella Béguelin, S.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (Aug 2011). https://doi.org/10.1007/978-3-642-22792-9_5 2

19. Becker, A., Ducas, L., Gama, N., Laarhoven, T.: New directions in nearest neighbor searching with applications to lattice sieving. In: SODA ’16: Proceedings of the twenty-seventh annual ACM-SIAM symposium on Discrete algorithms. pp. 10–24. Society for Industrial and Applied Mathematics (2016) 3

20. Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: Jung, J., Holz, T. (eds.) USENIX Security 2015. pp. 207–221. USENIX Association (Aug 2015) 3

21. Bernstein, D.J., Persichetti, E.: Towards KEM unification. Cryptology ePrint Archive, Report 2018/526 (2018), https://eprint.iacr.org/2018/526 13

22. Bindel, N., Hamburg, M., Hövelmanns, K., Hülsing, A., Persichetti, E.: Tighter proofs of CCA security in the quantum random oracle model. In: Hofheinz, D., Rosen, A. (eds.) TCC 2019, Part II. LNCS, vol. 11892, pp. 61–90. Springer, Heidelberg (Dec 2019). https://doi.org/10.1007/978-3-030-36033-7_3 3

23. Blanchette, J., Mahboubi, A. (eds.): Handbook of Proof Assistants. Springer-Verlag (2025), to appear 3

24. Boneh, D., Dagdelen, Ö., Fischlin, M., Lehmann, A., Schaffner, C., Zhandry, M.: Random oracles in a quantum world. In: Lee, D.H., Wang, X. (eds.) ASIACRYPT 2011. LNCS, vol. 7073, pp. 41–69. Springer, Heidelberg (Dec 2011). https://doi.org/10.1007/978-3-642-25385-0_3 3, 4

25. Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J.M., Schwabe, P., Stehlé, D.: CRYSTALS-Kyber: a CCA-secure module-lattice-based KEM. In: 2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018. pp. 353–367. IEEE (2018), https://eprint.iacr.org/2017/634 1, 2, 3, 8, 9, 10, 12

26. Cremers, C., Fontaine, C., Jacomme, C.: A logic and an interactive prover for the computational post-quantum security of protocols. In: 2022 IEEE Symposium on Security and Privacy. pp. 125–141. IEEE Computer Society Press (May 2022). https://doi.org/10.1109/SP46214.2022.9833800 4
27. D'Anvers, J.P., Karmakar, A., Roy, S.S., Vercauteren, F., Mera, J.M.B., Beirendonck, M.V., Basso, A.: SABER. Tech. rep., National Institute of Standards and Technology (2020), available at https://csrc.nist.gov/projects/post-quantum-cryptography/post-quantum-cryptography-standardization/round-3-submissions 3

28. Ducas, L.: Shortest vector from lattice sieving: A few dimensions for free. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018, Part I. LNCS, vol. 10820, pp. 125–145. Springer, Heidelberg (Apr / May 2018). https://doi.org/10.1007/978-3-319-78381-9_5 3

29. Ducas, L., Pulles, L.N.: Does the dual-sieve attack on learning with errors even work? In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part III. LNCS, vol. 14083, pp. 37–69. Springer, Heidelberg (Aug 2023). https://doi.org/10.1007/978-3-031-38548-3_2 3

30. Duman, J., Hövelmanns, K., Kiltz, E., Lyubashevsky, V., Seiler, G.: Faster lattice-based KEMs via a generic fujisaki-okamoto transform using prefix hashing. In: Vigna, G., Shi, E. (eds.) ACM CCS 2021. pp. 2722–2737. ACM Press (Nov 2021). https://doi.org/10.1145/3460120.3484819 3

31. Fujisaki, E., Okamoto, T.: Secure integration of asymmetric and symmetric encryption schemes. In: Wiener, M.J. (ed.) CRYPTO’99. LNCS, vol. 1666, pp. 537–554. Springer, Heidelberg (Aug 1999). https://doi.org/10.1007/3-540-48405-1_34 6, 13

32. Fujisaki, E., Okamoto, T.: Secure integration of asymmetric and symmetric encryption schemes. Journal of Cryptology 26(1), 80–101 (Jan 2013). https://doi.org/10.1007/s00145-011-9114-1 6, 13

33. Gentry, C., Peikert, C., Vaikuntanathan, V.: Trapdoors for hard lattices and new cryptographic constructions. In: Ladner, R.E., Dwork, C. (eds.) 40th ACM STOC. pp. 197–206. ACM Press (May 2008). https://doi.org/10.1145/1374376.1374407 3, 4

34. Grubbs, P., Maram, V., Paterson, K.G.: Anonymous, robust post-quantum public key encryption. In: Dunkelman, O., Dziembowski, S. (eds.) EUROCRYPT 2022, Part III. LNCS, vol. 13277, pp. 402–432. Springer, Heidelberg (May / Jun 2022). https://doi.org/10.1007/978-3-031-07082-2_15 3, 6

35. Guo, Q., Johansson, T.: Faster dual lattice attacks for solving LWE with applications to CRYSTALS. In: Tibouchi, M., Wang, H. (eds.) ASIACRYPT 2021, Part IV. LNCS, vol. 13093, pp. 33–62. Springer, Heidelberg (Dec 2021). https://doi.org/10.1007/978-3-030-92068-5_2 3

36. Guo, Q., Johansson, T., Nilsson, A.: A key-recovery timing attack on post-quantum primitives using the Fujisaki-Okamoto transformation and its application on FrodoKEM. In: Micciancio, D., Ristenpart, T. (eds.) CRYPTO 2020, Part II. LNCS, vol. 12171, pp. 359–386. Springer, Heidelberg (Aug 2020). https://doi.org/10.1007/978-3-030-56880-1_13 3

37. Hamburg, M., Hermelink, J., Primas, R., Samardjiska, S., Schamberger, T., Streit, S., Strieder, E., van Vrendendaal, C.: Chosen ciphertext k-trace attacks on masked CCA2 secure kyber. IACR TCHES 2021(4), 88–113 (2021). https://doi.org/10.46586/tches.v2021.i4.88-113, https://tches.iacr.org/index.php/TCHES/article/view/9061 3

38. Hermelink, J., Mårtensson, E., Samardjiska, S., Pessl, P., Rodosek, G.D.: Belief propagation meets lattice reduction: Security estimates for error-tolerant key recovery from decryption errors. IACR TCHES 2023(4), 287–317 (2023). https://doi.org/10.46586/tches.v2023.i4.287-317 3

39. Hermelink, J., Streit, S., Strieder, E., Thieme, K.: Adapting belief propagation to counter shuffling of NTTs. IACR TCHES 2023(1), 60–88 (2023). https://doi.org/10.46586/tches.v2023.i1.60-88 3

40. Hofheinz, D., Hövelmanns, K., Kiltz, E.: A modular analysis of the Fujisaki-Okamoto transformation. In: Kalai, Y., Reyzin, L. (eds.) TCC 2017, Part I. LNCS, vol. 10677, pp. 341–371. Springer, Heidelberg (Nov 2017). https://doi.org/10.1007/978-3-319-70500-2_12 6, 10, 13, 14, 15, 16, 26

41. Hofheinz, D., Hövelmanns, K., Kiltz, E.: A modular analysis of the Fujisaki-Okamoto transformation. Cryptology ePrint Archive, Report 2017/604 (2017), https://eprint.iacr.org/2017/604 10, 13, 14, 15, 16, 26

42. Hövelmanns, K., Hülsing, A., Majenz, C.: Failing gracefully: Decryption failures and the fujisaki-okamoto transform. In: Agrawal, S., Lin, D. (eds.) ASIACRYPT 2022, Part IV. LNCS, vol. 13794, pp. 414–443. Springer, Heidelberg (Dec 2022). https://doi.org/10.1007/978-3-031-22972-5_15 3

43. Hövelmanns, K., Kiltz, E., Schäge, S., Unruh, D.: Generic authenticated key exchange in the quantum random oracle model. In: Kiayias, A., Kohlweiss, M., Wallden, P., Zikas, V. (eds.) PKC 2020, Part II. LNCS, vol. 12111, pp. 389–422. Springer, Heidelberg (May 2020). https://doi.org/10.1007/978-3-030-45388-6_14 13

44. Hülsing, A., Meijers, M., Strub, P.Y.: Formal verification of Saber’s public-key encryption scheme in EasyCrypt. In: Dodis, Y., Shrimpton, T. (eds.) CRYPTO 2022, Part I. LNCS, vol. 13507, pp. 622–653. Springer, Heidelberg (Aug 2022). https://doi.org/10.1007/978-3-031-15802-5_22 2, 3, 8

45. Jiang, H., Zhang, Z., Chen, L., Wang, H., Ma, Z.: IND-CCA-secure key encapsulation mechanism in the quantum random oracle model, revisited. In: Shacham, H., Boldyreva, A. (eds.) CRYPTO 2018, Part III. LNCS, vol. 10993, pp. 96–125. Springer, Heidelberg (Aug 2018). https://doi.org/10.1007/978-3-319-96878-0_4 3

46. Kreuzer, K.: Verification of correctness and security properties for CRYSTALS-KYBER. Cryptology ePrint Archive, Report 2023/087 (2023), https://eprint.iacr.org/2023/087 3, 8, 10

47. Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 1–23. Springer, Heidelberg (May / Jun 2010). https://doi.org/10.1007/978-3-642-13190-5_1 6, 9
27. D'Anvers, J.P., Karmakar, A., Roy, S.S., Vercauteren, F., Mera, J.M.B., Beirendonck, M.V., Basso, A.: SABER. Tech. rep., National Institute of Standards and Technology (2020), available at https://csrc.nist.gov/projects/post-quantum-cryptography/post-quantum-cryptography-standardization/round-3-submissions 3

28. Ducas, L.: Shortest vector from lattice sieving: A few dimensions for free. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018, Part I. LNCS, vol. 10820, pp. 125–145. Springer, Heidelberg (Apr / May 2018). https://doi.org/10.1007/978-3-319-78381-9_5 3

29. Ducas, L., Pulles, L.N.: Does the dual-sieve attack on learning with errors even work? In: Handschuh, H., Lysyanskaya, A. (eds.) CRYPTO 2023, Part III. LNCS, vol. 14083, pp. 37–69. Springer, Heidelberg (Aug 2023). https://doi.org/10.1007/978-3-031-38548-3_2 3

30. Duman, J., Hövelmanns, K., Kiltz, E., Lyubashevsky, V., Seiler, G.: Faster lattice-based KEMs via a generic fujisaki-okamoto transform using prefix hashing. In: Vigna, G., Shi, E. (eds.) ACM CCS 2021. pp. 2722–2737. ACM Press (Nov 2021). https://doi.org/10.1145/3460120.3484819 3

31. Fujisaki, E., Okamoto, T.: Secure integration of asymmetric and symmetric encryption schemes. In: Wiener, M.J. (ed.) CRYPTO'99. LNCS, vol. 1666, pp. 537–554. Springer, Heidelberg (Aug 1999). https://doi.org/10.1007/3-540-48405-1_34 6, 13

32. Fujisaki, E., Okamoto, T.: Secure integration of asymmetric and symmetric encryption schemes. Journal of Cryptology 26(1), 80–101 (Jan 2013). https://doi.org/10.1007/s00145-011-9114-1 6, 13

33. Gentry, C., Peikert, C., Vaikuntanathan, V.: Trapdoors for hard lattices and new cryptographic constructions. In: Ladner, R.E., Dwork, C. (eds.) 40th ACM STOC. pp. 197–206. ACM Press (May 2008). https://doi.org/10.1145/1374376.1374407 3, 4

34. Grubbs, P., Maram, V., Paterson, K.G.: Anonymous, robust post-quantum public key encryption. In: Dunkelman, O., Dziembowski, S. (eds.) EUROCRYPT 2022, Part III. LNCS, vol. 13277, pp. 402–432. Springer, Heidelberg (May / Jun 2022). https://doi.org/10.1007/978-3-031-07082-2_15 3, 6

35. Guo, Q., Johansson, T.: Faster dual lattice attacks for solving LWE with applications to CRYSTALS. In: Tibouchi, M., Wang, H. (eds.) ASIACRYPT 2021, Part IV. LNCS, vol. 13093, pp. 33–62. Springer, Heidelberg (Dec 2021). https://doi.org/10.1007/978-3-030-92068-5_2 3

36. Guo, Q., Johansson, T., Nilsson, A.: A key-recovery timing attack on post-quantum primitives using the Fujisaki-Okamoto transformation and its application on FrodoKEM. In: Micciancio, D., Ristenpart, T. (eds.) CRYPTO 2020, Part II. LNCS, vol. 12171, pp. 359–386. Springer, Heidelberg (Aug 2020). https://doi.org/10.1007/978-3-030-56880-1_13 3

37. Hamburg, M., Hermelink, J., Primas, R., Samardjiska, S., Schamberger, T., Streit, S., Strieder, E., van Vrendendaal, C.: Chosen ciphertext k-trace attacks on masked CCA2 secure kyber. IACR TCHES 2021(4), 88–113 (2021). https://doi.org/10.46586/tches.v2021.i4.88-113, https://tches.iacr.org/index.php/TCHES/article/view/9061 3

38. Hermelink, J., Mårtensson, E., Samardjiska, S., Pessl, P., Rodosek, G.D.: Belief propagation meets lattice reduction: Security estimates for error-tolerant key recovery from decryption errors. IACR TCHES 2023(4), 287–317 (2023). https://doi.org/10.46586/tches.v2023.i4.287-317 3

39. Hermelink, J., Streit, S., Strieder, E., Thieme, K.: Adapting belief propagation to counter shuffling of NTTs. IACR TCHES 2023(1), 60–88 (2023). https://doi.org/10.46586/tches.v2023.i1.60-88 3

40. Hofheinz, D., Hövelmanns, K., Kiltz, E.: A modular analysis of the Fujisaki-Okamoto transformation. In: Kalai, Y., Reyzin, L. (eds.) TCC 2017, Part I. LNCS, vol. 10677, pp. 341–371. Springer, Heidelberg (Nov 2017). https://doi.org/10.1007/978-3-319-70500-2_12 6, 10, 13, 14, 15, 16, 26

41. Hofheinz, D., Hövelmanns, K., Kiltz, E.: A modular analysis of the Fujisaki-Okamoto transformation. Cryptology ePrint Archive, Report 2017/604 (2017), https://eprint.iacr.org/2017/604 10, 13, 14, 15, 16, 26

42. Hövelmanns, K., Hülsing, A., Majenz, C.: Failing gracefully: Decryption failures and the fujisaki-okamoto transform. In: Agrawal, S., Lin, D. (eds.) ASIACRYPT 2022, Part IV. LNCS, vol. 13794, pp. 414–443. Springer, Heidelberg (Dec 2022). https://doi.org/10.1007/978-3-031-22972-5_15 3

43. Hövelmanns, K., Kiltz, E., Schäge, S., Unruh, D.: Generic authenticated key exchange in the quantum random oracle model. In: Kiayias, A., Kohlweiss, M., Wallden, P., Zikas, V. (eds.) PKC 2020, Part II. LNCS, vol. 12111, pp. 389–422. Springer, Heidelberg (May 2020). https://doi.org/10.1007/978-3-030-45388-6_14 13

44. Hülsing, A., Meijers, M., Strub, P.Y.: Formal verification of Saber's public-key encryption scheme in EasyCrypt. In: Dodis, Y., Shrimpton, T. (eds.) CRYPTO 2022, Part I. LNCS, vol. 13507, pp. 622–653. Springer, Heidelberg (Aug 2022). https://doi.org/10.1007/978-3-031-15802-5_22 2, 3, 8

45. Jiang, H., Zhang, Z., Chen, L., Wang, H., Ma, Z.: IND-CCA-secure key encapsulation mechanism in the quantum random oracle model, revisited. In: Shacham, H., Boldyreva, A. (eds.) CRYPTO 2018, Part III. LNCS, vol. 10993, pp. 96–125. Springer, Heidelberg (Aug 2018). https://doi.org/10.1007/978-3-319-96878-0_4 3

46. Kreuzer, K.: Verification of correctness and security properties for CRYSTALS-KYBER. Cryptology ePrint Archive, Report 2023/087 (2023), https://eprint.iacr.org/2023/087 3, 8, 10

47. Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 1–23. Springer, Heidelberg (May / Jun 2010). https://doi.org/10.1007/978-3-642-13190-5_1 6, 9
48. Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. Slides of the talk given by Chris Peikert at Eurocrypt 2010 (2010), https://iacr.org/conferences/eurocrypt2010/talks/slides-ideal-lwe.pdf 6

49. Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. Cryptology ePrint Archive, Report 2012/230 (2012), https://eprint.iacr.org/2012/230 9

50. Maram, V., Xagawa, K.: Post-quantum anonymity of Kyber. In: Boldyreva, A., Kolesnikov, V. (eds.) PKC 2023, Part I. LNCS, vol. 13940, pp. 3–35. Springer, Heidelberg (May 2023). https://doi.org/10.1007/978-3-031-31368-4_1 3, 6

51. Micciancio, D., Peikert, C.: Trapdoors for lattices: Simpler, tighter, faster, smaller. In: Pointcheval, D., Johansson, T. (eds.) EUROCRYPT 2012. LNCS, vol. 7237, pp. 700–718. Springer, Heidelberg (Apr 2012). https://doi.org/10.1007/978-3-642-29011-4_41 3

52. Micciancio, D., Voulgaris, P.: Faster exponential time algorithms for the shortest vector problem. In: SODA '10: Proceedings of the twenty-first annual ACM-SIAM symposium on Discrete algorithms. pp. 1468–1480. Society for Industrial and Applied Mathematics (2010) 3

53. National Institute of Standards and Technology: FIPS PUB 202 – SHA-3 standard: Permutation-based hash and extendable-output functions (2015), http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.202.pdf 7

54. National Institute of Standards and Technology: FIPS PUB 203 (Initial Public Draft) – module-lattice-based key-encapsulation mechanism standard (2023), https://csrc.nist.gov/pubs/fips/203/ipd 1, 7, 8, 18

55. Ngo, K., Dubrova, E., Guo, Q., Johansson, T.: A side-channel attack on a masked IND-CCA secure saber KEM implementation. IACR TCHES 2021(4), 676–707 (2021). https://doi.org/10.46586/tches.v2021.i4.676-707, https://tches.iacr.org/index.php/TCHES/article/view/9079 3

56. Nguyen, P.Q., Vidick, T.: Sieve algorithms for the shortest vector problemare practical. J. Math. Crypt. pp. 181–207 (2008), https://doi.org/10.1515/JMC.2008.009 3

57. Pessl, P., Prokop, L.: Fault attacks on CCA-secure lattice KEMs. IACR TCHES 2021(2), 37–60 (2021). https://doi.org/10.46586/tches.v2021.i2.37-60, https://tches.iacr.org/index.php/TCHES/article/view/8787 3

58. Primas, R., Pessl, P., Mangard, S.: Single-trace side-channel attacks on masked lattice-based encryption. In: Fischer, W., Homma, N. (eds.) CHES 2017. LNCS, vol. 10529, pp. 513–533. Springer, Heidelberg (Sep 2017). https://doi.org/10.1007/978-3-319-66787-4_25 3

59. Saito, T., Xagawa, K., Yamakawa, T.: Tightly-secure key-encapsulation mechanism in the quantum random oracle model. Cryptology ePrint Archive, Report 2017/1005 (2017), https://eprint.iacr.org/2017/1005 6

60. Saito, T., Xagawa, K., Yamakawa, T.: Tightly-secure key-encapsulation mechanism in the quantum random oracle model. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018, Part III. LNCS, vol. 10822, pp. 520–551. Springer, Heidelberg (Apr / May 2018). https://doi.org/10.1007/978-3-319-78372-7_17 3

61. Schwabe, P., Avanzi, R., Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J.M., Seiler, G., Stehlé, D.: CRYSTALS-KYBER. Tech. rep., National Institute of Standards and Technology (2017), available at https://csrc.nist.gov/projects/post-quantum-cryptography/post-quantum-cryptography-standardization/round-1-submissions 3

62. Schwabe, P., Avanzi, R., Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J.M., Seiler, G., Stehlé, D., Ding, J.: CRYSTALS-KYBER. Tech. rep., National Institute of Standards and Technology (2022), available at https://csrc.nist.gov/Projects/post-quantum-cryptography/selected-algorithms-2022 3

63. Targhi, E.E., Unruh, D.: Post-quantum security of the Fujisaki-Okamoto and OAEP transforms. In: Hirt, M., Smith, A.D. (eds.) TCC 2016-B, Part II. LNCS, vol. 9986, pp. 192–216. Springer, Heidelberg (Oct / Nov 2016). https://doi.org/10.1007/978-3-662-53644-5_8 3

64. Unruh, D.: Quantum relational hoare logic. Proc. ACM Program. Lang. 3(POPL), 33:1–33:31 (2019). https://doi.org/10.1145/3290346, https://doi.org/10.1145/3290346 4

65. Unruh, D.: Post-quantum verification of Fujisaki-Okamoto. In: Moriai, S., Wang, H. (eds.) ASIACRYPT 2020, Part I. LNCS, vol. 12491, pp. 321–352. Springer, Heidelberg (Dec 2020). https://doi.org/10.1007/978-3-030-64837-4_11 4

66. Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedTLS HMAC-DRBG. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) ACM CCS 2017. pp. 2007–2020. ACM Press (Oct / Nov 2017). https://doi.org/10.1145/3133956.3133974 3

67. Zhandry, M.: How to record quantum queries, and applications to quantum indifferentiability. In: Boldyreva, A., Micciancio, D. (eds.) CRYPTO 2019, Part II. LNCS, vol. 11693, pp. 239–268. Springer, Heidelberg (Aug 2019). https://doi.org/10.1007/978-3-030-26951-7_9 3

A Cryptographic Definitions

For a set $S$, $|S|$ denotes the cardinality of $S$. For a finite set $S$, we denote the sampling of a uniform random element $x$ by $x \leftarrow_S S$. We denote deterministic computation of an algorithm $A$ on input $x$ by $y \leftarrow A(x)$. We denote algorithms with access to an oracle $O$ by $A^O$. Unless stated otherwise, we assume all our algorithms to be probabilistic and denote the computation by $y \leftarrow_S A(x)$. When deterministically
48. Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. Slides of the talk given by Chris Peikert at Eurocrypt 2010 (2010), https://iacr.org/conferences/eurocrypt2010/talks/slides-ideal-lwe.pdf 6

49. Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. Cryptology ePrint Archive, Report 2012/230 (2012), https://eprint.iacr.org/2012/230 9

50. Maram, V., Xagawa, K.: Post-quantum anonymity of Kyber. In: Boldyreva, A., Kolesnikov, V. (eds.) PKC 2023, Part I. LNCS, vol. 13940, pp. 3–35. Springer, Heidelberg (May 2023). https://doi.org/10.1007/978-3-031-31368-4_1 3, 6

51. Micciancio, D., Peikert, C.: Trapdoors for lattices: Simpler, tighter, faster, smaller. In: Pointcheval, D., Johansson, T. (eds.) EUROCRYPT 2012. LNCS, vol. 7237, pp. 700–718. Springer, Heidelberg (Apr 2012). https://doi.org/10.1007/978-3-642-29011-4_41 3

52. Micciancio, D., Voulgaris, P.: Faster exponential time algorithms for the shortest vector problem. In: SODA '10: Proceedings of the twenty-first annual ACM-SIAM symposium on Discrete algorithms. pp. 1468–1480. Society for Industrial and Applied Mathematics (2010) 3

53. National Institute of Standards and Technology: FIPS PUB 202 – SHA-3 standard: Permutation-based hash and extendable-output functions (2015), http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.202.pdf 7

54. National Institute of Standards and Technology: FIPS PUB 203 (Initial Public Draft) – module-lattice-based key-encapsulation mechanism standard (2023), https://csrc.nist.gov/pubs/fips/203/ipd 1, 7, 8, 18

55. Ngo, K., Dubrova, E., Guo, Q., Johansson, T.: A side-channel attack on a masked IND-CCA secure saber KEM implementation. IACR TCHES 2021(4), 676–707 (2021). https://doi.org/10.46586/tches.v2021.i4.676-707, https://tches.iacr.org/index.php/TCHES/article/view/9079 3

56. Nguyen, P.Q., Vidick, T.: Sieve algorithms for the shortest vector problemare practical. J. Math. Crypt. pp. 181–207 (2008), https://doi.org/10.1515/JMC.2008.009 3

57. Pessl, P., Prokop, L.: Fault attacks on CCA-secure lattice KEMs. IACR TCHES 2021(2), 37–60 (2021). https://doi.org/10.46586/tches.v2021.i2.37-60, https://tches.iacr.org/index.php/TCHES/article/view/8787 3

58. Primas, R., Pessl, P., Mangard, S.: Single-trace side-channel attacks on masked lattice-based encryption. In: Fischer, W., Homma, N. (eds.) CHES 2017. LNCS, vol. 10529, pp. 513–533. Springer, Heidelberg (Sep 2017). https://doi.org/10.1007/978-3-319-66787-4_25 3

59. Saito, T., Xagawa, K., Yamakawa, T.: Tightly-secure key-encapsulation mechanism in the quantum random oracle model. Cryptology ePrint Archive, Report 2017/1005 (2017), https://eprint.iacr.org/2017/1005 6

60. Saito, T., Xagawa, K., Yamakawa, T.: Tightly-secure key-encapsulation mechanism in the quantum random oracle model. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018, Part III. LNCS, vol. 10822, pp. 520–551. Springer, Heidelberg (Apr / May 2018). https://doi.org/10.1007/978-3-319-78372-7_17 3

61. Schwabe, P., Avanzi, R., Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J.M., Seiler, G., Stehlé, D.: CRYSTALS-KYBER. Tech. rep., National Institute of Standards and Technology (2017), available at https://csrc.nist.gov/projects/post-quantum-cryptography/post-quantum-cryptography-standardization/round-1-submissions 3

62. Schwabe, P., Avanzi, R., Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J.M., Seiler, G., Stehlé, D., Ding, J.: CRYSTALS-KYBER. Tech. rep., National Institute of Standards and Technology (2022), available at https://csrc.nist.gov/Projects/post-quantum-cryptography/selected-algorithms-2022 3

63. Targhi, E.E., Unruh, D.: Post-quantum security of the Fujisaki-Okamoto and OAEP transforms. In: Hirt, M., Smith, A.D. (eds.) TCC 2016-B, Part II. LNCS, vol. 9986, pp. 192–216. Springer, Heidelberg (Oct / Nov 2016). https://doi.org/10.1007/978-3-662-53644-5_8 3

64. Unruh, D.: Quantum relational hoare logic. Proc. ACM Program. Lang. 3(POPL), 33:1–33:31 (2019). https://doi.org/10.1145/3290346, https://doi.org/10.1145/3290346 4

65. Unruh, D.: Post-quantum verification of Fujisaki-Okamoto. In: Moriai, S., Wang, H. (eds.) ASIACRYPT 2020, Part I. LNCS, vol. 12491, pp. 321–352. Springer, Heidelberg (Dec 2020). https://doi.org/10.1007/978-3-030-64837-4_11 4

66. Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedTLS HMAC-DRBG. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) ACM CCS 2017. pp. 2007–2020. ACM Press (Oct / Nov 2017). https://doi.org/10.1145/3133956.3133974 3

67. Zhandry, M.: How to record quantum queries, and applications to quantum indifferentiability. In: Boldyreva, A., Micciancio, D. (eds.) CRYPTO 2019, Part II. LNCS, vol. 11693, pp. 239–268. Springer, Heidelberg (Aug 2019). https://doi.org/10.1007/978-3-030-26951-7_9 3

A Cryptographic Definitions

For a set $S$, $|S|$ denotes the cardinality of $S$. For a finite set $S$, we denote the sampling of a uniform random element $x$ by $x \leftarrow_S S$. We denote deterministic computation of an algorithm $A$ on input $x$ by $y \leftarrow A(x)$. We denote algorithms with access to an oracle $O$ by $O^A$. Unless stated otherwise, we assume all our algorithms to be probabilistic and denote the computation by $y \leftarrow_S A(x)$. When deterministically
<table><caption>**Fig. 14.** Correctness of a PKE in the standard model and ROM.</caption><thead><tr><th>Game COR:</th><th>Game COR-RO:</th></tr></thead><tbody><tr><td>1: (pk, sk) &harr; Gen()</td><td>1: (pk, sk) &harr; Gen()</td></tr><tr><td>2: m &harr; A(pk, sk)</td><td>2: m &harr; A<sup>G</sup>(pk, sk)</td></tr><tr><td>3: c &harr; Enc(pk, m)</td><td>3: c &harr; Enc<sup>G</sup>(pk, m)</td></tr><tr><td>4: return (m &ne; Dec(sk, c))</td><td>4: return (m &ne; Dec<sup>G</sup>(sk, c))</td></tr></tbody></table>

computing a randomized algorithms by fixing its random coins $r$, we write: $y \leftarrow A(x; r)$. For the most part of this section we follow [40,41].

**Pseudorandomness.** Let $f: \mathcal{K} \times \mathcal{X} \to \mathcal{Y}$ be a function. We define the PRF advantage of an adversary $\mathcal{A}$ as

$$ \mathrm{Adv}_{\mathrm{f}}^{\mathrm{PRF}}(\mathcal{A}) = \left| \mathrm{Pr}[\mathcal{A}^{\mathrm{PRF}}(K, \cdot) \Rightarrow 1: K \leftarrow \mathcal{K}] - \mathrm{Pr}[\mathcal{A}^{\mathrm{F}}(\cdot) \Rightarrow 1: F \leftarrow \mathcal{F}(\mathcal{X} \to \mathcal{Y})] \right|. $$

When this advantage is small for all efficient adversaries, we say $f$ is a pseudorandom function. Let $g: \mathcal{K} \to \mathcal{Y}$ be a function. We define the PRG advantage of an adversary $\mathcal{A}$ as

$$ \mathrm{Adv}_{\mathrm{g}}^{\mathrm{PRG}}(\mathcal{A}) = \left| \mathrm{Pr}[\mathcal{A}(y) \Rightarrow 1: K \leftarrow \mathcal{K}; y \leftarrow g(K)] - \mathrm{Pr}[\mathcal{A}(y) \Rightarrow 1: y \leftarrow \mathcal{Y}] \right|. $$

When this advantage is small for all efficient adversaries, we say $g$ is a pseudorandom generator.

**Public-Key Encryption.** A public-key encryption scheme consists of three algorithms PKE = (Gen, Enc, Dec) and a finite message space $\mathcal{M}$. The key generation algorithm Gen outputs a key pair (pk, sk). The encryption algorithm Enc, on input $pk$ and a message $m \in \mathcal{M}$, outputs a ciphertext $c \leftarrow \mathrm{Enc}(pk, m)$. If necessary to derandomize encryption, we writing $c \leftarrow \mathrm{Enc}(pk, m; r)$, where $r \leftarrow \mathcal{R}$ and $\mathcal{R}$ is the randomness space. The decryption algorithm Dec, on input $sk$ and a ciphertext $c$, outputs either a message $m \leftarrow \mathrm{Dec}(sk, c) \in \mathcal{M}$ or a special symbol $\perp \notin \mathcal{M}$ to indicate that $c$ is not a valid ciphertext.

**CORRECTNESS.** Correctness of a PKE is defined as in Figure 14. We give both a standard model definition (left) and a definition in the random oracle model (ROM, right). Note that the adversary gets the secret key as an input. In the standard model, $\delta$-correctness means that for all (possibly unbounded) adversaries $\mathcal{A}$, $\mathrm{Pr}[\mathrm{COR}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1] \le \delta$. In the ROM, we extend the definition so that $\delta$ is parameterized by an upper bound on the number of queries placed by $\mathcal{A}$ to its random oracle.

**CIPHERTEXT SPREADNESS.** We say that PKE is $\gamma$-spread if, for every key pair $(pk, sk) \leftarrow \mathrm{Gen}()$ and every ciphertext $c$, $\mathrm{Pr}_{r \leftarrow \mathcal{R}}[c = \mathrm{Enc}(pk, m; r)] \le 2^{-\gamma}$.

**SECURITY.** We now define several security notions for public-key encryption.

**Definition 1 (OW-Atk).** Let PKE = (Gen, Enc, Dec) be a public-key encryption scheme with message space $\mathcal{M}$. For Atk $\in \{\mathrm{CPA}, \mathrm{PCVA}\}$, we give the OW-Atk security games in Figure 15. Note that, if Atk=CPA, we have $\mathcal{O} = \emptyset$; and if Atk=PCVA, we have $\mathcal{O} = \{\mathrm{Pco}, \mathrm{Cvo}\}$. We define the OW-Atk advantage function of an adversary $\mathcal{A}$ against PKE as $\mathrm{Adv}_{\mathrm{PKE}}^{\mathrm{OW-Atk}}(\mathcal{A}) = \mathrm{Pr}[\mathrm{OW-Atk}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1]$.

Note that the adversary wins the one-way game if it guesses the result of decrypting the challenge ciphertext, rather than the standard definition of finding the message that is originally encrypted. The two games have statistical distance $\delta$, if PKE is $\delta$-correct. We also define the more standard notion, allowing the adversary to output a list of guesses.

**Definition 2.** OWL-CPA Let PKE = (Gen, Enc, Dec) be a public-key encryption scheme with message space $\mathcal{M}$. We give the OWL-CPA security game in Figure 15. We define the OWL-CPA advantage function of an adversary $\mathcal{A}$ against PKE as $\mathrm{Adv}_{\mathrm{PKE}}^{\mathrm{OWL-CPA}}(\mathcal{A}) = \mathrm{Pr}[\mathrm{OWL-CPA}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1]$.

We conclude this section with the standard definition of IND-CPA security for a PKE.

**Definition 3.** IND-CPA Let PKE = (Gen, Enc, Dec) be a public-key encryption scheme with message space $\mathcal{M}$. We define the IND-CPA game as in Figure 16, and the IND-CPA advantage function of an adversary $\mathcal{A} = (\mathcal{A}_1, \mathcal{A}_2)$ against PKE as $\mathrm{Adv}_{\mathrm{PKE}}^{\mathrm{IND-CPA}}(\mathcal{A}) = |\mathrm{Pr}[\mathrm{IND-CPA}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1] - 1/2|$.

In the proof of the FO transform (see Section 5) we use this general lemma that is verified in EasyCrypt.
<table><caption>Fig. 14. Correctness of a PKE in the standard model and ROM.</caption><thead><tr><th>Game COR:</th><th>Game COR-RO:</th></tr></thead><tbody><tr><td>1: (pk, sk) &harr; Gen()</td><td>1: (pk, sk) &harr; Gen()</td></tr><tr><td>2: m &harr; A(pk, sk)</td><td>2: m &harr; A<sup>G</sup>(pk, sk)</td></tr><tr><td>3: c &harr; Enc(pk, m)</td><td>3: c &harr; Enc<sup>G</sup>(pk, m)</td></tr><tr><td>4: return (m &ne; Dec(sk, c))</td><td>4: return (m &ne; Dec<sup>G</sup>(sk, c))</td></tr></tbody></table>

computing a randomized algorithms by fixing its random coins $r$, we write: $y \leftarrow A(x; r)$. For the most part of this section we follow [40,41].

**Pseudorandomness.** Let $f: \mathcal{K} \times \mathcal{X} \to \mathcal{Y}$ be a function. We define the PRF advantage of an adversary $\mathcal{A}$ as

$$ \mathrm{Adv}_{\mathrm{f}}^{\mathrm{PRF}}(\mathcal{A}) = \left| \mathrm{Pr}[\mathcal{A}^{\mathrm{PRF}}(K, \cdot) \Rightarrow 1: K \leftarrow \mathcal{K}] - \mathrm{Pr}[\mathcal{A}^{\mathrm{F}}(\cdot) \Rightarrow 1: F \leftarrow \mathcal{F}(\mathcal{X} \to \mathcal{Y})] \right|. $$

When this advantage is small for all efficient adversaries, we say $f$ is a pseudorandom function. Let $g: \mathcal{K} \to \mathcal{Y}$ be a function. We define the PRG advantage of an adversary $\mathcal{A}$ as

$$ \mathrm{Adv}_{\mathrm{g}}^{\mathrm{PRG}}(\mathcal{A}) = \left| \mathrm{Pr}[\mathcal{A}(y) \Rightarrow 1: K \leftarrow \mathcal{K}; y \leftarrow g(K)] - \mathrm{Pr}[\mathcal{A}(y) \Rightarrow 1: y \leftarrow \mathcal{Y}] \right|. $$

When this advantage is small for all efficient adversaries, we say $g$ is a pseudorandom generator.

**Public-Key Encryption.** A public-key encryption scheme consists of three algorithms PKE = (Gen, Enc, Dec) and a finite message space $\mathcal{M}$. The key generation algorithm Gen outputs a key pair (pk, sk). The encryption algorithm Enc, on input $pk$ and a message $m \in \mathcal{M}$, outputs a ciphertext $c \leftarrow \mathrm{Enc}(pk, m)$. If necessary to derandomize encryption, we writing $c \leftarrow \mathrm{Enc}(pk, m; r)$, where $r \leftarrow \mathcal{R}$ and $\mathcal{R}$ is the randomness space. The decryption algorithm Dec, on input $sk$ and a ciphertext $c$, outputs either a message $m \leftarrow \mathrm{Dec}(sk, c) \in \mathcal{M}$ or a special symbol $\perp \notin \mathcal{M}$ to indicate that $c$ is not a valid ciphertext.

**CORRECTNESS.** Correctness of a PKE is defined as in Figure 14. We give both a standard model definition (left) and a definition in the random oracle model (ROM, right). Note that the adversary gets the secret key as an input. In the standard model, $\delta$-correctness means that for all (possibly unbounded) adversaries $\mathcal{A}$, $\mathrm{Pr}[\mathrm{COR}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1] \le \delta$. In the ROM, we extend the definition so that $\delta$ is parameterized by an upper bound on the number of queries placed by $\mathcal{A}$ to its random oracle.

**CIPHERTEXT SPREADNESS.** We say that PKE is $\gamma$-spread if, for every key pair $(pk, sk) \leftarrow \mathrm{Gen}()$ and every ciphertext $c$, $\mathrm{Pr}_{r \leftarrow \mathcal{R}}[c = \mathrm{Enc}(pk, m; r)] \le 2^{-\gamma}$.

**SECURITY.** We now define several security notions for public-key encryption.

**Definition 1 (OW-Atk).** Let PKE = (Gen, Enc, Dec) be a public-key encryption scheme with message space $\mathcal{M}$. For Atk $\in \{\mathrm{CPA}, \mathrm{PCVA}\}$, we give the OW-Atk security games in Figure 15. Note that, if Atk = CPA, we have $\mathcal{O} = \emptyset$; and if Atk = PCVA, we have $\mathcal{O} = \{\mathrm{Pco}, \mathrm{Cvo}\}$. We define the OW-Atk advantage function of an adversary $\mathcal{A}$ against PKE as $\mathrm{Adv}_{\mathrm{PKE}}^{\mathrm{OW-Atk}}(\mathcal{A}) = \mathrm{Pr}[\mathrm{OW-Atk}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1]$.

Note that the adversary wins the one-way game if it guesses the result of decrypting the challenge ciphertext, rather than the standard definition of finding the message that is originally encrypted. The two games have statistical distance $\delta$, if PKE is $\delta$-correct. We also define the more standard notion, allowing the adversary to output a list of guesses.

**Definition 2.** OWL-CPA Let PKE = (Gen, Enc, Dec) be a public-key encryption scheme with message space $\mathcal{M}$. We give the OWL-CPA security game in Figure 15. We define the OWL-CPA advantage function of an adversary $\mathcal{A}$ against PKE as $\mathrm{Adv}_{\mathrm{PKE}}^{\mathrm{OWL-CPA}}(\mathcal{A}) = \mathrm{Pr}[\mathrm{OWL-CPA}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1]$.

We conclude this section with the standard definition of IND-CPA security for a PKE.

**Definition 3.** IND-CPA Let PKE = (Gen, Enc, Dec) be a public-key encryption scheme with message space $\mathcal{M}$. We define the IND-CPA game as in Figure 16, and the IND-CPA advantage function of an adversary $\mathcal{A} = (\mathcal{A}_1, \mathcal{A}_2)$ against PKE as $\mathrm{Adv}_{\mathrm{PKE}}^{\mathrm{IND-CPA}}(\mathcal{A}) = |\mathrm{Pr}[\mathrm{IND-CPA}_{\mathrm{PKE}}^{\mathcal{A}} \Rightarrow 1] - 1/2|$.

In the proof of the FO transform (see Section 5) we use this general lemma that is verified in EasyCrypt.
<table><caption>Fig. 15. One-wayness of a PKE.</caption><thead><tr><th>Game OW-Atk:</th><th>Oracle Pco(m &isin; M, c):</th><th>Game OWL-CPA:</th></tr></thead><tbody><tr><td>1: (pk, sk) &larr; Gen()</td><td>1: return (m = Dec(sk, c))</td><td>1: (pk, sk) &larr; Gen()</td></tr><tr><td>2: m* &larr; &lang;M</td><td></td><td>2: m* &larr; &lang;M</td></tr><tr><td>3: c* &larr; Enc(pk, m*)</td><td>Oracle Cvo(c &ne; c*):</td><td>3: c* &larr; Enc(pk, m*)</td></tr><tr><td>4: m' &larr; A<sup>O</sup>(pk, c*)</td><td>1: m &larr; Dec(sk, c)</td><td>4: L &larr; A(pk, c*)</td></tr><tr><td>5: return Pco(m', c*)</td><td>2: return m &ne; &perp;</td><td>5: return m* &isin; L</td></tr></tbody></table>

<table><caption>Fig. 16. IND-CPA security of a PKE and IND-CCA security for a KEM.</caption><thead><tr><th>Game IND-CPA:</th><th>Game IND-CCA:</th><th>Oracle Decaps(c):</th></tr></thead><tbody><tr><td>1: (pk, sk) &larr; Gen()</td><td>1: (pk, sk) &larr; Gen()</td><td>1: If c = c* return &perp;</td></tr><tr><td>2: (m<sub>0</sub>, m<sub>1</sub>, st) &larr; &lang;A<sub>1</sub>(pk)</td><td>2: (k<sub>0</sub>, c*) &larr; &lang;Enc(pk)</td><td>2: k &larr; Dec(sk, c)</td></tr><tr><td>3: b &larr; &lang;{0, 1}</td><td>3: k<sub>1</sub> &larr; &lang;K</td><td>3: return k</td></tr><tr><td>4: c* &larr; &lang;Enc(pk, m<sub>b</sub>)</td><td>4: b &larr; &lang;{0, 1}</td><td></td></tr><tr><td>5: b' &larr; &lang;A<sub>2</sub>(st, c*)</td><td>5: b' &larr; &lang;A<sup>Decaps</sup>(pk, c*, k<sub>b</sub>)</td><td></td></tr><tr><td>6: return b' = b</td><td>6: return b' = b</td><td></td></tr></tbody></table>

**Lemma 1.** For all OWL-CPA adversary $\mathcal{B}$ returning a list of size at most $\text{MAX}$, there exists an IND-CPA adversary $\mathcal{A}$ such that

$$ \text{Adv}_{\text{PKE}}^{\text{OWL-CPA}}(\mathcal{B}) \le 2 \cdot \left( \frac{\text{MAX}}{|\mathcal{M}|} + \text{Adv}_{\text{PKE}}^{\text{IND-CPA}}(\mathcal{A}) \right) $$

*Proof (Sketch of formalization).* We define an IND-CPA adversary $\mathcal{A}$ that uses the OWL-CPA adversary $\mathcal{B}$ in the obvious way: i. choose challenge IND-CPA messages $(m_0, m_1)$ uniformly at random and run $\mathcal{B}$ on the challenge ciphertext; ii. if the list output by $\mathcal{B}$ contains $m_b$, but not $m_{-b}$, return $b$; iii. otherwise return a random bit $b'$.

We re-express the IND-CPA advantage using the standard form that conditions on the hidden bit, and get that:

$$ 2 \cdot \text{Adv}_{\text{PKE}}^{\text{IND-CPA}}(\mathcal{A}) = \left| \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(1) \Rightarrow 1] - \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(0) \Rightarrow 1] \right| $$

We then define a bad event in both experiments on the right-hand side of the above equation, which corresponds to $\mathcal{A}$ returning random bit $b'$. Clearly, this event occurs with the same probability in both experiments, and the output of both experiments are identically distributed when this event does occur. This means that

$$ 2 \cdot \text{Adv}_{\text{PKE}}^{\text{IND-CPA}}(\mathcal{A}) = \left| \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(1) \Rightarrow 1 \land \neg \text{bad}] - \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(0) \Rightarrow 1 \land \neg \text{bad}] \right| $$

The next step in the proof shows that

$$ \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(0) \Rightarrow 1 \land \neg \text{bad}] \le \text{MAX}/|\mathcal{M}|. $$

which follows from the fact that $m_1$ is information theoretically hidden from $\mathcal{B}$. A similar argument allows us to show that

$$ \left| \text{Adv}_{\text{PKE}}^{\text{OWL-CPA}}(\mathcal{B}) - \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(1) \Rightarrow 1 \land \neg \text{bad}] \right| \le \text{MAX}/|\mathcal{M}|. $$

The lemma follows from the above inequalities. The arguments above are also good examples of game-hopping proofs that the EasyCrypt logic was designed to handle. $\square$

**Key Encapsulation Mechanisms.** A key encapsulation mechanism KEM = (Gen, Enc, Dec) consists of three algorithms. The key generation algorithm Gen outputs a key pair $(pk, sk)$, where $pk$ also defines a finite key space $K$. The encapsulation algorithm Enc, on input $pk$, outputs a tuple $(k, c)$ where $c$ is said to be an encapsulation of the key $k$ which is contained in key space $K$. The deterministic decapsulation algorithm Dec, on input $sk$ and an encapsulation $c$, outputs either a key $k \leftarrow \text{Dec}(sk, c) \in K$ or a special symbol $\perp \notin K$ to indicate that $c$ is not a valid encapsulation. We call KEM $\delta$-correct if $\Pr[\text{Dec}(sk, c) \neq k | (pk, sk) \leftarrow \text{Gen}; (k, c) \leftarrow \text{Enc}(pk)] \le \delta$. Note that the above definition does not include a correctness adversary—and for this reason also makes sense in the random oracle model—because KEM ciphertexts do not depend on maliciously chosen messages.

**SECURITY.** We now define indistinguishability under chosen ciphertext attacks (IND-CCA) for a KEM.
<table><caption>Fig. 15. One-wayness of a PKE.</caption><thead><tr><th>Game OW-Atk:</th><th>Oracle Pco(m &isin; M, c):</th><th>Game OWL-CPA:</th></tr></thead><tbody><tr><td>1: (pk, sk) &larr; Gen()</td><td>1: return (m = Dec(sk, c))</td><td>1: (pk, sk) &larr; Gen()</td></tr><tr><td>2: m* &larr; &lang;M</td><td></td><td>2: m* &larr; &lang;M</td></tr><tr><td>3: c* &larr; Enc(pk, m*)</td><td>Oracle Cvo(c &ne; c*):</td><td>3: c* &larr; Enc(pk, m*)</td></tr><tr><td>4: m' &larr; A<sup>O</sup>(pk, c*)</td><td>1: m &larr; Dec(sk, c)</td><td>4: L &larr; A(pk, c*)</td></tr><tr><td>5: return Pco(m', c*)</td><td>2: return m &ne; &perp;</td><td>5: return m* &isin; L</td></tr></tbody></table>

<table><caption>Fig. 16. IND-CPA security of a PKE and IND-CCA security for a KEM.</caption><thead><tr><th>Game IND-CPA:</th><th>Game IND-CCA:</th><th>Oracle Decaps(c):</th></tr></thead><tbody><tr><td>1: (pk, sk) &larr; Gen()</td><td>1: (pk, sk) &larr; Gen()</td><td>1: If c = c* return &perp;</td></tr><tr><td>2: (m<sub>0</sub>, m<sub>1</sub>, st) &larr; &lang;A<sub>1</sub>(pk)</td><td>2: (k<sub>0</sub>, c*) &larr; &lang;Enc(pk)</td><td>2: k &larr; Dec(sk, c)</td></tr><tr><td>3: b &larr; &lang;{0, 1}</td><td>3: k<sub>1</sub> &larr; &lang;K</td><td>3: return k</td></tr><tr><td>4: c* &larr; &lang;Enc(pk, m<sub>b</sub>)</td><td>4: b &larr; &lang;{0, 1}</td><td></td></tr><tr><td>5: b' &larr; &lang;A<sub>2</sub>(st, c*)</td><td>5: b' &larr; &lang;A<sup>Decaps</sup>(pk, c*, k<sub>b</sub>)</td><td></td></tr><tr><td>6: return b' = b</td><td>6: return b' = b</td><td></td></tr></tbody></table>

**Lemma 1.** For all OWL-CPA adversary $\mathcal{B}$ returning a list of size at most $\text{MAX}$, there exists an IND-CPA adversary $\mathcal{A}$ such that

$$ \text{Adv}_{\text{PKE}}^{\text{OWL-CPA}}(\mathcal{B}) \le 2 \cdot \left( \frac{\text{MAX}}{|\mathcal{M}|} + \text{Adv}_{\text{PKE}}^{\text{IND-CPA}}(\mathcal{A}) \right) $$

*Proof (Sketch of formalization).* We define an IND-CPA adversary $\mathcal{A}$ that uses the OWL-CPA adversary $\mathcal{B}$ in the obvious way: i. choose challenge IND-CPA messages $(m_0, m_1)$ uniformly at random and run $\mathcal{B}$ on the challenge ciphertext; ii. if the list output by $\mathcal{B}$ contains $m_b$, but not $m_{-b}$, return $b$; iii. otherwise return a random bit $b'$.

We re-express the IND-CPA advantage using the standard form that conditions on the hidden bit, and get that:

$$ 2 \cdot \text{Adv}_{\text{PKE}}^{\text{IND-CPA}}(\mathcal{A}) = \left| \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(1) \Rightarrow 1] - \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(0) \Rightarrow 1] \right| $$

We then define a bad event in both experiments on the right-hand side of the above equation, which corresponds to $\mathcal{A}$ returning random bit $b'$. Clearly, this event occurs with the same probability in both experiments, and the output of both experiments are identically distributed when this event does occur. This means that

$$ 2 \cdot \text{Adv}_{\text{PKE}}^{\text{IND-CPA}}(\mathcal{A}) = \left| \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(1) \Rightarrow 1 \land \neg \text{bad}] - \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(0) \Rightarrow 1 \land \neg \text{bad}] \right| $$

The next step in the proof shows that

$$ \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(0) \Rightarrow 1 \land \neg \text{bad}] \le \text{MAX}/|\mathcal{M}|. $$

which follows from the fact that $m_1$ is information theoretically hidden from $\mathcal{B}$. A similar argument allows us to show that

$$ \left| \text{Adv}_{\text{PKE}}^{\text{OWL-CPA}}(\mathcal{B}) - \Pr[\text{CPA}_{\mathcal{A}}^{\text{PKE}}(1) \Rightarrow 1 \land \neg \text{bad}] \right| \le \text{MAX}/|\mathcal{M}|. $$

The lemma follows from the above inequalities. The arguments above are also good examples of game-hopping proofs that the EasyCrypt logic was designed to handle. $\square$

**Key Encapsulation Mechanisms.** A key encapsulation mechanism $\text{KEM} = (\text{Gen}, \text{Enc}, \text{Dec})$ consists of three algorithms. The key generation algorithm $\text{Gen}$ outputs a key pair $(pk, sk)$, where $pk$ also defines a finite key space $\mathcal{K}$. The encapsulation algorithm $\text{Enc}$, on input $pk$, outputs a tuple $(k, c)$ where $c$ is said to be an encapsulation of the key $k$ which is contained in key space $\mathcal{K}$. The deterministic decapsulation algorithm $\text{Dec}$, on input $sk$ and an encapsulation $c$, outputs either a key $k \leftarrow \text{Dec}(sk, c) \in \mathcal{K}$ or a special symbol $\perp \notin \mathcal{K}$ to indicate that $c$ is not a valid encapsulation. We call $\text{KEM}$ $\delta$-correct if $\Pr[\text{Dec}(sk, c) \neq k | (pk, sk) \leftarrow \text{Gen}; (k, c) \leftarrow \text{Enc}(pk)] \le \delta$. Note that the above definition does not include a correctness adversary—and for this reason also makes sense in the random oracle model—because $\text{KEM}$ ciphertexts do not depend on maliciously chosen messages.

**SECURITY.** We now define indistinguishability under chosen ciphertext attacks (IND-CCA) for a KEM.
**Definition 4.** IND-CCA. We define the IND-CCA game also in Figure 16 and the IND-CCA advantage function of an adversary $\mathcal{A}$ against KEM as

$$ \mathrm{Adv}_{\mathrm{KEM}}^{\mathrm{IND-CCA}}(\mathcal{A}) = \left| \Pr[\mathrm{IND-CCA}_{\mathrm{KEM}}^{\mathcal{A}} \Rightarrow 1] - 1/2 \right|. $$

## B Generic EasyCrypt Arguments

We now describe more in depth the generic arguments we make use of in our formal proofs, and some of the issues faced in applying them to the specific ML-KEM proof.

### B.1 Plug-and-Pray

The first generic result we use heavily in this proof is a plug-and-pray argument. In this argument, a parametric reduction $R_i$—for example, a reduction that simulates the $i$th query to an oracle in a specific way—is replaced, with some security loss, with a reduction $R$ that 1) makes a uniformly random guess as to the value of the parameter $i$ (within a bounded-size set $S$ of possible values); 2) runs the parametric reduction $R_i$; and 3) returns its result.

In such a setting, and for any event $E$, we will have, for every possible value $j$ of the index

$$ \Pr[R : E] = |S| \cdot \Pr[R : E \wedge i = j] $$

The plug-and-pray library formalizes the argument generically, allowing arbitrary instantiations or the reduction, guess and event, and further allowing the value of the index to be derived from the state of the experiment, instead of being externally quantified.

### B.2 Hybrids

The second result we heavily rely on in our ML-KEM proof is a generic hybrid argument, which captures generically union bound-style results in indistinguishability steps.

Consider two oracles $O_l$ and $O_r$ of the same type, and a distinguisher $D$ trying to distinguish them in at most $q$ queries. Our generic hybrid proves (entirely generically) that, for some distinguisher $D_1$ that makes at most 1 query to its oracle, we have

$$ |\Pr[D(O_l)] - \Pr[D(O_r)]| \le q \cdot |\Pr[D_1(O_l)] - \Pr[D_1(O_r)]| $$

The hybrid library formalizes the argument generically, allowing arbitrary instantiations of the oracle and distinguisher types, and also supporting the result where the oracle being replaced shares state with oracles that do not change from one side to the other.

### B.3 PROM

The final generic result we use formally captures the cryptographic argument that "a value is random and independent of the adversary's view." This was initially produced as part of the formalization of indistinguishability from a random oracle for SHA3 [9], and is therefore framed as an indistinguishability result between two different implementations of a programmable random oracle interface. This result shows that no context (or unbounded adversary) can distinguish between the *eager* and *lazy* versions of the oracles presented in Figure 17, where the latter omits line 1 of the sample algorithm. These oracles allow for globally initializing or resetting (init), or locally observing associated values (get), programming the random oracle (set), or eagerly (resp. lazily) sampling values associated with given entries (sample). In essence, the library establishes generically that sampling unused values can be deferred until they (or some behavior that depends on them) first become visible to the adversary or context.

The result itself is quite general, and hides away some of the complex program logics involved in proving it, allowing less expert users to more easily formalize complex proofs. However, its application in our setting, where we need to identify a specific query which will be sampled eagerly, is somewhat complex: we cannot simply sample the entire random function eagerly over an infinite domain, and neither can we predict the values of the queries the adversary will make. Most of the applications we make of this result in the ML-KEM proof first involve an indirection mapping query values to their index (essentially, and up to repeat queries, the first query would have index 1, the second query would have index 2, and so on), and eagerly sampling a map from integers (between 1 and the maximum number of queries). This essentially allows to partially sample the outputs of the function and later assign them to particular inputs as the adversary makes queries.
**Definition 4.** IND-CCA. We define the IND-CCA game also in Figure 16 and the IND-CCA advantage function of an adversary $\mathcal{A}$ against KEM as

$$ \mathrm{Adv}_{\mathrm{KEM}}^{\mathrm{IND-CCA}}(\mathcal{A}) = \left| \Pr[\mathrm{IND-CCA}_{\mathrm{KEM}}^{\mathcal{A}} \Rightarrow 1] - 1/2 \right|. $$

## B Generic EasyCrypt Arguments

We now describe more in depth the generic arguments we make use of in our formal proofs, and some of the issues faced in applying them to the specific ML-KEM proof.

### B.1 Plug-and-Pray

The first generic result we use heavily in this proof is a plug-and-pray argument. In this argument, a parametric reduction $R_i$—for example, a reduction that simulates the $i$th query to an oracle in a specific way—is replaced, with some security loss, with a reduction $R$ that 1) makes a uniformly random guess as to the value of the parameter $i$ (within a bounded-size set $S$ of possible values); 2) runs the parametric reduction $R_i$; and 3) returns its result.

In such a setting, and for any event $E$, we will have, for every possible value $j$ of the index

$$ \Pr[R : E] = |S| \cdot \Pr[R : E \wedge i = j] $$

The plug-and-pray library formalizes the argument generically, allowing arbitrary instantiations or the reduction, guess and event, and further allowing the value of the index to be derived from the state of the experiment, instead of being externally quantified.

### B.2 Hybrids

The second result we heavily rely on in our ML-KEM proof is a generic hybrid argument, which captures generically union bound-style results in indistinguishability steps.

Consider two oracles $O_l$ and $O_r$ of the same type, and a distinguisher $D$ trying to distinguish them in at most $q$ queries. Our generic hybrid proves (entirely generically) that, for some distinguisher $D_1$ that makes at most 1 query to its oracle, we have

$$ |\Pr[D(O_l)] - \Pr[D(O_r)]| \le q \cdot |\Pr[D_1(O_l)] - \Pr[D_1(O_r)]| $$

The hybrid library formalizes the argument generically, allowing arbitrary instantiations of the oracle and distinguisher types, and also supporting the result where the oracle being replaced shares state with oracles that do not change from one side to the other.

### B.3 PROM

The final generic result we use formally captures the cryptographic argument that "a value is random and independent of the adversary's view." This was initially produced as part of the formalization of indistinguishability from a random oracle for SHA3 [9], and is therefore framed as an indistinguishability result between two different implementations of a programmable random oracle interface. This result shows that no context (or unbounded adversary) can distinguish between the *eager* and *lazy* versions of the oracles presented in Figure 17, where the latter omits line 1 of the sample algorithm. These oracles allow for globally initializing or resetting (init), or locally observing associated values (get), programming the random oracle (set), or eagerly (resp. lazily) sampling values associated with given entries (sample). In essence, the library establishes generically that sampling unused values can be deferred until they (or some behavior that depends on them) first become visible to the adversary or context.

The result itself is quite general, and hides away some of the complex program logics involved in proving it, allowing less expert users to more easily formalize complex proofs. However, its application in our setting, where we need to identify a specific query which will be sampled eagerly, is somewhat complex: we cannot simply sample the entire random function eagerly over an infinite domain, and neither can we predict the values of the queries the adversary will make. Most of the applications we make of this result in the ML-KEM proof first involve an indirection mapping query values to their index (essentially, and up to repeat queries, the first query would have index 1, the second query would have index 2, and so on), and eagerly sampling a map from integers (between 1 and the maximum number of queries). This essentially allows to partially sample the outputs of the function and later assign them to particular inputs as the adversary makes queries.
<figure><img src="image_4.png" /><figcaption>**Fig. 17.** PROM oracles, in the lazy version the dashed box is removed</figcaption></figure>
<figure><img src="image_6.png" /><figcaption>**Fig. 17.** PROM oracles, in the lazy version the dashed box is removed</figcaption></figure>