WireRatchetDefs.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 3 of 43 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.

libsignal's symmetric ratchet with the counter inside the wire bytes

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

Plaintext normalization padOrTruncatePlain used to fit decrypted byte lists into the fixed-length message type Plain ℓ of ACD19 Theorem 5.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

namespace Ratchet

open HMAC HKDF CBC LibsignalAead MACScheme AEADScheme WireAEAD

variable {H : Type}

def padOrTruncatePlainL38–44 ↗#

Truncate or zero-pad a received plaintext to ℓ bytes (identity on ℓ-byte inputs).

def padOrTruncatePlain (ℓ : ℕ) (bs : List (BitVec 8)) : Plain ℓ :=
  ⟨(bs ++ List.replicate ℓ 0).take ℓ, byH:Typeℓ:ℕbs:List (BitVec 8)⊢ (List.take ℓ (bs ++ List.replicate ℓ 0)).length = ℓ simpAll goals completed! 🐙⟩

end Ratchet

end CryptoGames