Abstract
| Original language | English |
|---|---|
| Journal | Archive of Formal Proofs |
| Volume | 2018 |
| Publication status | Published - 2018 |
Fingerprint
Cite this
}
A verified LLL algorithm. / Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa.
In: Archive of Formal Proofs, Vol. 2018, 2018.Research output: Contribution to journal › Article › Academic
TY - JOUR
T1 - A verified LLL algorithm
AU - Divasón, Jose
AU - Joosten, Sebastiaan
AU - Thiemann, René
AU - Yamada, Akihisa
PY - 2018
Y1 - 2018
N2 - The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.
AB - The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.
M3 - Article
VL - 2018
JO - Archive of Formal Proofs
JF - Archive of Formal Proofs
SN - 2150-914x
ER -