Theorem8And12Statements.lean🔗

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

Theorems 8 and 12: authenticity and privacy of the Fig. 8 SM scheme (statements)

Trusted: definitions used by the statement. The theorems of Computational/Theorems/ use healEpoch and SM.specDF, the only definitions in this file. SchemeAdversary, Theorem8 and Theorem12 are in Computational/Proofs/SpecLemmas/Session/ACD19/SM/Theorem8And12Statements.lean, checked by Lean. See Computational/docs/TRUSTED_BASE.md §7.

In ACD19 (Alwen, Coretti, Dodis, ePrint 2018/1037, §5.3.2–5.3.3, Theorems 8 and 12), the Fig. 8 Double Ratchet secure-messaging scheme (LibsignalBinary/Specifications/CryptoGames/SM/Construction.lean) achieves authenticity and privacy for Δ_SM = 2 + Δ_CKA from a CKA scheme, a root PRF-PRNG, and an FS-AEAD scheme:

Adv^{auth}_{t*_L,t*}(A) ≤ Adv^{CKA}(R₁ A) + Adv^{PP}(R₂ A) + Σ_{j<q} Adv^{fs-aead}(R₃,j A),
`Adv^{priv}_{t*_L,t*}(A) ≤ 2·Adv^{CKA}(R₁ A) + 2·Adv^{PP}(R₂ A) + Adv^{fs-aead}(R₃ A)
- 2·Adv^{fs-aead}(R₃' A)`,

for q-query adversaries A, attacked epoch t*, last prior leak t*_L, and CKA healing epoch t_heal = t*_L + 2 (healEpoch). Theorem8 and Theorem12 parameterize over the reductions R₁, R₂, R₃, instantiated and proved in Computational/Proofs/CryptoGames/SM/.

Authenticity is a winning probability while CKA and PRF-PRNG advantages are real/ideal distances, so each hop costs 1× advantage, and R₃,j attacks the j-th epoch-t* FS-AEAD session and outputs a coin. Privacy is a bias (2·|Pr − 1/2|), so each distance hop costs 2× advantage (DEV-SM20) and the final FS-AEAD hop costs Adv(R₃) + 2·Adv(R₃'), where R₃' outputs a coin on forgery (DEV-SM25); ACD19 writes factor 1 on both bounds and omits the forgery term in Lemma 15.

@[expose] public section

open OracleComp OracleSpec ENNReal MeasureTheory

namespace CryptoGames.SM

abbrev specDFL53–56 ↗#

Six-oracle DeliverForge SM specification extending SM.spec with (Party × C × C) →ₒ Option (RecvResult Msg) for distinct ciphertexts sharing wire bytes.

abbrev specDF (St Msg Coins C : Type) :=
  SM.spec St Msg Coins C + ((Party × C × C) →ₒ Option (RecvResult Msg))

end CryptoGames.SM

namespace CryptoGames.SM.Construction

variable {KC Γ CCoins T I : Type} {KR Sig K : Type} {SS RS M E : Type}

def healEpochL64–72 ↗#

CKA challenge (healing) epoch t_heal = t*_L + 2, or 0 when t*_L = −∞.

DEV-SM27 (formalization): t*_L = −∞. ACD19 (§5.3.2, footnote 13) omits the case with no leak before t*, where the root RNG starts uncorrupted and no CKA step is needed. Setting healEpoch none = 0 places the CKA challenge at epoch 0, which has no challenge and thus zero advantage for every adversary.

def healEpoch : Option ℕ → ℕ
  | none => 0
  | some l => l + 2

end CryptoGames.SM.Construction