A Verified Efficient Implementation of the LLL Basis Reduction Algorithm

Ralph Bottesch, Max W. Haslbeck, René Thiemann
22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, EPiC Series in Computing 57, pp. 164 – 180, 2018.

 pdf  doi:10.29007/xwwh

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 approximately solves an NP-hard problem. The algorithm has several applications in number theory, computer algebra and cryptography.
Recently, the first mechanized soundness proof of the LLL algorithm has been developed in Isabelle/HOL. However, this proof did not include a formal statement of the algorithm’s complexity. Furthermore, the resulting implementation was inefficient in practice.
We address both of these shortcomings in this paper. First, we prove the correctness of a more efficient implementation of the LLL algorithm that uses only integer computations. Second, we formally prove statements on the polynomial running-time.

BibTex

@inproceedings{RBMHRT-LPAR18,
author = {Ralph Bottesch and Max W. Haslbeck and Ren\'e Thiemann},
title = {A Verified Efficient Implementation of the
{LLL} Basis Reduction Algorithm},
booktitle = {22nd International Conference on Logic for Programming,
Artificial Intelligence and Reasoning},
editor = {Gilles Barthe and Geoff Sutcliffe and Margus Veanes},
series = {EPiC Series in Computing},
volume = {57},
pages = {164--180},
year = {2018},
publisher = {EasyChair},
doi = {10.29007/xwwh}
}