Hacker News

Introduction to Formal Verification with Lean Part 1

Comments

Tutorial: Introduction to Formal Verification with Lean (Part 1)
Elena Cryptography Engineer

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-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.

The Lean Programming Language & Proof Assistant

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, lemmas 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 checkable 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:

(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.)

Tutorial

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 Lean

The Lean InfoView eval

You 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 4 + 5

And 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 "Hello " ++ "World!"

Some properties of Lean:

  • Follows standard mathematical conventions: e.g. #eval 4 + 5 * 6 evaluates to 4+(5*6)=34
  • No 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 string

But 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:

E(k, m) = k ⊕ m
D(k, c) = k ⊕ c

A significant part of the tutorial will be dedicated to proving the properties of bit-wise exclusive-OR (XOR):

  • commutativity: x ⊕ y = y ⊕ x
  • associativity: (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)
  • identity element: there exists 0 such that x ⊕ 0 = x
  • self-inverse: x ⊕ x = 0

And finally, we can show one-time pad is a Shannon Cipher by proving it adheres to the correctness property:

D(k, E(k, m)) = k ⊕ (k ⊕ m) = (k ⊕ k) ⊕ m = 0 ⊕ m = m

For this first tutorial we’ll do the following simple steps:

  1. Define bitstrings and the XOR function
  2. Prove necessary properties for XOR: commutativity, associativity, the identity element, self-inverse
  3. Define a Shannon Cipher, which has an encryption function, a decryption function, and the property that decryption “reverses” encryption (correctness)
  4. Show that a OTP, where encryption and decryption is XOR, is a Shannon Cipher

Ready for some fun? Let’s begin.

Tutorial Part 1: Define a BitString and XOR

The 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 Fields import libraries: Zmod n

First, import the finite field library ZMod from the mathematics library in Lean:

import Mathlib.Data.ZMod.Basic

In 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 definition: Vector, dependent type check

A 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) L

This is a dependent type, which gives a different instantiation for different values L in ℕ. We can check it:

#check BitString 3

Note 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 definition: implicit parameters, currying, lambda function

Now 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 :=
  zipWith (fun a b => a + b) x y

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:

#check zipWith

It 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. The 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 :=
  zipWith (fun a b => a + b) x y

Note 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 XOR

Okay now the real fun begins! Just for clarity, the content you should at least have now is:

import Mathlib.Data.ZMod.Basic
def BitString (L : ℕ) : Type := Vector (ZMod 2) L
def xor {L : ℕ} (x y : BitString L) : BitString L :=
  zipWith (fun a b => a + b) x y

Or whatever equivalent version works for you! We’ll add one more line; before the xor definition:

open scoped BitString

This will make sure Lean does not get confused with a different existing xor definition when we start proving things 😅

Continuing to follow the Boneh & Shoup book, we’ll now prove the properties as mentioned in the definition of xor (Example 2.1), starting with commutativity.

Prove commutativity of XOR; x ⊕ y = y ⊕ x

We start by proving commutativity for XOR, meaning x ⊕ y = y ⊕ x. This first property will take the most time to prove since it contains the first Lean proof of the tutorial. It’s split up into 3 steps.

Define lemma for commutativity: goals in Lean, lemma definition, sorry

We’ll define the commutativity property as a lemma and then prove it. As soon as you’ve written down the lemma, Lean will call it the “goal” of what is yet to be proven. Your task is to reduce the current goal into one or more smaller subgoals, which are closer to something you already know is true. Proving your statement then becomes a chain of reduction, similar to breaking up a programming problem into smaller subproblems.

The elements a lemma (or theorem) exist of in Lean:

  • Parameters: In this case, the parameters consist of two BitStrings; x and y.
  • Statement: The statement should express the commutativity property we want to prove for x and y: xor x y = xor y x.
  • Proof: The proof body.

The name of the lemma depends on preference; I picked the elegantly short xor_comm_property. Note that for the BitStrings we need the implicit parameter L:

lemma xor_comm_property {L : ℕ} (x y : BitString L) : xor x y = xor y x :=
  sorry

The sorry placeholder is not a crazy invention of mine, this is really the Lean placeholder, which you could read as “sorry I haven’t proven it yet”.

Prove lemma commutativity: step 1: tactics, by, ⊢, Vector.ext

We’ll build our proofs using tactics: instructions that help reduce the current goal. You’ll have many different options of steps you can apply, for example:

  • rewrite goal into an equivalent form
  • split goal into several subgoals
  • close a goal when it matches something you already know to be true

We start by removing sorry and replacing it with by, which indicates we’re going to prove this using tactics. This is useful, because Lean will help us by showing what our goal is and what progress we’re making. It looks something like this:

lemma xor_comm_property {L : ℕ} (x y : BitString L) : xor x y = xor y x :=
  by
    -- we will write tactics here
    sorry

In the InfoView, Lean says: the goal is to show that for L ∈ ℕ and x,y of type BitString L: x.xor y = y.xor x. (The goal is always preceded by ⊢.)

Onto the proof. What do we know? For every index i, if we calculate the corresponding element on both sides, they will be equal: (x.xor y)[i] = (y.xor x)[i] since (x[i] + y[i]) = (y[i] + x[i]) due to commutativity for addition in ℤ₂. So if we can split up our goal into L subgoals, ranging over i, then the remaining goal becomes proving a single equality of the single element on both sides.

To achieve this splitting into L subgoals, we can use an extensionality lemma, which says: “2 things are the same if they are made up of the same things”. This is a general type of lemma which applies for many types and for a vector it is accessible via Vector.ext (reference). We can use it as follows:

lemma xor_comm_property {L : ℕ} (x y : BitString L) : xor x y = xor y x :=
  by
    apply Vector.ext
    intro i
    intro hi
    -- still need to prove something...

Now in the editor you can see the goal has changed to:

⊢ ∀ (i : ℕ) (h : i < L), x.xor y i = y.xor x i

So still we have L ∈ ℕ and x,y of type BitString L, but the

Read on Hacker News ↗ ← Back to News

Comments

No comments yet. Start the discussion.