§4.2: Integrity

An adversary who knows every mix node's private key cannot forge a header that N = r + 1 honest nodes all accept, except with the probability of solving Problem P. The paper's algebraic identity for the last hop's MAC (γ_N = a_0 ⊕ ⋯ ⊕ a_{N-1}) is taken as the hypothesis DecompositionWitness, and Problem P's hardness as ProblemPHard.

Honest per-hop processing along a forged α_0

Each hop advances α_i ↦ α_i^{hb(α_i, s_i)} with s_i = α_i^{x_{n_i}} (§3.6).

structure Cryptlib.Protocols.Sphinx.Integrity.Sys (F G : Type) : Type

The generator and the blinding random oracle hb (§3.1).

• g : G
• hb : G → G → F

def Cryptlib.Protocols.Sphinx.Integrity.alphaSeq {F G : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G) (privKeys : ℕ → F) (alpha0 : G) : ℕ → G

α_i: α_0 blinded through i hops with private keys privKeys.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.Sphinx.Integrity.alphaSeq S privKeys alpha0 0 = alpha0

def Cryptlib.Protocols.Sphinx.Integrity.sAt {F G : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G) (privKeys : ℕ → F) (alpha0 : G) (i : ℕ) : G

s_i = α_i^{x_{n_i}}.

Equations

• Cryptlib.Protocols.Sphinx.Integrity.sAt S privKeys alpha0 i = privKeys i • Cryptlib.Protocols.Sphinx.Integrity.alphaSeq S privKeys alpha0 i

Problem P (§4.2)

Given random oracles f_0, ..., f_{2^κ-1}, ρ̂, ρ0, find x, y with ρ̂(x) = f_{ρ0(x)}(y).

structure Cryptlib.Protocols.Sphinx.Integrity.ProblemPInstance (Seed Idx Yy Kappa : Type) : Type

An instance of Problem P.

• ρhat : Seed → Kappa
• ρ0 : Seed → Idx
• f : Idx → Yy → Kappa

def Cryptlib.Protocols.Sphinx.Integrity.ProblemPInstance.Solves {Seed Idx Yy Kappa : Type} (P : ProblemPInstance Seed Idx Yy Kappa) (xy : Seed × Yy) : Prop

(x, y) solves P iff ρ̂(x) = f_{ρ0(x)}(y).

Equations

• P.Solves xy = (P.ρhat xy.1 = P.f (P.ρ0 xy.1) xy.2)

@[reducible, inline]

abbrev Cryptlib.Protocols.Sphinx.Integrity.ProblemPAdversary (Seed Idx Yy Kappa : Type) : Type

A Problem P adversary: given the instance, output a candidate (x, y).

Equations

• Cryptlib.Protocols.Sphinx.Integrity.ProblemPAdversary Seed Idx Yy Kappa = (Cryptlib.Protocols.Sphinx.Integrity.ProblemPInstance Seed Idx Yy Kappa → ProbComp (Seed × Yy))

noncomputable def Cryptlib.Protocols.Sphinx.Integrity.problemPSuccessProb {Seed Idx Yy Kappa : Type} (P : ProblemPInstance Seed Idx Yy Kappa) (B : ProblemPAdversary Seed Idx Yy Kappa) : ENNReal

The adversary's success probability against a fixed instance.

Equations

• Cryptlib.Protocols.Sphinx.Integrity.problemPSuccessProb P B = probEvent (B P) fun (xy : Seed × Yy) => P.Solves xy

def Cryptlib.Protocols.Sphinx.Integrity.ProblemPHard {Seed Idx Yy Kappa : Type} (ε : ENNReal) : Prop

Hypothesis: Problem P is hard.

Equations

• One or more equations did not get rendered due to their size.

The integrity game and its reduction to Problem P

structure Cryptlib.Protocols.Sphinx.Integrity.Forgery (F G : Type) : Type

A forged header: N node private keys, all known to the adversary, and a forged α_0.

• privKeys : ℕ → F
• alpha0 : G

def Cryptlib.Protocols.Sphinx.Integrity.inducedInstance {Seed Idx Yy Kappa : Type} (ρhat0 : Seed → Kappa) (ρ0 : Seed → Idx) (f : Idx → Yy → Kappa) : ProblemPInstance Seed Idx Yy Kappa

The Problem P instance a successful N-hop forgery reduces to.

Equations

• Cryptlib.Protocols.Sphinx.Integrity.inducedInstance ρhat0 ρ0 f = { ρhat := ρhat0, ρ0 := ρ0, f := f }

def Cryptlib.Protocols.Sphinx.Integrity.Forgery.k0 {F G Seed : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G) (hρ : G → Seed) (fga : Forgery F G) : Seed

k_0 = hρ(s_0), Problem P's x.

Equations

• Cryptlib.Protocols.Sphinx.Integrity.Forgery.k0 S hρ fga = hρ (Cryptlib.Protocols.Sphinx.Integrity.sAt S fga.privKeys fga.alpha0 0)

def Cryptlib.Protocols.Sphinx.Integrity.DecompositionWitness {F G Seed Idx Yy Kappa : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G) (hρ : G → Seed) (ρhat0 : Seed → Kappa) (ρ0 : Seed → Idx) (f : Idx → Yy → Kappa) (Accepted : Forgery F G → Prop) : Prop

Every accepted forgery's k_0 has a Problem P witness y = (k_1, ..., k_{N-1}, k_μ).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Cryptlib.Protocols.Sphinx.Integrity.reductionAdversary {F G Seed Idx Yy Kappa : Type} [Field F] [AddCommGroup G] [Module F G] [Nonempty Yy] (S : Sys F G) (hρ : G → Seed) (ρhat0 : Seed → Kappa) (ρ0 : Seed → Idx) (f : Idx → Yy → Kappa) (Game : ProbComp (Forgery F G)) (Accepted : Forgery F G → Prop) (hDecomp : DecompositionWitness S hρ ρhat0 ρ0 f Accepted) : ProblemPAdversary Seed Idx Yy Kappa

The reduction adversary: replay the honest chain to compute k_0 and answer with the witness from hDecomp.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Protocols.Sphinx.Integrity.integrity_bound {F G Seed Idx Yy Kappa : Type} [Field F] [AddCommGroup G] [Module F G] [Nonempty Yy] (S : Sys F G) (hρ : G → Seed) (ρhat0 : Seed → Kappa) (ρ0 : Seed → Idx) (f : Idx → Yy → Kappa) (ε : ENNReal) (hhard : ProblemPHard ε) (Game : ProbComp (Forgery F G)) (Accepted : Forgery F G → Prop) (hDecomp : DecompositionWitness S hρ ρhat0 ρ0 f Accepted) : probEvent Game Accepted ≤ ε

§4.2's bound: given hDecomp, the probability that Game accepts a forgery is bounded by Problem P's hardness.

@[reducible, inline]

abbrev Cryptlib.Protocols.Sphinx.Integrity.IntegrityBoundType {F G Seed Idx Yy Kappa : Type} [Field F] [AddCommGroup G] [Module F G] [Nonempty Yy] (S : Sys F G) (hρ : G → Seed) (ρhat0 : Seed → Kappa) (ρ0 : Seed → Idx) (f : Idx → Yy → Kappa) : Prop

The statement of integrity_bound.

Equations

• One or more equations did not get rendered due to their size.