src/crypto/aes/sbox.bend

bend-collections@1.0.0.0 · 161 lines · 6 definitions

1import Base
2
3# The AES S-box and the GF(2^8) doublings MixColumns needs, computed with
4# U32 bit operations only: no table and no branch reads a secret byte.
5#
6# The S-box is the depth-16, 113-gate (+ 4 NOT) circuit of Boyar and Peralta
7# ("A depth-16 circuit for the AES S-box", 2011; the gate list BearSSL's
8# aes_ct uses), evaluated on one byte with one bit per U32 (values 0 or 1).
9# Its input x0..x7 is the byte's bit 7..0 and its output s0..s7 the result's
10# bit 7..0. proofs/crypto/aes/sbox.bend proves it equal, on every input, to
11# FIPS 197's S-box (the inverse in GF(2^8) followed by the affine map).
12# Every mask is the first operand of U32.and, so the bits above the low
13# eight of an input never reach the result.
14def sbox_word(+x: U32) -> U32:
15  +x0 = U32.and(1, U32.shrn(x, 7n))
16  +x1 = U32.and(1, U32.shrn(x, 6n))
17  +x2 = U32.and(1, U32.shrn(x, 5n))
18  +x3 = U32.and(1, U32.shrn(x, 4n))
19  +x4 = U32.and(1, U32.shrn(x, 3n))
20  +x5 = U32.and(1, U32.shrn(x, 2n))
21  +x6 = U32.and(1, U32.shrn(x, 1n))
22  +x7 = U32.and(1, U32.shrn(x, 0n))
23  +y14 = U32.xor(x3, x5)
24  +y13 = U32.xor(x0, x6)
25  +y9 = U32.xor(x0, x3)
26  +y8 = U32.xor(x0, x5)
27  +t0 = U32.xor(x1, x2)
28  +y1 = U32.xor(t0, x7)
29  +y4 = U32.xor(y1, x3)
30  +y12 = U32.xor(y13, y14)
31  +y2 = U32.xor(y1, x0)
32  +y5 = U32.xor(y1, x6)
33  +y3 = U32.xor(y5, y8)
34  +t1 = U32.xor(x4, y12)
35  +y15 = U32.xor(t1, x5)
36  +y20 = U32.xor(t1, x1)
37  +y6 = U32.xor(y15, x7)
38  +y10 = U32.xor(y15, t0)
39  +y11 = U32.xor(y20, y9)
40  +y7 = U32.xor(x7, y11)
41  +y17 = U32.xor(y10, y11)
42  +y19 = U32.xor(y10, y8)
43  +y16 = U32.xor(t0, y11)
44  +y21 = U32.xor(y13, y16)
45  +y18 = U32.xor(x0, y16)
46  +t2 = U32.and(y12, y15)
47  +t3 = U32.and(y3, y6)
48  +t4 = U32.xor(t3, t2)
49  +t5 = U32.and(y4, x7)
50  +t6 = U32.xor(t5, t2)
51  +t7 = U32.and(y13, y16)
52  +t8 = U32.and(y5, y1)
53  +t9 = U32.xor(t8, t7)
54  +t10 = U32.and(y2, y7)
55  +t11 = U32.xor(t10, t7)
56  +t12 = U32.and(y9, y11)
57  +t13 = U32.and(y14, y17)
58  +t14 = U32.xor(t13, t12)
59  +t15 = U32.and(y8, y10)
60  +t16 = U32.xor(t15, t12)
61  +t17 = U32.xor(t4, t14)
62  +t18 = U32.xor(t6, t16)
63  +t19 = U32.xor(t9, t14)
64  +t20 = U32.xor(t11, t16)
65  +t21 = U32.xor(t17, y20)
66  +t22 = U32.xor(t18, y19)
67  +t23 = U32.xor(t19, y21)
68  +t24 = U32.xor(t20, y18)
69  +t25 = U32.xor(t21, t22)
70  +t26 = U32.and(t21, t23)
71  +t27 = U32.xor(t24, t26)
72  +t28 = U32.and(t25, t27)
73  +t29 = U32.xor(t28, t22)
74  +t30 = U32.xor(t23, t24)
75  +t31 = U32.xor(t22, t26)
76  +t32 = U32.and(t31, t30)
77  +t33 = U32.xor(t32, t24)
78  +t34 = U32.xor(t23, t33)
79  +t35 = U32.xor(t27, t33)
80  +t36 = U32.and(t24, t35)
81  +t37 = U32.xor(t36, t34)
82  +t38 = U32.xor(t27, t36)
83  +t39 = U32.and(t29, t38)
84  +t40 = U32.xor(t25, t39)
85  +t41 = U32.xor(t40, t37)
86  +t42 = U32.xor(t29, t33)
87  +t43 = U32.xor(t29, t40)
88  +t44 = U32.xor(t33, t37)
89  +t45 = U32.xor(t42, t41)
90  +z0 = U32.and(t44, y15)
91  +z1 = U32.and(t37, y6)
92  +z2 = U32.and(t33, x7)
93  +z3 = U32.and(t43, y16)
94  +z4 = U32.and(t40, y1)
95  +z5 = U32.and(t29, y7)
96  +z6 = U32.and(t42, y11)
97  +z7 = U32.and(t45, y17)
98  +z8 = U32.and(t41, y10)
99  +z9 = U32.and(t44, y12)
100  +z10 = U32.and(t37, y3)
101  +z11 = U32.and(t33, y4)
102  +z12 = U32.and(t43, y13)
103  +z13 = U32.and(t40, y5)
104  +z14 = U32.and(t29, y2)
105  +z15 = U32.and(t42, y9)
106  +z16 = U32.and(t45, y14)
107  +z17 = U32.and(t41, y8)
108  +t46 = U32.xor(z15, z16)
109  +t47 = U32.xor(z10, z11)
110  +t48 = U32.xor(z5, z13)
111  +t49 = U32.xor(z9, z10)
112  +t50 = U32.xor(z2, z12)
113  +t51 = U32.xor(z2, z5)
114  +t52 = U32.xor(z7, z8)
115  +t53 = U32.xor(z0, z3)
116  +t54 = U32.xor(z6, z7)
117  +t55 = U32.xor(z16, z17)
118  +t56 = U32.xor(z12, t48)
119  +t57 = U32.xor(t50, t53)
120  +t58 = U32.xor(z4, t46)
121  +t59 = U32.xor(z3, t54)
122  +t60 = U32.xor(t46, t57)
123  +t61 = U32.xor(z14, t57)
124  +t62 = U32.xor(t52, t58)
125  +t63 = U32.xor(t49, t58)
126  +t64 = U32.xor(z4, t59)
127  +t65 = U32.xor(t61, t62)
128  +t66 = U32.xor(z1, t63)
129  +s0 = U32.xor(t59, t63)
130  +s6 = U32.xor(t56, U32.xor(1, t62))
131  +s7 = U32.xor(t48, U32.xor(1, t60))
132  +t67 = U32.xor(t64, t65)
133  +s3 = U32.xor(t53, t66)
134  +s4 = U32.xor(t51, t66)
135  +s5 = U32.xor(t47, t65)
136  +s1 = U32.xor(t64, U32.xor(1, s3))
137  +s2 = U32.xor(t55, U32.xor(1, t67))
138  U32.or(U32.shln(s0, 7n), U32.or(U32.shln(s1, 6n), U32.or(U32.shln(s2, 5n), U32.or(U32.shln(s3, 4n), U32.or(U32.shln(s4, 3n), U32.or(U32.shln(s5, 2n), U32.or(U32.shln(s6, 1n), s7)))))))
139
140# The S-box. (The one-constructor match only opens the U32, no branch: it
141# keeps a proof about an unknown word from expanding the 117 gates.)
142def sbox(x: U32) -> U32:
143  match x:
144    case U32{w}: sbox_word(U32{w})
145
146# {02} * x in GF(2^8) (FIPS 197 section 4.2.1, xtime): shift left and, when
147# bit 7 was set, add x^8 = {1b}; the reduction mask is 0 - bit7, not a branch.
148def xtime_word(+x: U32) -> U32:
149  U32.xor(U32.and(254, U32.shln(x, 1n)), U32.and(27, U32.sub(0, U32.and(1, U32.shrn(x, 7n)))))
150
151def xtime(x: U32) -> U32:
152  match x:
153    case U32{w}: xtime_word(U32{w})
154
155# {03} * x = {02} * x + x.
156def mul3_word(+x: U32) -> U32:
157  U32.xor(xtime(x), U32.and(255, x))
158
159def mul3(x: U32) -> U32:
160  match x:
161    case U32{w}: mul3_word(U32{w})