HybridWith.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 8 of 332 lines trusted trust banner B3, trusted in part 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.

Hybrid games and reductions of ACD19 Thm 5, with an AD-dependent ideal ciphertext

Trusted in part. The CLI security theorems (Theorems/Main.lean under Computational/, Oom/Supporting.lean under Computational/Proofs/LibsignalCli/) use only IndexedOtccaSpec and slotToHybridHopIndex from this file: read them. The rest is used by no theorem of Computational/Theorems/. The Thm 5 hybrids and reductions among it are part of the statement of theorem5: read them to trust it. Every proof is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Hybrid encrypting oracle (encIdxWith, otOpsWith), (ℕ × AD)-indexed OT-CCA interface (IndexedOtccaSpec, IndexedOtccaState, otImpl), multi-slot OT-CCA reduction (multiSlotOtccaReduction), and hop-index encoding (slotToHybridHopIndex) with AD-dependent ideal ciphertexts ideal (i, a) (DEV-FS17).

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames.FSAEAD.Thm5

variable {CK MK AD M C : Type}

notation "St"L47 ↗#

local notation "St" => HSt CK MK AD M C

2 declarations not shown (lines 49–82): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.Thm5.encIdxWith, CryptoGames.FSAEAD.Thm5.otOpsWith

abbrev IndexedOtccaSpecL94–95 ↗#

(ℕ × AD)-indexed OT-CCA oracle interface (uniform coins plus encrypt/decrypt).

abbrev IndexedOtccaSpec (AD M C : Type) := unifSpec + AEADScheme.otccaSpec (ℕ × AD) M C

17 declarations not shown (lines 97–322): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.Thm5.IndexedOtccaState, CryptoGames.FSAEAD.Thm5.otImpl, CryptoGames.FSAEAD.Thm5.multiKind, CryptoGames.FSAEAD.Thm5.multiDecIdx, CryptoGames.FSAEAD.Thm5.multiEncIdxWith, CryptoGames.FSAEAD.Thm5.multiReceiveH, CryptoGames.FSAEAD.Thm5.multiDeliverH, CryptoGames.FSAEAD.Thm5.multiInjectH, CryptoGames.FSAEAD.Thm5.multiTransmitHWith, CryptoGames.FSAEAD.Thm5.multiChallengeHWith, CryptoGames.FSAEAD.Thm5.multiOraclesWith, CryptoGames.FSAEAD.Thm5.multiImplWith, CryptoGames.FSAEAD.Thm5.multiRunWith, CryptoGames.FSAEAD.Thm5.multiSlotOtccaReduction, CryptoGames.FSAEAD.Thm5.sampleKeys, CryptoGames.FSAEAD.Thm5.initOStM, CryptoGames.FSAEAD.Thm5.slotRedImpl

def slotToHybridHopIndexL324–329 ↗#

Map slot j < 2 * q + (maxSkip + 1) to its encoded hybrid hop index m, which the single-slot reductions decode into chain position m / 2 and lookahead bit isLookaheadHop m = (m % 2 == 1):

for j < 2 * q, slotToHybridHopIndex q j = j (interleaving 2 * k and 2 * k + 1 for k < q);
for j = 2 * q + d, slotToHybridHopIndex q j = 2 * (q + d) + 1 (the remaining lookahead hops k ≥ q).

def slotToHybridHopIndex (q j : ℕ) : ℕ :=
  if j < 2 * q then j else 2 * (j - q) + 1

end CryptoGames.FSAEAD.Thm5