DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.9

Functional Correctness of an Optimized Modular Inversion Algorithm

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

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{mahboubi_et_al:LIPIcs.ITP.2026.9,
  author =	{Mahboubi, Assia and Melquiond, Guillaume and Strub, Pierre-Yves and Vallejos Parada, Tom\'{a}s},
  title =	{{Functional Correctness of an Optimized Modular Inversion Algorithm}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.9},
  URN =		{urn:nbn:de:0030-drops-269839},
  doi =		{10.4230/LIPIcs.ITP.2026.9},
  annote =	{Keywords: deductive program verification, modular inversion algorithm, formal verification, Rocq, Why3}
}

Search Results

Documents authored by Vallejos Parada, Tomás

Functional Correctness of an Optimized Modular Inversion Algorithm

Abstract

Cite as

Thanks for your feedback!

Could not send message