Paper 2026/1086

A Machine-Checked EUF-CMA Proof for the Hybrid Fiat-Shamir Signature Scheme

Abstract

As cryptographic systems transition to post-quantum algorithms, hybrid signature schemes–combining a classical and post-quantum component so that security holds as long as either remains unbroken–are central to migration strategies mandated by NIST and IETF. The FS-FS construction proposed by Bindel and Hale (2023) is among the strongest known true hybrid signature designs. They combine two independent Fiat-Shamir components through a single shared challenge to achieve proof composability and simultaneous verification without the signature-stripping weaknesses of concatenation-based hybrids. Its EUF-CMA security, however, was stated as a theorem with only a brief informal sketch, with a complete proof in any model, informal or formal, left to future work. We close this gap with 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, so that the bound applies uniformly to any heterogeneous pair of Fiat-Shamir-based components. We prove two symmetric security bounds, one reducing to each component independently, so that security holds whenever either component is EUF-CMA secure; the corollary confirms the result is non-vacuous. We also construct reusable proof-patterns so that one can reason about the similarly structured reductions. As a check that the abstract bound is not an artefact of the Schnorr case, we further instantiate the second component with an Okamoto sigma-protocol, whose secret key and response are pairs of exponents rather than single scalars, and confirm that our main theorem applies to this pair without modification.