inst_cmac.bend

bend-osdev-crypto@0.1.0.0 · 23 lines · 2 definitions

1# CMAC as a MAC: cipher-modes' CMAC (NIST SP 800-38B, RFC 4493) over any
2# 128-bit block cipher (~K, ~key, ~enc). The instance:
3#   ~K, ~key, ~CrCmac.mac(~K, ~enc), ~CrCmac.verify(~K, ~enc)
4# for example AES-CMAC:
5#   ~X.CmAesKey, ~CrAes.key, ~CrCmac.mac(~X.CmAesKey, ~X.CmAes.encrypt),
6#   ~CrCmac.verify(~X.CmAesKey, ~X.CmAes.encrypt)
7# verify is the interface's named default (mac.bend: CrMac.verify_tag), so
8# its laws hold for CMAC by the generic proof; cipher-modes' own
9# Cmac.verify does the same comparison, but no law of cipher-modes ties it
10# to Cmac.mac.
11import Base
12import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
14import bend-osdev-cipher-modes@0.1.0.0/cmac.bend as CMc
15import bend-osdev-crypto@0.1.0.0/mac.bend as Mc
16
17# the 16-byte tag of m
18def CrCmac.mac(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, k: K, m: B.Octets) -> B.Octets:
19  CMc.Cmac.mac(~K, ~enc, k, m)
20
21# whether t is m's tag (every byte compared)
22def CrCmac.verify(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, k: K, m: B.Octets, t: B.Octets) -> Bool:
23  Mc.CrMac.verify_tag(~K, ~CrCmac.mac(~K, ~enc), k, m, t)