PlumX Metrics
Embed PlumX Metrics

Formalizing Coppersmith’s Method in Isabelle/HOL

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN: 1611-3349, Vol: 14960 LNAI, Page: 127-145
2024
  • 0
    Citations
  • 0
    Usage
  • 0
    Captures
  • 0
    Mentions
  • 0
    Social Media
Metric Options:   Counts1 Year3 Year

Conference Paper Description

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.

Provide Feedback

Have ideas for a new metric? Would you like to see something else here?Let us know