Note: this is a 1 unit graduate seminar. If you enrolled for more than 1 unit, you should change it to 1, or talk to the instructor.
The topic of CSE209B in Winter 2026 will be the formal verification of cryptographic proofs. The course will consists of a few introductory/tutorial lectures on the topic, followed by students’ presentations. The current plan is to focus on ProofFrog, a recent (and relatively simple) proof verification engine that allows to formally verify the “game-hopping” security proofs typically carried out by cryptographers using pen & paper. If time permits, we may also cover other tools, as well as theoretical work on the computational soundness of symbolic cryptography.
Prerequisites: Students attending this seminar are expected to be familiar with basic cryptographic security definitions and proofs, as taught in an introductory cryptography course.
Requirements: Beside attending class, students will experiment with ProofFrog, formally verifying some simple cryptographic constructions, and then give a presentation in class. Alternatively, students more interested in theoretical work, may read and present a research paper on the formal/symbolic analysis of cryptographic protocols.
These pointers are for general reference. We will cover only a small subset, initially focusing of ProofFrog.
See individual pages for tutorials and reading material, including the slides for the ProofFrog tutorial from CAPS 2025.