Primitives.lean🔗

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

Deterministic AEAD and its one-time CCA game

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

Defines deterministic AEAD (AEADScheme, ACD19 §2.2 Def. 1) and its one-time chosen-ciphertext hidden-bit game (OTCCAAdversary, otccaEncrypt, otccaDecrypt, otccaGame, otccaAdvantage, Def. 2 and Fig. 1).

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

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

CryptoGames.AEADScheme, CryptoGames.AEADScheme.enc, CryptoGames.AEADScheme.dec

namespace AEADScheme

variable {Key AssocData Message Ciphertext : Type}

abbrev otccaSpecL44–46 ↗#

Fig. 1 OT-CCA oracle interface: one-time encrypt and unbounded decrypt.

abbrev otccaSpec (AssocData Message Ciphertext : Type) :=
  ((AssocData × Message) →ₒ Option Ciphertext) + ((AssocData × Ciphertext) →ₒ Option Message)

structure OTCCAStateL48–52 ↗#

Fig. 1 OT-CCA game state: key, hidden bit, and optional challenge (a*, e*).

structure OTCCAState (Key AssocData Ciphertext : Type) where
  key : Key
  b : Bool
  chal : Option (AssocData × Ciphertext) := none

5 declarations not shown (lines 54–106): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.AEADScheme.OTCCAAdversary, CryptoGames.AEADScheme.otccaEncrypt, CryptoGames.AEADScheme.otccaDecrypt, CryptoGames.AEADScheme.otccaGame, CryptoGames.AEADScheme.otccaAdvantage

end AEADScheme

end CryptoGames