Fujisaki-Okamoto Shared Definitions

This file defines the shared objects used by the Fujisaki-Okamoto transform:

• explicit-coins PKEs as a specialization of AsymmEncAlg
• the induced randomized AsymmEncAlg
• spread notions and OW-CPA games for the ProbComp specialization
• OW-PCVA games for the general monadic interface

def AsymmEncAlg.ExplicitCoins.deltaCorrect {M PK SK R C : Type} (pke : ExplicitCoins ProbComp M PK SK R C) [DecidableEq M] [SampleableType R] (delta : ENNReal) : Prop

delta-correctness: failure in the canonical AsymmEncAlg.CorrectExp experiment occurs with probability at most delta.

def AsymmEncAlg.ExplicitCoins.gammaSpread {M PK SK R C : Type} (pke : ExplicitCoins ProbComp M PK SK R C) [SampleableType R] [DecidableEq C] (gamma : ENNReal) : Prop

gamma-spread: no ciphertext occurs with probability more than gamma for any fixed public key and plaintext.

def AsymmEncAlg.ExplicitCoins.OW_CPA_oracleSpec {M PK SK R C : Type} (_pke : ExplicitCoins ProbComp M PK SK R C) : OracleSpec (ℕ ⊕ M)

Oracle interface for the one-way under chosen-plaintext attack (OW-CPA) game.

The sum unifSpec + (M →ₒ C) gives the adversary two capabilities:

• unrestricted uniform sampling from any sampleable type
• an encryption oracle on chosen plaintexts M → C

@[reducible, inline]

abbrev AsymmEncAlg.ExplicitCoins.OW_CPA_Adversary {M PK SK R C : Type} (pke : ExplicitCoins ProbComp M PK SK R C) : Type

An OW-CPA adversary gets pk, a challenge ciphertext, and oracle access to chosen-plaintext encryptions.

def AsymmEncAlg.ExplicitCoins.OW_CPA_queryImpl {M PK SK R C : Type} (pke : ExplicitCoins ProbComp M PK SK R C) [SampleableType R] (pk : PK) : QueryImpl pke.OW_CPA_oracleSpec ProbComp

Implementation of the OW-CPA encryption oracle.

def AsymmEncAlg.ExplicitCoins.OW_CPA_Game {M PK SK R C : Type} (pke : ExplicitCoins ProbComp M PK SK R C) [SampleableType M] [SampleableType R] [DecidableEq M] (adversary : pke.OW_CPA_Adversary) : ProbComp Bool

Main one-way under chosen-plaintext attack (OW-CPA) experiment.

The game samples a fresh keypair and a uniform challenge message, forms the honest challenge ciphertext via the induced randomized AsymmEncAlg, runs the adversary with oracle access described by OW_CPA_oracleSpec, and returns true exactly when the adversary recovers the challenge message.

noncomputable def AsymmEncAlg.ExplicitCoins.OW_CPA_Advantage {M PK SK R C : Type} (pke : ExplicitCoins ProbComp M PK SK R C) [SampleableType M] [SampleableType R] [DecidableEq M] (adversary : pke.OW_CPA_Adversary) : ENNReal

OW-CPA advantage is the probability of recovering the sampled challenge plaintext.

def OW_PCVA_oracleSpec {ι : Type u} {spec : OracleSpec ι} {M PK SK C : Type} (_encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) : OracleSpec (ι ⊕ C × M ⊕ C)

Oracle interface for the one-way under plaintext-checking and validity attacks (OW-PCVA) game.

The sum spec + (((C × M) →ₒ Bool) + (C →ₒ Bool)) has three components:

• the ambient oracle interface spec
• a plaintext-checking oracle sending (c, msg) to whether c decrypts to msg
• a validity oracle sending c to whether c decrypts to some plaintext at all

@[reducible, inline]

abbrev OW_PCVA_Adversary {ι : Type u} {spec : OracleSpec ι} {M PK SK C : Type} (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) : Type u

An OW-PCVA adversary gets the public key and challenge ciphertext, and outputs a plaintext guess after querying the plaintext-checking and validity oracles.

def OW_PCVA_queryImpl {ι : Type u} {spec : OracleSpec ι} {M PK SK C : Type} (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) [DecidableEq M] (sk : SK) : QueryImpl (OW_PCVA_oracleSpec encAlg) (OracleComp spec)

Oracle implementation for OW-PCVA.

def OW_PCVA_Game {ι : Type u} {spec : OracleSpec ι} {M PK SK C : Type} {encAlg : AsymmEncAlg (OracleComp spec) M PK SK C} [SampleableType M] [DecidableEq M] (runtime : ProbCompRuntime (OracleComp spec)) (adversary : OW_PCVA_Adversary encAlg) : SPMF Bool

Main one-way under plaintext-checking and validity attacks (OW-PCVA) experiment.

The game generates a keypair, samples a uniform challenge message, encrypts it honestly, and then runs the adversary on the public key and challenge ciphertext. The adversary may query the ambient oracle interface spec, the plaintext-checking oracle, and the validity oracle, and the game returns true exactly when the final guess equals the hidden challenge message.

noncomputable def OW_PCVA_Advantage {ι : Type u} {spec : OracleSpec ι} {M PK SK C : Type} {encAlg : AsymmEncAlg (OracleComp spec) M PK SK C} [SampleableType M] [DecidableEq M] (runtime : ProbCompRuntime (OracleComp spec)) (adversary : OW_PCVA_Adversary encAlg) : ENNReal

OW-PCVA advantage is the message-recovery probability in the above game.