Document Open Access Logo

Formalizing the Hidden Number Problem in Isabelle/HOL

Authors Sage Binder , Eric Ren , Katherine Kosaian

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.23.pdf
  • Filesize: 0.99 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.23.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • hidden number problem
  • Babai’s nearest plane algorithm
  • cryptography
  • interactive theorem proving
  • Isabelle/HOL

Metrics

Abstract

We formalize the hidden number problem (HNP), as introduced in a seminal work by Boneh and Venkatesan in 1996, in Isabelle/HOL. Intuitively, the HNP involves demonstrating the existence of an algorithm (the "adversary") which can compute (with high probability) a hidden number α given access to a bit-leaking oracle. Originally developed to establish the security of Diffie-Hellman key exchange, the HNP has since been used not only for protocol security but also in cryptographic attacks, including notable ones on DSA and ECDSA. Further, as the HNP establishes an expressive paradigm for reasoning about security in the context of information leakage, many HNP variants for other specialized cryptographic applications have since been developed. A main contribution of our work is explicating and clarifying the HNP proof blueprint from the original source material; naturally, formalization forces us to make all assumptions and proof steps precise and transparent. For example, the source material did not explicitly define the adversary and only abstractly defined what information is being leaked; our formalization concretizes both definitions. Additionally, the HNP makes use of an instance of Babai’s nearest plane algorithm, which solves the approximate closest vector problem; we formalize this as a result of independent interest. Our formalizations of Babai’s algorithm and the HNP adversary are executable, setting up potential future work, e.g. in developing formally verified instances of cryptographic attacks.

Cite As Get BibTex

Sage Binder, Eric Ren, and Katherine Kosaian. Formalizing the Hidden Number Problem in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.23

Author Details

Sage Binder
  • University of Iowa, Iowa City, IA, USA
Eric Ren
  • Independent, Atlanta, GA, USA
Katherine Kosaian
  • University of Iowa, Iowa City, IA, USA

Acknowledgements

Thank you to Yong Kiam Tan for useful comments on the paper, and thank you to the anonymous ITP reviewers for their valuable feedback.

