LAWS.bend
bend-osdev-gf@0.1.2.0 · 292 lines · 0 definitions
1# GF(2^8) (gf.bend). For every reduction polynomial (every Gf8Field) and
2# every input, multiplication is commutative and associative, distributes
3# over addition, has 1 as its identity and 0 as its zero; addition is
4# commutative and associative, with 0 as its identity and every element its
5# own negative; xtime is multiplication by x; and powers add. (These are the
6# laws of the ring GF(2)[x] modulo the polynomial, which hold whether or not
7# the polynomial is irreducible.)
8#
9# For the named fields (AES's 0x11B and Reed-Solomon's 0x11D, both
10# irreducible): every nonzero element has an inverse, and is a power of the
11# field's generator, its logarithm (checked for all 255 nonzero bytes).
12#
13# Vectors: FIPS 197's worked products (section 4.2), the AES inverse of
14# 0x53 (0xCA), and the Reed-Solomon powers of x. The tables (tables.bend),
15# GF(2^128) (gf128.bend) and GF(2^m) (gfm.bend) laws follow.
16import Base
17import bend-osdev-bytes@0.1.1.1/bytes.bend as B
18import bend-osdev-gf@0.1.2.0/gf.bend as G
19import bend-osdev-gf@0.1.2.0/tables.bend as T
20import bend-osdev-gf@0.1.2.0/gf128.bend as H
21import bend-osdev-gf@0.1.2.0/gfm.bend as M
22
23# Multiplication: a commutative ring with identity, for every polynomial
24
25law mul_comm:
26 for +f: G.Gf8Field
27 for +a: U32
28 for +b: U32
29 {G.Gf8.mul(f, a, b) == G.Gf8.mul(f, b, a) : U32}
30
31law mul_assoc:
32 for +f: G.Gf8Field
33 for +a: U32
34 for +b: U32
35 for +c: U32
36 {G.Gf8.mul(f, G.Gf8.mul(f, a, b), c) == G.Gf8.mul(f, a, G.Gf8.mul(f, b, c)) : U32}
37
38law mul_distrib:
39 for +f: G.Gf8Field
40 for +a: U32
41 for +b: U32
42 for +c: U32
43 {G.Gf8.mul(f, a, G.Gf8.add(b, c)) == G.Gf8.add(G.Gf8.mul(f, a, b), G.Gf8.mul(f, a, c)) : U32}
44
45law mul_one:
46 for +f: G.Gf8Field
47 for +a: U32
48 {G.Gf8.mul(f, 1, a) == G.Gf8.elt(a) : U32}
49
50law mul_zero:
51 for +f: G.Gf8Field
52 for +a: U32
53 {G.Gf8.mul(f, 0, a) == 0 : U32}
54
55law xtime_mul_x:
56 for +f: G.Gf8Field
57 for +a: U32
58 {G.Gf8.xtime(f, a) == G.Gf8.mul(f, 2, a) : U32}
59
60# Addition: XOR, a group in which every element is its own negative
61
62law add_comm:
63 for +a: U32
64 for +b: U32
65 {G.Gf8.add(a, b) == G.Gf8.add(b, a) : U32}
66
67law add_assoc:
68 for +a: U32
69 for +b: U32
70 for +c: U32
71 {G.Gf8.add(G.Gf8.add(a, b), c) == G.Gf8.add(a, G.Gf8.add(b, c)) : U32}
72
73law add_zero:
74 for +a: U32
75 {G.Gf8.add(a, 0) == G.Gf8.elt(a) : U32}
76
77law add_self:
78 for +a: U32
79 {G.Gf8.add(a, a) == 0 : U32}
80
81# Powers: a^(m + n) = a^m * a^n
82
83law pow_add:
84 for +f: G.Gf8Field
85 for +a: U32
86 for +m: Nat
87 for +n: Nat
88 {G.Gf8.pow(f, a, Nat.add(m, n)) == G.Gf8.mul(f, G.Gf8.pow(f, a, m), G.Gf8.pow(f, a, n)) : U32}
89
90# Inverses and logarithms in the named fields, for every nonzero element
91
92law mul_inv_aes:
93 for +a: U32
94 for nz: {G.Gf8.is_zero(a) == False{} : Bool}
95 {G.Gf8.mul(G.Gf8.aes(), a, G.Gf8.inv(G.Gf8.aes(), a)) == 1 : U32}
96
97law mul_inv_rs:
98 for +a: U32
99 for nz: {G.Gf8.is_zero(a) == False{} : Bool}
100 {G.Gf8.mul(G.Gf8.rs(), a, G.Gf8.inv(G.Gf8.rs(), a)) == 1 : U32}
101
102law exp_log_aes:
103 for +a: U32
104 for nz: {G.Gf8.is_zero(a) == False{} : Bool}
105 {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), a)) == G.Gf8.elt(a) : U32}
106
107law exp_log_rs:
108 for +a: U32
109 for nz: {G.Gf8.is_zero(a) == False{} : Bool}
110 {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), a)) == G.Gf8.elt(a) : U32}
111
112law inv_zero:
113 for +f: G.Gf8Field
114 {G.Gf8.inv(f, 0) == 0 : U32}
115
116# Vectors: FIPS 197, section 4.2: {57} * {83} = {c1}, {57} * {13} = {fe},
117# and xtime: {57} * {02} = {ae}, {57} * {04} = {47}, {57} * {08} = {8e},
118# {57} * {10} = {07}
119
120law v_aes_mul:
121 {G.Gf8.mul(G.Gf8.aes(), 87, 131) == 193 : U32}
122
123law v_aes_mul13:
124 {G.Gf8.mul(G.Gf8.aes(), 87, 19) == 254 : U32}
125
126law v_aes_xtime:
127 {[G.Gf8.xtime(G.Gf8.aes(), 87), G.Gf8.mul(G.Gf8.aes(), 87, 4), G.Gf8.mul(G.Gf8.aes(), 87, 8), G.Gf8.mul(G.Gf8.aes(), 87, 16)] == [174, 71, 142, 7] : List<&2, U32>}
128
129# the inverse of {53} is {ca} (the AES S-box's first step)
130law v_aes_inv:
131 {G.Gf8.inv(G.Gf8.aes(), 83) == 202 : U32}
132
133# in the Reed-Solomon field x^8 = x^4 + x^3 + x^2 + 1 = 0x1D, and x has
134# order 255 (x^255 = 1): x generates the field
135law v_rs_x8:
136 {G.Gf8.exp(G.Gf8.rs(), 8n) == 29 : U32}
137
138law v_rs_order:
139 {G.Gf8.exp(G.Gf8.rs(), 255n) == 1 : U32}
140
141law v_div:
142 {G.Gf8.mul(G.Gf8.aes(), G.Gf8.div(G.Gf8.aes(), 87, 131), 131) == 87 : U32}
143
144# The tables (tables.bend), for the named fields and every input: the
145# table built by Gf8Tab.new is handed back unchanged beside each result, and
146# the result is the reference's: a product is Gf8.mul, a logarithm Gf8.log,
147# and the exponential of i (below 510) is Gf8.exp. They also give the
148# reference's results on these vectors.
149
150law tab_mul_aes:
151 for +a: U32
152 for +b: U32
153 {T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.aes()), a, b) == (T.Gf8Tab.new(G.Gf8.aes()), G.Gf8.mul(G.Gf8.aes(), a, b)) : T.Gf8Tab & U32}
154
155law tab_mul_rs:
156 for +a: U32
157 for +b: U32
158 {T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), a, b) == (T.Gf8Tab.new(G.Gf8.rs()), G.Gf8.mul(G.Gf8.rs(), a, b)) : T.Gf8Tab & U32}
159
160law tab_log_aes:
161 for +a: U32
162 {T.Gf8Tab.log(T.Gf8Tab.new(G.Gf8.aes()), a) == (T.Gf8Tab.new(G.Gf8.aes()), U32.from_nat(G.Gf8.log(G.Gf8.aes(), a))) : T.Gf8Tab & U32}
163
164law tab_log_rs:
165 for +a: U32
166 {T.Gf8Tab.log(T.Gf8Tab.new(G.Gf8.rs()), a) == (T.Gf8Tab.new(G.Gf8.rs()), U32.from_nat(G.Gf8.log(G.Gf8.rs(), a))) : T.Gf8Tab & U32}
167
168law tab_exp_aes:
169 for +i: U32
170 for +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool}
171 {T.Gf8Tab.exp(T.Gf8Tab.new(G.Gf8.aes()), i) == (T.Gf8Tab.new(G.Gf8.aes()), G.Gf8.exp(G.Gf8.aes(), U32.to_nat(i))) : T.Gf8Tab & U32}
172
173law tab_exp_rs:
174 for +i: U32
175 for +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool}
176 {T.Gf8Tab.exp(T.Gf8Tab.new(G.Gf8.rs()), i) == (T.Gf8Tab.new(G.Gf8.rs()), G.Gf8.exp(G.Gf8.rs(), U32.to_nat(i))) : T.Gf8Tab & U32}
177
178# a witness for tab_exp's hypothesis: the last entry, 509
179law witness_tab_exp:
180 {Nat.is_lt(U32.to_nat(509), 510n) == True{} : Bool}
181
182law v_tab_mul_aes:
183 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.aes()), 87, 131)) == 193 : U32}
184
185law v_tab_inv_aes:
186 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.inv(T.Gf8Tab.new(G.Gf8.aes()), 83)) == 202 : U32}
187
188law v_tab_mul_rs:
189 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 200, 77)) == G.Gf8.mul(G.Gf8.rs(), 200, 77) : U32}
190
191law v_tab_zero:
192 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 0, 77)) == 0 : U32}
193
194# GF(2^128) (gf128.bend): vectors only. GCM: Test Case 2 of the GCM
195# specification (McGrew and Viega; H = AES-128 of the zero block under the
196# zero key): X1 = C * H, and GHASH(H, C || lengths). CMAC: the subkeys of
197# SP 800-38B D.1 / RFC 4493 (L = AES-128(K, 0), K1 = 2L, K2 = 4L). The
198# others pin the bit orders against each other. Laws for every input would
199# compute on 128 symbolic bits through 128 rounds; ref/run.sh checks every
200# function against independent implementations instead (see the README).
201# H = 66e94bd4ef8a2c3b884cfa59ca342b2e, C = 0388dace60b6a392f328c2b971b2fe78,
202# and a = 0123456789abcdeffedcba9876543210.
203
204# 5e2ec746917062882c85b0685353deb7
205law v_gcm_x1:
206 {H.Gf128.mul_gcm(H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960), H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)) == H.Gf128.of_words(1580123974, 2440061576, 746958952, 1398005431) : H.Gf128}
207
208# f38cbb1ad69223dcc3457ae5b6b0f885 (one block of C, then the lengths: 0 bits
209# of A, 128 of C)
210law v_gcm_ghash:
211 {H.Gf128.ghash(H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558), [H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960), H.Gf128.of_words(0, 0, 0, 128)]) == H.Gf128.of_words(4086086426, 3599901660, 3276110565, 3065051269) : H.Gf128}
212
213# L = 7df76b0c1ab899b33e42f047b91b546f, K1 = fbeed618357133667c85e08f7236a8de,
214# K2 = f7ddac306ae266ccf90bc11ee46d513b
215law v_cmac_k1:
216 {H.Gf128.double_be(H.Gf128.of_words(2113366796, 448305587, 1044574279, 3105576047)) == H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798) : H.Gf128}
217
218law v_cmac_k2:
219 {H.Gf128.double_be(H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798)) == H.Gf128.of_words(4158499888, 1793222348, 4178297118, 3832369467) : H.Gf128}
220
221# GCM's x is the block 0x40 00 .. 00: mul_x_gcm is multiplication by it
222law v_gcm_mul_x:
223 {H.Gf128.mul_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(1073741824, 0, 0, 0)) == H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) : H.Gf128}
224
225law v_gcm_mul_x_value:
226 {H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(9544371, 3302352631, 4285422924, 992614664) : H.Gf128}
227
228# in big-endian order x is the number 2: double_be is multiplication by it
229law v_be_mul_x:
230 {H.Gf128.mul_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(0, 0, 0, 2)) == H.Gf128.double_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) : H.Gf128}
231
232law v_be_mul:
233 {H.Gf128.mul_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)) == H.Gf128.of_words(780021721, 1580971822, 2568813327, 4049188832) : H.Gf128}
234
235# XTS: the top bit of byte 15 wraps round as 0x87 into byte 0
236law v_xts_wrap:
237 {H.Gf128.double_le(H.Gf128.of_words(0, 0, 0, 255)) == H.Gf128.of_words(2264924160, 0, 0, 254) : H.Gf128}
238
239law v_xts_double:
240 {H.Gf128.double_le(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(38177486, 307731423, 4256789809, 3987235872) : H.Gf128}
241
242law v_gf128_octets:
243 {H.Gf128.of_octets(H.Gf128.to_octets(H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558))) == Done{H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)} : Result<&2, &2, H.Gf128Error, H.Gf128>}
244
245law v_gf128_short:
246 {H.Gf128.of_octets(B.Octets.zeros(15n)) == Fail{H.Gf128BadLength{15n}} : Result<&2, &2, H.Gf128Error, H.Gf128>}
247
248# GF(2^m) (gfm.bend). For every field and input: addition commutes. For
249# GF(2^4): multiplication commutes (all 256 pairs) and every nonzero element
250# has an inverse; for GF(2^5), inverses too. Vectors for the BCH fields: x^13
251# = x^4 + x^3 + x + 1, x has order 8191 (so generates GF(2^13)), a product,
252# an inverse and a logarithm (x^100 = 1664), from an independent model
253# (ref/gen.py).
254
255law gfm_add_comm:
256 for +f: M.GfmField
257 for +a: U32
258 for +b: U32
259 {M.Gfm.add(f, a, b) == M.Gfm.add(f, b, a) : U32}
260
261law gfm_mul_comm_gf16:
262 for +a: U32
263 for +b: U32
264 {M.Gfm.mul(M.Gfm.gf16(), a, b) == M.Gfm.mul(M.Gfm.gf16(), b, a) : U32}
265
266law gfm_mul_inv_gf16:
267 for +a: U32
268 for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf16(), a), 0) == False{} : Bool}
269 {M.Gfm.mul(M.Gfm.gf16(), a, M.Gfm.inv(M.Gfm.gf16(), a)) == 1 : U32}
270
271law gfm_mul_inv_gf32:
272 for +a: U32
273 for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf32(), a), 0) == False{} : Bool}
274 {M.Gfm.mul(M.Gfm.gf32(), a, M.Gfm.inv(M.Gfm.gf32(), a)) == 1 : U32}
275
276law v_bch13_x13:
277 {M.Gfm.exp(M.Gfm.bch13(), 13) == 27 : U32}
278
279law v_bch13_order:
280 {M.Gfm.exp(M.Gfm.bch13(), 8191) == 1 : U32}
281
282law v_bch13_mul:
283 {M.Gfm.mul(M.Gfm.bch13(), 1234, 5678) == 4994 : U32}
284
285law v_bch13_inv:
286 {M.Gfm.inv(M.Gfm.bch13(), 1234) == 2297 : U32}
287
288law v_bch13_log:
289 {M.Gfm.log(M.Gfm.bch13(), 1664) == 100 : U32}
290
291law v_bch14_mul:
292 {M.Gfm.mul(M.Gfm.bch14(), 12345, 6789) == 6882 : U32}