cmac.bend

bend-osdev-cipher-modes@0.1.0.0 · 87 lines · 15 definitions

1# CMAC (NIST SP 800-38B; RFC 4493 for AES-CMAC), a MAC over any 128-bit
2# block cipher (only its encryption is used; see cipher-modes.bend for the
3# template arguments).
4#   L = E(0^128), K1 = dbl(L), K2 = dbl(K1)
5#   dbl(X) = X << 1, xor 0x87 into the last byte when X's top bit was set
6#   the message in 16-byte blocks M_1 .. M_n (n >= 1); the last is xored with
7#   K1 if it is whole, else padded with 0x80 0x00 .. and xored with K2;
8#   the MAC is the last block of their CBC encryption (IV 0).
9# A message may arrive in pieces: start, update (any number of times) and
10# finish give the MAC of the pieces joined.
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
14
15# Subkeys
16
17def Cmac.dbl(b: M.CmBlock) -> M.CmBlock:
18  match b:
19    case M.CmBlock{+w0, +w1, +w2, +w3}:
20      M.CmBlock{U32.or(U32.shl(w0), U32.shrn(w1, 31n)), U32.or(U32.shl(w1), U32.shrn(w2, 31n)), U32.or(U32.shl(w2), U32.shrn(w3, 31n)), U32.xor(U32.shl(w3), U32.and(135, M.cm.mask(U32.shrn(w0, 31n))))}
21
22def cmac.k1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
23  Cmac.dbl(enc(k, M.CmBlock.zero()))
24
25def cmac.k2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
26  Cmac.dbl(cmac.k1(~K, ~enc, k))
27
28# the subkeys K1 and K2
29def Cmac.subkey1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
30  cmac.k1(~K, ~enc, k)
31
32def Cmac.subkey2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
33  cmac.k2(~K, ~enc, k)
34
35# The state: the chaining value x, and the bytes not yet processed (at most
36# 16, newest first) and their count. A full buffer is kept until the next byte
37# arrives, since the last block is treated differently.
38type CmacState is Data:
39  CmacState{x: M.CmBlock, buf: List<&2, U32>, n: Nat}
40
41def Cmac.start() -> CmacState:
42  CmacState{M.CmBlock.zero(), Nil{}, 0n}
43
44def cmac.push(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, full: Bool, +k: K, x: M.CmBlock, buf: List<&2, U32>, +n: Nat, b: U32) -> CmacState:
45  match full:
46    case True{}:
47      CmacState{enc(k, M.CmBlock.xor(x, M.cm.block_of(List.reverse(&2, U32, buf)))), Con{b, Nil{}}, 1n}
48    case False{}:
49      CmacState{x, Con{b, buf}, 1n+n}
50
51def cmac.step(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, s: CmacState, b: U32) -> CmacState:
52  match s:
53    case CmacState{x, buf, +n}:
54      cmac.push(~K, ~enc, Nat.is_eq(n, 16n), k, x, buf, n, b)
55
56def cmac.feed(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, xs: List<&2, U32>, s: CmacState) -> CmacState:
57  match xs:
58    case Nil{}:
59      s
60    case Con{h, t}:
61      cmac.feed(~K, ~enc, k, t, cmac.step(~K, ~enc, k, s, h))
62
63# the state after the bytes of m
64def Cmac.update(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, s: CmacState, m: B.Octets) -> CmacState:
65  cmac.feed(~K, ~enc, k, B.Octets.to_list(m), s)
66
67# the last block: whole, xor K1; partial (or empty), padded, xor K2
68def cmac.last(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, full: Bool, +k: K, x: M.CmBlock, last: List<&2, U32>) -> M.CmBlock:
69  match full:
70    case True{}:
71      enc(k, M.CmBlock.xor(M.CmBlock.xor(x, M.cm.block_of(last)), cmac.k1(~K, ~enc, k)))
72    case False{}:
73      enc(k, M.CmBlock.xor(M.CmBlock.xor(x, M.cm.block_of(B.append(last, Con{128, Nil{}}))), cmac.k2(~K, ~enc, k)))
74
75# the 16-byte MAC
76def Cmac.finish(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, s: CmacState) -> B.Octets:
77  match s:
78    case CmacState{x, buf, +n}:
79      M.CmBlock.to_octets(cmac.last(~K, ~enc, Nat.is_eq(n, 16n), k, x, List.reverse(&2, U32, buf)))
80
81# The MAC of m in one call
82def Cmac.mac(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, m: B.Octets) -> B.Octets:
83  Cmac.finish(~K, ~enc, k, Cmac.update(~K, ~enc, k, Cmac.start(), m))
84
85# whether tag is m's 16-byte MAC, compared with no early exit
86def Cmac.verify(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, m: B.Octets, tag: B.Octets) -> Bool:
87  M.cm.ct_eq(B.Octets.to_list(Cmac.mac(~K, ~enc, k, m)), B.Octets.to_list(tag))