References

  1. László Babai. On Lovász' lattice reduction and the nearest lattice point problem. Comb., 6(1):1-13, 1986. URL: https://doi.org/10.1007/BF02579403.
  2. Clemens Ballarin. Locales: A module system for mathematical theories. J. Autom. Reason., 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  3. Cécile Baritel-Ruet. Formal Security Proofs of Cryptographic Standards : A necessity achieved using EasyCrypt. Theses, Université Côte d'Azur, October 2020. URL: https://theses.hal.science/tel-03150443.
  4. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. SIGPLAN Not., 44(1):90-101, January 2009. URL: https://doi.org/10.1145/1594834.1480894.
  5. David Basin, Andreas Lochbihler, Ueli Maurer, and S Reza Sefidgar. Abstract modeling of system communication in constructive cryptography using CryptHOL. In 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pages 1-16. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00047.
  6. David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. CryptHOL: Game-based proofs in higher-order logic. J. Cryptol., 33(2):494-566, 2020. URL: https://doi.org/10.1007/S00145-019-09341-Z.
  7. Daniel J. Bernstein and Tung Chou. CryptAttackTester: high-assurance attack analysis. In Leonid Reyzin and Douglas Stebila, editors, CRYPTO, volume 14925 of LNCS, pages 141-182. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-68391-6_5.
  8. Sage Binder, Eric Ren, and Katherine Kosaian. The hidden number problem. Archive of Formal Proofs, June 2025. , Formal proof development. URL: https://isa-afp.org/entries/Hidden_Number_Problem.html.
  9. Dan Boneh, Shai Halevi, and Nick Howgrave-Graham. The modular inversion hidden number problem. In Colin Boyd, editor, ASIACRYPT, volume 2248 of LNCS, pages 36-51. Springer, 2001. URL: https://doi.org/10.1007/3-540-45682-1_3.
  10. Dan Boneh and Igor E. Shparlinski. On the unpredictability of bits of the elliptic curve Diffie-Hellman scheme. In Joe Kilian, editor, CRYPTO, volume 2139 of LNCS, pages 201-212. Springer, 2001. URL: https://doi.org/10.1007/3-540-44647-8_12.
  11. Dan Boneh and Ramarathnam Venkatesan. Hardness of computing the most significant bits of secret keys in Diffie-Hellman and related schemes. In Neal Koblitz, editor, CRYPTO, volume 1109 of LNCS, pages 129-142. Springer, 1996. URL: https://doi.org/10.1007/3-540-68697-5_11.
  12. Ralph Bottesch, Max W. Haslbeck, and René Thiemann. A verified efficient implementation of the LLL basis reduction algorithm. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR, volume 57 of EPiC Series in Computing, pages 164-180. EasyChair, 2018. URL: https://doi.org/10.29007/XWWH.
  13. Joachim Breitner and Nadia Heninger. Biased nonce sense: Lattice attacks against weak ECDSA signatures in cryptocurrencies. In Ian Goldberg and Tyler Moore, editors, FC, volume 11598 of LNCS, pages 3-20. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32101-7_1.
  14. David Butler. Formalising cryptography using CryptHOL. PhD thesis, University of Edinburgh, UK, 2020. URL: https://doi.org/10.7488/ERA/510.
  15. David Butler, David Aspinall, and Adrià Gascón. Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. In Jasmin Blanchette and Catalin Hritcu, editors, CPP, pages 229-243. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373815.
  16. David Butler and Andreas Lochbihler. Sigma protocols and commitment schemes. Archive of Formal Proofs, October 2019. , Formal proof development. URL: https://isa-afp.org/entries/Sigma_Commit_Crypto.html.
  17. David Butler, Andreas Lochbihler, David Aspinall, and Adrià Gascón. Formalising ∑-protocols and commitment schemes using CryptHOL. J. Autom. Reason., 65(4):521-567, 2021. URL: https://doi.org/10.1007/S10817-020-09581-W.
  18. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, and Akihisa Yamada. A Verified Factorization Algorithm for Integer Polynomials with Polynomial Complexity. Archive of Formal Proofs, February 2018. , Formal proof development. URL: https://isa-afp.org/entries/LLL_Factorization.html.
  19. Shuqin Fan, Wenbo Wang, and Qingfeng Cheng. Attacking OpenSSL implementation of ECDSA with a few signatures. In Edgar R. Weippl, Stefan Katzenbeisser, Christopher Kruegel, Andrew C. Myers, and Shai Halevi, editors, SIGSAC, pages 1505-1515. ACM, 2016. URL: https://doi.org/10.1145/2976749.2978400.
  20. Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak. Formal proof of polynomial-time complexity with quasi-interpretations. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 146-157, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167097.
  21. Nadia Heninger and Keegan Ryan. The hidden number problem with small unknown multipliers: Cryptanalyzing MEGA in six queries and other applications. In Alexandra Boldyreva and Vladimir Kolesnikov, editors, PKC, volume 13940 of LNCS, pages 147-176. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-31368-4_6.
  22. Martin Hlavác and Tomás Rosa. Extended hidden number problem and its cryptanalytic applications. In Eli Biham and Amr M. Youssef, editors, SAC, volume 4356 of LNCS, pages 114-133. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74462-7_9.
  23. Katharina Kreuzer. CRYSTALS-Kyber_Security. Archive of Formal Proofs, December 2023. , Formal proof development. URL: https://isa-afp.org/entries/CRYSTALS-Kyber_Security.html.
  24. Katharina Kreuzer. Hardness of Lattice Problems. Archive of Formal Proofs, february 2023. , Formal proof development. URL: https://isa-afp.org/entries/CVP_Hardness.html.
  25. Katharina Kreuzer. Verification of correctness and security properties for CRYSTALS-KYBER. IACR Cryptol. ePrint Arch., page 87, 2023. URL: https://eprint.iacr.org/2023/087.
  26. Katharina Kreuzer and Tobias Nipkow. Verification of NP-hardness reduction functions for exact lattice problems. In Brigitte Pientka and Cesare Tinelli, editors, CADE, volume 14132 of LNCS, pages 365-381. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_21.
  27. Kim Laine and Kristin E. Lauter. Key recovery for LWE in polynomial time. IACR Cryptol. ePrint Arch., page 176, 2015. URL: http://eprint.iacr.org/2015/176.
  28. Arjen Lenstra, Hendrik Lenstra, and Lovász László. Factoring polynomials with rational coefficients. Mathematische Annalen, 261, December 1982. URL: https://doi.org/10.1007/BF01457454.
  29. Andreas Lochbihler and S. Reza Sefidgar. Constructive cryptography in HOL. Archive of Formal Proofs, December 2018. , Formal proof development. URL: https://isa-afp.org/entries/Constructive_Cryptography.html.
  30. Andreas Lochbihler and S. Reza Sefidgar. A tutorial introduction to CryptHOL. IACR Cryptol. ePrint Arch., page 941, 2018. URL: https://eprint.iacr.org/2018/941.
  31. Ueli Maurer. Constructive cryptography-a new paradigm for security definitions and proofs. In Joint Workshop on Theory of Security and Applications, pages 33-56. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-27375-9_3.
  32. Ueli Maurer and Renato Renner. From indifferentiability to constructive cryptography (and back). In Theory of Cryptography: 14th International Conference, TCC 2016-B, Beijing, China, October 31-November 3, 2016, Proceedings, Part I 14, pages 3-24. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-53641-4_1.
  33. Robert Merget, Marcus Brinkmann, Nimrod Aviram, Juraj Somorovsky, Johannes Mittmann, and Jörg Schwenk. Raccoon attack: Finding and exploiting most-significant-bit-oracles in TLS-DH(E). In Michael D. Bailey and Rachel Greenstadt, editors, USENIX, pages 213-230. USENIX Association, 2021. URL: https://www.usenix.org/conference/usenixsecurity21/presentation/merget.
  34. Gabrielle De Micheli, Rémi Piau, and Cécile Pierrot. A tale of three signatures: Practical attack of ECDSA with wNAF. In Abderrahmane Nitaj and Amr M. Youssef, editors, AFRICACRYPT, volume 12174 of LNCS, pages 361-381. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51938-4_18.
  35. Elke De Mulder, Michael Hutter, Mark E. Marson, and Peter Pearson. Using Bleichenbacher’s solution to the hidden number problem to attack nonce leaks in 384-bit ECDSA: extended version. J. Cryptogr. Eng., 4(1):33-45, 2014. URL: https://doi.org/10.1007/S13389-014-0072-Z.
  36. Phong Q Nguyen. The dark side of the hidden number problem: Lattice attacks on DSA. In Cryptography and Computational Number Theory, pages 321-330. Springer, 2001. Google Scholar
  37. Phong Q. Nguyen and Igor E. Shparlinski. The insecurity of the Digital Signature Algorithm with partially known nonces. J. Cryptol., 15(3):151-176, 2002. URL: https://doi.org/10.1007/S00145-002-0021-3.
  38. Phong Q. Nguyen and Igor E. Shparlinski. The insecurity of the Elliptic Curve Digital Signature Algorithm with partially known nonces. Des. Codes Cryptogr., 30(2):201-217, 2003. URL: https://doi.org/10.1023/A:1025436905711.
  39. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  40. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, IWIL, volume 2 of EPiC Series in Computing, pages 1-11. EasyChair, 2010. URL: https://doi.org/10.29007/36DT.
  41. Keegan Ryan. Return of the hidden number problem. A widespread and novel key extraction attack on ECDSA and DSA. IACR Trans. Cryptogr. Hardw. Embed. Syst., 2019(1):146-168, 2019. URL: https://doi.org/10.13154/TCHES.V2019.I1.146-168.
  42. Noah Stephens-Davidowitz. Lecture 5: CVP and Babai’s Algorithm, august 2016. New York University, Lattices Mini Course. URL: https://www.noahsd.com/mini_lattices/05__babai.pdf.
  43. René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, and Akihisa Yamada. Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL. J. Autom. Reason., 64(5):827-856, 2020. URL: https://doi.org/10.1007/S10817-020-09552-1.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact