Formalizing Coppersmith’s Method in Isabelle/HOL

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.