Multi-Target Hash Assumptions (SM-PRE, SM-TCR)

The single-function multi-target preimage (SM-PRE) and target-collision (SM-TCR) resistance notions that hash-based signatures such as SLH-DSA / SPHINCS+ reduce to. Unlike plain one-wayness (HardnessAssumptions.OneWay) or collision resistance (HardnessAssumptions.CollisionResistance), the SPHINCS+ analysis crucially uses single-function multi-target hardness: the adversary is given p targets and wins by breaking any one of them. The p-fold loss relative to the single-target notions is intended to be recorded by separate bridge lemmas (future work), not baked into the advantage here.

The packaging mirrors LatticeCrypto.HardnessAssumptions.ShortIntegerSolution (the Problem/Adversary/experiment/advantage shape). The assumptions are stated over plain functions so that a (seed-fixed) TweakableHash can be plugged in.

References

• Bernstein et al., SPHINCS+ (the multi-target preimage / target-collision treatment)
• Hülsing, Rijneveld, Song, Schwabe, "Mitigating Multi-Target Attacks in Hash-Based Signatures"

Single-function multi-target preimage resistance (SM-PRE)

structure MultiTarget.PreimageProblem (X Y : Type) : Type

An SM-PRE problem for a fixed function f : X → Y: the challenger samples numTargets preimages (via sampleInputs) and exposes their images; the adversary must invert one.

• f : X → Y

  The fixed function whose preimage resistance is in question.

• numTargets : ℕ

  The number of targets the adversary is challenged on.

• sampleInputs : ProbComp (Fin self.numTargets → X)

  Sample all numTargets preimages at once.

structure MultiTarget.PreimageAdversary {X Y : Type} (prob : PreimageProblem X Y) : Type

An SM-PRE adversary: given the numTargets images, return an index and a preimage.

• run : (Fin prob.numTargets → Y) → ProbComp (Fin prob.numTargets × X)

  Given the target images, produce (i, x') aiming for f x' = yᵢ.

def MultiTarget.preimageExperiment {X Y : Type} {prob : PreimageProblem X Y} [DecidableEq Y] (adv : PreimageAdversary prob) : ProbComp Bool

The SM-PRE experiment: sample the preimages, run the adversary on their images, and check that the returned preimage hits the chosen target.

noncomputable def MultiTarget.preimageAdvantage {X Y : Type} {prob : PreimageProblem X Y} [DecidableEq Y] (adv : PreimageAdversary prob) : ENNReal

The SM-PRE advantage of an adversary.

Single-function multi-target target-collision resistance (SM-TCR)

structure MultiTarget.TcrProblem (Tweak M Y : Type) : Type

An SM-TCR problem for a fixed tweakable function f : Tweak → M → Y: the adversary commits numTargets target pairs (tweak, message), then must find, for one of them, a different message hashing (under the same tweak) to the same value.

• f : Tweak → M → Y

  The fixed tweakable function whose target-collision resistance is in question.

• numTargets : ℕ

  The number of targets the adversary commits to.

structure MultiTarget.TcrAdversary {Tweak M Y : Type} (prob : TcrProblem Tweak M Y) : Type 1

An SM-TCR adversary: a choose phase committing the target (tweak, message) pairs (with private state), and a forge phase producing a colliding message for one committed target.

• State : Type

  Private state carried from choose to forge.

• choose : ProbComp ((Fin prob.numTargets → Tweak × M) × self.State)

  Commit the numTargets target (tweak, message) pairs.

• forge : self.State → (Fin prob.numTargets → Y) → ProbComp (Fin prob.numTargets × M)

  Given the committed targets' hash values, produce (j, m') aiming for a collision at target j.

def MultiTarget.tcrExperiment {Tweak M Y : Type} {prob : TcrProblem Tweak M Y} [DecidableEq M] [DecidableEq Y] (adv : TcrAdversary prob) : ProbComp Bool

The SM-TCR experiment: commit the targets, run the forge phase on their hashes, and check that the forged message differs from the committed one yet collides under the same tweak.

noncomputable def MultiTarget.tcrAdvantage {Tweak M Y : Type} {prob : TcrProblem Tweak M Y} [DecidableEq M] [DecidableEq Y] (adv : TcrAdversary prob) : ENNReal

The SM-TCR advantage of an adversary.