Kdf.lean🔗

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

SPQR V1: HKDF-SHA256 key derivation (spqr/src/kdf.rs)

Trusted in part. The theorems of Computational/Theorems/ use the HKDF functions of this file (hkdfToVec, hkdfToSlice, hkdfToVecUnchecked, hkdfToSliceUnchecked, hkdfExtractBytes, hkdfMaxOkmLen, kdfInvalidLengthPanic, with bridges hkdfToSlice_of_le and hkdfToVec_of_le); the test helpers in Tests are checked by Lean (see Computational/docs/TRUSTED_BASE.md).

Panic-explicit model of spqr/src/kdf.rs:4–18 over an abstract SHA-256 compression function F, returning Except SpqrPanic Bytes with .error kdfInvalidLengthPanic when okmLen > 255 * 32.

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.HMAC CryptoGames.HKDF

abbrev hkdfMaxOkmLenL34–35 ↗#

Maximum HKDF-SHA256 output length in bytes (255 * 32 = 8160, RFC 5869 §2.3).

abbrev hkdfMaxOkmLen : ℕ := 255 * 32

abbrev kdfInvalidLengthPanicL37–39 ↗#

Panic site of spqr::kdf::hkdf_to_slice (src/kdf.rs:17) when okm_len > 255 * 32.

abbrev kdfInvalidLengthPanic : SpqrPanic :=
  .site "src/kdf.rs:17 InvalidLength"

def hkdfExtractBytesL41–43 ↗#

HKDF-Extract (HMAC-SHA256(salt, ikm), src/kdf.rs:15).

def hkdfExtractBytes (F : ShaState → List (BitVec 8) → ShaState) (salt ikm : Bytes) : Bytes :=
  hmacWith F salt ikm

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

CryptoVerification.LibsignalSpqrV1.hkdfExtractBytes_of_salt

def hkdfToSliceUncheckedL51–53 ↗#

def hkdfToSliceUnchecked (F : ShaState → List (BitVec 8) → ShaState)
    (salt ikm info : Bytes) (okmLen : ℕ) : Bytes :=
  hkdfExpand F (hkdfExtractBytes F salt ikm) info okmLen

def hkdfToSliceL55–62 ↗#

spqr::kdf::hkdf_to_slice (src/kdf.rs:14–18), panicking with kdfInvalidLengthPanic when okmLen > hkdfMaxOkmLen.

def hkdfToSlice (F : ShaState → List (BitVec 8) → ShaState)
    (salt ikm info : Bytes) (okmLen : ℕ) : Except SpqrPanic Bytes :=
  if okmLen ≤ hkdfMaxOkmLen then
    .ok (hkdfToSliceUnchecked F salt ikm info okmLen)
  else
    .error kdfInvalidLengthPanic

def hkdfToVecUncheckedL64–66 ↗#

def hkdfToVecUnchecked (F : ShaState → List (BitVec 8) → ShaState)
    (salt ikm info : Bytes) (okmLen : ℕ) : Bytes :=
  hkdfToSliceUnchecked F salt ikm info okmLen

def hkdfToVecL68–71 ↗#

spqr::kdf::hkdf_to_vec (src/kdf.rs:6–10).

def hkdfToVec (F : ShaState → List (BitVec 8) → ShaState)
    (salt ikm info : Bytes) (okmLen : ℕ) : Except SpqrPanic Bytes :=
  hkdfToSlice F salt ikm info okmLen

16 declarations not shown (lines 73–172): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.hkdfToSlice_of_le, CryptoVerification.LibsignalSpqrV1.hkdfToVec_of_le, CryptoVerification.LibsignalSpqrV1.Tests.K256, CryptoVerification.LibsignalSpqrV1.Tests.bigS0, CryptoVerification.LibsignalSpqrV1.Tests.bigS1, CryptoVerification.LibsignalSpqrV1.Tests.smallS0, CryptoVerification.LibsignalSpqrV1.Tests.smallS1, CryptoVerification.LibsignalSpqrV1.Tests.be32, CryptoVerification.LibsignalSpqrV1.Tests.schedule, CryptoVerification.LibsignalSpqrV1.Tests.sha256Compress, CryptoVerification.LibsignalSpqrV1.Tests.hexBytes, CryptoVerification.LibsignalSpqrV1.Tests.rfc5869_tc1_prk, CryptoVerification.LibsignalSpqrV1.Tests.rfc5869_tc1_okm, CryptoVerification.LibsignalSpqrV1.Tests.rfc5869_tc2_okm, CryptoVerification.LibsignalSpqrV1.Tests.rfc5869_tc3_okm, CryptoVerification.LibsignalSpqrV1.Tests.hkdfToSlice_invalidLength

end CryptoVerification.LibsignalSpqrV1