Formal Verification for Cryptographers: Proving the One-Time Pad with Lean
Introduction to Formal Verification with Lean Part 1
I guide cryptographic engineers through the basics of formal verification using Lean, a functional programming language and theorem prover. We start with a simple Hello World and move on to defining bitstrings and the XOR function. The core of this tutorial involves porting definitions from the Boneh and Shoup textbook to formally verify that the One-Time Pad protocol satisfies the correctness properties of a Shannon cipher.
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.
- danabramov
Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/
Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/
And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/
Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4
This is the best intro to Lean I know, plus it teaches you why a + b = b + a.
- kccqzy
I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you run it interactively and observe the goals at each step. In contrast languages like Idris do not use tactics and require explicit manipulation of proof objects; it’s a lot less automated and verbose. Using the function call analogy, it’s like having to write down every argument passed to a function call and name every return value. It’s more tedious to write but both the writer and the reader gain more by the explicitness. But in the age of AI, the tedium to write proofs without tactics really shouldn’t have mattered.
- mkw5053
If you like Lean, here are two more great, short books on proving things about your program (not with Lean, though):
1. https://mitpress.mit.edu/9780262527958/the-little-prover/
2. https://mitpress.mit.edu/9780262536431/the-little-typer/
David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.
- tantalor
The Natural Numbers Game is amazing, highly recommended.
> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.
- dev_dan_2
Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).
Small feedback:
- Great flow, explaination, motivation and so on! :)
- Typo: "conext" at the bottom
- If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)