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

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.

def parallelizationAdversary (_G P : Type) : Type 1

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.

def parallelTestingAdversary (_G P : Type) : Type 1

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.

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