This website stores cookies on your computer. These cookies are used to collect information about how you interact with our website and allow us to remember your browser. We use this information to improve and customize your browsing experience, for analytics and metrics about our visitors both on this website and other media, and for marketing purposes. By using this website, you accept and agree to be bound by UVic’s Terms of Use for web and social media privacy.  If you do not agree to the above, you can configure your browser’s setting to “do not track.”

Skip to main content
People Departments Maps Buildings Rooms A-Z
University
of Victoria
Apply Library
Sign in Online tools Sign out
Faculty of Graduate Studies

Ashely Blacquiere

  • BSc (University of Victoria, 2011)

Notice of the Final Oral Examination for the Degree of Master of Science

Topic

Verified Commitment Schemes and Reduction Proofs in the Lean Proof Assistant

Department of Computer Science

Date & location

  • Friday, April 24, 2026

  • 1:30 P.M.

  • Virtual Defence

Reviewers

Supervisory Committee

  • Dr. Bruce Kapron, Department of Computer Science, University of Victoria (Supervisor)

  • Dr. Yun Lu, Department of Computer Science, UVic (Member) 

External Examiner

  • Dr. Riham AlTawy, Department of Electrical and Computer Engineering, University of Victoria 

Chair of Oral Examination

  • Dr. Kieka Mynhardt, Department of Mathematics and Statistics, UVic

     

Abstract

This thesis presents a formalization of commitment schemes in the Lean 4 theorem prover, together with machine-checked proofs of their core security properties. Commitment schemes allow a party to commit to a value while keeping it hidden, with guarantees of binding (the value cannot be changed) and hiding (the value remains secret until revealed).

We develop a general, specification-driven framework for modeling commitment schemes and their security definitions in Lean, using a probabilistic monad to express adversarial games and reduction-based proofs. Within this framework, we formalize two canonical schemes: the Pedersen commitment scheme and the ElGamal commitment scheme. For Pedersen, we prove perfect hiding and computational binding via reduction to the discrete logarithm problem; for ElGamal, we prove perfect binding and computational hiding via reduction to the decisional Diffie–Hellman assumption.

This work contributes both concrete formalizations and reusable abstractions for cryptographic reasoning in Lean, advancing the emerging area of mechanized cryptography within the system.

Back to oral exams