proofs/crypto/kdf/proof.bend checks

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

10 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
import ./okm.bend as O
import ./laws.bend as Laws

Definitions

def is_done source · line 15 · raw

@r:Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>> -> Bool

def value source · line 22 · raw

@r:Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>> -> List<&2, U32>

def fail_done source · line 29 · raw

@+e:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError -> @+x:List<&2, U32> -> @+h:{Fail{e} == Done{x} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>} -> Empty

def done_inj source · line 32 · raw

@+x:List<&2, U32> -> @+y:List<&2, U32> -> @+h:{Done{x} == Done{y} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>} -> {x == y : List<&2, U32>}

def done_cong source · line 35 · raw

@+x:List<&2, U32> -> @+y:List<&2, U32> -> @+h:{x == y : List<&2, U32>} -> {Done{x} == Done{y} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>}

def expand_if source · line 42 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> @+b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand_if(prk, info, len, b) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/kdf/laws.as_result(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.expand_if(prk, info, len, b)) : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>}

def done_ok source · line 61 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> @+out:List<&2, U32> -> @+b:Bool -> @+eb:{Nat.is_le(len, 8160n) == b : Bool} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand_if(prk, info, len, b) == Done{out} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>} -> {Nat.is_le(len, 8160n) == True{} : Bool}

From expand's result: the length fits, and the value is the block stream.

def done_value source · line 68 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> @+out:List<&2, U32> -> @+b:Bool -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand_if(prk, info, len, b) == Done{out} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.blocks(len, prk, info, [], 1) == out : List<&2, U32>}

def done_okm source · line 76 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> @+out:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand(prk, info, len) == Done{out} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.okm(prk, info, len) == out : List<&2, U32>}

out is the specification's OKM.