Certain forgery after premature hash-key disclosure

Proved

QAlgorithms.Papers.Independent.Intake100.P41.premature_recycling_attack

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $K$ be a finite nonempty hash-key set, let $T=\{0,1\}^m$ , and let $h:K\times X\to T$ be any hash family. Fix distinct messages $x,x'\in X$ . Suppose Alice exports the hash key before Bob stops accepting the pending message. Consider an allowed subsequent use that reveals that key to Eve while the intercepted pair $(x,h_k(x)\oplus p)$ remains pending.

There is an attack depending only on the disclosed $k$ and intercepted pair, and not on the pad $p$ , such that

\Pr_{k,p}[\text{Bob accepts the substituted message }x']=1,

where $k$ and $p$ are independent and uniform. The known-key context supplies the key before the attack chooses its pair, and Bob then executes the ordinary verification rule. No AXU property is required. This witness explains why arbitrary reuse must wait until pending verification has closed; it does not assert that every subsequent application reveals the key.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P41

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intake100.P41

open QAlgorithms.Papers.Independent.Bridge50.P44 (xorWord verifyTag)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF pp.3,10: in the allowed context that discloses a prematurely exported
hash key, there is a substitution accepted with probability one before Bob's
pending verification closes. The attacker never receives the OTP. No AXU
assumption is needed, and the result concerns this premature-release context. -/
theorem premature_recycling_attack {K X : Type*} [Fintype K] [Nonempty K]
    {m : ℕ} (h : K → X → Tag m) (x xprime : X) (hne : x ≠ xprime) :
    ∃ a : K → X × Tag m → X × Tag m,
      uniformProbability (fun seed : K × Tag m =>
        let view := (prematureReleaseView h a seed.1 seed.2 x).2
        view.submitted.1 = xprime ∧ view.accepted = true) = 1 := by sorry

end QAlgorithms.Papers.Independent.Intake100.P41

end

Source

Key recycling in authentication, arXiv:1202.1229v3, PDF p. 10, Section 4 opening; Section 1.2 on p.3

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $K$ be any finite nonempty set, let $X$ be any type, let $m$ be any natural number, let $h:K\times X\to\{0,1\}^m$ be any function, and let $x,x'\in X$ satisfy $x\ne x'$ . There exists a function $a:K\times(X\times\{0,1\}^m)\to X\times\{0,1\}^m$ such that the following event has probability exactly $1$ when $k\in K$ and an $m$ -bit pad $p$ are chosen independently and uniformly: form the honest tag $t=h(k,x)\oplus p$ , reveal $k$ to the attack, and let $(y,s)=a(k,(x,t))$ ; then $y=x'$ and $s=h(k,y)\oplus p$ , so the submitted pair is accepted. Here $\oplus$ is coordinatewise exclusive-or, and the probability is the number of successful seeds $(k,p)$ divided by $|K|2^m$ . No restriction on $h$ is assumed, and $m=0$ , with its single empty tag, is included.

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph