DDHDefs.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 4 of 49 lines trusted trust banner B2, trusted: definitions used by the statement 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.

CKA party state for Diffie–Hellman ratchets (ACD19 §4.1.2)

Trusted: definitions used by the statement. The theorems of Computational/Theorems/ use every definition in this file: read them. The theorems here are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Defines the party state State of the Diffie–Hellman continuous-key-agreement (CKA) scheme of ACD19 §4.1.2, shared by the module-based scheme (Computational/Proofs/CryptoGames/CKA/DDHProofDefs.lean, DEV-CKA9) and libsignal's abstract-DH instantiation (CKA/LibsignalCKA.lean). A party holds either the peer's latest public element (pub h) or its own latest secret exponent (exp x).

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames.CKA.DDH

variable {F G : Type} [Field F] [AddCommGroup G] [Module F G]

inductive StateL36–39 ↗#

DDH-CKA party state (ACD19 §4.1.2): a peer public element pub h or a secret exponent exp x.

inductive State (F G : Type) where
  | pub (h : G)
  | exp (x : F)

notation "GameM"L45–50 ↗#

local notation "GameM" => StateT (GameState (State F G) G) ProbComp

end CryptoGames.CKA.DDH