The repository of public key proofs is here. The problem set is presented in a pdf file; we recommend you start reading the PDF then come back here.
The rest of this page is dedicated to a high-level description of a generic construction of Public Key Encryption (PKE) from a Key Encapsulation Mechanism (KEM) and a Data Encryption Mechanism (DEM); and of a result bounding its insecurity against Chosen Plaintext Attacks. We also give some insights into modelling the construction and the proof in a few formal verification tools. (Currently planned: ProofFrog [1] and EasyCrypt [2].)
⏳ 🚧 WIP 🚧 ⏳
References
[1]
R.
Evans, M. McKague, and D. Stebila, “ProofFrog: A tool for
verifying game-hopping proofs.”
https://eprint.iacr.org/2025/418.
[2]
G.
Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin,
“Computer-aided security proofs for the working
cryptographer,” in Advances in cryptology -
CRYPTO 2011 - 31st annual cryptology conference, santa
barbara, CA, USA, august 14-18, 2011. proceedings, 2011, vol. 6841,
pp. 71–90, https://www.easycrypt.info/.