Kosaian, K., Tan, Y. K., & Rozier, K. Y. (2024). Formalizing Coppersmith’s Method in Isabelle/HOL. In Intelligent Computer Mathematics (pp. 127–145). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-66997-2_8
Abstract:
We formalize Coppersmith’s method, an algorithm for finding
small (in magnitude) roots of univariate integer polynomials mod M,
in the theorem prover Isabelle/HOL. Our work is motivated by the goal
of moving cryptography into the realm of formal methods by formalizing
not only the correctness and security arguments behind cryptographic algorithms
but also the mathematics behind attacks on those algorithms.
Coppersmith’s method fits into this goal as it has important applications
in cryptography and is used in various attacks on the RSA algorithm for
public-key cryptography. We overview and give insights into our formalization,
which includes new contributions to Isabelle/HOL’s libraries,
and builds on the existing formalization of the Lenstra–Lenstra–Lovász
(LLL) algorithm for lattice basis reduction.
License type:
Publisher Copyright
Funding Info:
There was no specific funding for the research done
Description:
This version of the article has been accepted for publication, after peer review (when applicable) and is subject to Springer Nature’s AM terms of use, but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: http://dx.doi.org/10.1007/978-3-031-66997-2_8