The FS-FS hybrid signature scheme of Bindel and Hale [12] couples two independent Fiat-Shamir components through a single shared challenge c = H(w1, w2, D(m)), achieving one of the strongest known proof composability and simultaneous verification properties among hybrid designs, but its EUF-CMA security was stated without proof. We present the first machine-checked EUF-CMA security proof of the FS-FS hybrid, formalised in EasyCrypt in the Random Oracle Model and parametrised over abstract sigma-protocol interfaces; the bound applies to any heterogeneous FS-based pair, classical or post-quantum. We prove two symmetric security bounds, one reducing to each component independently, so that security holds whenever either component is EUF-CMA secure; the FS-FS-Schnorr corollary confirms the result is non-vacuous. We further show that the second-preimage-resistance assumption of [12] is subsumed by the ROM guessing term 1/|R|, reducing the effective assumptions from three to two: EUF-CMA of either component under the shared hybrid-hash challenge, and collision resistance of the digest. The mechanisation uncovers two proof obligations invisible at the theorem level—a logging invariant over the shared lazy oracle and a module-restriction framing argument for the abstract digest—which we isolate as reusable EasyCrypt proof patterns.
Note:
BibTeX
@misc{cryptoeprint:2026/1086,
author = {Sara Zain},
title = {A Machine-Checked {EUF}-{CMA} Proof for the Hybrid Fiat-Shamir Signature Scheme},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1086},
year = {2026},
url = {https://eprint.iacr.org/2026/1086}
}
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。