Learning With Errors

This file gives a general definition of the LWE problem. It is parameterized by the following:

• n: the dimension of the secret
• m: the number of samples
• p: the modulus (not necessarily prime)
• errSamp : ProbComp (Fin p): a probabilistic sampling algorithm for the error

(errSamp can potentially be replaced with χ : PMF (Fin p) instead, to be used with evalDistWhen with non-uniform distributions)

We define the (decision) LWE problem as a security experiment on an oracle that takes as input:

• A matrix A : Fin m → Fin n → Fin p
• A vector u : Fin m → Fin p, either sampled uniformly at random, or sampled from the LWE distribution s * A + e, where s : Fin n → Fin p is the secret and e : Fin m → Fin p has every entry sampled from errSamp.

The adversary wins if it can correctly guess which case the distribution is.

The search LWE problem instead asks that the adversary given A and u = s * A + e outputs the secret s.

def LWE_Distr (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p)) : ProbComp (Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m)

The LWE distribution (A, s * A + e)

def LWE_Uniform_Distr (n m p : ℕ) [NeZero p] : ProbComp (Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m)

The uniform distribution (A, u)

def LWE_Adversary (n m p : ℕ) : Type 1

An adversary for the decisional LWE problem. Takes in a pair (A, u) and outputs a boolean.

def LWE_Experiment (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p)) (adv : LWE_Adversary n m p) : ProbComp Bool

The decisional LWE experiment. If b = true, the distribution is LWE, otherwise it is uniform.

noncomputable def LWE_Advantage (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p)) (adv : LWE_Adversary n m p) : ℝ

def LWE_Game_0 (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p)) (adv : LWE_Adversary n m p) : ProbComp Bool

The first game of the decisional LWE assumption, where the distribution is LWE.

(we map true to () and false to failure)

def LWE_Game_1 (n m p : ℕ) [NeZero p] (adv : LWE_Adversary n m p) : ProbComp Bool

The second game of the decisional LWE assumption, where the distribution is uniform.

(we map true to () and false to failure)

def LWE_Search_Adversary (n m p : ℕ) : Type 1

An adversary for the search LWE problem. Takes in a pair (A, u) and outputs a vector s.

def LWE_Search_Experiment (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p)) (adv : LWE_Search_Adversary n m p) : ProbComp Bool

The search LWE experiment. The adversary wins if it can correctly guess the secret s.

noncomputable def LWE_Search_Advantage (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p)) (adv : LWE_Search_Adversary n m p) : ℝ

theorem LWE_Experiment_eq_LWE_Game_01 {n m p : ℕ} [NeZero p] {errSamp : ProbComp (Fin p)} {adv : LWE_Adversary n m p} : 2 * (LWE_Experiment n m p errSamp adv).advantage' = (LWE_Game_0 n m p errSamp adv).advantage₂' (LWE_Game_1 n m p adv)

The two ways of defining the decisional LWE assumption (via a single experiment or via two games) are equivalent.

(probably not correct)