Lean for Cryptanalysts: A Practical Introduction to Formal Proofs

Many results in cryptanalysis rest on mathematical arguments, such as an identity that connects two distinguishers or a property of an S-box that justifies a constraint in a search model. We usually check them by hand, so small mistakes can go unnoticed.

This post shows how to let a computer check such arguments using Lean, a language for writing mathematical proofs. We begin with a warm-up, the invertibility of a Feistel round, and then formalize an identity connecting linear and integral sums. By the end, you will be able to read these proofs, run them in your editor, and adapt them to claims from your own research.

No background in Lean is assumed. Familiarity with bits, block ciphers, and finite sums is enough.

Download the runnable tutorialLean 4.35.0 · Mathlib v4.35.0

What does Lean check?

Lean is a programming language for mathematics. Instead of writing a program that computes an answer, we write a theorem and its proof, and Lean checks that every step of the proof is valid. Such a tool is called an interactive theorem prover. It is interactive because it tells us, while we type, what remains to be proved.

A Lean file has three parts:

• Definitions of the objects we study, such as an S-box or a sum over all inputs.
• A theorem statement: assumptions, such as “$x$ is even”, and a claim, such as “$x^2$ is even”.
• A proof that the claim follows from the assumptions.

While we write a proof, a panel in the editor called the Infoview shows the assumptions we may use and the claim that still has to be proved. This remaining claim is called the goal. The proof is complete when no goal remains.

Most proofs are written as a sequence of commands called tactics. Each tactic performs one step of reasoning, much like one line of a handwritten proof. For example:

• simp simplifies the goal using definitions and known identities, such as $y\oplus y=0$.
• rw rewrites using an equation. If we know $x=y+1$, it replaces $x$ by $y+1$ in the goal.
• ring proves an identity by algebraic rearrangement, such as $(a+b)^2=a^2+2ab+b^2$.
• linarith proves a goal that follows from the assumptions by linear arithmetic, such as $x<z$ from $x<y$ and $y<z$.

Each tactic either proves the goal or replaces it with simpler goals. We will use these tactics in the examples below.

Some tactics are large programs, and large programs can have bugs. Lean therefore does not simply trust them. Each tactic produces a complete, detailed proof, and a small separate part of Lean, its kernel, checks that proof. We need to trust the kernel, not every tactic. The Lean reference explains this proof-checking process.

For a cryptanalyst, this catches familiar mistakes. A factor of two cannot disappear between two lines. A sum over half the inputs cannot quietly become a sum over all of them. A theorem about permutations cannot be applied to an arbitrary function until we prove that the function is a permutation.

Lean does not check whether our definitions describe what we intend. If we define an S-box with a wrong table entry, Lean will correctly prove facts about the wrong S-box. Choosing the definitions is our job. Lean checks the reasoning built on them, and anyone can rerun that check.

A warm-up: one Feistel round

Before the cryptanalytic example, we prove a fact every cryptanalyst knows. For a round function $F$ on $n$-bit words, one Feistel round maps a pair of words to

The round can be undone for every $F$, even when $F$ itself is not invertible: the map $(y_L,y_R)\mapsto(y_R\oplus F(y_L),\;y_L)$ restores the input, because $(x_L\oplus F(x_R))\oplus F(x_R)=x_L$.

This example needs nothing beyond Lean itself, so it is the quickest way to try the editor:

1. Install Lean. Follow the official setup guide. It walks you through installing VS Code, the Lean 4 extension for VS Code, and Lean itself.
2. Open the warm-up file. Download Warmup.lean and open it in VS Code.

The Infoview opens to the right of the file. If it does not, press Cmd+Shift+Enter, or Ctrl+Shift+Enter on Windows and Linux. It shows the proof at the position of the cursor, so we move through a proof by moving the cursor. Lean rechecks the file as we type. There is no compile button, and we do not need to save. If VS Code reports that no default toolchain is configured, run elan default stable in a terminal. elan is the tool that installs Lean versions and selects one.

The file starts with two definitions:

