BLS EUF-CMA Security via the co-CDH Reduction (ROM) #
Existential unforgeability of BLS signatures, reduced to the computational
co-Diffie-Hellman assumption in the bilinear group, with the hash-to-curve
function H modelled as a random oracle to G₁.
The reduction #
The forgery-extraction lemma forgery_is_cocdh_solution: a signature that passes
the pairing check on a message whose random-oracle hash is the co-CDH challenge
g₁ ^ᵍ a, under a public key pk = g₂ ^ʰ b, is exactly the co-CDH answer
g₁ ^ᵍ (a·b) — the element CoCDH_Game (Assumptions/CoCDH.lean) asks an
adversary to produce. It is proved from the pairing: bilinearity (e_zpowZMod_id)
plus non-degeneracy/injectivity of e(·, g₂) (e_inj_left, derived from
PairingGroup.e_first_arg_eq_one). No pairing axiom is added.
The reduction blsReduction turns a BLS forger into a co-CDH solver. It receives
the matched-exponent co-CDH instance (g₁ ^ᵍ x, g₂ ^ʰ x, u), runs the forger on
pk = g₂ ^ʰ x and challenge hash u, and answers the forger's chosen-message
signing queries with (g₁ ^ᵍ x) ^ᵍ r = (g₁ ^ᵍ r) ^ᵍ x (zpowZMod₁_zpowZMod₁ +
mul_comm), i.e. the BLS signature on the message whose oracle hash is g₁ ^ᵍ r.
The simulated signing oracle is identical to the real one, so the co-CDH game with
blsReduction F equals the BLS forgery game (blsForgeGame_eq_cocdh), giving the
bound blsForgeAdvantage F ≤ ε whenever co-CDH is ε-hard
(bls_forge_reduces_to_cocdh).
This is a Type-III BLS reduction: the secret exponent x is available in both
source groups (g₁ ^ᵍ x, g₂ ^ʰ x), which is what lets the reduction sign. This
matched-exponent form is the hardness assumption for the minimal-signature BLS
scheme (BLSCoCDHSecure).
Modelling boundaries #
His a random oracle toG₁(the BLS ROM assumption): the challenge hashuis uniform inG₁and the signing oracle is keyed on the hash discrete logr.- The reduction is for a single random-oracle challenge message (selective ROM);
the multi-query adaptive variant adds the usual
q_Hguessing factor. BLSCoCDHSecureis the matched-exponent (Type-III) co-CDH assumption.
References #
- Boneh, Lynn, Shacham. Short Signatures from the Weil Pairing. J. Cryptology, 2004, §3 (security from co-CDH in the ROM).
Pairing injectivity and the BLS identity #
Injectivity of e(·, g₂): pairing with the second generator is injective
on G₁. Follows from non-degeneracy (e_first_arg_eq_one).
The BLS identity over P: e(u ^ᵍ x, g₂) = e(u, g₂ ^ʰ x).
Forgery extraction (the heart of unforgeability) #
A signature passing the BLS pairing check e(σ, g₂) = e(u, g₂ ^ʰ x) is
forced to be u ^ᵍ x.
The pairing check is equivalent to being the co-CDH-style answer.
Forgery is a co-CDH solution. A BLS signature σ verifying on a message
whose hash is the co-CDH challenge g₁ ^ᵍ a, under pk = g₂ ^ʰ b, equals
g₁ ^ᵍ (a·b) — the target of Assumptions.CoCDH_Game.
Matched-exponent co-CDH (the Type-III BLS assumption) #
co-CDH solver for the matched-exponent (Type-III) instance: given
(g₁ ^ᵍ x, g₂ ^ʰ x, u), output u ^ᵍ x. The pairing makes the answer
verifiable (e(u^x, g₂) = e(u, g₂^x)) but not computable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matched-exponent co-CDH game: sample x ← Zₚ and u ← G₁, hand the
adversary (g₁ ^ᵍ x, g₂ ^ʰ x, u), win iff it returns u ^ᵍ x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matched-exponent co-CDH advantage.
Equations
Instances For
Matched-exponent co-CDH hardness assumption.
Equations
Instances For
The BLS forgery game and the reduction #
A BLS forger in the random-oracle model.
Given the public key pk, the random-oracle hash u = H(m*) of the
challenge message, and a chosen-message signing oracle keyed on the hash
discrete log r (returning the BLS signature on the message whose oracle
hash is g₁ ^ᵍ r), the forger outputs a candidate forgery σ ∈ G₁ on the
challenge message.
- run : CatCrypt.Crypto.PairingGroup.G₂ → CatCrypt.Crypto.PairingGroup.G₁ → (ZMod CatCrypt.Crypto.PairingGroup.p → CatCrypt.Core.SPComp CatCrypt.Crypto.PairingGroup.G₁) → CatCrypt.Core.SPComp CatCrypt.Crypto.PairingGroup.G₁
run pk u signOracleproduces a candidate forgery on the challenge message hashing tou.
Instances For
BLS forgery game (ROM, single challenge message). Sample the key x and the
challenge hash u; the forger gets pk = g₂ ^ʰ x, the hash u, and the
real signing oracle r ↦ (g₁ ^ᵍ r) ^ᵍ x; it wins iff its output passes the
BLS pairing check e(σ, g₂) = e(u, pk).
Equations
- One or more equations did not get rendered due to their size.
Instances For
BLS forgery advantage.
Equations
Instances For
BLS existential unforgeability in the ROM: all forgers bounded by ε.
Equations
Instances For
The reduction: a BLS forger becomes a matched-exponent co-CDH solver.
On instance (gx = g₁ ^ᵍ x, hx = g₂ ^ʰ x, u) it sets pk = hx, hands the
forger the challenge hash u, and answers signing queries with
gx ^ᵍ r = (g₁ ^ᵍ x) ^ᵍ r, returning the forger's output as the candidate
u ^ᵍ x.
Equations
- CatCryptCore.Crypto.BLSSig.blsReduction P F gx hx u = F.run hx u fun (r : ZMod CatCrypt.Crypto.PairingGroup.p) => CatCrypt.Core.SPComp.pure (CatCrypt.Crypto.PairingGroup.zpowZMod₁ gx r)
Instances For
The reduction simulates the BLS forgery game exactly: the co-CDH game on
blsReduction F is, as a probabilistic program, the BLS forgery game.
The signing oracle matches because (g₁ ^ᵍ x) ^ᵍ r = (g₁ ^ᵍ r) ^ᵍ x
(zpowZMod₁_zpowZMod₁, mul_comm); the win condition matches because the
pairing check is equivalent to σ = u ^ᵍ x (verify_iff_isAnswer).
Advantage transfer: the BLS forgery advantage equals the co-CDH advantage of the reduction.
BLS EUF reduces to co-CDH: if matched-exponent co-CDH is ε-hard, every
BLS forger has advantage at most ε. The conclusion bounds forgery using the
co-CDH hypothesis.
BLS is EUF-secure in the ROM under co-CDH. If matched-exponent (Type-III)
co-CDH on P is ε-hard, every BLS forger has advantage at most ε.