Construction.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 14 of 95 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.

FS-AEAD from AEAD and PRG: the symmetric ratchet (ACD19 Fig. 6, corrected)

Trusted in part. The theorems of Computational/Theorems/ use only the state types RatchetSenderState and RatchetReceiverState from this file: read them. fromAEADPRG, skipKeys and the theorems here are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Corrected symmetric ratchet of ACD19 Fig. 6 built from an AEADScheme, a position-indexed PRG family G p (DEV-FS10), and skip window maxSkip (DEV-FS7, DEV-FS8, DEV-FS9).

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames.FSAEAD

variable {ChainKey MessageKey AssocData Message Ciphertext : Type}

structure RatchetSenderStateL34–39 ↗#

Sender state of the symmetric ratchet (ACD19 Fig. 6 v_A = (w, iA)).

structure RatchetSenderState (ChainKey : Type) where
  /-- Current chain key (`w`). -/
  chainKey : ChainKey
  /-- Index of the last message sent (`iA`); `0` before the first message. -/
  lastIndex : ℕ

structure RatchetReceiverStateL41–48 ↗#

Receiver state of the symmetric ratchet (ACD19 Fig. 6 v_B = (w, iB, D)).

structure RatchetReceiverState (ChainKey MessageKey : Type) where
  /-- Current chain key (`w`), deriving the message key for `lastIndex + 1`. -/
  chainKey : ChainKey
  /-- Largest index received so far (`iB`); `0` before the first message. -/
  lastIndex : ℕ
  /-- Stored `(index, key)` pairs for skipped indices below `lastIndex` (`D`). -/
  skippedKeys : List (ℕ × MessageKey)

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

CryptoGames.FSAEAD.skipKeys, CryptoGames.FSAEAD.fromAEADPRG

end CryptoGames.FSAEAD