PQXDH in Lean

2.1. Deterministic KDF🔗

Definition2.1
group✓L∃∀N
Used by 6
Hover a use site to preview it.
Preview
Definition 3.1
Blueprint label
  • aead_spec
Uses target in
  • statement

A KDF is modeled as a deterministic map from input material to a derived key. The abstraction is intentionally minimal so protocol proofs can reason only about equality of derived outputs from equal transcripts. Used in the correctness proofs (Theorem 5.26, Theorem 5.27), which only need "same input implies same output" — no randomness or security assumptions.

Code for Definition2.1●1 definition
  • structure KDF.{u_1, u_2} (IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) : Type (max u_1 u_2)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    structure KDF.{u_1, u_2} (IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) : Type (max u_1 u_2)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    KDF as a deterministic function, for correctness proofs.

    Constructor

    KDF.mk.{u_1, u_2} {IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } (deriveI → K : IType u_1 → KType u_2) :
  KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_1 KType u_2

    Fields

    deriveI → K : IType u_1 → KType u_2
    complete