Hard Homogeneous Spaces

This file builds up the definition of security experiments for hard homogeneous spaces. We represent these spaces as an AddTorsor G P, i.e. a group G acting freely and transitively (equivalently bijectively) on the underlying set of points P.

If the AddTorsor is the action of exponention on a finite field these reduce to classical discrete log based assumptions.

def vectorizationAdversary (G P : Type) : Type 1

Equations

• vectorizationAdversary G P = (P → P → ProbComp G)

def vectorizationExp {G P : Type} [AddCommGroup G] [AddTorsor G P] [OracleComp.SelectableType P] [DecidableEq G] (adversary : vectorizationAdversary G P) : ProbComp Unit

Adversary tries to determine a vector between the two points. Generalization of discrete log problem where the vector is the exponent.

Equations

• vectorizationExp adversary = do let p₁ ← $ᵗP let p₂ ← $ᵗP let g ← adversary p₁ p₂ guard (p₂ -ᵥ p₁ = g)

def parallelizationAdversary (_G P : Type) : Type 1

Equations

• parallelizationAdversary _G P = (P → P → P → ProbComp P)

def parallelizationExp {G P : Type} [AddCommGroup G] [AddTorsor G P] [OracleComp.SelectableType P] [OracleComp.SelectableType G] [DecidableEq P] (adversary : parallelizationAdversary G P) : ProbComp Unit

Adversary tries to determine a point completing a parallelogram in point space. Analogue of the Diffie-Hellman problem.

Equations

• parallelizationExp adversary = do let x ← $ᵗP let g₁ ← $ᵗG let g₂ ← $ᵗG let x₁ : P := g₁ +ᵥ x let x₂ : P := g₂ +ᵥ x let x₃ ← adversary x x₁ x₂ guard (x₃ = g₁ +ᵥ g₂ +ᵥ x)

def parallelTestingAdversary (_G P : Type) : Type 1

Equations

• parallelTestingAdversary _G P = (P → P → P → P → ProbComp Bool)

def parallelTesting_experiment {G P : Type} [AddCommGroup G] [AddTorsor G P] [OracleComp.SelectableType P] [OracleComp.SelectableType G] [DecidableEq G] (adversary : parallelTestingAdversary G P) : ProbComp Unit

Adversary tries to tell if a set of points form a parallelogram in point space. Analogue of the decisional Diffie-Hellman problem.

Equations

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

noncomputable def parallelTestingAdvantage {G P : Type} [AddCommGroup G] [AddTorsor G P] [OracleComp.SelectableType P] [OracleComp.SelectableType G] [DecidableEq G] (adversary : parallelTestingAdversary G P) : ENNReal

Equations

• parallelTestingAdvantage adversary = [=()|parallelTesting_experiment adversary] - 1 / 2