gf128.bend
bend-osdev-gf@0.1.2.0 · 172 lines · 0 definitions
1# bend-osdev-gf, GF(2^128): the field of GCM's GHASH (NIST SP 800-38D) and
2# of the tweak arithmetic in XTS (IEEE Std 1619), LRW and CMAC (NIST SP
3# 800-38B), all modulo x^128 + x^7 + x^2 + x + 1, in the three bit orders
4# they use.
5#
6# A Gf128 is a 16-byte block as four big-endian 32-bit words: byte 0 is the
7# top byte of w0, byte 15 the bottom byte of w3. The bit orders:
8#
9# * GCM (SP 800-38D, 6.3): bit 0 of the block, the most significant bit
10# of byte 0, is the coefficient of x^0; bit 127, the least significant
11# bit of byte 15, that of x^127. Multiplying by x shifts the block right
12# one bit, and a bit falling off the end adds R = 0xE1 || 0^120.
13# * big-endian (CMAC's doubling, SP 800-38B 6.1; LRW): the block is a
14# 128-bit big-endian number whose bit i is the coefficient of x^i.
15# Multiplying by x shifts it left one bit, and a carry adds 0x87.
16# * little-endian (XTS, IEEE 1619 5.2): the block is a 128-bit
17# little-endian number (byte 0 least significant); multiplying by x
18# shifts it left one bit, and a carry adds 0x87 to byte 0.
19import Base
20import bend-osdev-bytes@0.1.1.1/bytes.bend as B
21
22type Gf128 is Data:
23 Gf128{w0: U32, w1: U32, w2: U32, w3: U32}
24
25type Gf128Error is Data:
26 Gf128BadLength{got: Nat}
27
28def Gf128.zero() -> Gf128:
29 Gf128{0, 0, 0, 0}
30
31def Gf128.of_words(w0: U32, w1: U32, w2: U32, w3: U32) -> Gf128:
32 Gf128{w0, w1, w2, w3}
33
34def Gf128.words(x: Gf128) -> List<&2, U32>:
35 match x:
36 case Gf128{w0, w1, w2, w3}:
37 [w0, w1, w2, w3]
38
39def Gf128.xor(a: Gf128, b: Gf128) -> Gf128:
40 match a b:
41 case Gf128{a0, a1, a2, a3} Gf128{b0, b1, b2, b3}:
42 Gf128{U32.xor(a0, b0), U32.xor(a1, b1), U32.xor(a2, b2), U32.xor(a3, b3)}
43
44def Gf128.is_eq(a: Gf128, b: Gf128) -> Bool:
45 match a b:
46 case Gf128{a0, a1, a2, a3} Gf128{b0, b1, b2, b3}:
47 Bool.and(U32.is_eq(a0, b0), Bool.and(U32.is_eq(a1, b1), Bool.and(U32.is_eq(a2, b2), U32.is_eq(a3, b3))))
48
49# Bytes
50
51def gf128.word(a: U32, b: U32, c: U32, d: U32) -> U32:
52 U32.or(U32.shln(U32.and(255, a), 24n), U32.or(U32.shln(U32.and(255, b), 16n), U32.or(U32.shln(U32.and(255, c), 8n), U32.and(255, d))))
53
54def gf128.of_list.go(xs: List<&2, U32>) -> Gf128:
55 match xs:
56 case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
57 Gf128{gf128.word(a0, a1, a2, a3), gf128.word(a4, a5, a6, a7), gf128.word(a8, a9, a10, a11), gf128.word(a12, a13, a14, a15)}
58 case o:
59 Gf128.zero()
60
61def gf128.of_list.pick(ok: Bool, +n: Nat, +xs: List<&2, U32>) -> Result<&2, &2, Gf128Error, Gf128>:
62 match ok:
63 case True{}:
64 Done{gf128.of_list.go(xs)}
65 case False{}:
66 Fail{Gf128BadLength{n}}
67
68# the block of 16 bytes (any other length is refused)
69def Gf128.of_octets(+o: B.Octets) -> Result<&2, &2, Gf128Error, Gf128>:
70 +n = B.Octets.len(o)
71 gf128.of_list.pick(Nat.is_eq(n, 16n), n, B.Octets.to_list(o))
72
73def Gf128.to_octets(x: Gf128) -> B.Octets:
74 match x:
75 case Gf128{w0, w1, w2, w3}:
76 B.Octets.concat([B.Octets.be32(w0), B.Octets.be32(w1), B.Octets.be32(w2), B.Octets.be32(w3)])
77
78def Gf128.hex(x: Gf128) -> String:
79 B.Octets.hex(Gf128.to_octets(x))
80
81# all ones if the low bit of b is set, else 0
82def gf128.mask(b: U32) -> U32:
83 U32.sub(0, U32.and(b, 1))
84
85def Gf128.and_mask(a: Gf128, +m: U32) -> Gf128:
86 match a:
87 case Gf128{w0, w1, w2, w3}:
88 Gf128{U32.and(w0, m), U32.and(w1, m), U32.and(w2, m), U32.and(w3, m)}
89
90# Multiplication by x
91
92# GCM's order: shift right one bit; bit 127 falling off adds 0xE1 to byte 0
93def Gf128.mul_x_gcm(v: Gf128) -> Gf128:
94 match v:
95 case Gf128{+w0, +w1, +w2, +w3}:
96 Gf128{U32.xor(U32.shr(w0), U32.and(3774873600, gf128.mask(w3))), U32.or(U32.shr(w1), U32.shln(w0, 31n)), U32.or(U32.shr(w2), U32.shln(w1, 31n)), U32.or(U32.shr(w3), U32.shln(w2, 31n))}
97
98# big-endian (CMAC's doubling, LRW): shift left one bit; a carry adds 0x87
99# to byte 15
100def Gf128.double_be(v: Gf128) -> Gf128:
101 match v:
102 case Gf128{+w0, +w1, +w2, +w3}:
103 Gf128{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, gf128.mask(U32.shrn(w0, 31n))))}
104
105# little-endian (XTS): every byte shifts left one bit, taking the top bit of
106# the byte before it; the top bit of byte 15 adds 0x87 to byte 0
107
108# each byte of w shifted left, with the carries between w's own bytes
109def gf128.le.shift(+w: U32) -> U32:
110 U32.or(U32.and(4278124286, U32.shl(w)), U32.and(65793, U32.shrn(w, 15n)))
111
112# the carry out of w's last byte, into the first byte of the next word
113def gf128.le.carry(w: U32) -> U32:
114 U32.shln(U32.and(128, w), 17n)
115
116def Gf128.double_le(v: Gf128) -> Gf128:
117 match v:
118 case Gf128{+w0, +w1, +w2, +w3}:
119 Gf128{U32.xor(gf128.le.shift(w0), U32.and(2264924160, gf128.mask(U32.shrn(w3, 7n)))), U32.or(gf128.le.shift(w1), gf128.le.carry(w0)), U32.or(gf128.le.shift(w2), gf128.le.carry(w1)), U32.or(gf128.le.shift(w3), gf128.le.carry(w2))}
120
121# GCM's multiplication (SP 800-38D, Algorithm 1): Z = 0, V = Y; for each
122# bit X_i of X, from bit 0: if X_i, Z = Z + V; then V = V * x
123
124def gf128.gcm.bit(+x: U32, zv: Gf128 & Gf128) -> Gf128 & Gf128:
125 (z, +v) = zv
126 (Gf128.xor(z, Gf128.and_mask(v, gf128.mask(U32.shrn(x, 31n)))), Gf128.mul_x_gcm(v))
127
128# the 32 bits of the word x, from its top bit
129def gf128.gcm.word(n: Nat, +x: U32, zv: Gf128 & Gf128) -> Gf128 & Gf128:
130 match n:
131 case 0n:
132 zv
133 case 1n+k:
134 gf128.gcm.word(k, U32.shl(x), gf128.gcm.bit(x, zv))
135
136def gf128.fst(p: Gf128 & Gf128) -> Gf128:
137 (a, b) = p
138 a
139
140def Gf128.mul_gcm(x: Gf128, y: Gf128) -> Gf128:
141 match x:
142 case Gf128{w0, w1, w2, w3}:
143 gf128.fst(gf128.gcm.word(32n, w3, gf128.gcm.word(32n, w2, gf128.gcm.word(32n, w1, gf128.gcm.word(32n, w0, (Gf128.zero(), y))))))
144
145# GHASH (SP 800-38D, 6.4): Y = (Y + X_i) * H for each block X_i
146def Gf128.ghash_update(+h: Gf128, y: Gf128, x: Gf128) -> Gf128:
147 Gf128.mul_gcm(Gf128.xor(y, x), h)
148
149def Gf128.ghash.go(xs: List<&2, Gf128>, +h: Gf128, y: Gf128) -> Gf128:
150 match xs:
151 case Nil{}:
152 y
153 case Con{x, rest}:
154 Gf128.ghash.go(rest, h, Gf128.ghash_update(h, y, x))
155
156def Gf128.ghash(+h: Gf128, xs: List<&2, Gf128>) -> Gf128:
157 Gf128.ghash.go(xs, h, Gf128.zero())
158
159# The big-endian multiplication (LRW): Horner's rule over the bits of b,
160# from the top: z = z * x + bit * a
161
162def gf128.be.word(n: Nat, +x: U32, +a: Gf128, z: Gf128) -> Gf128:
163 match n:
164 case 0n:
165 z
166 case 1n+k:
167 gf128.be.word(k, U32.shl(x), a, Gf128.xor(Gf128.double_be(z), Gf128.and_mask(a, gf128.mask(U32.shrn(x, 31n)))))
168
169def Gf128.mul_be(+a: Gf128, b: Gf128) -> Gf128:
170 match b:
171 case Gf128{w0, w1, w2, w3}:
172 gf128.be.word(32n, w3, a, gf128.be.word(32n, w2, a, gf128.be.word(32n, w1, a, gf128.be.word(32n, w0, a, Gf128.zero()))))