spec/crypto/hmac.bend

bend-collections@1.0.0.0 · 58 lines · 11 definitions

1import Base
2import bend-collections@1.0.0.0/spec/crypto/sha.bend as FIPS
3
4# Executable specification of HMAC-SHA256: RFC 2104 section 2, in the
5# step-by-step form of FIPS 198-1 section 4, over the FIPS 180-4 SHA-256
6# specification spec/crypto/sha.bend (after HACL*'s Spec.HMAC). Nothing of
7# the implementation (src/crypto/mac.bend) or of the SHA-256 implementation
8# is used. Bytes are U32 values 0..255, as everywhere in the library.
9
10# B, the block size of SHA-256 in bytes, and L, its output size.
11def block_len() -> Nat:
12  64n
13
14def hash_len() -> Nat:
15  32n
16
17# RFC 2104: ipad = the byte 0x36 repeated B times, opad = 0x5C repeated B times.
18def ipad() -> U32:
19  54
20
21def opad() -> U32:
22  92
23
24def hash(bytes: List<&2, U32>) -> List<&2, U32>:
25  FIPS.sha256_bytes(bytes)
26
27# FIPS 198-1 steps 1-3: a key of exactly B bytes is K0 itself; a longer key
28# is hashed first (K0 = H(K) || zeros); a shorter one is zero-padded to B.
29def shorten_if(+key: List<&2, U32>, fits: Bool) -> List<&2, U32>:
30  match fits:
31    case True{}:
32      key
33    case False{}:
34      hash(key)
35
36def shorten(+key: List<&2, U32>) -> List<&2, U32>:
37  shorten_if(key, Nat.is_le(List.length(&2, U32, key), block_len()))
38
39def zero_pad(+k: List<&2, U32>) -> List<&2, U32>:
40  List.append(&2, U32, k,
41    List.replicate(U32, Nat.sub(block_len(), List.length(&2, U32, k)), 0))
42
43def k0(+key: List<&2, U32>) -> List<&2, U32>:
44  zero_pad(shorten(key))
45
46# Byte-wise exclusive or of K0 with a pad byte (steps 4 and 7).
47def xor_pad(ks: List<&2, U32>, +pad: U32) -> List<&2, U32>:
48  match ks:
49    case Nil{}:
50      Nil{}
51    case k <> rest:
52      U32.xor(k, pad) <> xor_pad(rest, pad)
53
54# HMAC(K, text) = H((K0 ^ opad) || H((K0 ^ ipad) || text))   (steps 4-9).
55def hmac(+key: List<&2, U32>, text: List<&2, U32>) -> List<&2, U32>:
56  +k = k0(key)
57  hash(List.append(&2, U32, xor_pad(k, opad()),
58    hash(List.append(&2, U32, xor_pad(k, ipad()), text))))