proofs/crypto/kdf/okm.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/okm.bend as Okm

8 imports

import Base
import ../../../src/crypto/kdf.bend as KDF
import ../../../src/crypto/mac.bend as MAC
import ../../../spec/crypto/hkdf.bend as Spec
import ../../../spec/crypto/hmac.bend as HMAC
import ../mac/hmac.bend as MacP
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N

Definitions

def take_zero source · line 18 · raw

@+xs:List<&2, U32> -> {List.take(&2, U32, xs, 0n) == [] : List<&2, U32>}

def take_append_short source · line 25 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+n:Nat -> @+h:{Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool} -> {List.take(&2, U32, List.append(&2, U32, xs, ys), n) == List.take(&2, U32, xs, n) : List<&2, U32>}

def take_append_len source · line 37 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+k:Nat -> {List.take(&2, U32, List.append(&2, U32, xs, ys), Nat.add(List.length(&2, U32, xs), k)) == List.append(&2, U32, xs, List.take(&2, U32, ys, k)) : List<&2, U32>}

def take_take source · line 45 · raw

@+xs:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {List.take(&2, U32, List.take(&2, U32, xs, b), a) == List.take(&2, U32, xs, a) : List<&2, U32>}

def length_take source · line 57 · raw

@+xs:List<&2, U32> -> @+n:Nat -> @+h:{Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool} -> {List.length(&2, U32, List.take(&2, U32, xs, n)) == n : Nat}

def length_append source · line 69 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}

def le_len source · line 77 · raw

@+xs:List<&2, U32> -> @+k:Nat -> @+e:{List.length(&2, U32, xs) == 32n : Nat} -> @+h:{Nat.is_le(k, 32n) == True{} : Bool} -> {Nat.is_le(k, List.length(&2, U32, xs)) == True{} : Bool}

def peel32 source · line 83 · raw

@+q:Nat -> {Nat.divmod.go(Nat.add(32n+q, 31n), 31n, 0n, 0n) == Nat.divmod.go(Nat.add(q, 31n), 31n, 1n, 0n) : Pair(Nat, Nat)}

def div_step source · line 86 · raw

@+q:Nat -> {Nat.div(Nat.add(32n+q, 31n), 32n) == 1n+Nat.div(Nat.add(q, 31n), 32n) : Nat}

def ceil_ok source · line 93 · raw

@len:Nat -> {Nat.is_le(len, Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.block_count(len), 32n)) == True{} : Bool}

def short_case source · line 166 · raw

@+p:Nat -> @n:Nat -> @+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+prev:List<&2, U32> -> @+i:Nat -> @+hp:{Nat.is_le(1n+p, 32n) == True{} : Bool} -> @+h:{Nat.is_le(1n+p, Nat.mul(n, 32n)) == True{} : Bool} -> {List.take(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+p) == List.take(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.t_blocks(n, prk, info, prev, i), 1n+p) : List<&2, U32>}

A last, partial block: 1+p <= 32 bytes of T(i+1).

def go_chain source · line 177 · raw

@rem:Nat -> @n:Nat -> @+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+prev:List<&2, U32> -> @+i:Nat -> @+h:{Nat.is_le(rem, Nat.mul(n, 32n)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.blocks(rem, prk, info, prev, U32.from_nat(1n+i)) == List.take(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.t_blocks(n, prk, info, prev, i), rem) : List<&2, U32>}

The implementation's stream of blocks, cut to rem bytes, is the first rem bytes of RFC 5869's T(i+1) | ... | T(i+n), whenever those have rem bytes.

def blocks_len source · line 255 · raw

@n:Nat -> @+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+prev:List<&2, U32> -> @+i:Nat -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.t_blocks(n, prk, info, prev, i)) == Nat.mul(n, 32n) : Nat}

RFC 5869's T(1) | ... | T(n) has 32n bytes.

def okm_correct source · line 269 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.blocks(len, prk, info, [], 1) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.okm(prk, info, len) : List<&2, U32>}

def okm_length source · line 272 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.okm(prk, info, len)) == len : Nat}

def okm_prefix source · line 276 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.okm(prk, info, a) == List.take(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.okm(prk, info, b), a) : List<&2, U32>}