1	import Base
2	import ./sha/sha256.bend as SHA
3	import ./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	
17	def 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).
22	def 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	
31	def 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.
39	def 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.
44	def 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	
55	def 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).
62	def verify(+key: List<&2, U32>, msg: List<&2, U32>, tag: List<&2, U32>) -> Bool:
63	  Subtle.eq(sign(key, msg), tag)