Is circular security just three notions in a trench coat? The paper equates hinting PRGs, KDM SKE, and KDS weak PRFs.

Yet another lower-bound paper: black-box PRF-from-PRG constructions need linear-ish PRG calls, even for weak PRFs.

Can Lean model game hops and extract reductions? HOPSCOTCH says yes, with mechanized IND-CCA, ElGamal, and GGM proofs.

Attack on #Pencil shows collisions at ~2^(n-7)/2 queries, so the claimed beyond-birthday-bound security was optimistic.