Lamport signature

DefinitionLamport public key#✓fully proved

For a function \(f : X \to Y\) and a secret key \(sk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to X\), the public key is the map \(pk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to Y\) with \(pk(i, b) = f(sk(i, b))\).

def publicKey (sk : Fin ℓ × Bool → X) : Fin ℓ × Bool → Y := fun ib => f (sk ib)

Used by 4

Used byOne-time forgery game · Security reduction for Lamport one-time signatures · Correctness of Lamport signatures · Winning the Lamport one-time forgery game

DefinitionLamport signing#✓fully proved

The signature of a message \(m \in \{0, 1\}^\ell\) under a secret key \(sk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to X\) is \(\sigma \in X^\ell\) with \(\sigma_i = sk(i, m_i)\) for every position \(i < \ell\).

def sign (sk : Fin ℓ × Bool → X) (m : Fin ℓ → Bool) : Fin ℓ → X := fun i => sk (i, m i)

Used by 5

Used byOne-time forgery game · Security reduction for Lamport one-time signatures · Inverter built from a forger · Correctness of Lamport signatures · Winning the Lamport one-time forgery game

DefinitionLamport verification#✓fully proved

Let \(f : X \to Y\). A signature \(\sigma \in X^\ell\) on a message \(m \in \{0, 1\}^\ell\) is valid for a public key \(pk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to Y\) when \(f(\sigma_i) = pk(i, m_i)\) for every position \(i < \ell\).

def Verify (pk : Fin ℓ × Bool → Y) (m : Fin ℓ → Bool) (σ : Fin ℓ → X) : Prop :=
  ∀ i, f (σ i) = pk (i, m i)

Used by 4

Used byOne-time forgery game · Security reduction for Lamport one-time signatures · Correctness of Lamport signatures · Winning the Lamport one-time forgery game

TheoremCorrectness of Lamport signatures#✓fully proved

Let \(f : X \to Y\). For every secret key \(sk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to X\) and every message \(m \in \{0, 1\}^\ell\), the Lamport signature of \(m\) under \(sk\) is valid for \(m\) under the public key of \(sk\).

theorem verify_sign (sk : Fin ℓ × Bool → X) (m : Fin ℓ → Bool) :
    Verify f (publicKey f sk) m (sign sk m)

Uses 3

Statement usesLamport verification · Lamport public key · Lamport signing

StructureOne-time forger#✓fully proved

A one-time forger for messages of length \(\ell\), with random coins in a set \(R\), consists of two maps. The first takes a public key \(pk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to Y\) and coins \(r \in R\) and returns the message \(m \in \{0, 1\}^\ell\) whose signature the forger requests. The second takes a public key, a signature \(\sigma \in X^\ell\) and coins \(r\) and returns a message \(m' \in \{0, 1\}^\ell\) together with a signature \(\sigma' \in X^\ell\).

structure Forger (X Y R : Type*) (ℓ : ℕ) where
  /-- The message whose signature the forger requests. -/
  choose : (Fin ℓ × Bool → Y) → R → Fin ℓ → Bool
  /-- The forgery. -/
  forge : (Fin ℓ × Bool → Y) → (Fin ℓ → X) → R → (Fin ℓ → Bool) × (Fin ℓ → X)

Used by 4

Used byOne-time forgery game · Security reduction for Lamport one-time signatures · Inverter built from a forger · Winning the Lamport one-time forgery game

DefinitionWinning the Lamport one-time forgery game#✓fully proved

Let \(X\) be a nonempty finite set, \(Y\) a set with decidable equality, \(f : X \to Y\) a function, and \(\ell\) a message length; messages are bit strings \(m = (m_0, \dots, m_{\ell-1})\). A one-time forger \(A\) with random coins from a nonempty finite set \(R\) wins against a secret key \(sk\), which assigns \(sk(i, b) \in X\) to each position \(i < \ell\) and bit \(b\), with coins \(r \in R\) when the following holds. Let \(pk\) be the public key of \(sk\), given by \(pk(i, b) = f(sk(i, b))\); let \(m\) be the message that \(A\) chooses from \(pk\) and \(r\); and let \((m', \sigma')\) be the message and signature that \(A\) outputs from \(pk\), the signature \(i \mapsto sk(i, m_i)\) of \(m\) under \(sk\), and \(r\). Then \(m' \ne m\), and \(\sigma'\) is a valid signature on \(m'\) for \(pk\): \(f(\sigma'_i) = pk(i, m'_i)\) for every \(i < \ell\).

def Forger.Wins (A : Forger X Y R ℓ) (sk : Fin ℓ × Bool → X) (r : R) : Prop :=
  (A.forge (publicKey f sk) (sign sk (A.choose (publicKey f sk) r)) r).1 ≠
      A.choose (publicKey f sk) r ∧
    Verify f (publicKey f sk) (A.forge (publicKey f sk) (sign sk (A.choose (publicKey f sk) r)) r).1
      (A.forge (publicKey f sk) (sign sk (A.choose (publicKey f sk) r)) r).2

Uses 4 · Used by 2

Statement usesOne-time forger · Lamport verification · Lamport public key · Lamport signing

Used byOne-time forgery game · Security reduction for Lamport one-time signatures

DefinitionOne-time forgery game#✓fully proved

Let \(f : X \to Y\) with \(X\) finite and nonempty, and let \(A\) be a one-time forger for messages of length \(\ell\) with random coins in a finite nonempty set \(R\). The one-time forgery game is the distribution on \(\{\mathrm{true}, \mathrm{false}\}\) obtained by drawing a secret key \(sk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to X\) and coins \(r \in R\) uniformly and independently, and returning whether \(A\) wins against \(sk\) with coins \(r\).

noncomputable def forgeGame (A : Forger X Y R ℓ) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype ((Fin ℓ × Bool → X) × R)).map fun ω =>
    decide (A.Wins f ω.1 ω.2)

