2026-08-19T02:46:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24621 2025-12-12T15:10:03Z ddc:004 open_access

Formalizing the Hidden Number Problem in Isabelle/HOL Binder, Sage Ren, Eric Kosaian, Katherine hidden number problem Babai’s nearest plane algorithm cryptography interactive theorem proving Isabelle/HOL 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sage Binder and Eric Ren and Katherine Kosaian 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.23 urn:nbn:de:0030-drops-246216 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.23 eng https://creativecommons.org/licenses/by/4.0/legalcode