Research proof index

The post-keygen freshness endpoint is the same Boolean experiment as running signedFreshAdv in the direct stateful CMA game.

When the simulated signing loop produces some (w, z), the random-oracle cache contains a challenge c at (msg, w) satisfying ids.verify pk w c z = true. This is proved by induction on the loop counter: each abort iteration preserves the invariant (the cache only grows), and a successful iteration writes exactly the challenge used in verification.

The expected number of signing queries is the sum, over prefixes of the retry loop, of the probability that every attempt in the prefix aborts.

The expected weighted query cost of one signing attempt is the expectation of the queried commitment cost over the attempt output distribution.

Unit-cost specialization of the run formula: each signing attempt run tags its output with a single unit of cost (cf. signAttempt_run_withAddCost_eq).

Verification has expected weighted query cost equal to the cost of the single verification query when a signature is present, and 0 when the signature is none.