Project-declaredLean 4.32.0
Rom CRAdvantage le birthday
CollisionResistance.romCRAdvantage_le_birthday
Plain-language statement
ROM Collision Resistance birthday bound: for any t-query ROM-CR adversary A over a hash range Y, the advantage is bounded by (t+2) * (t+1) / (2 * |Y|) (a vacuous bound when |Y| = 0). The two extra queries account for the experiment's verification queries, which share the adversary's cache.
program verificationseparation logiccryptography
Source project: VCVio
Person-level attribution pending.