CryptoSecProofs

A Lean 4 library for cryptographic security proofs.

Overview

The files in the main CryptoSecProofs folder are organized as follows.

Root files

• ToMathlib.lean: General lemmas that don't fit anywhere else and could potentially be pushed to Mathlib.
• Negligible.lean: Some results about negligible functions. It includes the proof of a theorem by Bellare about the equivalence of two definitions of negligibility for a family of functions (namely, Theorem 3.2 from https://eprint.iacr.org/1997/004.pdf).
• Probability.lean: General results about probabilities. For example, we prove that if f : α → β is bijective, then drawing a uniformly from α and applying f yields the uniform distribution on β.

Hard Problems

This folder contains files defining hardness assumptions:

• CyclicGroups.lean: Hard problems in cyclic groups (discrete logarithm, CDH, DDH...).

Cryptosystems

This folder contains files defining various cryptographic primitives and schemes and related security proofs.

PKE

Public key encryption schemes:

• Defs.lean: Basic definitions about public-key encryption schemes (syntax, correctness, IND-CPA security).
• ElGamal.lean: The (basic) ElGamal public-key encryption scheme. We prove correctness and IND-CPA security. Inspired from the cryptolib library by Joey Lupo (which was written in Lean3).

Prerequisites

First, you need to install Lean4 on your machine.

Setup

Then, clone this repository and, from the root of the project, run

lake exe cache get
lake build

Lean resources

• Mathematics in Lean
• The Natural Number Game
• Theorem Proving in Lean 4
• Functional Programming in Lean
• Formalising Mathematics (by Kevin Buzzard)
• The Mechanics of Proof (by Heather Macbeth)
• An introduction to Lean 4 (by E. Cosme Llópez)
• Lean 4 Crash Course
• Common Lean Pitfalls
• Style guidelines
• Documentation guidelines