{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:26:01Z","timestamp":1748413561883,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319948201"},{"type":"electronic","value":"9783319948218"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2018,7,4]],"date-time":"2018-07-04T00:00:00Z","timestamp":1530662400000},"content-version":"vor","delay-in-days":184,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-319-94821-8_10","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T17:25:55Z","timestamp":1530638755000},"page":"160-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Formalization of the LLL Basis Reduction Algorithm"],"prefix":"10.1007","author":[{"given":"Jose","family":"Divas\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastiaan","family":"Joosten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Divas\u00f3n, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the Berlekamp\u2013Zassenhaus factorization algorithm. In: CPP 2017, pp. 17\u201329. ACM (2017)","DOI":"10.1145\/3018610.3018617"},{"key":"10_CR2","unstructured":"Divas\u00f3n, J., Joosten, S., Thiemann, R., Yamada, A.: A verified factorization algorithm for integer polynomials with polynomial complexity. Archive of Formal Proofs, Formal proof development, February 2018. http:\/\/isa-afp.org\/entries\/LLL_Factorization.html"},{"key":"10_CR3","unstructured":"Divas\u00f3n, J., Joosten, S., Thiemann, R., Yamada, A.: A verified LLL algorithm. Archive of Formal Proofs, Formal proof development, February 2018. http:\/\/isa-afp.org\/entries\/LLL_Basis_Reduction.html"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"issue":"2","key":"10_CR5","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol. 43, pp. 1\u201313 (2010)","DOI":"10.4204\/EPTCS.43.1"},{"key":"10_CR7","unstructured":"Lee, H.: Vector spaces. Archive of Formal Proofs, Formal proof development, August 2014. http:\/\/isa-afp.org\/entries\/VectorSpace.html"},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BF01457454","volume":"261","author":"AK Lenstra","year":"1982","unstructured":"Lenstra, A.K., Lenstra, H.W., Lov\u00e1sz, L.: Factoring polynomials with rational coefficients. Math. Ann. 261, 515\u2013534 (1982)","journal-title":"Math. Ann."},{"issue":"6","key":"10_CR9","doi-asserted-by":"publisher","first-page":"2008","DOI":"10.1137\/S0097539700373039","volume":"30","author":"D Micciancio","year":"2000","unstructured":"Micciancio, D.: The shortest vector in a lattice is hard to approximate to within some constant. SIAM J. Comput. 30(6), 2008\u20132035 (2000)","journal-title":"SIAM J. Comput."},{"key":"10_CR10","series-title":"Information Security and Cryptography","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02295-1","volume-title":"The LLL Algorithm - Survey and Applications","year":"2010","unstructured":"Nguyen, P.Q., Vall\u00e9e, B. (eds.): The LLL Algorithm - Survey and Applications. Information Security and Cryptography. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-02295-1"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"10_CR12","unstructured":"Storjohann, A.: Faster algorithms for integer lattice basis reduction. Technical report 249, Department of Computer Science, ETH Zurich (1996)"},{"key":"10_CR13","unstructured":"The FPLLL development team. fplll, a lattice reduction library (2016). https:\/\/github.com\/fplll\/fplll"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-319-43144-4_24","volume-title":"Interactive Theorem Proving","author":"R Thiemann","year":"2016","unstructured":"Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle\/HOL. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 391\u2013408. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_24"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: CPP 2016, pp. 88\u201399. ACM (2016)","DOI":"10.1145\/2854065.2854073"},{"key":"10_CR16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139856065","volume-title":"Modern Computer Algebra","author":"J von zur Gathen","year":"2013","unstructured":"von zur Gathen, J., Gerhard, J.: Modern Computer Algebra, 3rd edn. Cambridge University Press, New York (2013)","edition":"3"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,23]],"date-time":"2024-07-23T11:06:16Z","timestamp":1721732776000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"4 July 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}