{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:26:56Z","timestamp":1748413616631,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper describes the formal verification of NP-hardness reduction functions of two key problems relevant in algebraic lattice theory: the closest vector problem and the shortest vector problem, both in the infinity norm. The formalization uncovered a number of problems with the existing proofs in the literature. The paper describes how these problems were corrected in the formalization. The work was carried out in the proof assistant Isabelle.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_21","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"365-381","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification of\u00a0NP-Hardness Reduction Functions for\u00a0Exact Lattice Problems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4621-734X","authenticated-orcid":false,"given":"Katharina","family":"Kreuzer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0730-515X","authenticated-orcid":false,"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Ajtai, M.: Generating hard instances of lattice problems. Electron. Colloquium Comput. Complex. 3 (1996)","key":"21_CR1","DOI":"10.1145\/237814.237838"},{"doi-asserted-by":"crossref","unstructured":"Ajtai, M.: The shortest vector problem in L2 is NP-hard for randomized reductions (extended abstract). In: Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, STOC 1998, Dallas, Texas, USA, pp. 10\u201319. ACM Press (1998)","key":"21_CR2","DOI":"10.1145\/276698.276705"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02579403","volume":"6","author":"L Babai","year":"1986","unstructured":"Babai, L.: On Lov\u00e1sz\u2019 lattice reduction and the nearest lattice point problem. Combinatorica 6, 1\u201313 (1986)","journal-title":"Combinatorica"},{"unstructured":"Balbach, F.J.: The Cook-Levin theorem. Archive of Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/Cook_Levin.html. Formal proof development","key":"21_CR4"},{"key":"21_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6568-7","volume-title":"Sphere Packings, Lattices and Groups","author":"JH Conway","year":"1999","unstructured":"Conway, J.H., Sloane, N.J.A.: Sphere Packings, Lattices and Groups. Springer, New York (1999). https:\/\/doi.org\/10.1007\/978-1-4757-6568-7"},{"key":"21_CR6","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s00493-003-0019-y","volume":"23","author":"I Dinur","year":"2003","unstructured":"Dinur, I., Kindler, G., Raz, R., Safra, S.: Approximating CVP to within almost-polynomial factors is NP-hard. Combinatorica 23, 205\u2013243 (2003). https:\/\/doi.org\/10.1007\/s00493-003-0019-y","journal-title":"Combinatorica"},{"unstructured":"van Emde Boas, P.: Another NP-complete partition problem and the complexity of computing short vectors in a lattice. Technical report 81-04. Technical report, Mathematisch Instituut, Roetersstraat 15, 1018 WB Amsterdam, The Netherlands (1981)","key":"21_CR7"},{"doi-asserted-by":"publisher","unstructured":"G\u00e4her, L., Kunze, F.: Mechanising complexity theory: the Cook-Levin theorem in coq. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2021.20. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13915\/","key":"21_CR8","DOI":"10.4230\/LIPICS.ITP.2021.20"},{"doi-asserted-by":"crossref","unstructured":"Haviv, I., Regev, O.: Tensor-based hardness of the shortest vector problem to within almost polynomial factors. In: Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing, STOC 2007, pp. 469\u2013477. Association for Computing Machinery, New York (2007)","key":"21_CR9","DOI":"10.1145\/1250790.1250859"},{"issue":"5","key":"21_CR10","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1145\/1089023.1089027","volume":"52","author":"S Khot","year":"2005","unstructured":"Khot, S.: Hardness of approximating the shortest vector problem in lattices. J. ACM 52(5), 789\u2013808 (2005)","journal-title":"J. ACM"},{"unstructured":"Kreuzer, K.: Hardness of lattice problems. Archive of Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/CVP_Hardness.html. Formal proof development","key":"21_CR11"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BF01457454","volume":"261","author":"AK Lenstra","year":"1982","unstructured":"Lenstra, A.K., Lenstra, H., Lovasz, L.: Factoring polynomials with rational coefficients. Math. Ann. 261, 515\u2013534 (1982)","journal-title":"Math. Ann."},{"unstructured":"Liu, Y., Collins, R.: Frieze and wallpaper symmetry groups classification under affine and perspective distortion. Technical report. CMU-RI-TR-98-37, Carnegie Mellon University, Pittsburgh, PA (1998)","key":"21_CR13"},{"doi-asserted-by":"publisher","unstructured":"Micciancio, D.: The shortest vector in a lattice is hard to approximate to within some constant. In: Proceedings 39th Annual Symposium on Foundations of Computer Science (Cat. No. 98CB36280), pp. 92\u201398 (1998). https:\/\/doi.org\/10.1109\/SFCS.1998.743432","key":"21_CR14","DOI":"10.1109\/SFCS.1998.743432"},{"key":"21_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-0897-7","volume-title":"Complexity of Lattice Problems","author":"D Micciancio","year":"2002","unstructured":"Micciancio, D., Goldwasser, S.: Complexity of Lattice Problems. Springer, Boston (2002)"},{"key":"21_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-88702-7_5","volume-title":"Post-Quantum Cryptography","author":"D Micciancio","year":"2009","unstructured":"Micciancio, D., Regev, O.: Lattice-based cryptography. In: Bernstein, D.J., Buchmann, J., Dahmen, E. (eds.) Post-Quantum Cryptography, pp. 147\u2013191. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-540-88702-7_5"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics with Isabelle\/HOL. Springer, Cham (2014). http:\/\/concrete-semantics.org","key":"21_CR17","DOI":"10.1007\/978-3-319-10542-0"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"doi-asserted-by":"crossref","unstructured":"Rothvoss, T., Venzin, M.: Approximate CVP in time $$2^{0.802 n}$$ \u2013 now in any norm! arXiv:2110.02387 [cs] (2021)","key":"21_CR19","DOI":"10.1007\/978-3-031-06901-7_33"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:05:13Z","timestamp":1693609513000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}