Uses 5 · Used by 1

Statement usesOne-time forger · Winning the Lamport one-time forgery game · Lamport verification · Lamport public key · Lamport signing

Used bySecurity reduction for Lamport one-time signatures

DefinitionOne-wayness game#✓fully proved

Let \(f : X \to Y\) with \(X\) finite and nonempty, and let \(I\) be an inverter with random coins in a finite nonempty set \(\Omega\): given \(y \in Y\) and coins \(\omega \in \Omega\) it either outputs some \(x' \in X\) or fails. The one-wayness game for \(f\) is the distribution on \(\{\mathrm{true}, \mathrm{false}\}\) obtained by drawing \(x \in X\) and \(\omega \in \Omega\) uniformly and independently and returning true exactly when \(I\), run on \(f(x)\) with coins \(\omega\), outputs some \(x'\) with \(f(x') = f(x)\).

noncomputable def invertGame {Ω : Type*} [Fintype Ω] [Nonempty Ω] (I : Y → Ω → Option X) :
    PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (X × Ω)).map fun ω =>
    match I (f ω.1) ω.2 with
    | some x' => decide (f x' = f ω.1)
    | none => false

Used by 1

Used bySecurity reduction for Lamport one-time signatures

DefinitionPlanted public key#✓fully proved

Let \(f : X \to Y\). Given a secret key \(sk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to X\), a position \((i, b)\) and a value \(y \in Y\), the planted public key takes the value \(y\) at \((i, b)\) and the value \(f(sk(j, c))\) at every other position \((j, c)\).

def plant (sk : Fin ℓ × Bool → X) (ib : Fin ℓ × Bool) (y : Y) : Fin ℓ × Bool → Y :=
  fun jc => if jc = ib then y else f (sk jc)

Used by 2

Used bySecurity reduction for Lamport one-time signatures · Inverter built from a forger

DefinitionInverter built from a forger#✓fully proved

Let \(f : X \to Y\), let \(A\) be a one-time forger for messages of length \(\ell\) with coins in \(R\), and let \(y \in Y\). The inverter's coins are a position \((i, b)\) with \(i < \ell\) and \(b \in \{0, 1\}\), a secret key \(sk : \{0, \dots, \ell - 1\} \times \{0, 1\} \to X\) and forger coins \(r \in R\). It forms the public key \(pk\) with \(pk(i, b) = y\) and \(pk(j, c) = f(sk(j, c))\) for every other \((j, c)\), and runs \(A\) on \(pk\) with coins \(r\) to obtain the message \(m\) whose signature \(A\) requests. If \(m_i = b\) it fails. Otherwise it hands \(A\) the signature \((sk(j, m_j))_{j < \ell}\) of \(m\) under \(sk\) and obtains a forgery \((m', \sigma')\); it outputs \(\sigma'_i\) if \(m'_i = b\) and fails otherwise.

def invert (A : Forger X Y R ℓ) (y : Y) (ω : (Fin ℓ × Bool) × (Fin ℓ × Bool → X) × R) :
    Option X :=
  if A.choose (plant f ω.2.1 ω.1 y) ω.2.2 ω.1.1 = ω.1.2 then none
  else if (A.forge (plant f ω.2.1 ω.1 y) (sign ω.2.1 (A.choose (plant f ω.2.1 ω.1 y) ω.2.2))
      ω.2.2).1 ω.1.1 = ω.1.2 then
    some ((A.forge (plant f ω.2.1 ω.1 y) (sign ω.2.1 (A.choose (plant f ω.2.1 ω.1 y) ω.2.2))
      ω.2.2).2 ω.1.1)
  else none

Uses 3 · Used by 1

Statement usesOne-time forger · Planted public key · Lamport signing

Used bySecurity reduction for Lamport one-time signatures

TheoremSecurity reduction for Lamport one-time signatures#✓fully proved

Let \(f : X \to Y\) be a function on a finite nonempty set \(X\), let \(\ell \ge 1\) be the message length, and let \(A\) be a one-time forger whose random coins range over a finite nonempty set \(R\). Then the probability that \(A\) wins the one-time forgery game against the Lamport scheme built from \(f\) is at most \(2\ell\) times the probability that the inverter built from \(A\) wins the one-wayness game for \(f\).

This is the reduction behind Katz and Lindell, Theorem 12.16: if \(f\) is one-way, then Lamport's scheme is one-time secure.

theorem forgeGame_le [NeZero ℓ] (A : Forger X Y R ℓ) :
    (forgeGame f A true).toReal ≤ 2 * ℓ * (invertGame f (invert f A) true).toReal

Uses 9

Statement usesOne-time forger · One-time forgery game · Inverter built from a forger · One-wayness game

Proof usesWinning the Lamport one-time forgery game · Lamport verification · Planted public key · Lamport public key · Lamport signing

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.