CAPS 2025 Tutorial

ProofFrog was one of the examples presented at the Workshop on Computer-Aided Proofs of Security (CAPS) at Eurocrypt 2025.

The presentation walked through the pen-and-paper proof that the KEM-DEM construction is IND-CPA-secure, then showed the analogous proof in ProofFrog.

A tutorial file walking through the pen-and-paper and ProofFrog proofs side-by-side, as well as executable ProofFrog files, can be found in the proof-ladders asymmetric ladder repository on Github.

The Joy of Cryptography-style proof for KEM-DEM IND-CPA security by Mike Rosulek (with awesome animations) can be found at https://garbledcircus.com/kemdem/left-right.