2.2. Random Oracle KDF
An oracle type I -> K implemented by VCV-io's randomOracle
(lazy cached uniform sampling). Used in the security proofs
(passive message secrecy), where the KDF is modeled as a random
oracle per the paper's assumption 4 (section 2.5).
Code for Definition2.2●1 definition
Associated Lean declarations
-
KDFOracle[complete]
Associated Lean declarations
-
KDFOracle[complete]
-
def KDFOracle (I
TypeKType: TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.) : OracleSpecOracleSpec.{u, v} (ι : Type u) : Type (max u (v + 1))An `OracleSpec ι` is specieifes a set of oracles indexed by `ι`. Defined as a map from each input to the type of the oracle's output.ITypedef KDFOracle (I
TypeKType: TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.) : OracleSpecOracleSpec.{u, v} (ι : Type u) : Type (max u (v + 1))An `OracleSpec ι` is specieifes a set of oracles indexed by `ι`. Defined as a map from each input to the type of the oracle's output.ITypeKDF as a random oracle, for security proofs.
The paper makes the same distinction: correctness is unconditional, security assumes the ROM.