Abstract

The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography. In a recent paper, we presented the first formal soundness proof of the LLL algorithm. However, this proof did not include a formal statement of its complexity. Therefore, in this paper we provide two formal statements on the polynomial runtime. First, we formally prove a polynomial bound on the number of arithmetic operations. And second, we show that the numbers during the execution stay polynomial in size, so that each arithmetic operation can be performed in polynomial time.

BibTeX

@misc{LLL-Isabelle18,
  author      = "Max W. Haslbeck and Ren{\'e} Thiemann",
  title       = "Formal Verification of Bounds for the LLL Basis Reduction Algorithm",
  howpublised = "online",
  note        = "Presented at the Isabelle Workshop 2018",
  url         = "https://sketis.net/isabelle/isabelle-workshop-2018",
  year        = 2018
}