1	import Base
2	import ../../../src/crypto/mac.bend as MAC
3	import ../../../spec/crypto/hmac.bend as Spec
4	import ../../../spec/crypto/subtle.bend as SubtleSpec
5	
6	# The clauses of src/crypto/mac.bend (HMAC-SHA256), proved in proof.bend.
7	# Every clause is for every key, message and tag (any U32 lists).
8	
9	# sign is RFC 2104 / FIPS 198-1 HMAC over FIPS 180-4 SHA-256.
10	law Sign.correct:
11	  for +key: List<&2, U32>
12	  for +msg: List<&2, U32>
13	  {MAC.sign(key, msg) == Spec.hmac(key, msg) : List<&2, U32>}
14	
15	# Every tag is 32 bytes.
16	law Sign.length:
17	  for +key: List<&2, U32>
18	  for +msg: List<&2, U32>
19	  {List.length(&2, U32, MAC.sign(key, msg)) == 32n : Nat}
20	
21	# verify is the reference comparison of the tag with the specified HMAC.
22	law Verify.value:
23	  for +key: List<&2, U32>
24	  for +msg: List<&2, U32>
25	  for +tag: List<&2, U32>
26	  {MAC.verify(key, msg, tag) == SubtleSpec.equal(Spec.hmac(key, msg), tag) : Bool}
27	
28	# The tag of a message verifies.
29	law Verify.accepts:
30	  for +key: List<&2, U32>
31	  for +msg: List<&2, U32>
32	  {MAC.verify(key, msg, MAC.sign(key, msg)) == True{} : Bool}
33	
34	# A tag that verifies is the tag.
35	law Verify.sound:
36	  for +key: List<&2, U32>
37	  for +msg: List<&2, U32>
38	  for +tag: List<&2, U32>
39	  for +h: {MAC.verify(key, msg, tag) == True{} : Bool}
40	  {tag == MAC.sign(key, msg) : List<&2, U32>}
41	
42	# Any other tag is rejected.
43	law Verify.rejects:
44	  for +key: List<&2, U32>
45	  for +msg: List<&2, U32>
46	  for +tag: List<&2, U32>
47	  for ne: {tag != MAC.sign(key, msg) : List<&2, U32>}
48	  {MAC.verify(key, msg, tag) == False{} : Bool}