§4.4: Indistinguishability of forward and reply messages

Models the first challenge hop's tuple ((α0,β0,γ0),δ0) over a generic DDH group with ρ/μ/π as PRGs; the paper reduces general j to j = 0. Assumptions: DDH, and that hρ, hμ, hπ at a fresh s0 are jointly pseudorandom (jointKeyPRG). General j and reply-vs-nymserver indistinguishability are not mechanized.

structure Cryptlib.Protocols.Sphinx.Indistinguishability.Sys (F G Seed KeyMu KeyPi Beta Gamma Delta : Type) : Type

§3.1's system parameters: the generator g, the random oracles hρ, hμ, hπ, and ρ/μ/π.

• g : G
• hρ : G → Seed
• hμ : G → KeyMu
• hπ : G → KeyPi
• ρgen : Seed → Beta
• μeval : KeyMu → Beta → Gamma
• πenc : KeyPi → Delta → Delta

structure Cryptlib.Protocols.Sphinx.Indistinguishability.Choice (Beta Delta : Type) : Type

The two challenge branches: the routing plaintext XORed into β0, and δ0's plaintext.

• betaPt : Beta
• deltaPt : Delta

def Cryptlib.Protocols.Sphinx.Indistinguishability.buildFrom {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (α0 s0 : G) (c : Choice Beta Delta) : G × Beta × Gamma × Delta

Hop 0's tuple ((α0,β0,γ0),δ0) from α0 = x • g and s0.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.buildFrom S α0 s0 c = (α0, c.betaPt + S.ρgen (S.hρ s0), S.μeval (S.hμ s0) (c.betaPt + S.ρgen (S.hρ s0)), S.πenc (S.hπ s0) c.deltaPt)

@[reducible, inline]

abbrev Cryptlib.Protocols.Sphinx.Indistinguishability.Adversary {G Beta Gamma Delta : Type} : Type

An adversary that guesses which challenge branch produced hop 0's tuple.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.Adversary = (G × Beta × Gamma × Delta → ProbComp Bool)

def Cryptlib.Protocols.Sphinx.Indistinguishability.gameReal {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] (A : Adversary) (c0 c1 : Choice Beta Delta) : ProbComp Bool

Game G (§4.4) at j = 0: hop 0's tuple built from branch b with the real DH secret.

Equations

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

def Cryptlib.Protocols.Sphinx.Indistinguishability.game2 {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] (A : Adversary) (c0 c1 : Choice Beta Delta) : ProbComp Bool

Game G2: s0 replaced by an independent random group element.

Equations

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

noncomputable def Cryptlib.Protocols.Sphinx.Indistinguishability.advantage {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] (A : Adversary) (c0 c1 : Choice Beta Delta) : ℝ

The adversary's advantage in game G over a coin flip.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.advantage S A c0 c1 = |Pr[= true | Cryptlib.Protocols.Sphinx.Indistinguishability.gameReal S A c0 c1].toReal - 1 / 2|

def Cryptlib.Protocols.Sphinx.Indistinguishability.ddhAdversaryOf {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (A : Adversary) (c0 c1 : Choice Beta Delta) : DiffieHellman.DDHAdversary F G

The DDH adversary built from an Adversary.

Equations

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

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_gameReal_eq_ddhExpReal {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] (A : Adversary) (c0 c1 : Choice Beta Delta) : Pr[= true | gameReal S A c0 c1] = Pr[= true | DiffieHellman.ddhExpReal S.g (ddhAdversaryOf S A c0 c1)]

ddhExpReal equals gameReal.

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_game2_eq_ddhExpRand {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] (A : Adversary) (c0 c1 : Choice Beta Delta) : Pr[= true | game2 S A c0 c1] = Pr[= true | DiffieHellman.ddhExpRand S.g (ddhAdversaryOf S A c0 c1)]

ddhExpRand equals game2.

def Cryptlib.Protocols.Sphinx.Indistinguishability.buildFromKeys {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (α0 : G) (seed : Seed) (kmu : KeyMu) (kpi : KeyPi) (c : Choice Beta Delta) : G × Beta × Gamma × Delta

buildFrom with the three oracle outputs as arguments.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.buildFromKeys S α0 seed kmu kpi c = (α0, c.betaPt + S.ρgen seed, S.μeval kmu (c.betaPt + S.ρgen seed), S.πenc kpi c.deltaPt)

@[simp]

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.buildFrom_eq_buildFromKeys {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (α0 s0 : G) (c : Choice Beta Delta) : buildFrom S α0 s0 c = buildFromKeys S α0 (S.hρ s0) (S.hμ s0) (S.hπ s0) c

def Cryptlib.Protocols.Sphinx.Indistinguishability.game2' {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType (Seed × KeyMu × KeyPi)] (A : Adversary) (c0 c1 : Choice Beta Delta) : ProbComp Bool

Game G2': the three oracle outputs replaced by an independent uniform triple.

Equations

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

def Cryptlib.Protocols.Sphinx.Indistinguishability.jointKeyPRG {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) : PRGScheme F (Seed × KeyMu × KeyPi)

The map c' ↦ (hρ(c'•g), hμ(c'•g), hπ(c'•g)) as a PRG; G2 and G2' are its real and ideal experiments.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.jointKeyPRG S = { gen := fun (c' : F) => (S.hρ (c' • S.g), S.hμ (c' • S.g), S.hπ (c' • S.g)) }

def Cryptlib.Protocols.Sphinx.Indistinguishability.jointAdversaryOf {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (A : Adversary) (c0 c1 : Choice Beta Delta) (x : F) : PRGScheme.PRGAdversary (Seed × KeyMu × KeyPi)

The jointKeyPRG reduction adversary.

Equations

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

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_game2_eq_prgRealExp_joint {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] (A : Adversary) (c0 c1 : Choice Beta Delta) : Pr[= true | game2 S A c0 c1] = Pr[= true | do let x ← $ᵗ F (jointKeyPRG S).prgRealExp (jointAdversaryOf S A c0 c1 x)]

The jointKeyPRG real experiment equals game2.

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_game2'_eq_prgIdealExp_joint {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType (Seed × KeyMu × KeyPi)] (A : Adversary) (c0 c1 : Choice Beta Delta) : Pr[= true | game2' S A c0 c1] = Pr[= true | do let x ← $ᵗ F PRGScheme.prgIdealExp (jointAdversaryOf S A c0 c1 x)]

The jointKeyPRG ideal experiment equals game2'.

def Cryptlib.Protocols.Sphinx.Indistinguishability.combinedGen {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (c : Choice Beta Delta) (p : Seed × KeyMu × KeyPi) : Beta × Gamma × Delta

ρ/μ/π combined into one PRG (seed, kmu, kpi) ↦ (β0, γ0, δ0) for a fixed branch c.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.combinedGen S c p = (c.betaPt + S.ρgen p.1, S.μeval p.2.1 (c.betaPt + S.ρgen p.1), S.πenc p.2.2 c.deltaPt)

def Cryptlib.Protocols.Sphinx.Indistinguishability.combinedPRG {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (c : Choice Beta Delta) : PRGScheme (Seed × KeyMu × KeyPi) (Beta × Gamma × Delta)

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.combinedPRG S c = { gen := Cryptlib.Protocols.Sphinx.Indistinguishability.combinedGen S c }

def Cryptlib.Protocols.Sphinx.Indistinguishability.combinedAdversaryOf {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) (A : Adversary) (x : F) (b : Bool) : PRGScheme.PRGAdversary (Beta × Gamma × Delta)

The combined-PRG reduction adversary.

Equations

• Cryptlib.Protocols.Sphinx.Indistinguishability.combinedAdversaryOf S A x b t = do let guess ← A (x • S.g, t.1, t.2.1, t.2.2) pure (b == guess)

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_game2'_eq_prgRealExp_combined {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType (Seed × KeyMu × KeyPi)] (A : Adversary) (c0 c1 : Choice Beta Delta) : Pr[= true | game2' S A c0 c1] = Pr[= true | do let x ← $ᵗ F let b ← $ᵗ Bool (combinedPRG S (if b = true then c1 else c0)).prgRealExp (combinedAdversaryOf S A x b)]

def Cryptlib.Protocols.Sphinx.Indistinguishability.game3 {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType (Beta × Gamma × Delta)] (A : Adversary) (_c0 _c1 : Choice Beta Delta) : ProbComp Bool

Game G3: β0, γ0, δ0 replaced by an independent uniform triple.

Equations

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

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_game3_eq_prgIdealExp_combined {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType (Beta × Gamma × Delta)] (A : Adversary) (c0 c1 : Choice Beta Delta) : Pr[= true | game3 S A c0 c1] = Pr[= true | do let x ← $ᵗ F let b ← $ᵗ Bool PRGScheme.prgIdealExp (combinedAdversaryOf S A x b)]

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.probTrue_game3 {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType (Beta × Gamma × Delta)] (A : Adversary) [∀ (v : G × Beta × Gamma × Delta), NeverFail (A v)] (c0 c1 : Choice Beta Delta) : Pr[= true | game3 S A c0 c1].toReal = 1 / 2

In G3 a NeverFail adversary guesses b with probability exactly 1/2.

theorem Cryptlib.Protocols.Sphinx.Indistinguishability.advantage_le {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType Beta] [SampleableType Gamma] [SampleableType Delta] [SampleableType (Seed × KeyMu × KeyPi)] (A : Adversary) [∀ (v : G × Beta × Gamma × Delta), NeverFail (A v)] (c0 c1 : Choice Beta Delta) (εDDH εJoint εPRG : ℝ) (hddh : DiffieHellman.ddhDistAdvantage S.g (ddhAdversaryOf S A c0 c1) ≤ εDDH) (hjointPRG : |Pr[= true | game2 S A c0 c1].toReal - Pr[= true | game2' S A c0 c1].toReal| ≤ εJoint) (hprg : |Pr[= true | game2' S A c0 c1].toReal - Pr[= true | game3 S A c0 c1].toReal| ≤ εPRG) : advantage S A c0 c1 ≤ εDDH + εJoint + εPRG

§4.4: the advantage is bounded by the DDH advantage (hddh), the joint-key PRG advantage (hjointPRG), and the combined ρ/μ/π PRG advantage (hprg).

@[reducible, inline]

abbrev Cryptlib.Protocols.Sphinx.Indistinguishability.AdvantageLeType {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] (S : Sys F G Seed KeyMu KeyPi Beta Gamma Delta) [SampleableType F] [SampleableType Beta] [SampleableType Gamma] [SampleableType Delta] [SampleableType (Seed × KeyMu × KeyPi)] : Prop

The statement of advantage_le.

Equations

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