LAWS.bend
bend-osdev-gf@0.1.0.0 · 258 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.0.0/bytes.bend as B
18import bend-osdev-gf@0.1.0.0/gf.bend as G
19import bend-osdev-gf@0.1.0.0/tables.bend as T
20import bend-osdev-gf@0.1.0.0/gf128.bend as H
21import bend-osdev-gf@0.1.0.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) give the reference's results on these vectors;
145# they are tied to the reference for every input by the exhaustive runtime
146# check in check.bend and by ref/run.sh (see the README).
147
148law v_tab_mul_aes:
149 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.aes()), 87, 131)) == 193 : U32}
150
151law v_tab_inv_aes:
152 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.inv(T.Gf8Tab.new(G.Gf8.aes()), 83)) == 202 : U32}
153
154law v_tab_mul_rs:
155 {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}
156
157law v_tab_zero:
158 {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 0, 77)) == 0 : U32}
159
160# GF(2^128) (gf128.bend): vectors only. GCM: Test Case 2 of the GCM
161# specification (McGrew and Viega; H = AES-128 of the zero block under the
162# zero key): X1 = C * H, and GHASH(H, C || lengths). CMAC: the subkeys of
163# SP 800-38B D.1 / RFC 4493 (L = AES-128(K, 0), K1 = 2L, K2 = 4L). The
164# others pin the bit orders against each other. Laws for every input would
165# compute on 128 symbolic bits through 128 rounds; ref/run.sh checks every
166# function against independent implementations instead (see the README).
167# H = 66e94bd4ef8a2c3b884cfa59ca342b2e, C = 0388dace60b6a392f328c2b971b2fe78,
168# and a = 0123456789abcdeffedcba9876543210.
169
170# 5e2ec746917062882c85b0685353deb7
171law v_gcm_x1:
172 {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}
173
174# f38cbb1ad69223dcc3457ae5b6b0f885 (one block of C, then the lengths: 0 bits
175# of A, 128 of C)
176law v_gcm_ghash:
177 {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}
178
179# L = 7df76b0c1ab899b33e42f047b91b546f, K1 = fbeed618357133667c85e08f7236a8de,
180# K2 = f7ddac306ae266ccf90bc11ee46d513b
181law v_cmac_k1:
182 {H.Gf128.double_be(H.Gf128.of_words(2113366796, 448305587, 1044574279, 3105576047)) == H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798) : H.Gf128}
183
184law v_cmac_k2:
185 {H.Gf128.double_be(H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798)) == H.Gf128.of_words(4158499888, 1793222348, 4178297118, 3832369467) : H.Gf128}
186
187# GCM's x is the block 0x40 00 .. 00: mul_x_gcm is multiplication by it
188law v_gcm_mul_x:
189 {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}
190
191law v_gcm_mul_x_value:
192 {H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(9544371, 3302352631, 4285422924, 992614664) : H.Gf128}
193
194# in big-endian order x is the number 2: double_be is multiplication by it
195law v_be_mul_x:
196 {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}
197
198law v_be_mul:
199 {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}
200
201# XTS: the top bit of byte 15 wraps round as 0x87 into byte 0
202law v_xts_wrap:
203 {H.Gf128.double_le(H.Gf128.of_words(0, 0, 0, 255)) == H.Gf128.of_words(2264924160, 0, 0, 254) : H.Gf128}
204
205law v_xts_double:
206 {H.Gf128.double_le(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(38177486, 307731423, 4256789809, 3987235872) : H.Gf128}
207
208law v_gf128_octets:
209 {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>}
210
211law v_gf128_short:
212 {H.Gf128.of_octets(B.Octets.zeros(15n)) == Fail{H.Gf128BadLength{15n}} : Result<&2, &2, H.Gf128Error, H.Gf128>}
213
214# GF(2^m) (gfm.bend). For every field and input: addition commutes. For
215# GF(2^4): multiplication commutes (all 256 pairs) and every nonzero element
216# has an inverse; for GF(2^5), inverses too. Vectors for the BCH fields: x^13
217# = x^4 + x^3 + x + 1, x has order 8191 (so generates GF(2^13)), a product,
218# an inverse and a logarithm (x^100 = 1664), from an independent model
219# (ref/gen.py).
220
221law gfm_add_comm:
222 for +f: M.GfmField
223 for +a: U32
224 for +b: U32
225 {M.Gfm.add(f, a, b) == M.Gfm.add(f, b, a) : U32}
226
227law gfm_mul_comm_gf16:
228 for +a: U32
229 for +b: U32
230 {M.Gfm.mul(M.Gfm.gf16(), a, b) == M.Gfm.mul(M.Gfm.gf16(), b, a) : U32}
231
232law gfm_mul_inv_gf16:
233 for +a: U32
234 for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf16(), a), 0) == False{} : Bool}
235 {M.Gfm.mul(M.Gfm.gf16(), a, M.Gfm.inv(M.Gfm.gf16(), a)) == 1 : U32}
236
237law gfm_mul_inv_gf32:
238 for +a: U32
239 for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf32(), a), 0) == False{} : Bool}
240 {M.Gfm.mul(M.Gfm.gf32(), a, M.Gfm.inv(M.Gfm.gf32(), a)) == 1 : U32}
241
242law v_bch13_x13:
243 {M.Gfm.exp(M.Gfm.bch13(), 13) == 27 : U32}
244
245law v_bch13_order:
246 {M.Gfm.exp(M.Gfm.bch13(), 8191) == 1 : U32}
247
248law v_bch13_mul:
249 {M.Gfm.mul(M.Gfm.bch13(), 1234, 5678) == 4994 : U32}
250
251law v_bch13_inv:
252 {M.Gfm.inv(M.Gfm.bch13(), 1234) == 2297 : U32}
253
254law v_bch13_log:
255 {M.Gfm.log(M.Gfm.bch13(), 1664) == 100 : U32}
256
257law v_bch14_mul:
258 {M.Gfm.mul(M.Gfm.bch14(), 12345, 6789) == 6882 : U32}