def mask_pad

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

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/spec/crypto/hmac.bend as Spec
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

50# mask is zero padding to n bytes followed by the byte-wise XOR.
51def mask_pad(+key: List<&2, U32>, +n: Nat, +pad: U32, +hp: {U32.xor(0, pad) == pad : U32}, +h: {Nat.is_le(List.length(&2, U32, key), n) == True{} : Bool}) -> {MAC.mask(key, n, pad) == Spec.xor_pad(List.append(&2, U32, key, List.replicate(U32, Nat.sub(n, List.length(&2, U32, key)), 0)), pad) : List<&2, U32>}:
52  match key n:
53    case Nil{} 0n:
54      {==}
55    case Nil{} 1n+ +p:
56      mask_nil(1n+p, pad, hp)
57    case k <> rest 0n:
58      Empty.absurd({MAC.mask(k <> rest, 0n, pad) == Spec.xor_pad(List.append(&2, U32, k <> rest, List.replicate(U32, Nat.sub(0n, List.length(&2, U32, k <> rest)), 0)), pad) : List<&2, U32>}, L.false_true(h))
59    case +k <> +rest 1n+ +p:
60      %mask_pad(rest, p, pad, hp, h) : {U32.xor(k, pad) <> MAC.mask(rest, p, pad) == U32.xor(k, pad) <> _ : List<&2, U32>}
61      {==}