{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:40:04Z","timestamp":1748414404659,"version":"3.41.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66997-2_8","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"127-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing Coppersmith\u2019s Method in\u00a0Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9336-6006","authenticated-orcid":false,"given":"Katherine","family":"Kosaian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7033-2463","authenticated-orcid":false,"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"8_CR1","unstructured":"Ajani, Y., Bright, C.: A hybrid SAT and lattice reduction approach for integer factorization. In: \u00c1brah\u00e1m, E., Sturm, T. (eds.) SC-Square@ISSAC. CEUR Workshop Proceedings, vol.\u00a03455, pp. 39\u201343. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3455\/short1.pdf"},{"issue":"2","key":"8_CR2","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, M., Barthe, G., Bhargavan, K., Blanchet, B., Cremers, C., Liao, K., Parno, B.: SoK: computer-aided cryptography. In: SP, pp. 777\u2013795. IEEE (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00008","DOI":"10.1109\/SP40001.2021.00008"},{"key":"8_CR4","unstructured":"Barth, B.: Estonia suspends national 760,000 ID cards found prone to encryption vulnerability. SC Magazine (2017). https:\/\/www.scmagazine.com\/news\/estonia-suspends-national-760000-id-cards-found-prone-to-encryption-vulnerability"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22792-9_5"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., Pointcheval, D., B\u00e9guelin, S.Z.: Verified security of redundancy-free encryption from Rabin and RSA. In: Yu, T., Danezis, G., Gligor, V.D. (eds.) CCS, pp. 724\u2013735. ACM (2012). https:\/\/doi.org\/10.1145\/2382196.2382272","DOI":"10.1145\/2382196.2382272"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MSEC.2022.3154689","volume":"20","author":"DA Basin","year":"2022","unstructured":"Basin, D.A., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real-world, cryptographic protocols. IEEE Secur. Priv. 20(3), 24\u201332 (2022). https:\/\/doi.org\/10.1109\/MSEC.2022.3154689","journal-title":"IEEE Secur. Priv."},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/S00145-019-09341-Z","volume":"33","author":"DA Basin","year":"2020","unstructured":"Basin, D.A., Lochbihler, A., Sefidgar, S.R.: CryptHOL: game-based proofs in higher-order logic. J. Cryptol. 33(2), 494\u2013566 (2020). https:\/\/doi.org\/10.1007\/S00145-019-09341-Z","journal-title":"J. Cryptol."},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Blanchet, B., Cheval, V., Cortier, V.: ProVerif with lemmas, induction, fast subsumption, and much more. In: SP, pp. 69\u201386. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833653","DOI":"10.1109\/SP46214.2022.9833653"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-44647-8_17","volume-title":"Advances in Cryptology \u2014 CRYPTO 2001","author":"D Boneh","year":"2001","unstructured":"Boneh, D.: Simplified OAEP for the RSA and Rabin functions. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 275\u2013291. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44647-8_17"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-030-81685-8_31","volume-title":"Computer Aided Verification","author":"B Boston","year":"2021","unstructured":"Boston, B., et al.: Verified cryptographic code for everybody. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 645\u2013668. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_31"},{"key":"8_CR12","unstructured":"Bottesch, R., Divas\u00f3n, J., Thiemann, R.: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation. Arch. Formal Proofs, March 2021. https:\/\/isa-afp.org\/entries\/Modular_arithmetic_LLL_and_HNF_algorithms.html, Formal proof development"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) LPAR. EPiC Series in Computing, vol.\u00a057, pp. 164\u2013180. EasyChair (2018). https:\/\/doi.org\/10.29007\/XWWH","DOI":"10.29007\/XWWH"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Butler, D.: Formalising cryptography using CryptHOL. Ph.D. thesis, University of Edinburgh, UK (2020). https:\/\/doi.org\/10.7488\/ERA\/510","DOI":"10.7488\/ERA\/510"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Butler, D., Aspinall, D., Gasc\u00f3n, A.: Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. In: Blanchette, J., Hritcu, C. (eds.) CPP, pp. 229\u2013243. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373815","DOI":"10.1145\/3372885.3373815"},{"issue":"4","key":"8_CR16","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/S10817-020-09581-W","volume":"65","author":"D Butler","year":"2021","unstructured":"Butler, D., Lochbihler, A., Aspinall, D., Gasc\u00f3n, A.: Formalising $$\\sum $$-protocols and commitment schemes using CryptHOL. J. Autom. Reason. 65(4), 521\u2013567 (2021). https:\/\/doi.org\/10.1007\/S10817-020-09581-W","journal-title":"J. Autom. Reason."},{"key":"8_CR17","unstructured":"Canan, J.W.: Defending against cyber threats. Aerospace Am. 41, 22\u201327 (2011). https:\/\/www.aiaa.org\/docs\/default-source\/uploadedfiles\/publications\/aerospace-america-october-2011.pdf?sfvrsn=3062b789_2"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-68339-9_14","volume-title":"Advances in Cryptology \u2014 EUROCRYPT \u201996","author":"D Coppersmith","year":"1996","unstructured":"Coppersmith, D.: Finding a small root of a univariate modular equation. In: Maurer, U. (ed.) EUROCRYPT 1996. LNCS, vol. 1070, pp. 155\u2013165. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-68339-9_14"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-94821-8_10","volume-title":"Interactive Theorem Proving","author":"J Divas\u00f3n","year":"2018","unstructured":"Divas\u00f3n, J., Joosten, S., Thiemann, R., Yamada, A.: A formalization of the LLL basis reduction algorithm. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 160\u2013177. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_10"},{"key":"8_CR20","unstructured":"Divas\u00f3n, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified factorization algorithm for integer polynomials with polynomial complexity. Archive of Formal Proofs, February 2018. https:\/\/isa-afp.org\/entries\/LLL_Factorization.html, Formal proof development"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: SP, pp. 1202\u20131219. IEEE (2019). https:\/\/doi.org\/10.1109\/SP.2019.00005","DOI":"10.1109\/SP.2019.00005"},{"key":"8_CR22","unstructured":"Galbraith, S.D.: Mathematics of Public Key Cryptography. Cambridge University Press, Cambridge (2012). https:\/\/www.math.auckland.ac.nz\/%7Esgal018\/crypto-book\/crypto-book.html"},{"key":"8_CR23","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch. p.\u00a0181 (2005)"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Haselwarter, P.G., et al.: SSProve: a foundational framework for modular cryptographic proofs in Coq. ACM Trans. Program. Lang. Syst. 45(3), 15:1\u201315:61 (2023). https:\/\/doi.org\/10.1145\/3594735","DOI":"10.1145\/3594735"},{"key":"8_CR25","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: ACM SIGSAM PLMMS, pp. 38\u201345 (2009)"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Howgrave-Graham, N.: Finding small roots of univariate modular equations revisited. In: Darnell, M. (ed.) Cryptography and Coding, 6th IMA International Conference, Cirencester, UK, December 17-19, 1997, Proceedings. Lecture Notes in Computer Science, vol.\u00a01355, pp. 131\u2013142. Springer, Cham (1997). https:\/\/doi.org\/10.1007\/BFB0024458","DOI":"10.1007\/BFB0024458"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Huch, F., Krauss, A.: Findfacts: a scalable theorem search. CoRR abs\/2204.14191 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2204.14191","DOI":"10.48550\/ARXIV.2204.14191"},{"key":"8_CR28","unstructured":"Kamm\u00fcller, F.: Higher order model checking in isabelle for human centric infrastructure security (2023). https:\/\/arxiv.org\/abs\/2312.17555"},{"issue":"4","key":"8_CR29","doi-asserted-by":"publisher","first-page":"517","DOI":"10.3934\/amc.2019034","volume":"13","author":"N Koblitz","year":"2019","unstructured":"Koblitz, N., Menezes, A.: Critical perspectives on provable security: fifteen years of \u201canother look\u2019\u2019 papers. Adv. Math. Commun. 13(4), 517\u2013558 (2019). https:\/\/doi.org\/10.3934\/amc.2019034","journal-title":"Adv. Math. Commun."},{"key":"8_CR30","unstructured":"Kosaian, K., Tan, Y.K.: Formalizing coppersmith\u2019s method. Archive of Formal Proofs, June 2024. https:\/\/www.isa-afp.org\/entries\/Coppersmith_Method.html, Formal proof development"},{"key":"8_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1365\/s13291-020-00221-1","volume":"123","author":"A Koutsoukou-Argyraki","year":"2021","unstructured":"Koutsoukou-Argyraki, A.: Formalising mathematics-in praxis; a mathematician\u2019s first experiences with Isabelle\/HOL and the why and how of getting started. Jahresber. Deutsch. Math.-Verein. 123, 3\u201326 (2021). https:\/\/doi.org\/10.1365\/s13291-020-00221-1","journal-title":"Jahresber. Deutsch. Math.-Verein."},{"key":"8_CR32","unstructured":"Kreuzer, K.: Verification of correctness and security properties for CRYSTALS-KYBER. IACR Cryptol. ePrint Arch. p.\u00a087 (2023). https:\/\/eprint.iacr.org\/2023\/087"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Kreuzer, K., Nipkow, T.: Verification of NP-hardness reduction functions for exact lattice problems. In: Pientka, B., Tinelli, C. (eds.) CADE, LNCS, vol. 14132, pp. 365\u2013381. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_21","DOI":"10.1007\/978-3-031-38499-8_21"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Lenstra, A., Lenstra, H., L\u00e1szl\u00f3, L.: Factoring polynomials with rational coefficients. Mathematische Annalen 261 (1982). https:\/\/doi.org\/10.1007\/BF01457454","DOI":"10.1007\/BF01457454"},{"key":"8_CR35","unstructured":"Lindenberg, C., Wirt, K., Buchmann, J.: Formal proof for the correctness of RSA-PSS. IACR Cryptol. ePrint Arch. p.\u00a011 (2006). http:\/\/eprint.iacr.org\/2006\/011"},{"key":"8_CR36","unstructured":"Lochbihler, A., Sefidgar, S.R.: A tutorial introduction to CryptHOL. IACR Cryptol. ePrint Arch. p.\u00a0941 (2018). https:\/\/eprint.iacr.org\/2018\/941"},{"key":"8_CR37","unstructured":"Martin-Dorel, \u00c9.: Contributions to the formal verification of arithmetic algorithms. (Contributions \u00e0 la v\u00e9rification formelle d\u2019algorithmes arithm\u00e9tiques). Ph.D. thesis, \u00c9cole normale sup\u00e9rieure de Lyon, France (2012). https:\/\/tel.archives-ouvertes.fr\/tel-00745553"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Hanrot, G., Mayero, M., Th\u00e9ry, L.: Formally verified certificate checkers for hardest-to-round computation. J. Autom. Reason. 54(1), 1\u201329 (2015). https:\/\/doi.org\/10.1007\/S10817-014-9312-2","DOI":"10.1007\/S10817-014-9312-2"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Nemec, M., S\u00fds, M., Svenda, P., Klinec, D., Matyas, V.: The return of Coppersmith\u2019s attack: practical factorization of widely used RSA moduli. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) ACM CCS, pp. 1631\u20131648. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3133969","DOI":"10.1145\/3133956.3133969"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Nguyen, P.Q., Vall\u00e9e, B. (eds.): The LLL Algorithm - Survey and Applications. Information Security and Cryptography, Springer, Cham (2010). https:\/\/doi.org\/10.1007\/978-3-642-02295-1","DOI":"10.1007\/978-3-642-02295-1"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Klein, G.: Isar: a language for structured proofs, pp. 3\u201369. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0_5","DOI":"10.1007\/978-3-319-10542-0_5"},{"key":"8_CR42","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"},{"issue":"3","key":"8_CR43","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363\u2013397 (1989). https:\/\/doi.org\/10.1007\/BF00248324","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"8_CR44","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1\u20132), 85\u2013128 (1998). https:\/\/doi.org\/10.3233\/JCS-1998-61-205","journal-title":"J. Comput. Secur."},{"key":"8_CR45","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL. EPiC Series in Computing, vol.\u00a02, pp. 1\u201311. EasyChair (2010). https:\/\/doi.org\/10.29007\/36DT","DOI":"10.29007\/36DT"},{"key":"8_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-662-46666-7_4","volume-title":"Principles of Security and Trust","author":"A Petcher","year":"2015","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53\u201372. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46666-7_4"},{"key":"8_CR47","doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: EverCrypt: a fast, verified, cross-platform cryptographic provider. In: SP, pp. 983\u20131002. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00114","DOI":"10.1109\/SP40000.2020.00114"},{"issue":"2","key":"8_CR48","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"RL Rivest","year":"1978","unstructured":"Rivest, R.L., Shamir, A., Adleman, L.M.: A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM 21(2), 120\u2013126 (1978). https:\/\/doi.org\/10.1145\/359340.359342","journal-title":"Commun. ACM"},{"key":"8_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"KY Rozier","year":"2016","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2"},{"key":"8_CR50","unstructured":"Stathopoulos, Y., Koutsoukou-Argyraki, A., Paulson, L.C.: SErAPIS: a concept-oriented search engine for the isabelle libraries based on natural language. In: Online proceedings of the Isabelle Workshop affiliated to IJCAR 2020 (virtual) (2020). https:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Alexandria\/Serapis.pdf"},{"issue":"5","key":"8_CR51","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/S10817-020-09552-1","volume":"64","author":"R Thiemann","year":"2020","unstructured":"Thiemann, R., Bottesch, R., Divas\u00f3n, J., Haslbeck, M.W., Joosten, S.J.C., Yamada, A.: Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle\/HOL. J. Autom. Reason. 64(5), 827\u2013856 (2020). https:\/\/doi.org\/10.1007\/S10817-020-09552-1","journal-title":"J. Autom. Reason."},{"key":"8_CR52","volume-title":"Introduction to Cryptography with Coding Theory","author":"W Trappe","year":"2005","unstructured":"Trappe, W., Washington, L.C.: Introduction to Cryptography with Coding Theory, 2nd edn. Prentice-Hall Inc, USA (2005)","edition":"2"},{"key":"8_CR53","doi-asserted-by":"publisher","unstructured":"Unruh, D.: Quantum relational hoare logic. Proc. ACM Program. Lang. 3(POPL), 33:1\u201333:31 (2019). https:\/\/doi.org\/10.1145\/3290346","DOI":"10.1145\/3290346"},{"issue":"2","key":"8_CR54","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0022-314X(01)92763-5","volume":"95","author":"M Van Hoeij","year":"2002","unstructured":"Van Hoeij, M.: Factoring polynomials and the knapsack problem. J. Number Theory 95(2), 167\u2013189 (2002)","journal-title":"J. Number Theory"},{"key":"8_CR55","unstructured":"Werner, D.: Hackers as allies. Aerospace America, pp. 24\u201330, June 2020. https:\/\/aerospaceamerica.aiaa.org\/features\/hackers-as-allies\/"},{"key":"8_CR56","unstructured":"Whitley, A.: Cryptographic standards. Archive of Formal Proofs, June 2023. https:\/\/isa-afp.org\/entries\/Crypto_Standards.html, Formal proof development"},{"issue":"3","key":"8_CR57","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/MSP.2010.938758","volume":"28","author":"D W\u00fcbben","year":"2011","unstructured":"W\u00fcbben, D., Seethaler, D., Jald\u00e9n, J., Matz, G.: Lattice reduction. IEEE Sig.Process. Mag. 28(3), 70\u201391 (2011). https:\/\/doi.org\/10.1109\/MSP.2010.938758","journal-title":"IEEE Sig.Process. Mag."},{"key":"8_CR58","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) CCS, pp. 1789\u20131806. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66997-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:35Z","timestamp":1748412335000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}