A Formalization of the LLL Basis Reduction Algorithm

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

doi:10.1007/978-3-319-94821-8_10

A Formalization of the LLL Basis Reduction Algorithm

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

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

5 Citations (Scopus)

139 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 language	English
Title of host publication	Interactive Theorem Proving
Subtitle of host publication	9th International Conference, ITP 2018. Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018. Proceedings
Editors	Jeremy Avigad, Assia Mahboubi
Publisher	Springer
Chapter	10
Pages	160-177
Number of pages	18
ISBN (Electronic)	978-3-319-94821-8
ISBN (Print)	978-3-319-94820-1
DOIs	https://doi.org/10.1007/978-3-319-94821-8_10
Publication status	Published - 4 Jul 2018

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10895
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

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

A formalizationFinal published version, 406 KB

http://link.springer.com/10.1007/978-3-319-94821-8_10

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é et al. / 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 = jul,

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",

address = "Germany",

}

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é et al.
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 proceeding › Chapter › Academic › peer-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). doi: 10.1007/978-3-319-94821-8_10

A Formalization of the LLL Basis Reduction Algorithm

Abstract

Publication series

Access to Document

Fingerprint

Cite this