Security.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 4 of 69 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 security statement: ACD19 Thm 5 for the symmetric ratchet

Trusted in part. The theorems of Computational/Theorems/ use only RatchetAdversary from this file: read it. Everything else here is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

States ACD19 Thm 5 (Theorem5Statement) for the symmetric ratchet fromAEADPRG against a RatchetAdversary, parameterized by explicit reductions prgRed and aeadRed (DEV-FS15) under windowed correctness (DEV-FS5) and uncompromised-record corr-B blocking (DEV-FS6); AD-dependent ideal ciphertexts (DEV-FS17) and restricted-AD correctness (DEV-FS18) are stated in SecurityWith.lean and Theorem5On.lean.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames.FSAEAD

variable {ChainKey MessageKey AssocData Message Ciphertext : Type}
  [DecidableEq AssocData] [DecidableEq Message] [DecidableEq Ciphertext]
  [SampleableType ChainKey] [SampleableType MessageKey] [SampleableType Ciphertext]

abbrev RatchetAdversaryL37–40 ↗#

FS-AEAD adversary against fromAEADPRG (ACD19 Def. 15).

abbrev RatchetAdversary (ChainKey MessageKey AssocData Message Ciphertext : Type) :=
  Adversary (RatchetSenderState ChainKey) (RatchetReceiverState ChainKey MessageKey)
    AssocData Message (ℕ × Ciphertext)

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

CryptoGames.FSAEAD.Theorem5Statement

end CryptoGames.FSAEAD