Search Results

Documents authored by Binder, Sage

Artifact
Software
DOI: 10.4230/artifacts.27121
Apply2Isar

Authors: Sage Binder, Hanna Lachnitt, and Katherine Kosaian

Abstract
Cite as

Sage Binder, Hanna Lachnitt, Katherine Kosaian. Apply2Isar (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27121,
   title = {{Apply2Isar}}, 
   author = {Binder, Sage and Lachnitt, Hanna and Kosaian, Katherine},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:8753f0c693cdc7159375110e6dd9d977e62984a8;origin=https://github.com/sagebinder/apply2isar;visit=swh:1:snp:d413b506ca05f076c64c1ed2cf58f8c55da2f875;anchor=swh:1:rev:ecca6ce39f971746f0f3e35caf20e818819079d0}{\texttt{swh:1:dir:8753f0c693cdc7159375110e6dd9d977e62984a8}} (visited on 2026-07-16)},
   url = {https://github.com/sagebinder/apply2isar},
   doi = {10.4230/artifacts.27121},
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.18
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

Authors: Sage Binder, Hanna Lachnitt, and Katherine Kosaian

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proofs since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style proofs to declarative Isar. This allows users to write complex, possibly fragile apply-style proofs, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.
Cite as

Sage Binder, Hanna Lachnitt, and Katherine Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{binder_et_al:LIPIcs.ITP.2026.18,
  author =	{Binder, Sage and Lachnitt, Hanna and Kosaian, Katherine},
  title =	{{Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.18},
  URN =		{urn:nbn:de:0030-drops-269925},
  doi =		{10.4230/LIPIcs.ITP.2026.18},
  annote =	{Keywords: Proof Assistants, Isabelle/HOL, Isabelle/ML, Isabelle/Isar, Proof Refactoring}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.23
Formalizing the Hidden Number Problem in Isabelle/HOL

Authors: Sage Binder, Eric Ren, and Katherine Kosaian

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{binder_et_al:LIPIcs.ITP.2025.23,
  author =	{Binder, Sage and Ren, Eric and Kosaian, Katherine},
  title =	{{Formalizing the Hidden Number Problem in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.23},
  URN =		{urn:nbn:de:0030-drops-246216},
  doi =		{10.4230/LIPIcs.ITP.2025.23},
  annote =	{Keywords: hidden number problem, Babai’s nearest plane algorithm, cryptography, interactive theorem proving, Isabelle/HOL}
}
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact