1	import Base
2	import ../../../src/crypto/mac.bend as MAC
3	import ../../../src/crypto/subtle.bend as Subtle
4	import ../../../spec/crypto/hmac.bend as Spec
5	import ../../../spec/crypto/subtle.bend as SubtleSpec
6	import ../subtle/laws.bend as SubtleLaws
7	import ../subtle/proof.bend as SubtleProof
8	import ./hmac.bend as P
9	import ./laws.bend as Laws
10	
11	# Gate for src/crypto/mac.bend: `bend proofs/crypto/mac/proof.bend`.
12	# Sign: hmac.bend (the key block, then the two hashes through the proved
13	# SHA-256). Verify: subtle.eq is list equality (proofs/crypto/subtle).
14	
15	def Laws.Sign.correct(key, msg):
16	  P.sign_correct(key, msg)
17	
18	def Laws.Sign.length(key, msg):
19	  P.sign_len(key, msg)
20	
21	def Laws.Verify.value(key, msg, tag):
22	  %P.sign_correct(key, msg) : {Subtle.eq(MAC.sign(key, msg), tag) == SubtleSpec.equal(_, tag) : Bool}
23	  SubtleLaws.Eq.value(MAC.sign(key, msg), tag)
24	
25	def Laws.Verify.accepts(key, msg):
26	  SubtleLaws.Eq.refl(MAC.sign(key, msg))
27	
28	def Laws.Verify.sound(key, msg, tag, h):
29	  Equal.sym(List<&2, U32>, MAC.sign(key, msg), tag, SubtleLaws.Eq.sound(MAC.sign(key, msg), tag, h))
30	
31	def rejects(+key: List<&2, U32>, +msg: List<&2, U32>, +tag: List<&2, U32>, ne: {tag != MAC.sign(key, msg) : List<&2, U32>}, +b: Bool, +eb: {MAC.verify(key, msg, tag) == b : Bool}) -> {MAC.verify(key, msg, tag) == False{} : Bool}:
32	  match b:
33	    case True{}:
34	      Empty.absurd({MAC.verify(key, msg, tag) == False{} : Bool}, ne(Laws.Verify.sound(key, msg, tag, eb)))
35	    case False{}:
36	      eb
37	
38	def Laws.Verify.rejects(key, msg, tag, ne):
39	  rejects(key, msg, tag, ne, MAC.verify(key, msg, tag), {==})