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.