def feistel {n : Nat} (F : BitVec n → BitVec n)
    (x : BitVec n × BitVec n) : BitVec n × BitVec n :=
  (x.2, x.1 ^^^ F x.2)

def feistelInv {n : Nat} (F : BitVec n → BitVec n)
    (y : BitVec n × BitVec n) : BitVec n × BitVec n :=
  (y.2 ^^^ F y.1, y.1)

Read the first definition piece by piece:

• def feistel introduces a definition named feistel.
• A colon means “has type.” Nat is the type of natural numbers, BitVec n is the type of $n$-bit words, and BitVec n × BitVec n is the type of pairs of words.
• (F : BitVec n → BitVec n) is the round function. The arrow → describes a function’s input and output types, so F may be any function from $n$-bit words to $n$-bit words.
• {n : Nat} is an implicit argument. Lean infers the word size from the type of F, so we never supply n ourselves.
• The result follows :=. x.1 and x.2 are the two halves of x, ^^^ is XOR, and F x.2 applies F to x.2. Function application uses spaces, without parentheses.

Typing symbols. In VS Code, type a backslash, an abbreviation, and a space: \to gives →, and \times or \x gives ×. Most abbreviations are LaTeX command names, so you can often guess them. To find out how to type a symbol you see, hover over it with the mouse.

feistelInv follows the same pattern. Now the theorem, with one tactic for each step of the handwritten argument:

theorem feistel_inverse {n : Nat} (F : BitVec n → BitVec n)
    (l r : BitVec n) :
    feistelInv F (feistel F (l, r)) = (l, r) := by
  simp only [feistel, feistelInv]
  rw [BitVec.xor_assoc]
  rw [BitVec.xor_self]
  rw [BitVec.xor_zero]

theorem feistel_inverse names the statement. The objects it talks about come before the last colon, and the claim comes after it. Since n, F, l, and r are arbitrary, the theorem covers every word size, every round function, and every input. := by starts the proof, and each following line is one tactic:

1. simp only [feistel, feistelInv] unfolds the two definitions, simplifying (a, b).1 to a, and does nothing else. The goal becomes (l ^^^ F r ^^^ F r, r) = (l, r). Since ^^^ groups from the left, its first entry is $(l\oplus F(r))\oplus F(r)$.
2. rw [BitVec.xor_assoc] rewrites with the library fact that XOR is associative, regrouping the first entry as $l\oplus(F(r)\oplus F(r))$.
3. rw [BitVec.xor_self] uses $y\oplus y=0$. Here 0#n is Lean’s notation for the $n$-bit zero word.
4. rw [BitVec.xor_zero] uses $y\oplus 0=y$. Both sides are now identical, so rw closes the goal automatically.

Step through the proof with the buttons below, or move the cursor from line to line in the editor. The Infoview lists the assumptions n, F, l, and r, followed by the goal after the symbol ⊢ (read “turnstile”; in logic, $\Gamma\vdash\varphi$ means that $\varphi$ can be proved from the assumptions $\Gamma$). At the end of the last line, the Infoview shows Goals accomplished!

The last view shows what happens without step 2. Delete the line rw [BitVec.xor_assoc], and Lean underlines BitVec.xor_self in red. The pattern ?m.11 ^^^ ?m.11, where ?m.11 stands for any word, needs the same word twice, side by side. In l ^^^ F r ^^^ F r, the two copies of F r are not yet grouped together. A handwritten proof uses associativity without comment; Lean requires it as an explicit step. Undo the change with Cmd+Z (Ctrl+Z).

Once each step is clear, the whole proof fits in one line, and the file contains this version too:

example {n : Nat} (F : BitVec n → BitVec n) (l r : BitVec n) :
    feistelInv F (feistel F (l, r)) = (l, r) := by
  simp [feistel, feistelInv, BitVec.xor_assoc]

example states and proves a claim without giving it a name. Without only, simp also uses the identities it knows by default, such as BitVec.xor_self and BitVec.xor_zero, and finds the order of the steps itself. Experienced users often prefer such one-line proofs. The step-by-step version shows what each step does.

