Ownership
Proved: spend forgery -- producing a short (s, e) with A *ᵥ s + e = t for a
target you were not given -- cast as a VCVio SIS.Problem, with the honest
blinded witness always valid; the [A | I | -t] augmentation reshaping that
inhomogeneous instance into VCVio's HOMOGENEOUS matrix-SIS, with an EQUALITY of
advantages and a validity predicate equal on the nose to SIS.matrixProblem's;
and the ML-DSA instance, where winning the game is literally producing a signing
key (ownershipValid_mldsaShort_iff_isSigningKey).
Assumed: HNF absorption and MLWE pseudorandomness of t -- the challenge here
is the scheme's distribution, not uniform -- and the whole Fiat-Shamir /
signature-of-knowledge layer. See docs/msis-reshaping.md.
OwnershipKey
A stealth public key viewed as an ownership statement: the public matrix A
and the target t.
structure OwnershipKey (R : Type) [CommRing R] (k l : ℕ) where
/-- The public matrix of the ownership relation. -/
A : Matrix (Fin k) (Fin l) R
/-- The target vector: the stealth public key proper. -/
t : Fin k → RownershipValid
A spend witness (s, e) is valid when it is short and satisfies the
ownership relation A * s + e = t.
def ownershipValid
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(key : OwnershipKey R k l) (w : (Fin l → R) × (Fin k → R)) : Bool :=
isShort w && decide (key.A *ᵥ w.1 + w.2 = key.t)ownershipSISProblem
def ownershipSISProblem (keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool) :
SIS.Problem (OwnershipKey R k l) ((Fin l → R) × (Fin k → R)) where
sampleChallenge := keyGen
isValid := ownershipValid isShortspendForgeryAdvantage
noncomputable def spendForgeryAdvantage (keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(adv : SIS.Adversary (ownershipSISProblem keyGen isShort)) : ℝ≥0∞ :=
SIS.advantage (ownershipSISProblem keyGen isShort) advspendForgeryAdvantage_ne_top
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem spendForgeryAdvantage_ne_top (keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(adv : SIS.Adversary (ownershipSISProblem keyGen isShort)) :
spendForgeryAdvantage keyGen isShort adv ≠ ⊤ :=
ne_top_of_le_ne_top ENNReal.one_ne_top probOutput_le_onespendForgeryAdvantageReal
noncomputable def spendForgeryAdvantageReal (keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(adv : SIS.Adversary (ownershipSISProblem keyGen isShort)) : ℝ :=
(spendForgeryAdvantage keyGen isShort adv).toRealhonest_witness_valid
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem honest_witness_valid (A : Matrix (Fin k) (Fin l) R) (s₁ s' : Fin l → R) (s₂ e' : Fin k → R)
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(hshort : isShort (s₁ + s', s₂ + e') = true) :
ownershipValid isShort ⟨A, A *ᵥ s' + e' + (A *ᵥ s₁ + s₂)⟩ (s₁ + s', s₂ + e')
= true := byproof
simp only [ownershipValid, hshort, Bool.true_and, decide_eq_true_eq]
exact blinded_is_ownership_witness A s₁ s' s₂ e'1. Spend forgery as a search problem
augmentedMatrix
The [A | I | -t] augmentation of an ownership key: the k × (l+k+1)
matrix whose homogeneous kernel elements with last coordinate 1 are exactly
the ownership witnesses for (A, t).
def augmentedMatrix (key : OwnershipKey R k l) :
Matrix (Fin k) (Fin (l + k + 1)) R :=
Matrix.of fun i =>
Fin.append (Fin.append (key.A i) ((1 : Matrix (Fin k) (Fin k) R) i)) ![-key.t i]augmentedWitness
def augmentedWitness (w : (Fin l → R) × (Fin k → R)) : Fin (l + k + 1) → R :=
Fin.append (Fin.append w.1 w.2) ![1]readKey
def readKey (M : Matrix (Fin k) (Fin (l + k + 1)) R) : OwnershipKey R k l where
A := fun i j => M i ((j.castAdd k).castAdd 1)
t := fun i => -M i (Fin.natAdd (l + k) 0)augmentedShort
def augmentedShort [DecidableEq R]
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(z : Fin (l + k + 1) → R) : Bool :=
isShort (fun j => z ((j.castAdd k).castAdd 1),
fun j => z ((Fin.natAdd l j).castAdd 1)) &&
decide (z (Fin.natAdd (l + k) 0) = 1)readKey_augmentedMatrix
@[simp] theorem readKey_augmentedMatrix (key : OwnershipKey R k l) :
readKey (augmentedMatrix key) = key := byproof
obtain ⟨A, t⟩ := key
simp only [readKey, augmentedMatrix, Matrix.of_apply, Fin.append_left,
Fin.append_right, Matrix.cons_val_fin_one, neg_neg]augmentedWitness_ne_zero
The augmented witness is never the zero vector: its marker coordinate is
1. This is the x ≠ 0 conjunct of VCVio's matrix-SIS validity.
axioms: propext, Quot.sound · sorry-free ✓
theorem augmentedWitness_ne_zero [Nontrivial R]
(w : (Fin l → R) × (Fin k → R)) : augmentedWitness w ≠ 0 := byproof
intro h
have : augmentedWitness w (Fin.natAdd (l + k) 0) = 0 := by rw [h]; rfl
simp only [augmentedWitness, Fin.append_right, Matrix.cons_val_fin_one] at this
exact one_ne_zero thisaugmentedMatrix_mulVec_augmentedWitness
theorem augmentedMatrix_mulVec_augmentedWitness (key : OwnershipKey R k l)
(w : (Fin l → R) × (Fin k → R)) :
augmentedMatrix key *ᵥ augmentedWitness w = key.A *ᵥ w.1 + w.2 - key.t := byproof
funext i
simp only [Matrix.mulVec, dotProduct, augmentedMatrix, augmentedWitness,
Matrix.of_apply, Pi.add_apply, Pi.sub_apply]
rw [Fin.sum_univ_add, Fin.sum_univ_add]
simp only [Fin.append_left, Fin.append_right, Matrix.cons_val_fin_one,
Fin.sum_univ_one, Matrix.one_apply, ite_mul, one_mul, zero_mul,
Finset.sum_ite_eq, Finset.mem_univ, if_true, mul_one]
ringaugmented_isValid_eq_ownershipValid
theorem augmented_isValid_eq_ownershipValid [DecidableEq R] [Nontrivial R]
(isShort : ((Fin l → R) × (Fin k → R)) → Bool) (key : OwnershipKey R k l)
(w : (Fin l → R) × (Fin k → R)) :
(decide (augmentedWitness w ≠ 0) &&
augmentedShort isShort (augmentedWitness w) &&
decide (augmentedMatrix key *ᵥ augmentedWitness w = 0))
= ownershipValid isShort key w := byproof
rw [augmentedMatrix_mulVec_augmentedWitness]
simp only [augmentedShort_augmentedWitness, augmentedWitness_ne_zero,
ne_eq, not_false_eq_true, decide_true, Bool.true_and, ownershipValid,
sub_eq_zero]augmentedSISProblem
def augmentedSISProblem [DecidableEq R]
(keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool) :
SIS.Problem (Matrix (Fin k) (Fin (l + k + 1)) R) (Fin (l + k + 1) → R) where
sampleChallenge := do
let key ← keyGen
return augmentedMatrix key
isValid M z := decide (z ≠ 0) && augmentedShort isShort z && decide (M *ᵥ z = 0)augmentedAdversary
def augmentedAdversary [DecidableEq R]
(keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(adv : SIS.Adversary (ownershipSISProblem keyGen isShort)) :
SIS.Adversary (augmentedSISProblem keyGen isShort) :=
fun M => do
let w ← adv (readKey M)
return augmentedWitness wspendForgeryAdvantage_eq_sis_advantage
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem spendForgeryAdvantage_eq_sis_advantage [DecidableEq R] [Nontrivial R]
(keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(adv : SIS.Adversary (ownershipSISProblem keyGen isShort)) :
spendForgeryAdvantage keyGen isShort adv
= SIS.advantage (augmentedSISProblem keyGen isShort)
(augmentedAdversary keyGen isShort adv) := byproof
simp only [spendForgeryAdvantage, SIS.advantage, SIS.experiment,
ownershipSISProblem, augmentedSISProblem, augmentedAdversary,
bind_assoc, pure_bind, readKey_augmentedMatrix,
augmented_isValid_eq_ownershipValid]spendForgeryAdvantage_le_augmentedSIS
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem spendForgeryAdvantage_le_augmentedSIS [DecidableEq R] [Nontrivial R]
(keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(adv : SIS.Adversary (ownershipSISProblem keyGen isShort)) :
spendForgeryAdvantage keyGen isShort adv
≤ SIS.advantage (augmentedSISProblem keyGen isShort)
(augmentedAdversary keyGen isShort adv) :=
le_of_eq (spendForgeryAdvantage_eq_sis_advantage keyGen isShort adv)honest_augmented_witness_valid
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem honest_augmented_witness_valid [DecidableEq R] [Nontrivial R]
(keyGen : ProbComp (OwnershipKey R k l))
(A : Matrix (Fin k) (Fin l) R) (s₁ s' : Fin l → R) (s₂ e' : Fin k → R)
(isShort : ((Fin l → R) × (Fin k → R)) → Bool)
(hshort : isShort (s₁ + s', s₂ + e') = true) :
(augmentedSISProblem keyGen isShort).isValid
(augmentedMatrix ⟨A, A *ᵥ s' + e' + (A *ᵥ s₁ + s₂)⟩)
(augmentedWitness (s₁ + s', s₂ + e')) = true := byproof
simp only [augmentedSISProblem, augmented_isValid_eq_ownershipValid]
exact honest_witness_valid A s₁ s' s₂ e' isShort hshortaugmentedSISProblem_isValid_eq_matrixProblem
The reshaped problem's validity predicate IS VCVio's SIS.matrixProblem
predicate at n = k, m = l + k + 1: a spend forger is scored by exactly the
function SIS.matrixProblem scores solutions by.
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem augmentedSISProblem_isValid_eq_matrixProblem
(keyGen : ProbComp (OwnershipKey R k l))
(isShort : ((Fin l → R) × (Fin k → R)) → Bool) :
(augmentedSISProblem keyGen isShort).isValid
= (SIS.matrixProblem k (l + k + 1) (augmentedShort isShort)).isValid :=
rfl2. Reshaping into homogeneous matrix-SIS
rq_one_ne_zero
Rq is nontrivial: the constant polynomial 1 differs from 0 in its
degree-zero coefficient. Needed for the z ≠ 0 conjunct of matrix-SIS
validity.
theorem rq_one_ne_zero : (1 : Rq) ≠ (0 : Rq) := byproof
intro h
have h1 : (1 : Rq) =
Vector.ofFn (fun i : Fin ringDegree => if (i : ℕ) = 0 then (1 : Coeff) else 0) := rfl
rw [h1] at h
have h0 := congrArg (fun v : Vector Coeff ringDegree => v.get ⟨0, by norm_num [ringDegree]⟩) h
rw [Vector.get_ofFn, Rq.get_zero] at h0
simp only [↓reduceIte] at h0
exact absurd h0 (by decide)instNontrivialRq
instance instNontrivialRq : Nontrivial Rq := ⟨1, 0, rq_one_ne_zero⟩mldsaShort
def mldsaShort (bound : ℕ) (w : (Fin l → Rq) × (Fin k → Rq)) : Bool :=
decide ((∀ i, cInfNorm (w.1 i) ≤ bound) ∧ (∀ i, cInfNorm (w.2 i) ≤ bound))ownershipValid_mldsaShort_iff_isSigningKey
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem ownershipValid_mldsaShort_iff_isSigningKey (bound : ℕ)
(key : OwnershipKey Rq k l) (w : (Fin l → Rq) × (Fin k → Rq)) :
ownershipValid (mldsaShort bound) key w = true
↔ IsSigningKey key.A key.t w.1 w.2 bound := byproof
simp only [ownershipValid, mldsaShort, Bool.and_eq_true, decide_eq_true_eq,
IsSigningKey, IsOwnershipWitness, IsShortPair]
exact and_commmldsa_spendForgeryAdvantage_eq_sis_advantage
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem mldsa_spendForgeryAdvantage_eq_sis_advantage
(keyGen : ProbComp (OwnershipKey Rq k l)) (bound : ℕ)
(adv : SIS.Adversary (ownershipSISProblem keyGen (mldsaShort bound))) :
spendForgeryAdvantage keyGen (mldsaShort bound) adv
= SIS.advantage (augmentedSISProblem keyGen (mldsaShort bound))
(augmentedAdversary keyGen (mldsaShort bound) adv) :=
spendForgeryAdvantage_eq_sis_advantage keyGen (mldsaShort bound) adv