Construction.lean🔗

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

The Signal-based SM scheme (ACD19 Fig. 8)

Trusted in part. The theorems of Computational/Theorems/ use only the types Header and PartyState from this file: read them. initParty, send, receive, scheme and the theorems here are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Generic secure-messaging scheme of ACD19 §5.1 (Alwen, Coretti, Dodis, ePrint 2018/1037) built from a continuous key agreement scheme cka, a root PRF-PRNG prng, and a per-epoch FS-AEAD scheme fs (Ratchet/LibsignalSMInstance.lean instantiates it for libsignal).

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames.SM.Construction

abbrev HeaderL35–42 ↗#

Message header h = (t, T_t) (T = none encodes λ in epoch 0), passed as FS-AEAD associated data.

DEV-SM11 (formalization): no FS-Stop, FS-Max or ℓ_prv. ACD19 Fig. 8 sends ℓ_prv so the receiver can erase old sessions via FS-Max and FS-Stop. Here old sessions are retained, the header is (t, T), and old-epoch forgeries are handled in the SM game (DEV-SM7; see DEV-LS13 for libsignal's previous_counter).

abbrev Header (T : Type) := ℕ × Option T

structure PartyStateL44–62 ↗#

Per-party state for ACD19 Fig. 8.

structure PartyState (Γ T Sig SS RS : Type) where
  /-- Party identifier (`A` or `B`). -/
  id : Party
  /-- Root PRF-PRNG state `σ_root`. -/
  root : Sig
  /-- Current sending FS-AEAD session `v[t_cur]`.

  **DEV-SM12 (formalization): only the current sending session is kept.** ACD19 Fig. 8 indexes
  `v[t]` for every `t`, whereas sending sessions of past epochs are never reused. -/
  vS : Option SS
  /-- Receiving FS-AEAD sessions `v[t]` indexed by epoch `t`. -/
  vR : ℕ → Option RS
  /-- CKA state `γ`. -/
  γ : Γ
  /-- Current CKA message `T_cur`. -/
  curCkaMsg : Option T
  /-- Current epoch counter `t_cur`. -/
  tcur : ℕ

4 declarations not shown (lines 71–153): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.SM.Construction.initParty, CryptoGames.SM.Construction.send, CryptoGames.SM.Construction.receive, CryptoGames.SM.Construction.scheme

end CryptoGames.SM.Construction