Tutorial: Introduction to Formal Verification with Lean (Part 1) - HashCloak

Formal 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-ioDisclaimer: 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.The Lean programming language & proof assistantLean 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:Book & exercises for beginners: The Hitchhiker’s Guide to Logical VerificationIntroductory books on the Lean website: Functional Programming in Lean. Great if you already know functional programming.Theorem Proving in Lean 4. A more mathematical aim.Natural Numbers Game. Interactive game to learn proving in Lean directly in the browser.(The reason I created this specific exercise even though so many great resources already exist, is the specific overlap with cryptography; VCV-io has amazing proofs for cryptography but is too advanced for beginners and doesn’t have tutorials.)TutorialLet’s get started. The tutorial has 4 parts after we do a quick “Hello World!” (part 2 is the longest). Everything is in Lean 4 and the idea is for you to code along.All code shown with line numbers is code that is needed for the final result. Code that has no line numbers is not yet completed or is just to check something and can be safely removed.Finally, at the beginning of the subsections there is a small comment containing the new concepts shared in that section.Hello world in Leanthe Lean InfoViewevalYou can download Lean locally, or use an online editor such as https://live.lean-lang.org/ which will look something like this (below). On the left side you’ll write Lean and on the right side is the Lean Infoview with useful information and tips.To make sure everything works fine, write something like#eval 1+1And verify that the outcome is shown in the InfoView on the right-hand side.For the traditional “Hello World!”, we can do either of the following:#eval "Hello World!"#eval String.append "Hello " "World!"#eval String.append "Hello " (if 1 > 2 then "Lean!" else "World!")Some properties of Lean:Follows standard mathematical conventions: e.g. #eval 4 + 5 * 6 evaluates to 4+(5*6)=34No parenthesis to hold function arguments, i.e in Lean you write f x instead of f(x)Functions are first-class values in Lean, they get treated just like any value such as a number or a stringBut let’s not get ahead of ourselves; we’ll learn each necessary Lean topic as we go.

What does the book say? I.e. what do we want to port to Lean?We know more or less what we want to define, but the crux is that for using Lean we need clarity and precision. What exactly do we want to define and how exactly are we going to define it? This is why we use the Boneh & Shoup book, so the math we need is already written out and we only need to worry about translating it to Lean.First, there is the definition of a Shannon cipher (2.1.1), which has 3 properties. The first two tell us what the encryption and decryption functions are and the last one is the correctness property, which says that decryption after encryption should return the original message.The specific example we are interested in is the one-time pad, where encryption and decryption are simply XOR-ing:A significant part of the tutorial will be dedicated to proving the properties of bit-wise exclusive-OR (XOR):And finally, we can show one-time pad is a Shannon Cipher by proving it adheres to the correctness property:For this first tutorial we’ll do the following simple steps:Define bitstrings and the XOR functionProve necessary properties for XOR commutativityassociativitythe identity elementself-inverseDefine a Shannon Cipher, which has an encryption functiona decryption functionthe property that decryption “reverses” encryption (correctness)Show that a OTP, where encryption and decryption is XOR, is a Shannon CipherReady for some fun? Let’s begin.Tutorial Part 1: Define a BitString and XORThe one-time pad will be defined over keys K, messages M and ciphertexts C which are all bit strings of the same length L; K:= M := C := {0,1}ᴸ.In the definition of XOR we need addition modulo 2. So it will be helpful for us to see {0,1}ᴸ as ℤ₂ᴸ and use arithmetics over ℤ₂ in Lean.Finite Fieldsimport librariesZmod nFirst, import the finite field library ZMod from the mathematics library in Lean:import Mathlib.Data.ZMod.BasicIn this predefined library ZMod n defines the integers modulo n, which comes with modular arithmetic pre-implemented. (

You can read more about already implemented types by holding Cmd/Ctrl + clicking on them, e.g. checkout ZMod n.)Tryout some simple modular arithmetic to get familiar with ZMod, for example 5 + 6 mod 7:#eval (5: ZMod 7) + (6: ZMod 7)Now we can define the domain of K, M, L by creating a new type that is a vector of elements from ZMod 2.BitString definitionVectordependent typecheckA nice thing about Lean is that we don’t have to fix bit string length L; we can just say L in ℕ, like we would in math. (Type “\N” to write ℕ in Lean.)The predefined type Vector α n creates a vector of length n with elements of type α. So we can use Vector (ZMod 2) L for defining our custom type ℤ₂ᴸ:def BitString (L: ℕ): Type := Vector (ZMod 2) LThis is a dependent type, which gives a different instantiation for different values L in ℕ. We can check it: (prefix a comment in Lean with --)#check BitString 5 --BitString 5 : TypeNote that #eval won’t work because there is nothing to evaluate, but #check displays the type of the expression, which in this case works fine.XOR definitionimplicit parameterscurryinglambda functionNow we define the function xor on input bit strings x = [x_1, …, x_L] and y = [y_1, …, y_L] to be [x_1 +₂ y_1, …, x_L +₂ y_L] if +₂ is addition modulo 2.How can we define this in Lean? Think about the function signature in math: ℤ₂ᴸ × ℤ₂ᴸ → ℤ₂ᴸ. There are several options of how to do this (there are always many ways to achieve the same thing in Lean), we’ll go with:def xor {L: ℕ} (x y: BitString L): (BitString L)Here, parameter L is implicit. Now we need the “function body”.To easily iterate over the two input vectors and add them component-wise, we can use the predefined function zipWith available on vectors.

Let’s understand the type of zipWith:def zipWith (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ nIt takes as arguments a function f and two vectors as and bs, and returns a vector of the same length as as and bs. Note that the types of the vector elements can be distinct (although it’s not the case for xor).The function type f : α → β → φ means: it takes an element of type α and an element of type β and it returns an element of type φ. In math we would write α × β → φ. The approach Lean uses is called currying; a function with multiple arguments is represented as a sequence of functions, each taking a single argument. This means you can do partial application and makes the code very flexible. So we can read f : α → β → φ as f : α → (β → φ), which shows that when you give it the first element of type α, you end up with a function β → φ to which you then give an element of type β and end up with an output of type φ.So what zipWith does is walk over two vectors in parallel and performs operation f on the two current elements. In the case of xor we want it to walk over x and y and add them modulo 2.def xor {L: ℕ} (x y: BitString L): (BitString L) := -- TODO define f Vector.zipWith f x yThe final piece of the puzzle is how to define the function f we want to pass to zipWith, knowing it needs to perform addition on the elements. We can use a lambda function, which can be written in a compact way like this: fun x => x + 1 (e.g. return the successor of a natural number).Putting it together:def xor {L: ℕ} (x y: BitString L): (BitString L) := Vector.zipWith (fun a b => a + b) x yNote that this will work correctly, because the type of BitString has elements in ℤ₂ and thus addition will automatically be addition mod 2.Tutorial Part 2: Prove properties of XOROkay now the real fun begins!Just for clarity, the content you should at least have now is:import Mathlib.