Document Open Access Logo

Functional Correctness of an Optimized Modular Inversion Algorithm

Authors Assia Mahboubi , Guillaume Melquiond , Pierre-Yves Strub , Tomás Vallejos Parada

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.9.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Logic and verification
  • Security and privacy → Logic and verification
  • Security and privacy → Mathematical foundations of cryptography
  • Theory of computation → Cryptographic primitives
Keywords
  • deductive program verification
  • modular inversion algorithm
  • formal verification
  • Rocq
  • Why3

Metrics

Abstract

This article describes the first mechanized proof of functional correctness of an algorithm due to Pornin (2020), for computing modular inverses via an optimized extended binary GCD algorithm. This algorithm is widely used in cryptography applications, due to its speed and constant-timeness. But this speed comes from the use of approximate computations during its loop iterations. In particular, the pen-and-paper proof of the fact that sufficiently many loop iterations were performed is especially intricate (and the originally published version was actually wrong), which negatively impacts the trust in the applications that rely on the algorithm. In this work, we expand the notes provided in the original description by Pornin into a complete formal proof. We discuss the challenges raised by its mechanization, which eventually relies on the collaboration of deductive program verification and interactive theorem proving through the use of the tools Rocq and Why3.

Cite As Get BibTex

Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, and Tomás Vallejos Parada. Functional Correctness of an Optimized Modular Inversion Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.9

Author Details

Assia Mahboubi
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France
  • Vrije Universiteit Amsterdam, The Netherlands
Guillaume Melquiond
  • Inria, ENS de Lyon, CNRS, Université Lyon 1, LIP, UMR 5668, Lyon, France
Pierre-Yves Strub
  • PQShield, Paris, France
Tomás Vallejos Parada
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101001995).

Supplementary Materials

References

  1. José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, and Pierre-Yves Strub. Formally verifying Kyber - Episode V: machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. In Leonid Reyzin and Douglas Stebila, editors, 44th Annual International Cryptology Conference, volume 14921 of Lecture Notes in Computer Science, pages 384-421, 2024. URL: https://doi.org/10.1007/978-3-031-68379-4_12.
  2. Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. EasyCrypt: A tutorial. In Alessandro Aldini, Javier Lopez, and Fabio Martinelli, editors, Foundations of Security Analysis and Design VII, volume 8604 of Lecture Notes in Computer Science, pages 146-166, 2014. URL: https://doi.org/10.1007/978-3-319-10082-1_6.
  3. Daniel J. Bernstein. Hull light, 2023. URL: https://cr.yp.to/2023/hull-light-20230416.sage.
  4. Daniel J. Bernstein and Bo-Yin Yang. Fast constant-time gcd computation and modular inversion. Cryptology ePrint Archive, Paper 2019/266, 2019. URL: https://eprint.iacr.org/2019/266.
  5. François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. Preserving user proofs across specification changes. In Ernie Cohen and Andrey Rybalchenko, editors, 5th International Conference on Verified Software: Theories, Tools, and Experiments, volume 8164 of Lecture Notes in Computer Science, pages 191-201, Menlo Park, CA, USA, May 2013. URL: https://doi.org/10.1007/978-3-642-54108-7_10.
  6. Richard P. Brent and Paul Zimmermann. Modern Computer Arithmetic. Cambridge Monographs on Applied and Computational Mathematics. Cambridge University Press, 2010. Google Scholar
  7. Billy Bob Brumley and Nicola Tuveri. Remote timing attacks are still practical. In Vijay Atluri and Claudia Díaz, editors, 16th European Symposium on Research in Computer Security, volume 6879 of Lecture Notes in Computer Science, pages 355-371, September 2011. URL: https://doi.org/10.1007/978-3-642-23822-2_20.
  8. Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. Constant-time foundations for the new Spectre era. In Alastair F. Donaldson and Emina Torlak, editors, 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 913-926, June 2020. URL: https://doi.org/10.1145/3385412.3385970.
  9. John Harrison. The s2n-bignum library of formally verified ECC software. In 25th Workshop on Elliptic Curve Cryptography, October 2024. URL: https://troll.iis.sinica.edu.tw/ecc24/slides/3-05-ecc2024_harrison.pdf.
  10. Paul C. Kocher. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In Neal Koblitz, editor, 16th Annual International Cryptology Conference, volume 1109 of Lecture Notes in Computer Science, pages 104-113, 1996. URL: https://doi.org/10.1007/3-540-68697-5_9.
  11. Robert Y. Lewis and Paul-Nicolas Madelaine. Simplifying casts and coercions (extended abstract). In Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, and Sophie Tourret, editors, 7th Workshop on Practical Aspects of Automated Reasoning, volume 2752 of CEUR Workshop Proceedings, pages 53-62, 2020. URL: https://ceur-ws.org/Vol-2752/paper4.pdf.
  12. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, October 2020. URL: https://doi.org/10.5281/zenodo.3999478.
  13. Guillaume Melquiond and Raphaël Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. Journal of Symbolic Computation, 115:74-95, 2023. URL: https://doi.org/10.1016/j.jsc.2022.07.007.
  14. Russell O'Connor and Andrew Poelstra. Formal verification of the Safegcd implementation, 2025. URL: https://doi.org/10.48550/arXiv.2507.17956.
  15. Christine Paulin-Mohring. Inductive definitions in the system Coq: rules and properties. In Marc Bezem and Jan Friso Groote, editors, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 328-345, March 1993. URL: https://doi.org/10.1007/BFb0037116.
  16. Thomas Pornin. Optimized binary GCD for modular inversion. Cryptology ePrint Archive, Paper 2020/972, 2020. URL: https://eprint.iacr.org/2020/972.
  17. Kazuhiko Sakaguchi. Reflexive tactics for algebra, revisited. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, volume 237 of LIPIcs, pages 29:1-29:22, August 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.29.
  18. Samuel Weiser, David Schrammel, Lukas Bodner, and Raphael Spreitzer. Big numbers - Big troubles: Systematically analyzing nonce leakage in (EC)DSA implementations. In Srdjan Capkun and Franziska Roesner, editors, 29th USENIX Security Symposium, pages 1767-1784, August 2020. URL: https://www.usenix.org/conference/usenixsecurity20/presentation/weiser.
  19. Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. In David Evans, Tal Malkin, and Dongyan Xu, editors, ACM SIGSAC Conference on Computer and Communications Security, pages 1789-1806, October 2017. URL: https://doi.org/10.1145/3133956.3134043.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact