Paper 2026/1086

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

Abstract

Hybrid signatures are a practical approach to post-quantum migration, but their security analysis becomes subtle when two Fiat-Shamir (FS) components are binded through a single shared challenge. This paper presents the first machine-checked proof of EUF-CMA security for the FS-FS hybrid construction of Bindel and Hale (2023) formalised in EasyCrypt in the Random Oracle Model (ROM). The proof is parametrised over abstract component interfaces and establishes the intended either-component security guarantee: for either choice of component, a hybrid forgery can be reduced to an EUF-CMA forgery against that component, together with the collision resistance of the message digest and a random-oracle guessing term. In this ROM formulation, the proof does not require an independent second-preimage-resistance assumption for the challenge hash. The mechanisation makes explicit two proof obligations arising from the hybrid structure and the abstract digest: an invariant linking the lazy-oracle state to an explicit query log at the verification point, and a module-restriction framing argument for the digest-collision reduction. We further machine-check honest-signing correctness for a concrete Schnorr-Schnorr instantiation and instantiate the abstract security proof with a Schnorr-Okamoto component pair without changing the core game-hopping argument. The formalisation thereby makes explicit the assumptions, invariants, and composition structure underlying the security argument for the FS-FS hybrid.