spec/crypto/hmac.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/hmac.bend as Hmac
2 imports
import Base import ./sha.bend as FIPS
Definitions
def block_len source · line 11 · raw
Nat
B, the block size of SHA-256 in bytes, and L, its output size.
def hash_len source · line 14 · raw
Nat
def ipad source · line 18 · raw
U32
RFC 2104: ipad = the byte 0x36 repeated B times, opad = 0x5C repeated B times.
def opad source · line 21 · raw
U32
def hash source · line 24 · raw
@bytes:List<&2, U32> -> List<&2, U32>
def shorten_if source · line 29 · raw
@+key:List<&2, U32> -> @fits:Bool -> List<&2, U32>
FIPS 198-1 steps 1-3: a key of exactly B bytes is K0 itself; a longer key is hashed first (K0 = H(K) || zeros); a shorter one is zero-padded to B.
def shorten source · line 36 · raw
@+key:List<&2, U32> -> List<&2, U32>
def zero_pad source · line 39 · raw
@+k:List<&2, U32> -> List<&2, U32>
def k0 source · line 43 · raw
@+key:List<&2, U32> -> List<&2, U32>
def xor_pad source · line 47 · raw
@ks:List<&2, U32> -> @+pad:U32 -> List<&2, U32>
Byte-wise exclusive or of K0 with a pad byte (steps 4 and 7).
def hmac source · line 55 · raw
@+key:List<&2, U32> -> @text:List<&2, U32> -> List<&2, U32>
HMAC(K, text) = H((K0 ^ opad) || H((K0 ^ ipad) || text)) (steps 4-9).