xcbc.bend

bend-osdev-crypto@0.1.0.0 · 80 lines · 10 definitions

1# XCBC-MAC over any block cipher (the block-cipher interface, block.bend), as
2# RFC 3566 (The AES-XCBC-MAC-96 Algorithm and Its Use With IPsec, 2003)
3# defines it for AES-128, after J. Black and P. Rogaway's three-key
4# construction:
5#   K1 = E(K, 0x01..01), K2 = E(K, 0x02..02), K3 = E(K, 0x03..03)
6#   E[0] = 0; E[i] = E(K1, M[i] xor E[i-1]) for every block but the last;
7#   the last block whole:  E[n] = E(K1, M[n] xor E[n-1] xor K2)
8#   the last block short (or an empty message): padded with one 1 bit and
9#   zeros to a block, E[n] = E(K1, pad(M[n]) xor E[n-1] xor K3)
10# and the tag is E[n] (RFC 3566 truncates it to 96 bits for IPsec:
11# CrXcbc.mac96). Over another cipher the constants are blocks of 0x01, 0x02,
12# 0x03 bytes of its block size, and K1 must be a key the cipher takes (its
13# key size equal to its block size, as for AES-128).
14#
15# As a MAC (mac.bend): ~CrXcbcKey<K>, ~CrXcbc.key(..), ~CrXcbc.mac(..),
16# ~CrXcbc.verify(..), verify the interface's named default, so the MAC laws
17# hold for XCBC over every cipher (LAWS.bend: xcbc_accepts).
18import Base
19import bend-osdev-bytes@0.1.0.0/bytes.bend as B
20import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
21import bend-osdev-crypto@0.1.0.0/mac.bend as Mc
22import bend-osdev-crypto@0.1.0.0/octets.bend as O
23
24# one block of bytes encrypted (a string the format refuses stays as it is)
25def cr.xcbc.encb(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_to: Blk -> B.Octets, +k: K, x: Maybe<&2, Blk>, +o: B.Octets) -> B.Octets:
26  match x:
27    case None{}:
28      o
29    case Some{b}:
30      blk_to(enc(k, b))
31
32def cr.xcbc.e(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +o: B.Octets) -> B.Octets:
33  cr.xcbc.encb(~K, ~Blk, ~enc, ~blk_to, k, blk_of(o), o)
34
35# An XCBC key: the cipher's key schedule of K1, and K2 and K3 as bytes
36type CrXcbcKey<-K: Data> is Data:
37  CrXcbcKey{k1: K, k2: B.Octets, k3: B.Octets}
38
39def cr.xcbc.key.of(~K: Data, ~Blk: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K) -> Result<&2, &2, Cr.CrError, CrXcbcKey<K>>:
40  +k2 = cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.rep(bsize, 2))
41  +k3 = cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.rep(bsize, 3))
42  Result.map(&2, &2, Cr.CrError, K, CrXcbcKey<K>, k1 => CrXcbcKey{k1, k2, k3}, key(cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.rep(bsize, 1))))
43
44# The key from a raw key K (refused when the cipher refuses K or K1)
45def CrXcbc.key(~K: Data, ~Blk: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, o: B.Octets) -> Result<&2, &2, Cr.CrError, CrXcbcKey<K>>:
46  Result.bind(&2, &2, Cr.CrError, K, CrXcbcKey<K>, key(o), k => cr.xcbc.key.of(~K, ~Blk, ~bsize, ~key, ~enc, ~blk_of, ~blk_to, k))
47
48def cr.xcbc.full(full: Bool, +bsize: Nat, +k2: B.Octets, +k3: B.Octets, +p: B.Octets) -> B.Octets:
49  match full:
50    case True{}:
51      O.CrOct.xor(p, k2)
52    case False{}:
53      O.CrOct.xor(B.Octets.append(p, B.Octets.cons(128, B.Octets.zeros(Nat.sub(bsize, Nat.add(B.Octets.len(p), 1n))))), k3)
54
55# the CBC-MAC over the pieces from E = e; the last piece is whole or short
56def cr.xcbc.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k1: K, +k2: B.Octets, +k3: B.Octets, ps: List<&2, List<&2, U32>>, +e: B.Octets) -> B.Octets:
57  match ps:
58    case Nil{}:
59      cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k1, O.CrOct.xor(cr.xcbc.full(False{}, bsize, k2, k3, B.Octets.empty()), e))
60    case Con{p, t}:
61      match t:
62        case Nil{}:
63          +po = B.Octets.of_list(p)
64          cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k1, O.CrOct.xor(cr.xcbc.full(Nat.is_eq(B.Octets.len(po), bsize), bsize, k2, k3, po), e))
65        case Con{q, u}:
66          cr.xcbc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k1, k2, k3, Con{q, u}, cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k1, O.CrOct.xor(B.Octets.of_list(p), e)))
67
68# The tag of m (one block)
69def CrXcbc.mac(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrXcbcKey<K>, m: B.Octets) -> B.Octets:
70  match kk:
71    case CrXcbcKey{+k1, +k2, +k3}:
72      cr.xcbc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k1, k2, k3, O.CrOct.pieces(bsize, B.Octets.to_list(m)), B.Octets.zeros(bsize))
73
74# RFC 3566's AES-XCBC-MAC-96: the tag's first 12 bytes
75def CrXcbc.mac96(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrXcbcKey<K>, m: B.Octets) -> B.Octets:
76  B.Octets.take(12n, CrXcbc.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, kk, m))
77
78# whether t is m's tag (every byte compared; the MAC interface's default)
79def CrXcbc.verify(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrXcbcKey<K>, m: B.Octets, t: B.Octets) -> Bool:
80  Mc.CrMac.verify_tag(~CrXcbcKey<K>, ~CrXcbc.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to), kk, m, t)