Finally, compare the general theorem with a finite check:

def toyF (r : BitVec 4) : BitVec 4 := r &&& 3

theorem toy_inverse :
    ∀ l r : BitVec 4, feistelInv toyF (feistel toyF (l, r)) = (l, r) := by
  decide

toyF keeps the two low bits of a 4-bit word and clears the others, because &&& is bitwise AND. It is far from invertible. ∀ (typed \forall) means “for every.” The tactic decide proves the statement by checking all $2^8$ inputs. This works only because the word size and the round function are fixed. The theorem feistel_inverse needs no enumeration and covers infinitely many cases. The cryptanalytic proof below works the same way.

As an exercise, prove that feistel also undoes feistelInv. The statement is at the end of the file, and the same four steps prove it. Together, the two theorems show that the round is a permutation.

Setting up the tutorial project

The cryptanalytic example uses Mathlib, Lean’s community library of mathematics. It provides finite sums and many of the tactics we use. Setting up the project takes four steps. The download in step 3 is large, so start it now and let it run while you read the next section.

1. Download the tutorial. Download and extract the tutorial project. It contains the complete Lean source, the exact versions of Lean and Mathlib it was checked with, and a short README.

2. Open the folder, not just the file. In VS Code, choose File → Open Folder… and select the extracted lean-for-cryptanalysts folder. Lean reads the project settings in this folder to find Mathlib.

3. Download Mathlib. Open a terminal in VS Code (Terminal → New Terminal) and run:

   lake exe cache get

   Lake is Lean’s project tool. This command downloads Mathlib already compiled, which needs about 7 GB of disk space. If the terminal reports lake: command not found, restart VS Code so that it finds the new installation.

4. Open LeanForCryptanalysts.lean. The first time, Lean needs a moment to load Mathlib before it can check the file.

A small cryptanalytic argument

Fix a key and regard encryption as a permutation $E$ of $V=\mathbb{F}_2^n$, where $n$ is the block size. For masks $\alpha,\beta\in V$, $\alpha\cdot x$ denotes the dot product over $\mathbb{F}_2$. We use two signed sums. The linear sum

is the correlation of the linear approximation with masks $\alpha$ and $\beta$, without the factor $2^{-n}$. For a set of plaintexts $\mathcal{X}\subseteq V$, the signed integral sum is

If $\mathcal{X}$ contains $M$ plaintexts and $N_1$ of them satisfy $\beta\cdot E(x)=1$, then $I_\beta(\mathcal{X};E)=M-2N_1$. In particular, $I_\beta(\mathcal{X};E)=0$ exactly when $\beta\cdot E$ is balanced on $\mathcal{X}$.

We take the simplest plaintext structure, an affine halfspace:

For nonzero $\alpha$, the halfspaces $\mathcal{X}_0$ and $\mathcal{X}_1$ split $V$ into two halves of $2^{n-1}$ plaintexts each. With $\alpha$, $\beta$, and $E$ fixed, we abbreviate

The argument has two steps:

• Splitting. On $\mathcal{X}_b$, we have $(-1)^{\alpha\cdot x}=(-1)^b$. Splitting the linear sum into the two halfspaces therefore gives $L=I_0-I_1$.
• Balance. Since $E$ is a permutation and $\beta\neq0$, the bit $\beta\cdot E(x)$ is zero for exactly half of all $x\in V$. Thus $I_0+I_1=0$.

Together, they give the following identity for every permutation $E$ and all nonzero masks $\alpha$ and $\beta$:

For the formalization, $\alpha$ selects the leftmost input bit and $\beta$ the leftmost output bit. We write an input as $x=(b,z)$, where $b$ is the selected bit and $z\in\mathbb{F}_2^m$ holds the remaining $m=n-1$ bits. Then $\alpha\cdot x=b$, so $\mathcal{X}_b$ contains the inputs whose selected bit equals $b$, and $\beta\cdot E(x)$ is the selected bit of $E(x)$.

Here is an eight-input illustration with $n=3$, where $\alpha$ and $\beta$ select the leftmost bit as above. The toy permutation flips the selected bit exactly when the other two bits are both one. Applying it twice restores the input.

