CBCDecDefs.lean🔗

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

AES-256-CBC decryption with strict PKCS#7 unpadding

Trusted in part. The theorems of Computational/Theorems/ use only blockToBytesLE, cbcDecRaw, cbcDecryptBlocks, chunks16, pkcs7Unpad from this file: read those. Everything else here is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Specifies libsignal's signal_crypto::aes_256_cbc_decrypt over an abstract inverse block cipher D : AesKey → Block → Block on arbitrary input byte strings, and packages it with encryption into the full CipherScheme cbcPkcs7.

@[expose] public section

namespace CryptoGames

namespace CBC

Bytes and blocks

def blockToBytesLEL33–36 ↗#

The 16 little-endian bytes of a block: byte j is bits 8j .. 8j+7, inverse of bytesToBlock on 16-byte lists.

def blockToBytesLE (b : Block) : List (BitVec 8) :=
  List.ofFn fun j : Fin 16 => b.extractLsb' (8 * j.val) 8

def chunks16L38–41 ↗#

Split a byte string into 16-byte blocks via bytesToBlock, dropping any trailing partial chunk.

def chunks16 (bs : List (BitVec 8)) : List Block :=
  List.ofFn fun i : Fin (bs.length / 16) => bytesToBlock ((bs.drop (16 * i.val)).take 16)

CBC decryption and PKCS#7 unpadding

def cbcDecryptBlocksL45–49 ↗#

CBC decryption with inverse block function g from initial chaining value prev (the IV): P₁ = g C₁ ⊕ prev, Pᵢ₊₁ = g Cᵢ₊₁ ⊕ Cᵢ.

def cbcDecryptBlocks (g : Block → Block) (prev : Block) : List Block → List Block
  | [] => []
  | c :: cs => (g c ^^^ prev) :: cbcDecryptBlocks g c cs

def pkcs7UnpadL51–61 ↗#

Strict PKCS#7 unpadding (block-padding Pkcs7::unpad): with n the last byte, reject if bs is empty, n = 0, n > 16, or any of the last n bytes differs from n; otherwise drop the last n bytes.

def pkcs7Unpad (bs : List (BitVec 8)) : Option (List (BitVec 8)) :=
  match bs.getLast? with
  | none => none
  | some last =>
    let n := last.toNat
    if n = 0 ∨ 16 < n ∨ bs.length < n then none
    else if (bs.drop (bs.length - n)).all (· == last) then some (bs.take (bs.length - n))
    else none

def cbcDecRawL63–69 ↗#

libsignal's aes_256_cbc_decrypt over abstract inverse cipher D: reject if ct is empty or its length is not a multiple of 16; otherwise CBC-decrypt the 16-byte blocks from iv and apply strict PKCS#7 unpadding.

def cbcDecRaw (D : AesKey → Block → Block) (k : AesKey) (iv : Block)
    (ct : List (BitVec 8)) : Option (List (BitVec 8)) :=
  if ct = [] ∨ ct.length % 16 ≠ 0 then none
  else pkcs7Unpad ((cbcDecryptBlocks (D k) iv (chunks16 ct)).flatMap blockToBytesLE)

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

CryptoGames.CBC.cbcPkcs7

end CBC

end CryptoGames