KeyInd1KeyRo.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 14 of 63 lines trusted source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Key indistinguishability with one-key identities and a random-oracle key derivation

Trusted: definitions used by the statement. Lemma 1 (PqxdhCorrectAndSecureδ, Security/HeadlineDelta.lean) bounds KeyInd1KeyRoAdvantage on pqxdhKeyIndImpl1KeyRo, and clause 2 of the PQXDH CLI statements (e.g. CliPqxdhElfSecure) uses KeyIndRoGap. Read with Computational/Specifications/Pqxdh/Game.lean (pqxdhKeyIndImpl), Assumptions.lean (GapDhWithSign, KemShCr, GapSigEufCma), and KeyInd1KeyReal.lean. See Computational/docs/TRUSTED_BASE.md and Computational/docs/DEVIATIONS.md (DEV-CLI16).

The CLI statements relate the real one-key handshake game (KeyInd1KeyRealAdvantage) to the one-key random-oracle game (KeyInd1KeyRoAdvantage, replacing P.hkdfDerive96 with HkdfRO, DEV-PQ14) via KeyIndRoGap, while Lemma 1 bounds KeyInd1KeyRoAdvantage under GapSigEufCma, KemShCr, and GapDhWithSign. Against pqxdhKeyIndImpl1KeyReal, pqxdhKeyIndImpl1KeyRo differs only in using evalHkdfOrRo true (HkdfRO) rather than evalHkdfOrRo false (P.hkdfDerive96), as checked in Computational/Tests/Guards/KeyInd1KeyRoGuard.lean.

@[expose] public section

set_option autoImplicit false

namespace SignalPqxdh

open OracleComp OracleSpec ENNReal

def pqxdhKeyIndImpl1KeyRoL40–48 ↗#

Key-indistinguishability oracle with single-scalar identities and random-oracle key derivation. Delegates .initPrin u to pqxdhKeyIndImpl1KeyReal and all other queries to pqxdhKeyIndImpl true S P, which uses one shared lazy HkdfRO cache (evalHkdfOrRo true) across .roQuery, initiate*, and accept* and disables .revealDhSecrets.

def pqxdhKeyIndImpl1KeyRo (S : Setup) (P : Primitives) :
    QueryImpl (keyIndSpec S) (StateT (KeyIndState S) ProbComp) := fun q =>
  match q with
  | .initPrin u => pqxdhKeyIndImpl1KeyReal S P (.initPrin u)
  | q => pqxdhKeyIndImpl true S P q

def KeyInd1KeyRoAdvantageL50–54 ↗#

Distinguishing advantage of A in pqxdhKeyInd1KeyExpForHandshake against pqxdhKeyIndImpl1KeyRo.

noncomputable def KeyInd1KeyRoAdvantage (S : Setup) (P : Primitives) (A : KeyIndAdversary S) :
    ℝ≥0∞ :=
  𝒟[pqxdhKeyInd1KeyExpForHandshake S P (pqxdhKeyIndImpl1KeyRo S P) A].boolBias

1 declaration not shown (lines 56–64): theorems, which Lean checks, or definitions that no headline statement uses

SignalPqxdh.KeyIndRoGap

end SignalPqxdh