Our goal is to prove the identity for every block size and every permutation, beyond the eight inputs in the illustration. This is the halfspace case of the linear-to-integral conversion, but its short proof is enough for our first formalization.

Reading the algebraic step in Lean

Start with the last algebraic step. Suppose three integers satisfy $I_0+I_1=0$ and $L=I_0-I_1$. In Lean, we write the following. It is the first theorem in LeanForCryptanalysts.lean, so you can follow along in the editor.

import Mathlib

theorem halfspace_algebra (I₀ I₁ L : ℤ)
    (hbalance : I₀ + I₁ = 0)
    (hlinear : L = I₀ - I₁) :
    L = 2 * I₀ := by
  linarith

Compared with the warm-up, three things are new:

• import Mathlib loads Mathlib, which provides the tactic linarith.
• (I₀ I₁ L : ℤ) introduces three arbitrary integers. ℤ (typed \Z) is the type of integers, and subscripts such as ₀ are typed \0.
• (hbalance : ...) and (hlinear : ...) are assumptions. They are written like the other arguments and given names, so that we can refer to them later.

As before, the claim L = 2 * I₀ follows the last colon. linarith proves it from the assumptions by linear arithmetic.

There are no particular values assigned to these integers. The theorem covers all integers satisfying its hypotheses. Lean does not establish the hypotheses by this step. We will prove them from the cryptographic definitions below.

As in the warm-up, place the cursor at the start of the linarith line, line 22 of the file, and then at its end. The figure below shows both views.

Next, break the proof on purpose. Delete the line (hbalance : I₀ + I₁ = 0). Lean immediately underlines linarith in red and reports the error shown in the third view above.

The message shows how linarith works. To prove an equality, it proves two inequalities, each by contradiction. In the first case, named h1, it assumes the opposite inequality, L < 2 * I₀, and searches the assumptions for a contradiction. a✝ is the temporary name Lean gives this extra assumption. Without hbalance, there is no contradiction to find. For example, $I_0=1$, $I_1=0$, and $L=1$ satisfy $L=I_0-I_1$ but not $L=2I_0$. Undo the deletion with Cmd+Z (Ctrl+Z), and the error disappears.

This loop is how we work with Lean: write a step, look at what remains, and continue until no goals remain.

Defining the cryptographic objects

Now we give the sums their actual meaning. Lean’s Bool type has two values, false and true. We use them for bits zero and one. A Boolean is not a number in Lean, so before raising $-1$ to a bit, we convert the bit to $0$ or $1$:

def sign (b : Bool) : ℤ :=
  (-1) ^ b.toNat

theorem sign_false : sign false = 1 := by
  rfl

theorem sign_true : sign true = -1 := by
  rfl

Here sign takes a Boolean value b and returns the integer $(-1)^b$. The dot notation b.toNat applies the library function Bool.toNat to b, turning false and true into 0 and 1. The tactic rfl proves an equality when both sides become identical after unfolding definitions and computing. Here, sign false computes to $(-1)^0=1$.

We separate the selected bit from the remaining bits:

abbrev State (m : ℕ) := Bool × BitVec m

ℕ (typed \N) is Mathlib’s notation for Nat. A State m pairs one Boolean coordinate with an $m$-bit word: $n=m+1$ bits in total. abbrev gives this type a convenient name. As in the warm-up, a pair is written (b, z), and .1 selects its first coordinate.

With this representation, x.1 is $\alpha\cdot x$ and (E x).1 is $\beta\cdot E(x)$. The two sums become:

def halfSum {m : ℕ} (E : State m → State m) (b : Bool) : ℤ :=
  ∑ z : BitVec m, sign (E (b, z)).1

def linearSum {m : ℕ} (E : State m → State m) : ℤ :=
  ∑ x : State m, sign x.1 * sign (E x).1

