CBCDefs.lean🔗

Tier 2 · definitions used by the computational proof and symbolic proof 6 headline theorems depend on it 54 of 150 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.

Declarations on this page (11)

AES-256-CBC with PKCS#7 padding as a one-time cipher

Trusted in part. The theorems of Computational/Theorems/ use only AesKey, Block, Plain, bytesToBlock, cbcEncrypt, cbcScheme, nBlocks, padLen, pkcs7Blocks, pkcs7Bytes, cbcPkcs7EncryptOnly from this file: read them. Everything else here is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Models libsignal's signal_crypto::aes_256_cbc_encrypt over an abstract AES-256 block function E : AesKey → Block → Block (DEV-AEAD14), together with monadic CBC cbcM, the PRF wrapper blockPRF, and the one-time IND-CPA-to-PRF reduction cbcRed (CBC.lean). Decryption is specified separately in CBCDecDefs.lean.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

namespace CBC

abbrev BlockL35–36 ↗#

A 128-bit AES block.

abbrev Block := BitVec 128

abbrev AesKeyL38–39 ↗#

A 256-bit AES key.

abbrev AesKey := BitVec 256

def cbcEncryptL41–52 ↗#

CBC encryption of the blocks P with block function f, starting from the chaining value prev (the IV): C₁ = f (P₁ ⊕ prev), Cᵢ₊₁ = f (Pᵢ₊₁ ⊕ Cᵢ).

DEV-AEAD8 (libsignal): the IV is part of the key. libsignal derives the IV with HKDF (the HMAC-based key derivation) together with the keys, and never transmits it. So the IV is part of the one-time key (k, iv) and not of the ciphertext. Effect: none.

def cbcEncrypt (f : Block → Block) (prev : Block) :
    {n : ℕ} → List.Vector Block n → List.Vector Block n
  | 0, _ => List.Vector.nil
  | _ + 1, P =>
    let c := f (P.head ^^^ prev)
    c ::ᵥ cbcEncrypt f c P.tail

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

CryptoGames.CBC.cbcM

PKCS#7 padding

abbrev PlainL66–73 ↗#

A plaintext of exactly ℓ bytes. CBC with PKCS#7 reveals the length, so the game fixes it.

DEV-AEAD2 (libsignal): one plaintext length per session. ACD19 Def. 2 compares the real ciphertext with a uniformly random one. AES-CBC with PKCS#7 padding reveals the number of blocks, so every plaintext of a session has the same length ℓ; the end-to-end adversary's messages have type CBC.Plain ℓ. Effect: restricts the adversary (no claim for sessions that mix message lengths).

abbrev Plain (ℓ : ℕ) := List.Vector (BitVec 8) ℓ

def nBlocksL75–76 ↗#

Number of ciphertext blocks for an ℓ-byte plaintext.

def nBlocks (ℓ : ℕ) : ℕ := ℓ / 16 + 1

def padLenL78–79 ↗#

PKCS#7 pad length: 16 − (ℓ mod 16), always in 1..16.

def padLen (ℓ : ℕ) : ℕ := 16 - ℓ % 16

def pkcs7BytesL81–83 ↗#

The padded byte string: m followed by padLen ℓ copies of the byte padLen ℓ.

def pkcs7Bytes {ℓ : ℕ} (m : Plain ℓ) : List (BitVec 8) :=
  m.toList ++ List.replicate (padLen ℓ) (BitVec.ofNat 8 (padLen ℓ))

def bytesToBlockL85–88 ↗#

Little-endian block of (up to) 16 bytes: byte j occupies bits 8j .. 8j+7, as in an AArch64 16-byte load.

def bytesToBlock (bs : List (BitVec 8)) : Block :=
  bs.foldr (fun b acc => (acc <<< 8) ||| b.zeroExtend 128) 0

def pkcs7BlocksL90–92 ↗#

PKCS#7 padding split into nBlocks ℓ blocks: block i is bytes 16i .. 16i+15.

def pkcs7Blocks {ℓ : ℕ} (m : Plain ℓ) : List.Vector Block (nBlocks ℓ) :=
  List.Vector.ofFn fun i => bytesToBlock (((pkcs7Bytes m).drop (16 * i.val)).take 16)

The cipher and the PRF

def cbcSchemeL96–102 ↗#

CBC with key (k, iv) applied to a deterministic block encoding encode of the message. Decryption is out of scope and always rejects.

def cbcScheme {M : Type} {n : ℕ} (E : AesKey → Block → Block)
    (encode : M → List.Vector Block n) :
    CipherScheme (AesKey × Block) M (List.Vector Block n) where
  enc k m := cbcEncrypt (E k.1) k.2 (encode m)
  dec _ _ := none

abbrev cbcPkcs7EncryptOnlyL104–112 ↗#

libsignal's AES-256-CBC with PKCS#7 padding on ℓ-byte plaintexts, AES abstracted as E.

DEV-AEAD14 (machine model): AES and SHA-256 are arbitrary functions. The AES-256 block function E here and the SHA-256 compression function F of AEAD/HMACDefs.lean are parameters, because in the binary they are hooks whose machine code is not verified (DEV-E8). The assumptions (blockPRF E and HMAC are PRFs) are about whatever the hooks compute. Effect: none.

abbrev cbcPkcs7EncryptOnly (E : AesKey → Block → Block) (ℓ : ℕ) :
    CipherScheme (AesKey × Block) (Plain ℓ) (List.Vector Block (nBlocks ℓ)) :=
  cbcScheme E pkcs7Blocks

3 declarations not shown (lines 114–147): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.CBC.blockPRF, CryptoGames.CBC.cbcRedImpl, CryptoGames.CBC.cbcRed

end CBC

end CryptoGames