src/crypto/mac.bend

bend-collections-laws-crypto@1.0.0.0 · 63 lines · 7 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
4
5# HMAC-SHA256 (RFC 2104, FIPS 198-1), on the verified SHA-256.
6#
7#   sign(key, msg) -> tag          32-byte tag
8#   verify(key, msg, tag) -> Bool  constant-time comparison of the tag
9#
10# Bytes are U32 values 0..255 (the library's byte convention). Keys of any
11# length are accepted: a key longer than the 64-byte block is hashed first,
12# a shorter one is zero-padded (RFC 2104 section 2). The specification is
13# spec/crypto/hmac.bend; proofs/crypto/mac/proof.bend proves sign equal to
14# it for every key and message, verify(k, m, sign(k, m)) == True, and that
15# verify rejects every other tag.
16
17def block_len() -> Nat:
18  64n
19
20# Whether a key fits in the block, looking at no more than 65 of its bytes
21# (the length of a long key is never computed).
22def fits(key: List<&2, U32>, n: Nat) -> Bool:
23  match key n:
24    case Nil{} _:
25      True{}
26    case k <> rest 0n:
27      False{}
28    case k <> rest 1n+p:
29      fits(rest, p)
30
31def block_key_if(+key: List<&2, U32>, short: Bool) -> List<&2, U32>:
32  match short:
33    case True{}:
34      key
35    case False{}:
36      SHA.sha256_bytes(key)
37
38# The key as it enters the block: itself, or its digest when too long.
39def block_key(+key: List<&2, U32>) -> List<&2, U32>:
40  block_key_if(key, fits(key, block_len()))
41
42# The n-byte block (key zero-padded to n bytes) XOR the pad byte, in one
43# pass: past the end of the key a byte is 0 XOR pad = pad.
44def mask(key: List<&2, U32>, n: Nat, +pad: U32) -> List<&2, U32>:
45  match key n:
46    case Nil{} 0n:
47      Nil{}
48    case Nil{} 1n+p:
49      pad <> mask(Nil{}, p, pad)
50    case k <> rest 0n:
51      Nil{}
52    case k <> rest 1n+p:
53      U32.xor(k, pad) <> mask(rest, p, pad)
54
55def sign(+key: List<&2, U32>, msg: List<&2, U32>) -> List<&2, U32>:
56  +k = block_key(key)
57  SHA.sha256_bytes(List.append(&2, U32, mask(k, block_len(), 92),
58    SHA.sha256_bytes(List.append(&2, U32, mask(k, block_len(), 54), msg))))
59
60# The tag is compared in constant time (subtle.eq: no early exit on the
61# contents; only the lengths, which are public, are compared directly).
62def verify(+key: List<&2, U32>, msg: List<&2, U32>, tag: List<&2, U32>) -> Bool:
63  Subtle.eq(sign(key, msg), tag)