proofs/crypto/mac/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 48 lines · 6 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Spec
4import bend-collections-laws-crypto@1.0.0.0/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.
10law 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.
16law 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.
22law 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.
29law 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.
35law 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.
43law 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}