mac.bend
1# The MAC interface (message authentication codes).
2#
3# A MAC (template arguments, in this order):
4# ~K: Data its key, prepared
5# ~key: B.Octets -> Result<&2, &2, CrError, K> the key of a raw key,
6# refusing a length the MAC
7# does not take
8# ~compute: K -> B.Octets -> B.Octets the tag of a message
9# ~verify: K -> B.Octets -> B.Octets -> Bool whether a tag is the
10# message's
11# Laws (README.md, "Laws"):
12# accepts verify(k, m, compute(k, m)) == True, for every key and message
13# agrees verify(k, m, t) == B.Octets.is_eq(compute(k, m), t), for every
14# tag t: verify accepts exactly the computed tag
15#
16# CrMac.verify_tag is the named default ~verify: it compares the computed
17# tag with every byte of the given one (no early exit; Octets.is_eq), and
18# satisfies both laws for every ~compute (LAWS.bend: mac_verify_tag_*). The
19# instances: HMAC over any hash (hmac.bend), CMAC over any 128-bit block
20# cipher (cipher-modes' Cmac.mac) and Michael (inst_michael.bend). PBKDF2
21# (pbkdf2.bend) takes any MAC as its PRF.
22import Base
23import bend-osdev-bytes@0.1.0.0/bytes.bend as B
24import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
25
26# whether t is m's tag, comparing every byte
27def CrMac.verify_tag(~K: Data, ~compute: K -> B.Octets -> B.Octets, k: K, m: B.Octets, t: B.Octets) -> Bool:
28 B.Octets.is_eq(compute(k, m), t)
29
30# the tag of m under a raw key
31def CrMac.compute_with(~K: Data, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~compute: K -> B.Octets -> B.Octets, key_o: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
32 Result.map(&2, &2, Cr.CrError, K, B.Octets, k => compute(k, m), key(key_o))