Research proof index

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.