proofs/crypto/kdf/laws.bend open laws/TODOs

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

3 imports

import Base
import ../../../src/crypto/kdf.bend as KDF
import ../../../spec/crypto/hkdf.bend as Spec

Laws

law Extract.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 17 · raw

@+salt:List<&2, U32> -> @+ikm:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.extract(salt, ikm) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.extract(salt, ikm) : List<&2, U32>}

extract is RFC 5869 section 2.2 (HMAC-SHA256(salt, IKM)).

law Expand.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 23 · raw

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

expand is RFC 5869 section 2.3, and fails exactly where it is undefined.

law Expand.done openits proof in laws_crypto.bend does not pass the checker (fails)source · line 29 · raw

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

law Expand.too_long openits proof in laws_crypto.bend does not pass the checker (fails)source · line 36 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> @+h:{Nat.is_le(len, 8160n) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand(prk, info, len) == Fail{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.LengthTooLarge{}} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>}

law Expand.length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 44 · 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>>} -> {List.length(&2, U32, out) == len : Nat}

The output has the requested length.

law Expand.prefix openits proof in laws_crypto.bend does not pass the checker (fails)source · line 53 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+out:List<&2, U32> -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand(prk, info, b) == Done{out} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.expand(prk, info, a) == Done{List.take(&2, U32, out, a)} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>}

A shorter output is a prefix of a longer one (same key and info).

law Hkdf.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 64 · raw

@+salt:List<&2, U32> -> @+ikm:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.hkdf(salt, ikm, info, len) == as_result(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.hkdf(salt, ikm, info, len)) : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.KdfError, List<&2, U32>>}

hkdf is extract then expand.

law Okm.length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 72 · 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}

The specification's OKM (any length): L bytes, and prefixes of each other.

law Okm.prefix openits proof in laws_crypto.bend does not pass the checker (fails)source · line 78 · 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>}

Definitions

def as_result source · line 9 · raw

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

The specification's partial expand, as the implementation's result type.