A Formalization of the LLL Basis Reduction Algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)
41 Downloads (Pure)

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 this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.
Original languageEnglish
Title of host publicationInteractive Theorem Proving
Subtitle of host publication9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings
EditorsJeremy Avigad, Assia Mahboubi
PublisherSpringer
Chapter10
Pages160-177
Number of pages18
ISBN (Electronic)978-3-319-94821-8
ISBN (Print)978-3-319-94820-1
DOIs
Publication statusPublished - 4 Jul 2018

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10895
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Formalization
LLL Algorithm
Computer Algebra
Number theory
Soundness
NP-hard Problems
Cryptography
Polynomial-time Algorithm
Univariate
Factorization
Polynomial time
Integrate
Polynomial
Integer
Approximation

Cite this

Divasón, J., Joosten, S., Thiemann, R., & Yamada, A. (2018). A Formalization of the LLL Basis Reduction Algorithm. In J. Avigad, & A. Mahboubi (Eds.), Interactive Theorem Proving: 9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings (pp. 160-177). (Lecture Notes in Computer Science; Vol. 10895). Springer. https://doi.org/10.1007/978-3-319-94821-8_10
Divasón, Jose ; Joosten, Sebastiaan ; Thiemann, René ; Yamada, Akihisa. / A Formalization of the LLL Basis Reduction Algorithm. Interactive Theorem Proving: 9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings. editor / Jeremy Avigad ; Assia Mahboubi. Springer, 2018. pp. 160-177 (Lecture Notes in Computer Science).
@inbook{72f25ed465d14e85a452b33f7206ae23,
title = "A Formalization of the LLL Basis Reduction Algorithm",
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 this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.",
author = "Jose Divas{\'o}n and Sebastiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada",
note = "Open Access",
year = "2018",
month = "7",
day = "4",
doi = "10.1007/978-3-319-94821-8_10",
language = "English",
isbn = "978-3-319-94820-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "160--177",
editor = "Jeremy Avigad and Assia Mahboubi",
booktitle = "Interactive Theorem Proving",

}

Divasón, J, Joosten, S, Thiemann, R & Yamada, A 2018, A Formalization of the LLL Basis Reduction Algorithm. in J Avigad & A Mahboubi (eds), Interactive Theorem Proving: 9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings. Lecture Notes in Computer Science, vol. 10895, Springer, pp. 160-177. https://doi.org/10.1007/978-3-319-94821-8_10

A Formalization of the LLL Basis Reduction Algorithm. / Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa.

Interactive Theorem Proving: 9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings. ed. / Jeremy Avigad; Assia Mahboubi. Springer, 2018. p. 160-177 (Lecture Notes in Computer Science; Vol. 10895).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

TY - CHAP

T1 - A Formalization of the LLL Basis Reduction Algorithm

AU - Divasón, Jose

AU - Joosten, Sebastiaan

AU - Thiemann, René

AU - Yamada, Akihisa

N1 - Open Access

PY - 2018/7/4

Y1 - 2018/7/4

N2 - 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 this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

AB - 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 this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

U2 - 10.1007/978-3-319-94821-8_10

DO - 10.1007/978-3-319-94821-8_10

M3 - Chapter

SN - 978-3-319-94820-1

T3 - Lecture Notes in Computer Science

SP - 160

EP - 177

BT - Interactive Theorem Proving

A2 - Avigad, Jeremy

A2 - Mahboubi, Assia

PB - Springer

ER -

Divasón J, Joosten S, Thiemann R, Yamada A. A Formalization of the LLL Basis Reduction Algorithm. In Avigad J, Mahboubi A, editors, Interactive Theorem Proving: 9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings. Springer. 2018. p. 160-177. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-94821-8_10