GoKawiilFormal verification is a tool to verify correctness of (mathematical) statements. Where we use pen and paper to write a math proof, we could actually use a formal verification tool to write down the proof in code and get it machine-checked, to know for sure the proof is correct. Examples of these tools are Rocq (formally Coq), Isabelle and, the topic for this tutorial, Lean .
In this tutorial we'll write some simple statements about cryptography and their proofs in Lean. So this aims to be fun for cryptographic engineers who are new to formal verification or want to refresh their knowledge of the basics of formal verification.
Specifically, we'll do a walkthrough the very basics of Lean and then formally verify the One-Time Pad (OTP) protocol, first popularized by Claude Shannon but described earlier by Frank Miller and Gilbert Vernam .
The goal for this tutorial is to take formal definitions and proofs about simpler cryptography protocols, such the One-Time Pad, and port them to Lean. We use Dan Boneh and Victor Shoup's "A Graduate Course in Applied Cryptography" as the main source for definitions and proofs.
By the end of this tutorial, you should be able to go through other formalized cryptography Lean proofs such as those from VCV-io
Disclaimer: this is by no means intended to give best practices in Lean, but rather an introduction that might make sense to and be fun for cryptography people.
Lean was created in 2013 by Leonardo de Moura , then at Microsoft Research. It is a functional programming language and theorem prover.
It can be used by mathematicians to write down their axioms, lemma’s and theorems and add proofs where needed. If the proof gets compiled by Lean, that means it’s correct (assuming trust in the Lean compiler). The benefit, apart from checkeable proofs, is that it is easier to break up proofs into sub-proofs and collaborate. Furthermore, Lean can help you complete proofs by automatically searching and applying missing pieces.
However, Lean is also “just” a programming language. Specifically, it is a pure functional programming language, meaning its programs don’t have side effects and functions are treated as first class values. We’ll see more about the latter in the tutorial.
There are many great resources in order to get started with Lean. Here are a few:
... continue reading