Defs.lean🔗

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

Forward-secure AEAD: syntax and security game (ACD19 Def. 14, Fig. 5, Def. 15)

Trusted in part. The theorems of Computational/Theorems/ use only Adversary, AdversaryComp, FSAEADScheme, ReceiveResult, spec from this file: read them. Everything else here is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Syntax (FSAEADScheme) and hidden-bit security game (game, advantage, MakesAtMostQueries) for forward-secure AEAD after ACD19 §4.2.1 (Defs. 14–15, Fig. 5). Pure state transitions transmit, challenge, corruptSender, corruptReceiver, deliver, and inject operate on State, Record, and isCompromised.

Deviations in this file: DEV-FS1, DEV-FS2, DEV-FS3, DEV-FS4, DEV-FS5, DEV-FS6, DEV-FS11, DEV-FS21. Companion FS-AEAD deviations appear in Construction.lean (DEV-FS7, DEV-FS10), Security.lean (DEV-FS12, DEV-FS15), SecurityWith.lean (DEV-FS17), PubDefs.lean (DEV-FS19, DEV-FS20), Theorem5.lean (DEV-FS16), and Theorem5On.lean (DEV-FS18); see Computational/docs/DEVIATIONS.md.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

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

CryptoGames.FSAEADScheme.maxSkip, CryptoGames.FSAEADScheme.initSender, CryptoGames.FSAEADScheme, CryptoGames.FSAEADScheme.receive, CryptoGames.FSAEADScheme.initReceiver, CryptoGames.FSAEADScheme.send

namespace FSAEAD

inductive ReceiveResultL63–67 ↗#

Result of a receive oracle: rejected, or accepted i m (m = none when masked for a challenge).

inductive ReceiveResult (Message : Type) where
  | rejected
  | accepted (i : ℕ) (m : Option Message)
  deriving DecidableEq

abbrev specL69–80 ↗#

ACD19 Fig. 5 oracle interface (transmit, challenge, corruptSender, corruptReceiver, deliver, inject).

DEV-FS3 (formalization): req and end. Failed req preconditions and calls after ended return none without modifying state; FS-Rcv errors leave v_B unchanged.

abbrev spec (SenderState ReceiverState AssocData Message Ciphertext : Type) :=
  ((AssocData × Message) →ₒ Option Ciphertext)
  + ((AssocData × Message × Message) →ₒ Option Ciphertext)
  + (Unit →ₒ Option SenderState)
  + (Unit →ₒ Option (SenderState × ReceiverState))
  + ((AssocData × Ciphertext) →ₒ Option (ReceiveResult Message))
  + ((AssocData × Ciphertext) →ₒ Option (ReceiveResult Message))

abbrev AdversaryCompL82–84 ↗#

Computation with uniform coins and the Fig. 5 FS-AEAD oracles.

abbrev AdversaryComp (SenderState ReceiverState AssocData Message Ciphertext : Type) :=
  OracleComp (unifSpec + spec SenderState ReceiverState AssocData Message Ciphertext)

abbrev AdversaryL86–88 ↗#

FS-AEAD adversary outputting a Boolean guess for b.

abbrev Adversary (SenderState ReceiverState AssocData Message Ciphertext : Type) :=
  AdversaryComp SenderState ReceiverState AssocData Message Ciphertext Bool

variable {Key SenderState ReceiverState AssocData Message Ciphertext : Type}

notation "Comp"L94 ↗#

local notation "Comp" => AdversaryComp SenderState ReceiverState AssocData Message Ciphertext

16 declarations not shown (lines 96–253): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.transmitQuery, CryptoGames.FSAEAD.challengeQuery, CryptoGames.FSAEAD.corruptSenderQuery, CryptoGames.FSAEAD.corruptReceiverQuery, CryptoGames.FSAEAD.deliverQuery, CryptoGames.FSAEAD.injectQuery, CryptoGames.FSAEAD.Record.ad, CryptoGames.FSAEAD.Record.ct, CryptoGames.FSAEAD.Record, CryptoGames.FSAEAD.Record.idx, CryptoGames.FSAEAD.Record.msg, CryptoGames.FSAEAD.State.receiverIdx, CryptoGames.FSAEAD.State.ended, CryptoGames.FSAEAD.State.b, CryptoGames.FSAEAD.State.senderCorruptedAt, CryptoGames.FSAEAD.State.senderState, CryptoGames.FSAEAD.State.win, CryptoGames.FSAEAD.State.lastSentIdx, CryptoGames.FSAEAD.State.receiverState, CryptoGames.FSAEAD.State.challengesInTransit, CryptoGames.FSAEAD.State.inTransit, CryptoGames.FSAEAD.State, CryptoGames.FSAEAD.State.isCompromised, CryptoGames.FSAEAD.State.removeFromTransit, CryptoGames.FSAEAD.transmit, CryptoGames.FSAEAD.challenge, CryptoGames.FSAEAD.corruptSender, CryptoGames.FSAEAD.corruptReceiver, CryptoGames.FSAEAD.deliver, CryptoGames.FSAEAD.inject

section Game

variable [DecidableEq AssocData] [DecidableEq Message] [DecidableEq Ciphertext]
  (fs : FSAEADScheme Key SenderState ReceiverState AssocData Message Ciphertext)

notation "GameM"L262–263 ↗#

local notation "GameM" =>
  StateT (State SenderState ReceiverState AssocData Message Ciphertext) ProbComp

10 declarations not shown (lines 265–307): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.transmitImpl, CryptoGames.FSAEAD.challengeImpl, CryptoGames.FSAEAD.corruptSenderImpl, CryptoGames.FSAEAD.corruptReceiverImpl, CryptoGames.FSAEAD.deliverImpl, CryptoGames.FSAEAD.injectImpl, CryptoGames.FSAEAD.oracleImpl, CryptoGames.FSAEAD.initState, CryptoGames.FSAEAD.game, CryptoGames.FSAEAD.advantage

def MakesAtMostQueriesL309–312 ↗#

A makes at most q queries to the Fig. 5 FS-AEAD oracles.

def MakesAtMostQueries (A : Adversary SenderState ReceiverState AssocData Message Ciphertext)
    (q : ℕ) : Prop :=
  A.IsQueryBoundP (· matches .inr _) q

end Game

end FSAEAD

end CryptoGames