law cmac_streaming

bend-osdev-cipher-modes@0.1.0.0 · LAWS.bend:56

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/cmac.bend as CM

56# CMAC in pieces: the state after a ++ b is the state after a, then b, for
57# every cipher, key and state (so start, update .. update, finish is the MAC
58# of the pieces joined)
59law cmac_streaming:
60  for ~K: Data
61  for ~enc: K -> M.CmBlock -> M.CmBlock
62  for +k: K
63  for s: CM.CmacState
64  for +a: B.Octets
65  for +b: B.Octets
66  {CM.Cmac.update(~K, ~enc, k, s, B.Octets.append(a, b)) == CM.Cmac.update(~K, ~enc, k, CM.Cmac.update(~K, ~enc, k, s, a), b) : CM.CmacState}