One-Way Functions and Trapdoor Permutations

This file defines one-way functions (OWFs) and one-way trapdoor permutations (OW-TDPs), along with their security experiments.

One-Way Functions

A function f : X → Y is one-way if no efficient adversary, given f(x) for a random x, can find any preimage x' with f(x') = f(x).

Trapdoor Permutations

A trapdoor permutation has a key generation algorithm that produces a public key pk and a secret key sk. The forward direction f(pk, ·) is a permutation that is hard to invert given only pk; the secret key enables efficient inversion via f⁻¹(sk, ·).

Main Definitions

• OWFAdversary X Y — an adversary trying to invert f.
• owfExp — the one-wayness experiment.
• TrapdoorPermutation PK SK X — a trapdoor permutation scheme.
• TDPAdversary PK X — an adversary trying to invert the TDP.
• tdpExp — the TDP inversion experiment.

One-Way Functions

def OneWay.OWFAdversary (X Y : Type) : Type

An OWF adversary receives f(x) and tries to find a preimage.

def OneWay.owfExp {X Y : Type} [SampleableType X] [DecidableEq Y] (f : X → Y) (adversary : OWFAdversary X Y) : ProbComp Bool

One-wayness experiment: sample x uniformly, give the adversary f(x), and check whether the adversary's output is a valid preimage.

noncomputable def OneWay.owfAdvantage {X Y : Type} [SampleableType X] [DecidableEq Y] (f : X → Y) (adversary : OWFAdversary X Y) : ENNReal

OWF advantage: the probability of successfully inverting f.

Trapdoor Permutations

structure OneWay.TrapdoorPermutation (PK SK X : Type) : Type

A trapdoor permutation with key spaces PK/SK and domain X. The forward direction is a permutation computable from the public key; the inverse requires the secret key (the trapdoor).

• keygen : ProbComp (PK × SK)
• forward : PK → X → X
• inverse : SK → X → X

def OneWay.TrapdoorPermutation.Correct {X PK SK : Type} (tdp : TrapdoorPermutation PK SK X) : Prop

A trapdoor permutation is correct if inversion recovers the original input for all honestly generated key pairs.

def OneWay.TDPAdversary (PK X : Type) : Type

A TDP adversary receives the public key and a challenge y = f(pk, x), and tries to find a valid preimage of y.

def OneWay.tdpExp {X PK SK : Type} [SampleableType X] [DecidableEq X] (tdp : TrapdoorPermutation PK SK X) (adversary : TDPAdversary PK X) : ProbComp Bool

TDP inversion experiment: generate keys, sample x uniformly, and check whether the adversary outputs a valid preimage of f(pk, x).

noncomputable def OneWay.tdpAdvantage {X PK SK : Type} [SampleableType X] [DecidableEq X] (tdp : TrapdoorPermutation PK SK X) (adversary : TDPAdversary PK X) : ENNReal

TDP advantage: the probability of successfully producing a valid preimage without the trapdoor.