Paper 2025/1122 Original: eprint.iacr.org/2025/1122 ↗
Mechanizing Nested Hybrid Arguments
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.
Metadata
- Available format(s)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2026-02-19: last updated
- 2025-06-14: published
- Short URL
- https://ia.cr/2025/1122
- License
- https://creativecommons.org/licenses/by-sa/4.0/
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}
}