halfSum E b is $I_b=I_\beta(\mathcal{X}_b;E)$: it fixes the selected bit to b and sums over the remaining bits z. linearSum E is $L=L_{\alpha,\beta}(E)$, written with the product $(-1)^{\alpha\cdot x}(-1)^{\beta\cdot E(x)}$, which equals $(-1)^{\alpha\cdot x\oplus\beta\cdot E(x)}$.

The notation ∑ z : BitVec m, ..., with ∑ typed \sum, sums over every $m$-bit word. As in the warm-up, {m : ℕ} is an implicit argument, inferred from the type of E.

Both definitions accept any function. The permutation assumption belongs in the theorem, precisely where we need it. Selecting single bits keeps the code small. Other nonzero masks $\alpha$ and $\beta$ reduce to this case by an invertible linear change of coordinates on the input and output.

Building the complete proof

We organize the proof into the same two steps as the argument above, splitting and balance:

1. split_linear proves that linearSum E = halfSum E false - halfSum E true for any function E.
2. balanced_halves proves that halfSum E false + halfSum E true = 0 when E is bijective.

The downloadable file proves both facts. Their full proofs are below, so they can be inspected without interrupting the main argument.

theorem split_linear {m : ℕ} (E : State m → State m) :
    linearSum E = halfSum E false - halfSum E true := by
  simp only [linearSum, Fintype.sum_prod_type, Fintype.sum_bool,
    sign_false, sign_true, one_mul, neg_one_mul,
    Finset.sum_neg_distrib, halfSum]
  ring

theorem balanced_halves {m : ℕ} (E : State m → State m)
    (hE : Function.Bijective E) :
    halfSum E false + halfSum E true = 0 := by
  have reorder :
      (∑ x : State m, sign (E x).1) =
        ∑ y : State m, sign y.1 :=
    Equiv.sum_comp (Equiv.ofBijective E hE) (fun y => sign y.1)
  simpa [Fintype.sum_prod_type, halfSum, sign, add_comm] using reorder

The main theorem combines these facts with our first algebraic proof. Step through it with the buttons, or place the cursor on each line in the editor:

Each have proves one intermediate fact and adds it to the assumptions under the given name. The two new assumptions have exactly the form of the assumptions of halfspace_algebra, with halfSum E false, halfSum E true, and linearSum E in place of $I_0$, $I_1$, and $L$. So exact can finish the goal by applying halfspace_algebra. Each _ asks Lean to infer one of these three arguments. The proof follows the handwritten argument closely, with each intermediate fact checked separately.

We have proved a statement about every block size and every bijective E. The proof does not loop through possible ciphers or keys.

From an identity to divisibility

The identity has an immediate consequence:

In Lean, ∣ means “divides.” It is not the vertical bar on the keyboard; type it as \mid or \dvd. We add the divisibility hypothesis and reuse the identity:

