Methods for implementing post-quantum cryptography standards based on OCaml-oriented modular architecture
DOI:
https://doi.org/10.30837/rt.2026.1.224.05Keywords:
post-quantum cryptography, OCaml, ML-KEM, ML-DSA, SLH-DSA, NTT, modular cryptographic architecture, formal verificationAbstract
The development of quantum computing introduces fundamental risks to modern cryptographic systems used for protecting network infrastructure and software platforms. Following the publication of post-quantum cryptography standards by the National Institute of Standards and Technology (NIST) in 2024, including ML-KEM (FIPS 203), ML-DSA (FIPS 204), and SLH-DSA (FIPS 205), the need for efficient software implementation of post-quantum primitives in high-assurance programming environments has emerged. This paper proposes a multilayer architecture for post-quantum cryptographic algorithm implementation using the OCaml module system and functor-based parameterization of cryptographic primitives.
The proposed architecture is based on separating the software stack into a type-safe OCaml API layer, an algebraic cryptographic logic layer, and a low-level constant-time primitive layer implemented via C interfaces. Special attention is given to the implementation of Number Theoretic Transform (NTT) operations, centered binomial distribution (CBD) sampling for ML-KEM and ML-DSA.
To ensure implementation quality, NIST KAT vectors were integrated, along with side-channel statistical analysis tools including dudect, Valgrind, and TIMECOP.
The proposed architecture aims to minimize the trusted computing base, isolate cryptographically sensitive arithmetic operations, and enable future formal verification via coq-of-ocaml. The approach establishes the foundation for an OCaml-oriented post-quantum cryptography ecosystem and can be used for developing high-assurance cryptographic software.
References
Avanzi R., Bos J., Ducas L. et al. CRYSTALS-Kyber: Algorithm Specifications and Supporting Documenta-tion (version 3.02). NIST PQC Submission. 2021. URL: https://pq-crystals.org/kyber/data/kyber-specification-round3-20210804.pdf
Ducas L., Kiltz E., Lepoint T. et al. CRYSTALS-Dilithium: Algorithm Specifications and Supporting Docu-mentation (version 3.1). NIST PQC Submission. 2021. URL: https://pq-crystals.org/dilithium/
Bernstein D. J., Hülsing A., Kölbl S. et al. The SPHINCS+ Signature Framework. Advances in Cryptology – CRYPTO 2019. Springer, 2019. P. 390–420. DOI: 10.1007/978-3-030-26948-7_16
Fouque P.-A., Hoffstein J., Kirchner P. et al. Falcon: Fast-Fourier Lattice-based Compact Signatures over NTRU. NIST PQC Submission. 2020. URL: https://falcon-sign.info/
Almeida J. B., Barbosa M., Barthe G. et al. A Machine-Checked Proof of the Correctness of Kyber // IACR Transactions on Cryptographic Hardware and Embedded Systems. 2023. Vol. 2023, No. 4. P. 94–117.
Almeida J. B., Barbosa M., Barthe G. et al. Formally Verifying Kyber: IND-CCA Security in EasyCrypt. Advances in Cryptology – CRYPTO 2024. Springer, 2024.
Barbosa M., Barthe G., Grégoire B. et al. Machine-Checked Security Proofs of Dilithium in EasyCrypt. Ad-vances in Cryptology – CRYPTO 2023. Springer, 2023.
Barbosa M., Barthe G., Hülsing A. et al. A Tight Security Proof for SPHINCS+ in EasyCrypt. Advances in Cryptology – ASIACRYPT 2024. Springer, 2024.
Polubelova M., Protzenko J., Ho S. et al. libcrux: A Formally Verified, High-Assurance Cryptographic Pro-vider. Cryspen Technical Report. 2024. URL: https://cryspen.com/libcrux/
Janssen D., Breitner J., Bhargavan K. KyberSlash: Timing Attacks on Kyber Implementations. 2024. URL: https://kyberslash.cr.yp.to/
Almeida J. B., Baritel-Ruet C., Barbosa M. et al. Machine-Checked Proofs for Cryptographic Standards: In-differentiability of SPONGE and Secure High-Assurance Implementations of SHA-3 // Proceedings of the 2019 ACM SIGSAC. P. 1607–1622. DOI: 10.1145/3319535.3363211
Claret G., Zykin M. Formal Verification of OCaml Programs with coq-of-ocaml. Formal Land Technical Re-port. 2023. URL: https://formal.land/
Erbsen A., Philipoom J., Gross J. et al. Simple High-Level Code for Cryptographic Arithmetic – With Proofs, Without Compromises // IEEE Symposium on Security and Privacy. 2019. P. 1202–1219. DOI: 10.1109/SP.2019.00005
Stebila D., Mosca M. Post-Quantum Key Exchange for the Internet and the Open Quantum Safe Project. Se-lected Areas in Cryptography – SAC 2016. Springer, 2017. P. 14–37. DOI: 10.1007/978-3-319-69453-5_2
Willems D. ff: A Library for Finite Field Arithmetic in OCaml. opam package. 2022. URL: https://gitlab.com/nomadic-labs/cryptography/ocaml-ff
Lucas D. et al. mirage-crypto: Cryptographic Primitives for MirageOS. opam package. 2024. URL: https://github.com/mirage/mirage-crypto
Zinzindohoué J.-K., Bhargavan K., Protzenko J. et al. HACL*: A Verified Modern Cryptographic Library // Proceedings of the 2017 ACM SIGSAC. P. 1789–1806. DOI: 10.1145/3133956.3134043
Merigoux D. Constant-Time Operations in OCaml: Lessons from eqaf. OCaml Workshop 2020.
Khalimov, G., Kotukh, Y., Kolisnyk, M., & Khalimova, S., Sievierinov, O. (2024). LINE: Cryptosystem based on linear equations for logarithmic signatures // Cryptology ePrint Archive: Report 2024/697. https://ia.cr/2024/697
Khalimov G., Kotukh Y., Kolisnyk M., Khalimova S., Sievierinov O., & Korobchynskyi, M. Digital signa-ture scheme based on linear equations // K. Arai (Ed.). Advances in Information and Communication. FICC 2025. Lec-ture Notes in Networks and Systems. 2025. Vol. 1285. Springer. https://doi.org/10.1007/978-3-031-84460-7_46
Khalimov G., Kotukh Y., Kolisnyk M., Khalimova S., Sievierinov O., & Volkov O. SIGNLINE: Digital sig-nature scheme based on linear equations cryptosystem // 2024 4th International Conference on Electrical, Computer, Communications and Mechatronics Engineering (ICECCME) (p. 1–9). IEEE. https://doi.org/10.1109/ICECCME62383.2024.10796704
Kotukh Y., Severinov E., Vlasov O., Tenytska A., & Zarudna E. Some results of development of crypto-graphic transformations schemes using non-abelian groups // Radiotekhnika. 2021. No 204. P.66–72.
Kotukh Y., & Khalimov G. Hard problems for non-abelian group cryptography // Fifth International Scien-tific and Technical Conference “Computer and Information Systems and Technologies”. 2021. https://doi.org/10.30837/csitic52021232176
Kotukh Y., Khalimov G., Dzhura I., & Hivrenko H. Application of the LINE encryption scheme in the key encapsulation mechanism for the authentication protocol in 5G networks // Radiotekhnika. 2025. No 219. P. 36–45. https://doi.org/10.30837/rt.2024.4.219.04
Kotukh Y., Khalimov G., Korobchynskyi M., Rudenko M., Liubchak V., Matsyuk S., & Chashchyn M. Re-search horizons in group cryptography in the context of post-quantum cryptosystems development // Radiotekhnika. 2024. No 216. P.62–72. https://doi.org/10.30837/rt.2024.1.216.05
Kotukh Y., & Khalimov G. Towards practical cryptoanalysis of systems based on word problems and loga-rithmic signatures // Information security: Problems and prospects. 2022. P. 55–60.
Khalimov G., & Kotukh Y. Cryptographic strengthening of MST3 cryptosystem via automorphism group of Suzuki function fields // arXiv preprint arXiv:2504.07318. 2025.https://arxiv.org/abs/2504.07318
Khalimov G., & Kotukh Y. MST3 encryption improvement with three-parameter group of Hermitian func-tion field // arXiv preprint arXiv:2504.15391. 2025. https://arxiv.org/abs/2504.15391
Khalimov G., & Kotukh Y. Advanced MST3 encryption scheme based on generalized Suzuki 2-groups // arXiv preprint arXiv:2504.11804. 2025. https://arxiv.org/abs/2504.11804
Khalimov G., & Kotukh Y. Improved MST3 encryption scheme based on small Ree groups // arXiv preprint arXiv:2504.10947. 2025. https://arxiv.org/abs/2504.10947
Khalimov G., Kotukh Y., & Khalimova S. Encryption scheme based on the automorphism group of the Ree function field // IEEE 7th International Conference on Internet of Things: Systems, Management and Security (IOTSMS).2020. P. 1–8.
Khalimov G., Didmanidze I., Sievierinov O., Kotukh Y., & Shonia O. Encryption scheme based on the automorphism group of the Suzuki function field // IEEE International Conference on Problems of Infocommunications, Science and Technology (PIC S&T 2020). P. 383–387.
Khalimov G., Kotukh Y., & Khalimova S. Improved encryption scheme based on the automorphism group of the Ree function field // IEEE International IOT, Electronics and Mechatronics Conference (IEMTRONICS). 2021.
Khalimov G., Kotukh Y., & Khalimova S. (2019). MST3 cryptosystem based on the automorphism group of the Hermitian function field // IEEE International Scientific-Practical Conference Problems of Infocommunications, Science and Technology (PIC S&T 2019). P. 865–868.
Khalimov G., Kotukh Y., Didmanidze I., Sievierinov O., Khalimova S., & Vlasov A.. Towards three-parameter group encryption scheme for MST3 cryptosystem improvement // IEEE 5th World Conference on Smart Trends in Systems Security and Sustainability (WorldS4). 2021. P. 204–211.
Khalimov G., Kotukh Y., Didmanidze I., & Khalimova S. Encryption scheme based on small Ree groups // Proceedings of the 2021 7th International Conference on Computer Technology Applications (ICCTA ’21). 2021. P. 33–37.
Downloads
Published
How to Cite
Issue
Section
License
Authors who publish with this journal agree to the following terms:
1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
2. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
3. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
