Mechanizing Nested Hybrid Arguments

Markus Krabbe Larsen; Carsten Schürmann

Paper 2025/1122

Mechanizing Nested Hybrid Arguments

Markus Krabbe Larsen

, IT University of Copenhagen

Carsten Schürmann

, IT University of Copenhagen

Abstract

Hybrid arguments are prevalent in cryptographic security proofs, however, existing mechanizations in proof assistants are not as general as they could be. In this paper, we prove a general theorem about the admissibility of hybrid arguments that encompasses the query-counting, multi-instance, and nested case. We present three case studies about public-key encryption, which demonstrate the generality of the theorem. The results of this paper are achieved in the setting of state-separating proofs and the theory is integrated into and the case studies are mechanized in Nominal-SSProve.

Note: The formalization described in the paper is available at: https://github.com/MarkusKL/ssprove/tree/for-submission-jan26 Nominal-SSProve is available at: https://github.com/MarkusKL/nominal-ssprove

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Preprint.
Keywords: formal verification Rocq state-separating proofs hybrid arguments public-key cryptography
Contact author(s): krml @ itu dk
carsten @ itu dk
History: 2026-02-19: revised; 2025-06-14: received; See all versions
Short URL: https://ia.cr/2025/1122
License: CC BY-SA

BibTeX

@misc{cryptoeprint:2025/1122,
      author = {Markus Krabbe Larsen and Carsten Schürmann},
      title = {Mechanizing Nested Hybrid Arguments},
      howpublished = {Cryptology {ePrint} Archive, Paper 2025/1122},
      year = {2025},
      url = {https://eprint.iacr.org/2025/1122}
}