theorem transfer_divisibility {m : ℕ} (E : State m → State m)
    (hE : Function.Bijective E) (t : ℕ)
    (hdiv : (2 : ℤ) ^ (t + 1) ∣ linearSum E) :
    (2 : ℤ) ^ t ∣ halfSum E false := by
  rw [halfspace_identity E hE, pow_succ'] at hdiv
  exact (mul_dvd_mul_iff_left (by norm_num : (2 : ℤ) ≠ 0)).mp hdiv

rw [...] at hdiv rewrites the hypothesis using two equalities: $L=2I_0$ and $2^{t+1}=2\cdot2^t$. It becomes $2\cdot2^t\mid2I_0$. The next line cancels the common nonzero factor. The library lemma states that this cancellation is valid, and .mp uses its forward implication. norm_num proves the numerical side condition $2\ne0$. The annotation (2 : ℤ) makes clear that this is integer divisibility.

For example, if $2^{10}$ divides $L$, then $2^9$ divides $I_0$, the signed integral sum over the halfspace $\mathcal{X}_0$. Also, $L=0$ gives $I_0=0$: the bit $\beta\cdot E(x)$ is balanced on $\mathcal{X}_0$. The same conclusions hold on $\mathcal{X}_1$ because $I_1=-I_0$.

The result is useful for keyed ciphers too. A block cipher is a family of permutations $E_K$, one for each key $K$, so the theorem applies to each $E_K$ separately. Lean can express this without enumerating the key space:

theorem all_keys {Key : Type} {m : ℕ}
    (E : Key → State m → State m)
    (hE : ∀ K, Function.Bijective (E K)) :
    ∀ K, linearSum (E K) = 2 * halfSum (E K) false := by
  intro K
  exact halfspace_identity (E K) (hE K)

Key : Type leaves the key type arbitrary. intro K fixes an arbitrary key for the proof of the ∀ statement. The function E K is $E_K$, encryption under that key. This illustrates how a general lemma becomes reusable across cipher families.

Finite checks and missing assumptions

Lean can also check finite claims by exact computation. For our three-bit illustration, define:

def toy (x : State 2) : State 2 :=
  (Bool.xor x.1 (x.2 == 3), x.2)

theorem toy_values :
    halfSum toy false = 2 ∧
    halfSum toy true = -2 ∧
    linearSum toy = 4 := by
  decide +kernel

.2 selects the two-bit word. == tests whether it equals binary 11, and Bool.xor flips the first bit in that case. The symbol ∧ (typed \and or \wedge) means “and.” For these finite statements, decide +kernel works like decide in the warm-up, but carries out the computation directly in Lean’s kernel. The tutorial also proves that applying toy twice returns the original state, establishing that it is a permutation.

This kind of finite proof is useful for small S-box identities and exact local table entries. Its cost grows with the computation. The symbolic halfspace proof above instead works at arbitrary block sizes without enumerating the inputs.

Now consider the constant function sending every input to zero. It is not a permutation. On three-bit inputs it has $I_0=I_1=4$ and $L=0$, so $L=2I_0$ is false. The tutorial includes a checked counterexample:

def constantMap (_ : State 2) : State 2 := (false, 0)

theorem missing_hypothesis_counterexample :
    linearSum constantMap = 0 ∧
    halfSum constantMap false = 4 ∧
    linearSum constantMap ≠ 2 * halfSum constantMap false := by
  decide +kernel

Here _ names an input that the function ignores, and ≠ (typed \ne) means “is not equal to.” Removing the bijectivity assumption from the general theorem would prevent the proof from using balanced_halves. This concrete counterexample explains why the assumption matters. A tactic failing on its own would only mean that the tactic did not complete the proof.

Checking and adapting the example

The editor checks the file while you work. To check the whole project from the command line, as a reviewer would, run this in the project folder:

lake build

The complete file wraps the examples in a namespace, a grouping of names that prevents collisions with other projects. Its module and public section lines make the file’s organization explicit and allow its results to be imported elsewhere. Its final commands include:

#print axioms halfspace_identity

This command lists the foundational assumptions on which the theorem depends. For this tutorial the list contains Lean’s standard propext, Classical.choice, and Quot.sound. There are no additional assumed cryptographic claims. Lean also permits an unfinished proof marker called sorry, so a file that merely opens or compiles is not necessarily a completed formalization. The supplied project treats warnings as errors and contains no such placeholders.

For a first exercise, change the toy permutation and prove its new sums. Then try proving $L=-2I_1$ from the same two helper lemmas. A completed proof of that second identity is included as other_half in the download.

When applying Lean to your own work, start with a small claim that later arguments rely on: a normalization identity, a local cipher property, or a conversion between two statistics. Write its assumptions explicitly, prove the needed intermediate facts, and give each result a mathematical name. Small checked results can then support larger arguments, while remaining understandable to a reader.

If your results are already written in LaTeX, Tex2Lean can help with a first draft. It uses a language model to read a paper, translate its results into a Lean project, and work on proofs that Lean then checks. It is designed mainly for papers about algorithms. The usual caution applies: Lean checks the proofs, but you still need to confirm that the translated definitions and statements say what the paper means, and that no sorry remains.

For further study, Theorem Proving in Lean introduces the language and proof methods. Mathematics in Lean develops practical examples with Mathlib. The goal is to make formal proof part of ordinary cryptanalytic work: an argument we can explain, inspect, and check again.