def sign_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/mac/hmac.bend:84

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Spec
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/laws.bend as ShaLaws

84def sign_correct(+key: List<&2, U32>, +msg: List<&2, U32>) -> {MAC.sign(key, msg) == Spec.hmac(key, msg) : List<&2, U32>}:
85  %Equal.sym(List<&2, U32>, MAC.mask(MAC.block_key(key), 64n, 92), Spec.xor_pad(Spec.k0(key), 92), block_mask(key, 92, {==})) : {SHA.sha256_bytes(List.append(&2, U32, _, SHA.sha256_bytes(List.append(&2, U32, MAC.mask(MAC.block_key(key), 64n, 54), msg)))) == FIPS.sha256_bytes(outer(key, msg)) : List<&2, U32>}
86  %Equal.sym(List<&2, U32>, MAC.mask(MAC.block_key(key), 64n, 54), Spec.xor_pad(Spec.k0(key), 54), block_mask(key, 54, {==})) : {SHA.sha256_bytes(List.append(&2, U32, Spec.xor_pad(Spec.k0(key), 92), SHA.sha256_bytes(List.append(&2, U32, _, msg)))) == FIPS.sha256_bytes(outer(key, msg)) : List<&2, U32>}
87  %Equal.sym(List<&2, U32>, SHA.sha256_bytes(inner(key, msg)), FIPS.sha256_bytes(inner(key, msg)), ShaLaws.sha256_bytes_correct(inner(key, msg))) : {SHA.sha256_bytes(List.append(&2, U32, Spec.xor_pad(Spec.k0(key), 92), _)) == FIPS.sha256_bytes(outer(key, msg)) : List<&2, U32>}
88  ShaLaws.sha256_bytes_correct(outer(key, msg))