Formalizing Coppersmith's Method

Katherine Kosaian 📧 and Yong Kiam Tan 📧

June 10, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize Coppersmith's method, an algorithm for finding small (in magnitude) roots of univariate integer polynomials mod M. Coppersmith's method has important applications in cryptography and is used in various attacks on the RSA algorithm for public-key cryptography. We also formalize a related (more lightweight) result with slightly weaker bounds; we split out the generic mathematical results underlying both this lightweight result and Coppersmith's method into a dedicated locale, which could be used to prove other "Coppersmith-like" results. Our work builds on the existing formalization of the Lenstra–Lenstra–Lovász (LLL) algorithm for lattice basis reduction, and our formalization adds a determinant bound on the length of the short vector produced by the LLL algorithm.


BSD License


Session Coppersmith_Method