/src/nss-nspr/nss/lib/freebl/verified/Hacl_P384.c
Line | Count | Source (jump to first uncovered line) |
1 | | /* MIT License |
2 | | * |
3 | | * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation |
4 | | * Copyright (c) 2022-2023 HACL* Contributors |
5 | | * |
6 | | * Permission is hereby granted, free of charge, to any person obtaining a copy |
7 | | * of this software and associated documentation files (the "Software"), to deal |
8 | | * in the Software without restriction, including without limitation the rights |
9 | | * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
10 | | * copies of the Software, and to permit persons to whom the Software is |
11 | | * furnished to do so, subject to the following conditions: |
12 | | * |
13 | | * The above copyright notice and this permission notice shall be included in all |
14 | | * copies or substantial portions of the Software. |
15 | | * |
16 | | * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
17 | | * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, |
18 | | * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE |
19 | | * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER |
20 | | * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, |
21 | | * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE |
22 | | * SOFTWARE. |
23 | | */ |
24 | | |
25 | | #include "Hacl_P384.h" |
26 | | |
27 | | #include "internal/Hacl_Krmllib.h" |
28 | | #include "internal/Hacl_Bignum_Base.h" |
29 | | |
30 | | static inline uint64_t |
31 | | bn_is_eq_mask(uint64_t *x, uint64_t *y) |
32 | 678 | { |
33 | 678 | uint64_t mask = 0xFFFFFFFFFFFFFFFFULL; |
34 | 678 | KRML_MAYBE_FOR6(i, |
35 | 678 | 0U, |
36 | 678 | 6U, |
37 | 678 | 1U, |
38 | 678 | uint64_t uu____0 = FStar_UInt64_eq_mask(x[i], y[i]); |
39 | 678 | mask = uu____0 & mask;); |
40 | 678 | uint64_t mask1 = mask; |
41 | 678 | return mask1; |
42 | 678 | } |
43 | | |
44 | | static inline void |
45 | | bn_cmovznz(uint64_t *a, uint64_t b, uint64_t *c, uint64_t *d) |
46 | 202 | { |
47 | 202 | uint64_t mask = ~FStar_UInt64_eq_mask(b, 0ULL); |
48 | 202 | KRML_MAYBE_FOR6(i, |
49 | 202 | 0U, |
50 | 202 | 6U, |
51 | 202 | 1U, |
52 | 202 | uint64_t *os = a; |
53 | 202 | uint64_t uu____0 = c[i]; |
54 | 202 | uint64_t x = uu____0 ^ (mask & (d[i] ^ uu____0)); |
55 | 202 | os[i] = x;); |
56 | 202 | } |
57 | | |
58 | | static inline void |
59 | | bn_add_mod(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d) |
60 | 2.15M | { |
61 | 2.15M | uint64_t c10 = 0ULL; |
62 | 2.15M | { |
63 | 2.15M | uint64_t t1 = c[4U * 0U]; |
64 | 2.15M | uint64_t t20 = d[4U * 0U]; |
65 | 2.15M | uint64_t *res_i0 = a + 4U * 0U; |
66 | 2.15M | c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t1, t20, res_i0); |
67 | 2.15M | uint64_t t10 = c[4U * 0U + 1U]; |
68 | 2.15M | uint64_t t21 = d[4U * 0U + 1U]; |
69 | 2.15M | uint64_t *res_i1 = a + 4U * 0U + 1U; |
70 | 2.15M | c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t10, t21, res_i1); |
71 | 2.15M | uint64_t t11 = c[4U * 0U + 2U]; |
72 | 2.15M | uint64_t t22 = d[4U * 0U + 2U]; |
73 | 2.15M | uint64_t *res_i2 = a + 4U * 0U + 2U; |
74 | 2.15M | c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t11, t22, res_i2); |
75 | 2.15M | uint64_t t12 = c[4U * 0U + 3U]; |
76 | 2.15M | uint64_t t2 = d[4U * 0U + 3U]; |
77 | 2.15M | uint64_t *res_i = a + 4U * 0U + 3U; |
78 | 2.15M | c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t12, t2, res_i); |
79 | 2.15M | } |
80 | 2.15M | KRML_MAYBE_FOR2(i, |
81 | 2.15M | 4U, |
82 | 2.15M | 6U, |
83 | 2.15M | 1U, |
84 | 2.15M | uint64_t t1 = c[i]; |
85 | 2.15M | uint64_t t2 = d[i]; |
86 | 2.15M | uint64_t *res_i = a + i; |
87 | 2.15M | c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t1, t2, res_i);); |
88 | 2.15M | uint64_t c0 = c10; |
89 | 2.15M | uint64_t tmp[6U] = { 0U }; |
90 | 2.15M | uint64_t c1 = 0ULL; |
91 | 2.15M | { |
92 | 2.15M | uint64_t t1 = a[4U * 0U]; |
93 | 2.15M | uint64_t t20 = b[4U * 0U]; |
94 | 2.15M | uint64_t *res_i0 = tmp + 4U * 0U; |
95 | 2.15M | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t20, res_i0); |
96 | 2.15M | uint64_t t10 = a[4U * 0U + 1U]; |
97 | 2.15M | uint64_t t21 = b[4U * 0U + 1U]; |
98 | 2.15M | uint64_t *res_i1 = tmp + 4U * 0U + 1U; |
99 | 2.15M | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t10, t21, res_i1); |
100 | 2.15M | uint64_t t11 = a[4U * 0U + 2U]; |
101 | 2.15M | uint64_t t22 = b[4U * 0U + 2U]; |
102 | 2.15M | uint64_t *res_i2 = tmp + 4U * 0U + 2U; |
103 | 2.15M | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t11, t22, res_i2); |
104 | 2.15M | uint64_t t12 = a[4U * 0U + 3U]; |
105 | 2.15M | uint64_t t2 = b[4U * 0U + 3U]; |
106 | 2.15M | uint64_t *res_i = tmp + 4U * 0U + 3U; |
107 | 2.15M | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t12, t2, res_i); |
108 | 2.15M | } |
109 | 2.15M | KRML_MAYBE_FOR2(i, |
110 | 2.15M | 4U, |
111 | 2.15M | 6U, |
112 | 2.15M | 1U, |
113 | 2.15M | uint64_t t1 = a[i]; |
114 | 2.15M | uint64_t t2 = b[i]; |
115 | 2.15M | uint64_t *res_i = tmp + i; |
116 | 2.15M | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t2, res_i);); |
117 | 2.15M | uint64_t c11 = c1; |
118 | 2.15M | uint64_t c2 = c0 - c11; |
119 | 2.15M | KRML_MAYBE_FOR6(i, |
120 | 2.15M | 0U, |
121 | 2.15M | 6U, |
122 | 2.15M | 1U, |
123 | 2.15M | uint64_t *os = a; |
124 | 2.15M | uint64_t x = (c2 & a[i]) | (~c2 & tmp[i]); |
125 | 2.15M | os[i] = x;); |
126 | 2.15M | } |
127 | | |
128 | | static inline uint64_t |
129 | | bn_sub(uint64_t *a, uint64_t *b, uint64_t *c) |
130 | 797 | { |
131 | 797 | uint64_t c1 = 0ULL; |
132 | 797 | { |
133 | 797 | uint64_t t1 = b[4U * 0U]; |
134 | 797 | uint64_t t20 = c[4U * 0U]; |
135 | 797 | uint64_t *res_i0 = a + 4U * 0U; |
136 | 797 | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t20, res_i0); |
137 | 797 | uint64_t t10 = b[4U * 0U + 1U]; |
138 | 797 | uint64_t t21 = c[4U * 0U + 1U]; |
139 | 797 | uint64_t *res_i1 = a + 4U * 0U + 1U; |
140 | 797 | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t10, t21, res_i1); |
141 | 797 | uint64_t t11 = b[4U * 0U + 2U]; |
142 | 797 | uint64_t t22 = c[4U * 0U + 2U]; |
143 | 797 | uint64_t *res_i2 = a + 4U * 0U + 2U; |
144 | 797 | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t11, t22, res_i2); |
145 | 797 | uint64_t t12 = b[4U * 0U + 3U]; |
146 | 797 | uint64_t t2 = c[4U * 0U + 3U]; |
147 | 797 | uint64_t *res_i = a + 4U * 0U + 3U; |
148 | 797 | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t12, t2, res_i); |
149 | 797 | } |
150 | 797 | KRML_MAYBE_FOR2(i, |
151 | 797 | 4U, |
152 | 797 | 6U, |
153 | 797 | 1U, |
154 | 797 | uint64_t t1 = b[i]; |
155 | 797 | uint64_t t2 = c[i]; |
156 | 797 | uint64_t *res_i = a + i; |
157 | 797 | c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t2, res_i);); |
158 | 797 | uint64_t c10 = c1; |
159 | 797 | return c10; |
160 | 797 | } |
161 | | |
162 | | static inline void |
163 | | bn_sub_mod(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d) |
164 | 890k | { |
165 | 890k | uint64_t c10 = 0ULL; |
166 | 890k | { |
167 | 890k | uint64_t t1 = c[4U * 0U]; |
168 | 890k | uint64_t t20 = d[4U * 0U]; |
169 | 890k | uint64_t *res_i0 = a + 4U * 0U; |
170 | 890k | c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t20, res_i0); |
171 | 890k | uint64_t t10 = c[4U * 0U + 1U]; |
172 | 890k | uint64_t t21 = d[4U * 0U + 1U]; |
173 | 890k | uint64_t *res_i1 = a + 4U * 0U + 1U; |
174 | 890k | c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t10, t21, res_i1); |
175 | 890k | uint64_t t11 = c[4U * 0U + 2U]; |
176 | 890k | uint64_t t22 = d[4U * 0U + 2U]; |
177 | 890k | uint64_t *res_i2 = a + 4U * 0U + 2U; |
178 | 890k | c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t11, t22, res_i2); |
179 | 890k | uint64_t t12 = c[4U * 0U + 3U]; |
180 | 890k | uint64_t t2 = d[4U * 0U + 3U]; |
181 | 890k | uint64_t *res_i = a + 4U * 0U + 3U; |
182 | 890k | c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t12, t2, res_i); |
183 | 890k | } |
184 | 890k | KRML_MAYBE_FOR2(i, |
185 | 890k | 4U, |
186 | 890k | 6U, |
187 | 890k | 1U, |
188 | 890k | uint64_t t1 = c[i]; |
189 | 890k | uint64_t t2 = d[i]; |
190 | 890k | uint64_t *res_i = a + i; |
191 | 890k | c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t2, res_i);); |
192 | 890k | uint64_t c0 = c10; |
193 | 890k | uint64_t tmp[6U] = { 0U }; |
194 | 890k | uint64_t c1 = 0ULL; |
195 | 890k | { |
196 | 890k | uint64_t t1 = a[4U * 0U]; |
197 | 890k | uint64_t t20 = b[4U * 0U]; |
198 | 890k | uint64_t *res_i0 = tmp + 4U * 0U; |
199 | 890k | c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t1, t20, res_i0); |
200 | 890k | uint64_t t10 = a[4U * 0U + 1U]; |
201 | 890k | uint64_t t21 = b[4U * 0U + 1U]; |
202 | 890k | uint64_t *res_i1 = tmp + 4U * 0U + 1U; |
203 | 890k | c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t10, t21, res_i1); |
204 | 890k | uint64_t t11 = a[4U * 0U + 2U]; |
205 | 890k | uint64_t t22 = b[4U * 0U + 2U]; |
206 | 890k | uint64_t *res_i2 = tmp + 4U * 0U + 2U; |
207 | 890k | c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t11, t22, res_i2); |
208 | 890k | uint64_t t12 = a[4U * 0U + 3U]; |
209 | 890k | uint64_t t2 = b[4U * 0U + 3U]; |
210 | 890k | uint64_t *res_i = tmp + 4U * 0U + 3U; |
211 | 890k | c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t12, t2, res_i); |
212 | 890k | } |
213 | 890k | KRML_MAYBE_FOR2(i, |
214 | 890k | 4U, |
215 | 890k | 6U, |
216 | 890k | 1U, |
217 | 890k | uint64_t t1 = a[i]; |
218 | 890k | uint64_t t2 = b[i]; |
219 | 890k | uint64_t *res_i = tmp + i; |
220 | 890k | c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t1, t2, res_i);); |
221 | 890k | uint64_t c11 = c1; |
222 | 890k | KRML_MAYBE_UNUSED_VAR(c11); |
223 | 890k | uint64_t c2 = 0ULL - c0; |
224 | 890k | KRML_MAYBE_FOR6(i, |
225 | 890k | 0U, |
226 | 890k | 6U, |
227 | 890k | 1U, |
228 | 890k | uint64_t *os = a; |
229 | 890k | uint64_t x = (c2 & tmp[i]) | (~c2 & a[i]); |
230 | 890k | os[i] = x;); |
231 | 890k | } |
232 | | |
233 | | static inline void |
234 | | bn_mul(uint64_t *a, uint64_t *b, uint64_t *c) |
235 | 1.48M | { |
236 | 1.48M | memset(a, 0U, 12U * sizeof(uint64_t)); |
237 | 1.48M | KRML_MAYBE_FOR6( |
238 | 1.48M | i0, |
239 | 1.48M | 0U, |
240 | 1.48M | 6U, |
241 | 1.48M | 1U, |
242 | 1.48M | uint64_t bj = c[i0]; |
243 | 1.48M | uint64_t *res_j = a + i0; |
244 | 1.48M | uint64_t c1 = 0ULL; |
245 | 1.48M | { |
246 | 1.48M | uint64_t a_i = b[4U * 0U]; |
247 | 1.48M | uint64_t *res_i0 = res_j + 4U * 0U; |
248 | 1.48M | c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c1, res_i0); |
249 | 1.48M | uint64_t a_i0 = b[4U * 0U + 1U]; |
250 | 1.48M | uint64_t *res_i1 = res_j + 4U * 0U + 1U; |
251 | 1.48M | c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, bj, c1, res_i1); |
252 | 1.48M | uint64_t a_i1 = b[4U * 0U + 2U]; |
253 | 1.48M | uint64_t *res_i2 = res_j + 4U * 0U + 2U; |
254 | 1.48M | c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, bj, c1, res_i2); |
255 | 1.48M | uint64_t a_i2 = b[4U * 0U + 3U]; |
256 | 1.48M | uint64_t *res_i = res_j + 4U * 0U + 3U; |
257 | 1.48M | c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, bj, c1, res_i); |
258 | 1.48M | } KRML_MAYBE_FOR2(i, |
259 | 1.48M | 4U, |
260 | 1.48M | 6U, |
261 | 1.48M | 1U, |
262 | 1.48M | uint64_t a_i = b[i]; |
263 | 1.48M | uint64_t *res_i = res_j + i; |
264 | 1.48M | c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c1, res_i);); |
265 | 1.48M | uint64_t r = c1; |
266 | 1.48M | a[6U + i0] = r;); |
267 | 1.48M | } |
268 | | |
269 | | static inline void |
270 | | bn_sqr(uint64_t *a, uint64_t *b) |
271 | 444k | { |
272 | 444k | memset(a, 0U, 12U * sizeof(uint64_t)); |
273 | 444k | KRML_MAYBE_FOR6( |
274 | 444k | i0, |
275 | 444k | 0U, |
276 | 444k | 6U, |
277 | 444k | 1U, |
278 | 444k | uint64_t *ab = b; |
279 | 444k | uint64_t a_j = b[i0]; |
280 | 444k | uint64_t *res_j = a + i0; |
281 | 444k | uint64_t c = 0ULL; |
282 | 444k | for (uint32_t i = 0U; i < i0 / 4U; i++) { |
283 | 444k | uint64_t a_i = ab[4U * i]; |
284 | 444k | uint64_t *res_i0 = res_j + 4U * i; |
285 | 444k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i0); |
286 | 444k | uint64_t a_i0 = ab[4U * i + 1U]; |
287 | 444k | uint64_t *res_i1 = res_j + 4U * i + 1U; |
288 | 444k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, a_j, c, res_i1); |
289 | 444k | uint64_t a_i1 = ab[4U * i + 2U]; |
290 | 444k | uint64_t *res_i2 = res_j + 4U * i + 2U; |
291 | 444k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, a_j, c, res_i2); |
292 | 444k | uint64_t a_i2 = ab[4U * i + 3U]; |
293 | 444k | uint64_t *res_i = res_j + 4U * i + 3U; |
294 | 444k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, a_j, c, res_i); |
295 | 444k | } for (uint32_t i = i0 / 4U * 4U; i < i0; i++) { |
296 | 444k | uint64_t a_i = ab[i]; |
297 | 444k | uint64_t *res_i = res_j + i; |
298 | 444k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i); |
299 | 444k | } uint64_t r = c; |
300 | 444k | a[i0 + i0] = r;); |
301 | 444k | uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(12U, a, a, a); |
302 | 444k | KRML_MAYBE_UNUSED_VAR(c0); |
303 | 444k | uint64_t tmp[12U] = { 0U }; |
304 | 444k | KRML_MAYBE_FOR6(i, |
305 | 444k | 0U, |
306 | 444k | 6U, |
307 | 444k | 1U, |
308 | 444k | FStar_UInt128_uint128 res = FStar_UInt128_mul_wide(b[i], b[i]); |
309 | 444k | uint64_t hi = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, 64U)); |
310 | 444k | uint64_t lo = FStar_UInt128_uint128_to_uint64(res); |
311 | 444k | tmp[2U * i] = lo; |
312 | 444k | tmp[2U * i + 1U] = hi;); |
313 | 444k | uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64(12U, a, tmp, a); |
314 | 444k | KRML_MAYBE_UNUSED_VAR(c1); |
315 | 444k | } |
316 | | |
317 | | static inline void |
318 | | bn_to_bytes_be(uint8_t *a, uint64_t *b) |
319 | 324 | { |
320 | 324 | uint8_t tmp[48U] = { 0U }; |
321 | 324 | KRML_MAYBE_UNUSED_VAR(tmp); |
322 | 324 | KRML_MAYBE_FOR6(i, 0U, 6U, 1U, store64_be(a + i * 8U, b[6U - i - 1U]);); |
323 | 324 | } |
324 | | |
325 | | static inline void |
326 | | bn_from_bytes_be(uint64_t *a, uint8_t *b) |
327 | 696 | { |
328 | 696 | KRML_MAYBE_FOR6(i, |
329 | 696 | 0U, |
330 | 696 | 6U, |
331 | 696 | 1U, |
332 | 696 | uint64_t *os = a; |
333 | 696 | uint64_t u = load64_be(b + (6U - i - 1U) * 8U); |
334 | 696 | uint64_t x = u; |
335 | 696 | os[i] = x;); |
336 | 696 | } |
337 | | |
338 | | static inline void |
339 | | p384_make_prime(uint64_t *n) |
340 | 4.93M | { |
341 | 4.93M | n[0U] = 0x00000000ffffffffULL; |
342 | 4.93M | n[1U] = 0xffffffff00000000ULL; |
343 | 4.93M | n[2U] = 0xfffffffffffffffeULL; |
344 | 4.93M | n[3U] = 0xffffffffffffffffULL; |
345 | 4.93M | n[4U] = 0xffffffffffffffffULL; |
346 | 4.93M | n[5U] = 0xffffffffffffffffULL; |
347 | 4.93M | } |
348 | | |
349 | | static inline void |
350 | | p384_make_order(uint64_t *n) |
351 | 50.0k | { |
352 | 50.0k | n[0U] = 0xecec196accc52973ULL; |
353 | 50.0k | n[1U] = 0x581a0db248b0a77aULL; |
354 | 50.0k | n[2U] = 0xc7634d81f4372ddfULL; |
355 | 50.0k | n[3U] = 0xffffffffffffffffULL; |
356 | 50.0k | n[4U] = 0xffffffffffffffffULL; |
357 | 50.0k | n[5U] = 0xffffffffffffffffULL; |
358 | 50.0k | } |
359 | | |
360 | | static inline void |
361 | | p384_make_a_coeff(uint64_t *a) |
362 | 119 | { |
363 | 119 | a[0U] = 0x00000003fffffffcULL; |
364 | 119 | a[1U] = 0xfffffffc00000000ULL; |
365 | 119 | a[2U] = 0xfffffffffffffffbULL; |
366 | 119 | a[3U] = 0xffffffffffffffffULL; |
367 | 119 | a[4U] = 0xffffffffffffffffULL; |
368 | 119 | a[5U] = 0xffffffffffffffffULL; |
369 | 119 | } |
370 | | |
371 | | static inline void |
372 | | p384_make_b_coeff(uint64_t *b) |
373 | 268k | { |
374 | 268k | b[0U] = 0x081188719d412dccULL; |
375 | 268k | b[1U] = 0xf729add87a4c32ecULL; |
376 | 268k | b[2U] = 0x77f2209b1920022eULL; |
377 | 268k | b[3U] = 0xe3374bee94938ae2ULL; |
378 | 268k | b[4U] = 0xb62b21f41f022094ULL; |
379 | 268k | b[5U] = 0xcd08114b604fbff9ULL; |
380 | 268k | } |
381 | | |
382 | | static inline void |
383 | | p384_make_g_x(uint64_t *n) |
384 | 217 | { |
385 | 217 | n[0U] = 0x3dd0756649c0b528ULL; |
386 | 217 | n[1U] = 0x20e378e2a0d6ce38ULL; |
387 | 217 | n[2U] = 0x879c3afc541b4d6eULL; |
388 | 217 | n[3U] = 0x6454868459a30effULL; |
389 | 217 | n[4U] = 0x812ff723614ede2bULL; |
390 | 217 | n[5U] = 0x4d3aadc2299e1513ULL; |
391 | 217 | } |
392 | | |
393 | | static inline void |
394 | | p384_make_g_y(uint64_t *n) |
395 | 217 | { |
396 | 217 | n[0U] = 0x23043dad4b03a4feULL; |
397 | 217 | n[1U] = 0xa1bfa8bf7bb4a9acULL; |
398 | 217 | n[2U] = 0x8bade7562e83b050ULL; |
399 | 217 | n[3U] = 0xc6c3521968f4ffd9ULL; |
400 | 217 | n[4U] = 0xdd8002263969a840ULL; |
401 | 217 | n[5U] = 0x2b78abc25a15c5e9ULL; |
402 | 217 | } |
403 | | |
404 | | static inline void |
405 | | p384_make_fmont_R2(uint64_t *n) |
406 | 460 | { |
407 | 460 | n[0U] = 0xfffffffe00000001ULL; |
408 | 460 | n[1U] = 0x0000000200000000ULL; |
409 | 460 | n[2U] = 0xfffffffe00000000ULL; |
410 | 460 | n[3U] = 0x0000000200000000ULL; |
411 | 460 | n[4U] = 0x0000000000000001ULL; |
412 | 460 | n[5U] = 0x0ULL; |
413 | 460 | } |
414 | | |
415 | | static inline void |
416 | | p384_make_fzero(uint64_t *n) |
417 | 1.08k | { |
418 | 1.08k | memset(n, 0U, 6U * sizeof(uint64_t)); |
419 | 1.08k | n[0U] = 0ULL; |
420 | 1.08k | } |
421 | | |
422 | | static inline void |
423 | | p384_make_fone(uint64_t *n) |
424 | 1.08k | { |
425 | 1.08k | n[0U] = 0xffffffff00000001ULL; |
426 | 1.08k | n[1U] = 0x00000000ffffffffULL; |
427 | 1.08k | n[2U] = 0x1ULL; |
428 | 1.08k | n[3U] = 0x0ULL; |
429 | 1.08k | n[4U] = 0x0ULL; |
430 | 1.08k | n[5U] = 0x0ULL; |
431 | 1.08k | } |
432 | | |
433 | | static inline void |
434 | | p384_make_qone(uint64_t *f) |
435 | 101 | { |
436 | 101 | f[0U] = 0x1313e695333ad68dULL; |
437 | 101 | f[1U] = 0xa7e5f24db74f5885ULL; |
438 | 101 | f[2U] = 0x389cb27e0bc8d220ULL; |
439 | 101 | f[3U] = 0x0ULL; |
440 | 101 | f[4U] = 0x0ULL; |
441 | 101 | f[5U] = 0x0ULL; |
442 | 101 | } |
443 | | |
444 | | static inline void |
445 | | fmont_reduction(uint64_t *res, uint64_t *x) |
446 | 1.88M | { |
447 | 1.88M | uint64_t n[6U] = { 0U }; |
448 | 1.88M | p384_make_prime(n); |
449 | 1.88M | uint64_t c0 = 0ULL; |
450 | 1.88M | KRML_MAYBE_FOR6( |
451 | 1.88M | i0, |
452 | 1.88M | 0U, |
453 | 1.88M | 6U, |
454 | 1.88M | 1U, |
455 | 1.88M | uint64_t qj = 4294967297ULL * x[i0]; |
456 | 1.88M | uint64_t *res_j0 = x + i0; |
457 | 1.88M | uint64_t c = 0ULL; |
458 | 1.88M | { |
459 | 1.88M | uint64_t a_i = n[4U * 0U]; |
460 | 1.88M | uint64_t *res_i0 = res_j0 + 4U * 0U; |
461 | 1.88M | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0); |
462 | 1.88M | uint64_t a_i0 = n[4U * 0U + 1U]; |
463 | 1.88M | uint64_t *res_i1 = res_j0 + 4U * 0U + 1U; |
464 | 1.88M | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1); |
465 | 1.88M | uint64_t a_i1 = n[4U * 0U + 2U]; |
466 | 1.88M | uint64_t *res_i2 = res_j0 + 4U * 0U + 2U; |
467 | 1.88M | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2); |
468 | 1.88M | uint64_t a_i2 = n[4U * 0U + 3U]; |
469 | 1.88M | uint64_t *res_i = res_j0 + 4U * 0U + 3U; |
470 | 1.88M | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i); |
471 | 1.88M | } KRML_MAYBE_FOR2(i, |
472 | 1.88M | 4U, |
473 | 1.88M | 6U, |
474 | 1.88M | 1U, |
475 | 1.88M | uint64_t a_i = n[i]; |
476 | 1.88M | uint64_t *res_i = res_j0 + i; |
477 | 1.88M | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i);); |
478 | 1.88M | uint64_t r = c; |
479 | 1.88M | uint64_t c1 = r; |
480 | 1.88M | uint64_t *resb = x + 6U + i0; |
481 | 1.88M | uint64_t res_j = x[6U + i0]; |
482 | 1.88M | c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb);); |
483 | 1.88M | memcpy(res, x + 6U, 6U * sizeof(uint64_t)); |
484 | 1.88M | uint64_t c00 = c0; |
485 | 1.88M | uint64_t tmp[6U] = { 0U }; |
486 | 1.88M | uint64_t c = 0ULL; |
487 | 1.88M | { |
488 | 1.88M | uint64_t t1 = res[4U * 0U]; |
489 | 1.88M | uint64_t t20 = n[4U * 0U]; |
490 | 1.88M | uint64_t *res_i0 = tmp + 4U * 0U; |
491 | 1.88M | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); |
492 | 1.88M | uint64_t t10 = res[4U * 0U + 1U]; |
493 | 1.88M | uint64_t t21 = n[4U * 0U + 1U]; |
494 | 1.88M | uint64_t *res_i1 = tmp + 4U * 0U + 1U; |
495 | 1.88M | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); |
496 | 1.88M | uint64_t t11 = res[4U * 0U + 2U]; |
497 | 1.88M | uint64_t t22 = n[4U * 0U + 2U]; |
498 | 1.88M | uint64_t *res_i2 = tmp + 4U * 0U + 2U; |
499 | 1.88M | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); |
500 | 1.88M | uint64_t t12 = res[4U * 0U + 3U]; |
501 | 1.88M | uint64_t t2 = n[4U * 0U + 3U]; |
502 | 1.88M | uint64_t *res_i = tmp + 4U * 0U + 3U; |
503 | 1.88M | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); |
504 | 1.88M | } |
505 | 1.88M | KRML_MAYBE_FOR2(i, |
506 | 1.88M | 4U, |
507 | 1.88M | 6U, |
508 | 1.88M | 1U, |
509 | 1.88M | uint64_t t1 = res[i]; |
510 | 1.88M | uint64_t t2 = n[i]; |
511 | 1.88M | uint64_t *res_i = tmp + i; |
512 | 1.88M | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);); |
513 | 1.88M | uint64_t c1 = c; |
514 | 1.88M | uint64_t c2 = c00 - c1; |
515 | 1.88M | KRML_MAYBE_FOR6(i, |
516 | 1.88M | 0U, |
517 | 1.88M | 6U, |
518 | 1.88M | 1U, |
519 | 1.88M | uint64_t *os = res; |
520 | 1.88M | uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); |
521 | 1.88M | os[i] = x1;); |
522 | 1.88M | } |
523 | | |
524 | | static inline void |
525 | | qmont_reduction(uint64_t *res, uint64_t *x) |
526 | 49.4k | { |
527 | 49.4k | uint64_t n[6U] = { 0U }; |
528 | 49.4k | p384_make_order(n); |
529 | 49.4k | uint64_t c0 = 0ULL; |
530 | 49.4k | KRML_MAYBE_FOR6( |
531 | 49.4k | i0, |
532 | 49.4k | 0U, |
533 | 49.4k | 6U, |
534 | 49.4k | 1U, |
535 | 49.4k | uint64_t qj = 7986114184663260229ULL * x[i0]; |
536 | 49.4k | uint64_t *res_j0 = x + i0; |
537 | 49.4k | uint64_t c = 0ULL; |
538 | 49.4k | { |
539 | 49.4k | uint64_t a_i = n[4U * 0U]; |
540 | 49.4k | uint64_t *res_i0 = res_j0 + 4U * 0U; |
541 | 49.4k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0); |
542 | 49.4k | uint64_t a_i0 = n[4U * 0U + 1U]; |
543 | 49.4k | uint64_t *res_i1 = res_j0 + 4U * 0U + 1U; |
544 | 49.4k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1); |
545 | 49.4k | uint64_t a_i1 = n[4U * 0U + 2U]; |
546 | 49.4k | uint64_t *res_i2 = res_j0 + 4U * 0U + 2U; |
547 | 49.4k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2); |
548 | 49.4k | uint64_t a_i2 = n[4U * 0U + 3U]; |
549 | 49.4k | uint64_t *res_i = res_j0 + 4U * 0U + 3U; |
550 | 49.4k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i); |
551 | 49.4k | } KRML_MAYBE_FOR2(i, |
552 | 49.4k | 4U, |
553 | 49.4k | 6U, |
554 | 49.4k | 1U, |
555 | 49.4k | uint64_t a_i = n[i]; |
556 | 49.4k | uint64_t *res_i = res_j0 + i; |
557 | 49.4k | c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i);); |
558 | 49.4k | uint64_t r = c; |
559 | 49.4k | uint64_t c1 = r; |
560 | 49.4k | uint64_t *resb = x + 6U + i0; |
561 | 49.4k | uint64_t res_j = x[6U + i0]; |
562 | 49.4k | c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb);); |
563 | 49.4k | memcpy(res, x + 6U, 6U * sizeof(uint64_t)); |
564 | 49.4k | uint64_t c00 = c0; |
565 | 49.4k | uint64_t tmp[6U] = { 0U }; |
566 | 49.4k | uint64_t c = 0ULL; |
567 | 49.4k | { |
568 | 49.4k | uint64_t t1 = res[4U * 0U]; |
569 | 49.4k | uint64_t t20 = n[4U * 0U]; |
570 | 49.4k | uint64_t *res_i0 = tmp + 4U * 0U; |
571 | 49.4k | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); |
572 | 49.4k | uint64_t t10 = res[4U * 0U + 1U]; |
573 | 49.4k | uint64_t t21 = n[4U * 0U + 1U]; |
574 | 49.4k | uint64_t *res_i1 = tmp + 4U * 0U + 1U; |
575 | 49.4k | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); |
576 | 49.4k | uint64_t t11 = res[4U * 0U + 2U]; |
577 | 49.4k | uint64_t t22 = n[4U * 0U + 2U]; |
578 | 49.4k | uint64_t *res_i2 = tmp + 4U * 0U + 2U; |
579 | 49.4k | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); |
580 | 49.4k | uint64_t t12 = res[4U * 0U + 3U]; |
581 | 49.4k | uint64_t t2 = n[4U * 0U + 3U]; |
582 | 49.4k | uint64_t *res_i = tmp + 4U * 0U + 3U; |
583 | 49.4k | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); |
584 | 49.4k | } |
585 | 49.4k | KRML_MAYBE_FOR2(i, |
586 | 49.4k | 4U, |
587 | 49.4k | 6U, |
588 | 49.4k | 1U, |
589 | 49.4k | uint64_t t1 = res[i]; |
590 | 49.4k | uint64_t t2 = n[i]; |
591 | 49.4k | uint64_t *res_i = tmp + i; |
592 | 49.4k | c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);); |
593 | 49.4k | uint64_t c1 = c; |
594 | 49.4k | uint64_t c2 = c00 - c1; |
595 | 49.4k | KRML_MAYBE_FOR6(i, |
596 | 49.4k | 0U, |
597 | 49.4k | 6U, |
598 | 49.4k | 1U, |
599 | 49.4k | uint64_t *os = res; |
600 | 49.4k | uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); |
601 | 49.4k | os[i] = x1;); |
602 | 49.4k | } |
603 | | |
604 | | static inline uint64_t |
605 | | bn_is_lt_prime_mask(uint64_t *f) |
606 | 238 | { |
607 | 238 | uint64_t tmp[6U] = { 0U }; |
608 | 238 | p384_make_prime(tmp); |
609 | 238 | uint64_t c = bn_sub(tmp, f, tmp); |
610 | 238 | uint64_t m = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); |
611 | 238 | return m; |
612 | 238 | } |
613 | | |
614 | | static inline void |
615 | | fadd0(uint64_t *a, uint64_t *b, uint64_t *c) |
616 | 2.15M | { |
617 | 2.15M | uint64_t n[6U] = { 0U }; |
618 | 2.15M | p384_make_prime(n); |
619 | 2.15M | bn_add_mod(a, n, b, c); |
620 | 2.15M | } |
621 | | |
622 | | static inline void |
623 | | fsub0(uint64_t *a, uint64_t *b, uint64_t *c) |
624 | 890k | { |
625 | 890k | uint64_t n[6U] = { 0U }; |
626 | 890k | p384_make_prime(n); |
627 | 890k | bn_sub_mod(a, n, b, c); |
628 | 890k | } |
629 | | |
630 | | static inline void |
631 | | fmul0(uint64_t *a, uint64_t *b, uint64_t *c) |
632 | 1.47M | { |
633 | 1.47M | uint64_t tmp[12U] = { 0U }; |
634 | 1.47M | bn_mul(tmp, b, c); |
635 | 1.47M | fmont_reduction(a, tmp); |
636 | 1.47M | } |
637 | | |
638 | | static inline void |
639 | | fsqr0(uint64_t *a, uint64_t *b) |
640 | 405k | { |
641 | 405k | uint64_t tmp[12U] = { 0U }; |
642 | 405k | bn_sqr(tmp, b); |
643 | 405k | fmont_reduction(a, tmp); |
644 | 405k | } |
645 | | |
646 | | static inline void |
647 | | from_mont(uint64_t *a, uint64_t *b) |
648 | 333 | { |
649 | 333 | uint64_t tmp[12U] = { 0U }; |
650 | 333 | memcpy(tmp, b, 6U * sizeof(uint64_t)); |
651 | 333 | fmont_reduction(a, tmp); |
652 | 333 | } |
653 | | |
654 | | static inline void |
655 | | to_mont(uint64_t *a, uint64_t *b) |
656 | 460 | { |
657 | 460 | uint64_t r2modn[6U] = { 0U }; |
658 | 460 | p384_make_fmont_R2(r2modn); |
659 | 460 | uint64_t tmp[12U] = { 0U }; |
660 | 460 | bn_mul(tmp, b, r2modn); |
661 | 460 | fmont_reduction(a, tmp); |
662 | 460 | } |
663 | | |
664 | | static inline void |
665 | | fexp_consttime(uint64_t *out, uint64_t *a, uint64_t *b) |
666 | 217 | { |
667 | 217 | uint64_t table[192U] = { 0U }; |
668 | 217 | uint64_t tmp[6U] = { 0U }; |
669 | 217 | uint64_t *t0 = table; |
670 | 217 | uint64_t *t1 = table + 6U; |
671 | 217 | p384_make_fone(t0); |
672 | 217 | memcpy(t1, a, 6U * sizeof(uint64_t)); |
673 | 217 | KRML_MAYBE_FOR15(i, |
674 | 217 | 0U, |
675 | 217 | 15U, |
676 | 217 | 1U, |
677 | 217 | uint64_t *t11 = table + (i + 1U) * 6U; |
678 | 217 | fsqr0(tmp, t11); |
679 | 217 | memcpy(table + (2U * i + 2U) * 6U, tmp, 6U * sizeof(uint64_t)); |
680 | 217 | uint64_t *t2 = table + (2U * i + 2U) * 6U; |
681 | 217 | fmul0(tmp, a, t2); |
682 | 217 | memcpy(table + (2U * i + 3U) * 6U, tmp, 6U * sizeof(uint64_t));); |
683 | 217 | uint32_t i0 = 380U; |
684 | 217 | uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, i0, 5U); |
685 | 217 | memcpy(out, (uint64_t *)table, 6U * sizeof(uint64_t)); |
686 | 6.94k | for (uint32_t i1 = 0U; i1 < 31U; i1++) { |
687 | 6.72k | uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U)); |
688 | 6.72k | const uint64_t *res_j = table + (i1 + 1U) * 6U; |
689 | 6.72k | KRML_MAYBE_FOR6(i, |
690 | 6.72k | 0U, |
691 | 6.72k | 6U, |
692 | 6.72k | 1U, |
693 | 6.72k | uint64_t *os = out; |
694 | 6.72k | uint64_t x = (c & res_j[i]) | (~c & out[i]); |
695 | 6.72k | os[i] = x;); |
696 | 6.72k | } |
697 | 217 | uint64_t tmp0[6U] = { 0U }; |
698 | 16.7k | for (uint32_t i1 = 0U; i1 < 76U; i1++) { |
699 | 16.4k | KRML_MAYBE_FOR5(i, 0U, 5U, 1U, fsqr0(out, out);); |
700 | 16.4k | uint32_t k = 380U - 5U * i1 - 5U; |
701 | 16.4k | uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, k, 5U); |
702 | 16.4k | memcpy(tmp0, (uint64_t *)table, 6U * sizeof(uint64_t)); |
703 | 527k | for (uint32_t i2 = 0U; i2 < 31U; i2++) { |
704 | 511k | uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U)); |
705 | 511k | const uint64_t *res_j = table + (i2 + 1U) * 6U; |
706 | 511k | KRML_MAYBE_FOR6(i, |
707 | 511k | 0U, |
708 | 511k | 6U, |
709 | 511k | 1U, |
710 | 511k | uint64_t *os = tmp0; |
711 | 511k | uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); |
712 | 511k | os[i] = x;); |
713 | 511k | } |
714 | 16.4k | fmul0(out, out, tmp0); |
715 | 16.4k | } |
716 | 217 | } |
717 | | |
718 | | static inline void |
719 | | p384_finv(uint64_t *res, uint64_t *a) |
720 | 217 | { |
721 | 217 | uint64_t b[6U] = { 0U }; |
722 | 217 | b[0U] = 0x00000000fffffffdULL; |
723 | 217 | b[1U] = 0xffffffff00000000ULL; |
724 | 217 | b[2U] = 0xfffffffffffffffeULL; |
725 | 217 | b[3U] = 0xffffffffffffffffULL; |
726 | 217 | b[4U] = 0xffffffffffffffffULL; |
727 | 217 | b[5U] = 0xffffffffffffffffULL; |
728 | 217 | fexp_consttime(res, a, b); |
729 | 217 | } |
730 | | |
731 | | static inline void |
732 | | p384_fsqrt(uint64_t *res, uint64_t *a) |
733 | 0 | { |
734 | 0 | uint64_t b[6U] = { 0U }; |
735 | 0 | b[0U] = 0x0000000040000000ULL; |
736 | 0 | b[1U] = 0xbfffffffc0000000ULL; |
737 | 0 | b[2U] = 0xffffffffffffffffULL; |
738 | 0 | b[3U] = 0xffffffffffffffffULL; |
739 | 0 | b[4U] = 0xffffffffffffffffULL; |
740 | 0 | b[5U] = 0x3fffffffffffffffULL; |
741 | 0 | fexp_consttime(res, a, b); |
742 | 0 | } |
743 | | |
744 | | static inline uint64_t |
745 | | load_qelem_conditional(uint64_t *a, uint8_t *b) |
746 | 208 | { |
747 | 208 | bn_from_bytes_be(a, b); |
748 | 208 | uint64_t tmp[6U] = { 0U }; |
749 | 208 | p384_make_order(tmp); |
750 | 208 | uint64_t c = bn_sub(tmp, a, tmp); |
751 | 208 | uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); |
752 | 208 | uint64_t bn_zero[6U] = { 0U }; |
753 | 208 | uint64_t res = bn_is_eq_mask(a, bn_zero); |
754 | 208 | uint64_t is_eq_zero = res; |
755 | 208 | uint64_t is_b_valid = is_lt_order & ~is_eq_zero; |
756 | 208 | uint64_t oneq[6U] = { 0U }; |
757 | 208 | memset(oneq, 0U, 6U * sizeof(uint64_t)); |
758 | 208 | oneq[0U] = 1ULL; |
759 | 208 | KRML_MAYBE_FOR6(i, |
760 | 208 | 0U, |
761 | 208 | 6U, |
762 | 208 | 1U, |
763 | 208 | uint64_t *os = a; |
764 | 208 | uint64_t uu____0 = oneq[i]; |
765 | 208 | uint64_t x = uu____0 ^ (is_b_valid & (a[i] ^ uu____0)); |
766 | 208 | os[i] = x;); |
767 | 208 | return is_b_valid; |
768 | 208 | } |
769 | | |
770 | | static inline void |
771 | | qmod_short(uint64_t *a, uint64_t *b) |
772 | 202 | { |
773 | 202 | uint64_t tmp[6U] = { 0U }; |
774 | 202 | p384_make_order(tmp); |
775 | 202 | uint64_t c = bn_sub(tmp, b, tmp); |
776 | 202 | bn_cmovznz(a, c, tmp, b); |
777 | 202 | } |
778 | | |
779 | | static inline void |
780 | | qadd(uint64_t *a, uint64_t *b, uint64_t *c) |
781 | 46 | { |
782 | 46 | uint64_t n[6U] = { 0U }; |
783 | 46 | p384_make_order(n); |
784 | 46 | bn_add_mod(a, n, b, c); |
785 | 46 | } |
786 | | |
787 | | static inline void |
788 | | qmul(uint64_t *a, uint64_t *b, uint64_t *c) |
789 | 9.39k | { |
790 | 9.39k | uint64_t tmp[12U] = { 0U }; |
791 | 9.39k | bn_mul(tmp, b, c); |
792 | 9.39k | qmont_reduction(a, tmp); |
793 | 9.39k | } |
794 | | |
795 | | static inline void |
796 | | qsqr(uint64_t *a, uint64_t *b) |
797 | 39.8k | { |
798 | 39.8k | uint64_t tmp[12U] = { 0U }; |
799 | 39.8k | bn_sqr(tmp, b); |
800 | 39.8k | qmont_reduction(a, tmp); |
801 | 39.8k | } |
802 | | |
803 | | static inline void |
804 | | from_qmont(uint64_t *a, uint64_t *b) |
805 | 156 | { |
806 | 156 | uint64_t tmp[12U] = { 0U }; |
807 | 156 | memcpy(tmp, b, 6U * sizeof(uint64_t)); |
808 | 156 | qmont_reduction(a, tmp); |
809 | 156 | } |
810 | | |
811 | | static inline void |
812 | | qexp_consttime(uint64_t *out, uint64_t *a, uint64_t *b) |
813 | 101 | { |
814 | 101 | uint64_t table[192U] = { 0U }; |
815 | 101 | uint64_t tmp[6U] = { 0U }; |
816 | 101 | uint64_t *t0 = table; |
817 | 101 | uint64_t *t1 = table + 6U; |
818 | 101 | p384_make_qone(t0); |
819 | 101 | memcpy(t1, a, 6U * sizeof(uint64_t)); |
820 | 101 | KRML_MAYBE_FOR15(i, |
821 | 101 | 0U, |
822 | 101 | 15U, |
823 | 101 | 1U, |
824 | 101 | uint64_t *t11 = table + (i + 1U) * 6U; |
825 | 101 | qsqr(tmp, t11); |
826 | 101 | memcpy(table + (2U * i + 2U) * 6U, tmp, 6U * sizeof(uint64_t)); |
827 | 101 | uint64_t *t2 = table + (2U * i + 2U) * 6U; |
828 | 101 | qmul(tmp, a, t2); |
829 | 101 | memcpy(table + (2U * i + 3U) * 6U, tmp, 6U * sizeof(uint64_t));); |
830 | 101 | uint32_t i0 = 380U; |
831 | 101 | uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, i0, 5U); |
832 | 101 | memcpy(out, (uint64_t *)table, 6U * sizeof(uint64_t)); |
833 | 3.23k | for (uint32_t i1 = 0U; i1 < 31U; i1++) { |
834 | 3.13k | uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U)); |
835 | 3.13k | const uint64_t *res_j = table + (i1 + 1U) * 6U; |
836 | 3.13k | KRML_MAYBE_FOR6(i, |
837 | 3.13k | 0U, |
838 | 3.13k | 6U, |
839 | 3.13k | 1U, |
840 | 3.13k | uint64_t *os = out; |
841 | 3.13k | uint64_t x = (c & res_j[i]) | (~c & out[i]); |
842 | 3.13k | os[i] = x;); |
843 | 3.13k | } |
844 | 101 | uint64_t tmp0[6U] = { 0U }; |
845 | 7.77k | for (uint32_t i1 = 0U; i1 < 76U; i1++) { |
846 | 7.67k | KRML_MAYBE_FOR5(i, 0U, 5U, 1U, qsqr(out, out);); |
847 | 7.67k | uint32_t k = 380U - 5U * i1 - 5U; |
848 | 7.67k | uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, k, 5U); |
849 | 7.67k | memcpy(tmp0, (uint64_t *)table, 6U * sizeof(uint64_t)); |
850 | 245k | for (uint32_t i2 = 0U; i2 < 31U; i2++) { |
851 | 237k | uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U)); |
852 | 237k | const uint64_t *res_j = table + (i2 + 1U) * 6U; |
853 | 237k | KRML_MAYBE_FOR6(i, |
854 | 237k | 0U, |
855 | 237k | 6U, |
856 | 237k | 1U, |
857 | 237k | uint64_t *os = tmp0; |
858 | 237k | uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); |
859 | 237k | os[i] = x;); |
860 | 237k | } |
861 | 7.67k | qmul(out, out, tmp0); |
862 | 7.67k | } |
863 | 101 | } |
864 | | |
865 | | static inline void |
866 | | p384_qinv(uint64_t *res, uint64_t *a) |
867 | 101 | { |
868 | 101 | uint64_t b[6U] = { 0U }; |
869 | 101 | b[0U] = 0xecec196accc52971ULL; |
870 | 101 | b[1U] = 0x581a0db248b0a77aULL; |
871 | 101 | b[2U] = 0xc7634d81f4372ddfULL; |
872 | 101 | b[3U] = 0xffffffffffffffffULL; |
873 | 101 | b[4U] = 0xffffffffffffffffULL; |
874 | 101 | b[5U] = 0xffffffffffffffffULL; |
875 | 101 | qexp_consttime(res, a, b); |
876 | 101 | } |
877 | | |
878 | | static inline void |
879 | | point_add(uint64_t *x, uint64_t *y, uint64_t *xy) |
880 | 28.0k | { |
881 | 28.0k | uint64_t tmp[54U] = { 0U }; |
882 | 28.0k | uint64_t *t0 = tmp; |
883 | 28.0k | uint64_t *t1 = tmp + 36U; |
884 | 28.0k | uint64_t *x3 = t1; |
885 | 28.0k | uint64_t *y3 = t1 + 6U; |
886 | 28.0k | uint64_t *z3 = t1 + 12U; |
887 | 28.0k | uint64_t *t01 = t0; |
888 | 28.0k | uint64_t *t11 = t0 + 6U; |
889 | 28.0k | uint64_t *t2 = t0 + 12U; |
890 | 28.0k | uint64_t *t3 = t0 + 18U; |
891 | 28.0k | uint64_t *t4 = t0 + 24U; |
892 | 28.0k | uint64_t *t5 = t0 + 30U; |
893 | 28.0k | uint64_t *x1 = x; |
894 | 28.0k | uint64_t *y1 = x + 6U; |
895 | 28.0k | uint64_t *z10 = x + 12U; |
896 | 28.0k | uint64_t *x20 = y; |
897 | 28.0k | uint64_t *y20 = y + 6U; |
898 | 28.0k | uint64_t *z20 = y + 12U; |
899 | 28.0k | fmul0(t01, x1, x20); |
900 | 28.0k | fmul0(t11, y1, y20); |
901 | 28.0k | fmul0(t2, z10, z20); |
902 | 28.0k | fadd0(t3, x1, y1); |
903 | 28.0k | fadd0(t4, x20, y20); |
904 | 28.0k | fmul0(t3, t3, t4); |
905 | 28.0k | fadd0(t4, t01, t11); |
906 | 28.0k | uint64_t *y10 = x + 6U; |
907 | 28.0k | uint64_t *z11 = x + 12U; |
908 | 28.0k | uint64_t *y2 = y + 6U; |
909 | 28.0k | uint64_t *z21 = y + 12U; |
910 | 28.0k | fsub0(t3, t3, t4); |
911 | 28.0k | fadd0(t4, y10, z11); |
912 | 28.0k | fadd0(t5, y2, z21); |
913 | 28.0k | fmul0(t4, t4, t5); |
914 | 28.0k | fadd0(t5, t11, t2); |
915 | 28.0k | fsub0(t4, t4, t5); |
916 | 28.0k | uint64_t *x10 = x; |
917 | 28.0k | uint64_t *z1 = x + 12U; |
918 | 28.0k | uint64_t *x2 = y; |
919 | 28.0k | uint64_t *z2 = y + 12U; |
920 | 28.0k | fadd0(x3, x10, z1); |
921 | 28.0k | fadd0(y3, x2, z2); |
922 | 28.0k | fmul0(x3, x3, y3); |
923 | 28.0k | fadd0(y3, t01, t2); |
924 | 28.0k | fsub0(y3, x3, y3); |
925 | 28.0k | uint64_t b_coeff[6U] = { 0U }; |
926 | 28.0k | p384_make_b_coeff(b_coeff); |
927 | 28.0k | fmul0(z3, b_coeff, t2); |
928 | 28.0k | fsub0(x3, y3, z3); |
929 | 28.0k | fadd0(z3, x3, x3); |
930 | 28.0k | fadd0(x3, x3, z3); |
931 | 28.0k | fsub0(z3, t11, x3); |
932 | 28.0k | fadd0(x3, t11, x3); |
933 | 28.0k | uint64_t b_coeff0[6U] = { 0U }; |
934 | 28.0k | p384_make_b_coeff(b_coeff0); |
935 | 28.0k | fmul0(y3, b_coeff0, y3); |
936 | 28.0k | fadd0(t11, t2, t2); |
937 | 28.0k | fadd0(t2, t11, t2); |
938 | 28.0k | fsub0(y3, y3, t2); |
939 | 28.0k | fsub0(y3, y3, t01); |
940 | 28.0k | fadd0(t11, y3, y3); |
941 | 28.0k | fadd0(y3, t11, y3); |
942 | 28.0k | fadd0(t11, t01, t01); |
943 | 28.0k | fadd0(t01, t11, t01); |
944 | 28.0k | fsub0(t01, t01, t2); |
945 | 28.0k | fmul0(t11, t4, y3); |
946 | 28.0k | fmul0(t2, t01, y3); |
947 | 28.0k | fmul0(y3, x3, z3); |
948 | 28.0k | fadd0(y3, y3, t2); |
949 | 28.0k | fmul0(x3, t3, x3); |
950 | 28.0k | fsub0(x3, x3, t11); |
951 | 28.0k | fmul0(z3, t4, z3); |
952 | 28.0k | fmul0(t11, t3, t01); |
953 | 28.0k | fadd0(z3, z3, t11); |
954 | 28.0k | memcpy(xy, t1, 18U * sizeof(uint64_t)); |
955 | 28.0k | } |
956 | | |
957 | | static inline void |
958 | | point_double(uint64_t *x, uint64_t *xx) |
959 | 106k | { |
960 | 106k | uint64_t tmp[30U] = { 0U }; |
961 | 106k | uint64_t *x1 = x; |
962 | 106k | uint64_t *z = x + 12U; |
963 | 106k | uint64_t *x3 = xx; |
964 | 106k | uint64_t *y3 = xx + 6U; |
965 | 106k | uint64_t *z3 = xx + 12U; |
966 | 106k | uint64_t *t0 = tmp; |
967 | 106k | uint64_t *t1 = tmp + 6U; |
968 | 106k | uint64_t *t2 = tmp + 12U; |
969 | 106k | uint64_t *t3 = tmp + 18U; |
970 | 106k | uint64_t *t4 = tmp + 24U; |
971 | 106k | uint64_t *x2 = x; |
972 | 106k | uint64_t *y = x + 6U; |
973 | 106k | uint64_t *z1 = x + 12U; |
974 | 106k | fsqr0(t0, x2); |
975 | 106k | fsqr0(t1, y); |
976 | 106k | fsqr0(t2, z1); |
977 | 106k | fmul0(t3, x2, y); |
978 | 106k | fadd0(t3, t3, t3); |
979 | 106k | fmul0(t4, y, z1); |
980 | 106k | fmul0(z3, x1, z); |
981 | 106k | fadd0(z3, z3, z3); |
982 | 106k | uint64_t b_coeff[6U] = { 0U }; |
983 | 106k | p384_make_b_coeff(b_coeff); |
984 | 106k | fmul0(y3, b_coeff, t2); |
985 | 106k | fsub0(y3, y3, z3); |
986 | 106k | fadd0(x3, y3, y3); |
987 | 106k | fadd0(y3, x3, y3); |
988 | 106k | fsub0(x3, t1, y3); |
989 | 106k | fadd0(y3, t1, y3); |
990 | 106k | fmul0(y3, x3, y3); |
991 | 106k | fmul0(x3, x3, t3); |
992 | 106k | fadd0(t3, t2, t2); |
993 | 106k | fadd0(t2, t2, t3); |
994 | 106k | uint64_t b_coeff0[6U] = { 0U }; |
995 | 106k | p384_make_b_coeff(b_coeff0); |
996 | 106k | fmul0(z3, b_coeff0, z3); |
997 | 106k | fsub0(z3, z3, t2); |
998 | 106k | fsub0(z3, z3, t0); |
999 | 106k | fadd0(t3, z3, z3); |
1000 | 106k | fadd0(z3, z3, t3); |
1001 | 106k | fadd0(t3, t0, t0); |
1002 | 106k | fadd0(t0, t3, t0); |
1003 | 106k | fsub0(t0, t0, t2); |
1004 | 106k | fmul0(t0, t0, z3); |
1005 | 106k | fadd0(y3, y3, t0); |
1006 | 106k | fadd0(t0, t4, t4); |
1007 | 106k | fmul0(z3, t0, z3); |
1008 | 106k | fsub0(x3, x3, z3); |
1009 | 106k | fmul0(z3, t0, t1); |
1010 | 106k | fadd0(z3, z3, z3); |
1011 | 106k | fadd0(z3, z3, z3); |
1012 | 106k | } |
1013 | | |
1014 | | static inline void |
1015 | | point_zero(uint64_t *one) |
1016 | 544 | { |
1017 | 544 | uint64_t *x = one; |
1018 | 544 | uint64_t *y = one + 6U; |
1019 | 544 | uint64_t *z = one + 12U; |
1020 | 544 | p384_make_fzero(x); |
1021 | 544 | p384_make_fone(y); |
1022 | 544 | p384_make_fzero(z); |
1023 | 544 | } |
1024 | | |
1025 | | static inline void |
1026 | | point_mul(uint64_t *res, uint64_t *scalar, uint64_t *p) |
1027 | 272 | { |
1028 | 272 | uint64_t table[288U] = { 0U }; |
1029 | 272 | uint64_t tmp[18U] = { 0U }; |
1030 | 272 | uint64_t *t0 = table; |
1031 | 272 | uint64_t *t1 = table + 18U; |
1032 | 272 | point_zero(t0); |
1033 | 272 | memcpy(t1, p, 18U * sizeof(uint64_t)); |
1034 | 272 | KRML_MAYBE_FOR7(i, |
1035 | 272 | 0U, |
1036 | 272 | 7U, |
1037 | 272 | 1U, |
1038 | 272 | uint64_t *t11 = table + (i + 1U) * 18U; |
1039 | 272 | point_double(t11, tmp); |
1040 | 272 | memcpy(table + (2U * i + 2U) * 18U, tmp, 18U * sizeof(uint64_t)); |
1041 | 272 | uint64_t *t2 = table + (2U * i + 2U) * 18U; |
1042 | 272 | point_add(p, t2, tmp); |
1043 | 272 | memcpy(table + (2U * i + 3U) * 18U, tmp, 18U * sizeof(uint64_t));); |
1044 | 272 | point_zero(res); |
1045 | 272 | uint64_t tmp0[18U] = { 0U }; |
1046 | 26.3k | for (uint32_t i0 = 0U; i0 < 96U; i0++) { |
1047 | 26.1k | KRML_MAYBE_FOR4(i, 0U, 4U, 1U, point_double(res, res);); |
1048 | 26.1k | uint32_t k = 384U - 4U * i0 - 4U; |
1049 | 26.1k | uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(6U, scalar, k, 4U); |
1050 | 26.1k | memcpy(tmp0, (uint64_t *)table, 18U * sizeof(uint64_t)); |
1051 | 26.1k | KRML_MAYBE_FOR15( |
1052 | 26.1k | i1, |
1053 | 26.1k | 0U, |
1054 | 26.1k | 15U, |
1055 | 26.1k | 1U, |
1056 | 26.1k | uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i1 + 1U)); |
1057 | 26.1k | const uint64_t *res_j = table + (i1 + 1U) * 18U; |
1058 | 26.1k | for (uint32_t i = 0U; i < 18U; i++) { |
1059 | 26.1k | uint64_t *os = tmp0; |
1060 | 26.1k | uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); |
1061 | 26.1k | os[i] = x; |
1062 | 26.1k | }); |
1063 | 26.1k | point_add(res, tmp0, res); |
1064 | 26.1k | } |
1065 | 272 | } |
1066 | | |
1067 | | static inline void |
1068 | | point_mul_g(uint64_t *res, uint64_t *scalar) |
1069 | 217 | { |
1070 | 217 | uint64_t g[18U] = { 0U }; |
1071 | 217 | uint64_t *x = g; |
1072 | 217 | uint64_t *y = g + 6U; |
1073 | 217 | uint64_t *z = g + 12U; |
1074 | 217 | p384_make_g_x(x); |
1075 | 217 | p384_make_g_y(y); |
1076 | 217 | p384_make_fone(z); |
1077 | 217 | point_mul(res, scalar, g); |
1078 | 217 | } |
1079 | | |
1080 | | static inline void |
1081 | | point_mul_double_g(uint64_t *res, uint64_t *scalar1, uint64_t *scalar2, uint64_t *p) |
1082 | 55 | { |
1083 | 55 | uint64_t tmp[18U] = { 0U }; |
1084 | 55 | point_mul_g(tmp, scalar1); |
1085 | 55 | point_mul(res, scalar2, p); |
1086 | 55 | point_add(res, tmp, res); |
1087 | 55 | } |
1088 | | |
1089 | | static inline bool |
1090 | | ecdsa_sign_msg_as_qelem( |
1091 | | uint8_t *signature, |
1092 | | uint64_t *m_q, |
1093 | | uint8_t *private_key, |
1094 | | uint8_t *nonce) |
1095 | 46 | { |
1096 | 46 | uint64_t rsdk_q[24U] = { 0U }; |
1097 | 46 | uint64_t *r_q = rsdk_q; |
1098 | 46 | uint64_t *s_q = rsdk_q + 6U; |
1099 | 46 | uint64_t *d_a = rsdk_q + 12U; |
1100 | 46 | uint64_t *k_q = rsdk_q + 18U; |
1101 | 46 | uint64_t is_sk_valid = load_qelem_conditional(d_a, private_key); |
1102 | 46 | uint64_t is_nonce_valid = load_qelem_conditional(k_q, nonce); |
1103 | 46 | uint64_t are_sk_nonce_valid = is_sk_valid & is_nonce_valid; |
1104 | 46 | uint64_t p[18U] = { 0U }; |
1105 | 46 | point_mul_g(p, k_q); |
1106 | 46 | uint64_t zinv[6U] = { 0U }; |
1107 | 46 | uint64_t *px = p; |
1108 | 46 | uint64_t *pz = p + 12U; |
1109 | 46 | p384_finv(zinv, pz); |
1110 | 46 | fmul0(r_q, px, zinv); |
1111 | 46 | from_mont(r_q, r_q); |
1112 | 46 | qmod_short(r_q, r_q); |
1113 | 46 | uint64_t kinv[6U] = { 0U }; |
1114 | 46 | p384_qinv(kinv, k_q); |
1115 | 46 | qmul(s_q, r_q, d_a); |
1116 | 46 | from_qmont(m_q, m_q); |
1117 | 46 | qadd(s_q, m_q, s_q); |
1118 | 46 | qmul(s_q, kinv, s_q); |
1119 | 46 | bn_to_bytes_be(signature, r_q); |
1120 | 46 | bn_to_bytes_be(signature + 48U, s_q); |
1121 | 46 | uint64_t bn_zero0[6U] = { 0U }; |
1122 | 46 | uint64_t res = bn_is_eq_mask(r_q, bn_zero0); |
1123 | 46 | uint64_t is_r_zero = res; |
1124 | 46 | uint64_t bn_zero[6U] = { 0U }; |
1125 | 46 | uint64_t res0 = bn_is_eq_mask(s_q, bn_zero); |
1126 | 46 | uint64_t is_s_zero = res0; |
1127 | 46 | uint64_t m = are_sk_nonce_valid & (~is_r_zero & ~is_s_zero); |
1128 | 46 | bool res1 = m == 0xFFFFFFFFFFFFFFFFULL; |
1129 | 46 | return res1; |
1130 | 46 | } |
1131 | | |
1132 | | static inline bool |
1133 | | ecdsa_verify_msg_as_qelem( |
1134 | | uint64_t *m_q, |
1135 | | uint8_t *public_key, |
1136 | | uint8_t *signature_r, |
1137 | | uint8_t *signature_s) |
1138 | 55 | { |
1139 | 55 | uint64_t tmp[42U] = { 0U }; |
1140 | 55 | uint64_t *pk = tmp; |
1141 | 55 | uint64_t *r_q = tmp + 18U; |
1142 | 55 | uint64_t *s_q = tmp + 24U; |
1143 | 55 | uint64_t *u1 = tmp + 30U; |
1144 | 55 | uint64_t *u2 = tmp + 36U; |
1145 | 55 | uint64_t p_aff[12U] = { 0U }; |
1146 | 55 | uint8_t *p_x = public_key; |
1147 | 55 | uint8_t *p_y = public_key + 48U; |
1148 | 55 | uint64_t *bn_p_x = p_aff; |
1149 | 55 | uint64_t *bn_p_y = p_aff + 6U; |
1150 | 55 | bn_from_bytes_be(bn_p_x, p_x); |
1151 | 55 | bn_from_bytes_be(bn_p_y, p_y); |
1152 | 55 | uint64_t *px0 = p_aff; |
1153 | 55 | uint64_t *py0 = p_aff + 6U; |
1154 | 55 | uint64_t lessX = bn_is_lt_prime_mask(px0); |
1155 | 55 | uint64_t lessY = bn_is_lt_prime_mask(py0); |
1156 | 55 | uint64_t res0 = lessX & lessY; |
1157 | 55 | bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL; |
1158 | 55 | bool res; |
1159 | 55 | if (!is_xy_valid) { |
1160 | 0 | res = false; |
1161 | 55 | } else { |
1162 | 55 | uint64_t rp[6U] = { 0U }; |
1163 | 55 | uint64_t tx[6U] = { 0U }; |
1164 | 55 | uint64_t ty[6U] = { 0U }; |
1165 | 55 | uint64_t *px = p_aff; |
1166 | 55 | uint64_t *py = p_aff + 6U; |
1167 | 55 | to_mont(tx, px); |
1168 | 55 | to_mont(ty, py); |
1169 | 55 | uint64_t tmp1[6U] = { 0U }; |
1170 | 55 | fsqr0(rp, tx); |
1171 | 55 | fmul0(rp, rp, tx); |
1172 | 55 | p384_make_a_coeff(tmp1); |
1173 | 55 | fmul0(tmp1, tmp1, tx); |
1174 | 55 | fadd0(rp, tmp1, rp); |
1175 | 55 | p384_make_b_coeff(tmp1); |
1176 | 55 | fadd0(rp, tmp1, rp); |
1177 | 55 | fsqr0(ty, ty); |
1178 | 55 | uint64_t r = bn_is_eq_mask(ty, rp); |
1179 | 55 | uint64_t r0 = r; |
1180 | 55 | bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL; |
1181 | 55 | res = r1; |
1182 | 55 | } |
1183 | 55 | if (res) { |
1184 | 55 | uint64_t *px = p_aff; |
1185 | 55 | uint64_t *py = p_aff + 6U; |
1186 | 55 | uint64_t *rx = pk; |
1187 | 55 | uint64_t *ry = pk + 6U; |
1188 | 55 | uint64_t *rz = pk + 12U; |
1189 | 55 | to_mont(rx, px); |
1190 | 55 | to_mont(ry, py); |
1191 | 55 | p384_make_fone(rz); |
1192 | 55 | } |
1193 | 55 | bool is_pk_valid = res; |
1194 | 55 | bn_from_bytes_be(r_q, signature_r); |
1195 | 55 | bn_from_bytes_be(s_q, signature_s); |
1196 | 55 | uint64_t tmp10[6U] = { 0U }; |
1197 | 55 | p384_make_order(tmp10); |
1198 | 55 | uint64_t c = bn_sub(tmp10, r_q, tmp10); |
1199 | 55 | uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); |
1200 | 55 | uint64_t bn_zero0[6U] = { 0U }; |
1201 | 55 | uint64_t res1 = bn_is_eq_mask(r_q, bn_zero0); |
1202 | 55 | uint64_t is_eq_zero = res1; |
1203 | 55 | uint64_t is_r_valid = is_lt_order & ~is_eq_zero; |
1204 | 55 | uint64_t tmp11[6U] = { 0U }; |
1205 | 55 | p384_make_order(tmp11); |
1206 | 55 | uint64_t c0 = bn_sub(tmp11, s_q, tmp11); |
1207 | 55 | uint64_t is_lt_order0 = FStar_UInt64_gte_mask(c0, 0ULL) & ~FStar_UInt64_eq_mask(c0, 0ULL); |
1208 | 55 | uint64_t bn_zero1[6U] = { 0U }; |
1209 | 55 | uint64_t res2 = bn_is_eq_mask(s_q, bn_zero1); |
1210 | 55 | uint64_t is_eq_zero0 = res2; |
1211 | 55 | uint64_t is_s_valid = is_lt_order0 & ~is_eq_zero0; |
1212 | 55 | bool is_rs_valid = is_r_valid == 0xFFFFFFFFFFFFFFFFULL && is_s_valid == 0xFFFFFFFFFFFFFFFFULL; |
1213 | 55 | if (!(is_pk_valid && is_rs_valid)) { |
1214 | 0 | return false; |
1215 | 0 | } |
1216 | 55 | uint64_t sinv[6U] = { 0U }; |
1217 | 55 | p384_qinv(sinv, s_q); |
1218 | 55 | uint64_t tmp1[6U] = { 0U }; |
1219 | 55 | from_qmont(tmp1, m_q); |
1220 | 55 | qmul(u1, sinv, tmp1); |
1221 | 55 | uint64_t tmp12[6U] = { 0U }; |
1222 | 55 | from_qmont(tmp12, r_q); |
1223 | 55 | qmul(u2, sinv, tmp12); |
1224 | 55 | uint64_t res3[18U] = { 0U }; |
1225 | 55 | point_mul_double_g(res3, u1, u2, pk); |
1226 | 55 | uint64_t *pz0 = res3 + 12U; |
1227 | 55 | uint64_t bn_zero[6U] = { 0U }; |
1228 | 55 | uint64_t res10 = bn_is_eq_mask(pz0, bn_zero); |
1229 | 55 | uint64_t m = res10; |
1230 | 55 | if (m == 0xFFFFFFFFFFFFFFFFULL) { |
1231 | 0 | return false; |
1232 | 0 | } |
1233 | 55 | uint64_t x[6U] = { 0U }; |
1234 | 55 | uint64_t zinv[6U] = { 0U }; |
1235 | 55 | uint64_t *px = res3; |
1236 | 55 | uint64_t *pz = res3 + 12U; |
1237 | 55 | p384_finv(zinv, pz); |
1238 | 55 | fmul0(x, px, zinv); |
1239 | 55 | from_mont(x, x); |
1240 | 55 | qmod_short(x, x); |
1241 | 55 | uint64_t m0 = bn_is_eq_mask(x, r_q); |
1242 | 55 | bool res11 = m0 == 0xFFFFFFFFFFFFFFFFULL; |
1243 | 55 | return res11; |
1244 | 55 | } |
1245 | | |
1246 | | /******************************************************************************* |
1247 | | |
1248 | | Verified C library for ECDSA and ECDH functions over the P-384 NIST curve. |
1249 | | |
1250 | | This module implements signing and verification, key validation, conversions |
1251 | | between various point representations, and ECDH key agreement. |
1252 | | |
1253 | | *******************************************************************************/ |
1254 | | |
1255 | | /*****************/ |
1256 | | /* ECDSA signing */ |
1257 | | /*****************/ |
1258 | | |
1259 | | /** |
1260 | | Create an ECDSA signature WITHOUT hashing first. |
1261 | | |
1262 | | This function is intended to receive a hash of the input. |
1263 | | For convenience, we recommend using one of the hash-and-sign combined functions above. |
1264 | | |
1265 | | The argument `msg` MUST be at least 48 bytes (i.e. `msg_len >= 48`). |
1266 | | |
1267 | | NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs |
1268 | | smaller than 48 bytes. These libraries left-pad the input with enough zeroes to |
1269 | | reach the minimum 48 byte size. Clients who need behavior identical to OpenSSL |
1270 | | need to perform the left-padding themselves. |
1271 | | |
1272 | | The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. |
1273 | | |
1274 | | The outparam `signature` (R || S) points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1275 | | The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. |
1276 | | The arguments `private_key` and `nonce` point to 48 bytes of valid memory, i.e., uint8_t[48]. |
1277 | | |
1278 | | The function also checks whether `private_key` and `nonce` are valid values: |
1279 | | • 0 < `private_key` < the order of the curve |
1280 | | • 0 < `nonce` < the order of the curve |
1281 | | */ |
1282 | | bool |
1283 | | Hacl_P384_ecdsa_sign_p384_without_hash( |
1284 | | uint8_t *signature, |
1285 | | uint32_t msg_len, |
1286 | | uint8_t *msg, |
1287 | | uint8_t *private_key, |
1288 | | uint8_t *nonce) |
1289 | 46 | { |
1290 | 46 | uint64_t m_q[6U] = { 0U }; |
1291 | 46 | uint8_t mHash[48U] = { 0U }; |
1292 | 46 | memcpy(mHash, msg, 48U * sizeof(uint8_t)); |
1293 | 46 | KRML_MAYBE_UNUSED_VAR(msg_len); |
1294 | 46 | uint8_t *mHash48 = mHash; |
1295 | 46 | bn_from_bytes_be(m_q, mHash48); |
1296 | 46 | qmod_short(m_q, m_q); |
1297 | 46 | bool res = ecdsa_sign_msg_as_qelem(signature, m_q, private_key, nonce); |
1298 | 46 | return res; |
1299 | 46 | } |
1300 | | |
1301 | | /**********************/ |
1302 | | /* ECDSA verification */ |
1303 | | /**********************/ |
1304 | | |
1305 | | /** |
1306 | | Verify an ECDSA signature WITHOUT hashing first. |
1307 | | |
1308 | | This function is intended to receive a hash of the input. |
1309 | | For convenience, we recommend using one of the hash-and-verify combined functions above. |
1310 | | |
1311 | | The argument `msg` MUST be at least 48 bytes (i.e. `msg_len >= 48`). |
1312 | | |
1313 | | The function returns `true` if the signature is valid and `false` otherwise. |
1314 | | |
1315 | | The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. |
1316 | | The argument `public_key` (x || y) points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1317 | | The arguments `signature_r` and `signature_s` point to 48 bytes of valid memory, i.e., uint8_t[48]. |
1318 | | |
1319 | | The function also checks whether `public_key` is valid |
1320 | | */ |
1321 | | bool |
1322 | | Hacl_P384_ecdsa_verif_without_hash( |
1323 | | uint32_t msg_len, |
1324 | | uint8_t *msg, |
1325 | | uint8_t *public_key, |
1326 | | uint8_t *signature_r, |
1327 | | uint8_t *signature_s) |
1328 | 55 | { |
1329 | 55 | uint64_t m_q[6U] = { 0U }; |
1330 | 55 | uint8_t mHash[48U] = { 0U }; |
1331 | 55 | memcpy(mHash, msg, 48U * sizeof(uint8_t)); |
1332 | 55 | KRML_MAYBE_UNUSED_VAR(msg_len); |
1333 | 55 | uint8_t *mHash48 = mHash; |
1334 | 55 | bn_from_bytes_be(m_q, mHash48); |
1335 | 55 | qmod_short(m_q, m_q); |
1336 | 55 | bool res = ecdsa_verify_msg_as_qelem(m_q, public_key, signature_r, signature_s); |
1337 | 55 | return res; |
1338 | 55 | } |
1339 | | |
1340 | | /******************/ |
1341 | | /* Key validation */ |
1342 | | /******************/ |
1343 | | |
1344 | | /** |
1345 | | Public key validation. |
1346 | | |
1347 | | The function returns `true` if a public key is valid and `false` otherwise. |
1348 | | |
1349 | | The argument `public_key` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1350 | | |
1351 | | The public key (x || y) is valid (with respect to SP 800-56A): |
1352 | | • the public key is not the “point at infinity”, represented as O. |
1353 | | • the affine x and y coordinates of the point represented by the public key are |
1354 | | in the range [0, p – 1] where p is the prime defining the finite field. |
1355 | | • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation. |
1356 | | The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/ |
1357 | | */ |
1358 | | bool |
1359 | | Hacl_P384_validate_public_key(uint8_t *public_key) |
1360 | 64 | { |
1361 | 64 | uint64_t point_jac[18U] = { 0U }; |
1362 | 64 | uint64_t p_aff[12U] = { 0U }; |
1363 | 64 | uint8_t *p_x = public_key; |
1364 | 64 | uint8_t *p_y = public_key + 48U; |
1365 | 64 | uint64_t *bn_p_x = p_aff; |
1366 | 64 | uint64_t *bn_p_y = p_aff + 6U; |
1367 | 64 | bn_from_bytes_be(bn_p_x, p_x); |
1368 | 64 | bn_from_bytes_be(bn_p_y, p_y); |
1369 | 64 | uint64_t *px0 = p_aff; |
1370 | 64 | uint64_t *py0 = p_aff + 6U; |
1371 | 64 | uint64_t lessX = bn_is_lt_prime_mask(px0); |
1372 | 64 | uint64_t lessY = bn_is_lt_prime_mask(py0); |
1373 | 64 | uint64_t res0 = lessX & lessY; |
1374 | 64 | bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL; |
1375 | 64 | bool res; |
1376 | 64 | if (!is_xy_valid) { |
1377 | 0 | res = false; |
1378 | 64 | } else { |
1379 | 64 | uint64_t rp[6U] = { 0U }; |
1380 | 64 | uint64_t tx[6U] = { 0U }; |
1381 | 64 | uint64_t ty[6U] = { 0U }; |
1382 | 64 | uint64_t *px = p_aff; |
1383 | 64 | uint64_t *py = p_aff + 6U; |
1384 | 64 | to_mont(tx, px); |
1385 | 64 | to_mont(ty, py); |
1386 | 64 | uint64_t tmp[6U] = { 0U }; |
1387 | 64 | fsqr0(rp, tx); |
1388 | 64 | fmul0(rp, rp, tx); |
1389 | 64 | p384_make_a_coeff(tmp); |
1390 | 64 | fmul0(tmp, tmp, tx); |
1391 | 64 | fadd0(rp, tmp, rp); |
1392 | 64 | p384_make_b_coeff(tmp); |
1393 | 64 | fadd0(rp, tmp, rp); |
1394 | 64 | fsqr0(ty, ty); |
1395 | 64 | uint64_t r = bn_is_eq_mask(ty, rp); |
1396 | 64 | uint64_t r0 = r; |
1397 | 64 | bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL; |
1398 | 64 | res = r1; |
1399 | 64 | } |
1400 | 64 | if (res) { |
1401 | 56 | uint64_t *px = p_aff; |
1402 | 56 | uint64_t *py = p_aff + 6U; |
1403 | 56 | uint64_t *rx = point_jac; |
1404 | 56 | uint64_t *ry = point_jac + 6U; |
1405 | 56 | uint64_t *rz = point_jac + 12U; |
1406 | 56 | to_mont(rx, px); |
1407 | 56 | to_mont(ry, py); |
1408 | 56 | p384_make_fone(rz); |
1409 | 56 | } |
1410 | 64 | bool res1 = res; |
1411 | 64 | return res1; |
1412 | 64 | } |
1413 | | |
1414 | | /** |
1415 | | Private key validation. |
1416 | | |
1417 | | The function returns `true` if a private key is valid and `false` otherwise. |
1418 | | |
1419 | | The argument `private_key` points to 48 bytes of valid memory, i.e., uint8_t[48]. |
1420 | | |
1421 | | The private key is valid: |
1422 | | • 0 < `private_key` < the order of the curve |
1423 | | */ |
1424 | | bool |
1425 | | Hacl_P384_validate_private_key(uint8_t *private_key) |
1426 | 39 | { |
1427 | 39 | uint64_t bn_sk[6U] = { 0U }; |
1428 | 39 | bn_from_bytes_be(bn_sk, private_key); |
1429 | 39 | uint64_t tmp[6U] = { 0U }; |
1430 | 39 | p384_make_order(tmp); |
1431 | 39 | uint64_t c = bn_sub(tmp, bn_sk, tmp); |
1432 | 39 | uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); |
1433 | 39 | uint64_t bn_zero[6U] = { 0U }; |
1434 | 39 | uint64_t res = bn_is_eq_mask(bn_sk, bn_zero); |
1435 | 39 | uint64_t is_eq_zero = res; |
1436 | 39 | uint64_t res0 = is_lt_order & ~is_eq_zero; |
1437 | 39 | return res0 == 0xFFFFFFFFFFFFFFFFULL; |
1438 | 39 | } |
1439 | | |
1440 | | /******************************************************************************* |
1441 | | Parsing and Serializing public keys. |
1442 | | |
1443 | | A public key is a point (x, y) on the P-384 NIST curve. |
1444 | | |
1445 | | The point can be represented in the following three ways. |
1446 | | • raw = [ x || y ], 96 bytes |
1447 | | • uncompressed = [ 0x04 || x || y ], 97 bytes |
1448 | | • compressed = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes |
1449 | | |
1450 | | *******************************************************************************/ |
1451 | | |
1452 | | /** |
1453 | | Convert a public key from uncompressed to its raw form. |
1454 | | |
1455 | | The function returns `true` for successful conversion of a public key and `false` otherwise. |
1456 | | |
1457 | | The outparam `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1458 | | The argument `pk` points to 97 bytes of valid memory, i.e., uint8_t[97]. |
1459 | | |
1460 | | The function DOESN'T check whether (x, y) is a valid point. |
1461 | | */ |
1462 | | bool |
1463 | | Hacl_P384_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw) |
1464 | 0 | { |
1465 | 0 | uint8_t pk0 = pk[0U]; |
1466 | 0 | if (pk0 != 0x04U) { |
1467 | 0 | return false; |
1468 | 0 | } |
1469 | 0 | memcpy(pk_raw, pk + 1U, 96U * sizeof(uint8_t)); |
1470 | 0 | return true; |
1471 | 0 | } |
1472 | | |
1473 | | /** |
1474 | | Convert a public key from compressed to its raw form. |
1475 | | |
1476 | | The function returns `true` for successful conversion of a public key and `false` otherwise. |
1477 | | |
1478 | | The outparam `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1479 | | The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. |
1480 | | |
1481 | | The function also checks whether (x, y) is a valid point. |
1482 | | */ |
1483 | | bool |
1484 | | Hacl_P384_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw) |
1485 | 0 | { |
1486 | 0 | uint64_t xa[6U] = { 0U }; |
1487 | 0 | uint64_t ya[6U] = { 0U }; |
1488 | 0 | uint8_t *pk_xb = pk + 1U; |
1489 | 0 | uint8_t s0 = pk[0U]; |
1490 | 0 | uint8_t s01 = s0; |
1491 | 0 | bool b; |
1492 | 0 | if (!(s01 == 0x02U || s01 == 0x03U)) { |
1493 | 0 | b = false; |
1494 | 0 | } else { |
1495 | 0 | uint8_t *xb = pk + 1U; |
1496 | 0 | bn_from_bytes_be(xa, xb); |
1497 | 0 | uint64_t is_x_valid = bn_is_lt_prime_mask(xa); |
1498 | 0 | bool is_x_valid1 = is_x_valid == 0xFFFFFFFFFFFFFFFFULL; |
1499 | 0 | bool is_y_odd = s01 == 0x03U; |
1500 | 0 | if (!is_x_valid1) { |
1501 | 0 | b = false; |
1502 | 0 | } else { |
1503 | 0 | uint64_t y2M[6U] = { 0U }; |
1504 | 0 | uint64_t xM[6U] = { 0U }; |
1505 | 0 | uint64_t yM[6U] = { 0U }; |
1506 | 0 | to_mont(xM, xa); |
1507 | 0 | uint64_t tmp[6U] = { 0U }; |
1508 | 0 | fsqr0(y2M, xM); |
1509 | 0 | fmul0(y2M, y2M, xM); |
1510 | 0 | p384_make_a_coeff(tmp); |
1511 | 0 | fmul0(tmp, tmp, xM); |
1512 | 0 | fadd0(y2M, tmp, y2M); |
1513 | 0 | p384_make_b_coeff(tmp); |
1514 | 0 | fadd0(y2M, tmp, y2M); |
1515 | 0 | p384_fsqrt(yM, y2M); |
1516 | 0 | from_mont(ya, yM); |
1517 | 0 | fsqr0(yM, yM); |
1518 | 0 | uint64_t r = bn_is_eq_mask(yM, y2M); |
1519 | 0 | uint64_t r0 = r; |
1520 | 0 | bool is_y_valid = r0 == 0xFFFFFFFFFFFFFFFFULL; |
1521 | 0 | bool is_y_valid0 = is_y_valid; |
1522 | 0 | if (!is_y_valid0) { |
1523 | 0 | b = false; |
1524 | 0 | } else { |
1525 | 0 | uint64_t is_y_odd1 = ya[0U] & 1ULL; |
1526 | 0 | bool is_y_odd2 = is_y_odd1 == 1ULL; |
1527 | 0 | uint64_t zero[6U] = { 0U }; |
1528 | 0 | if (is_y_odd2 != is_y_odd) { |
1529 | 0 | fsub0(ya, zero, ya); |
1530 | 0 | } |
1531 | 0 | b = true; |
1532 | 0 | } |
1533 | 0 | } |
1534 | 0 | } |
1535 | 0 | if (b) { |
1536 | 0 | memcpy(pk_raw, pk_xb, 48U * sizeof(uint8_t)); |
1537 | 0 | bn_to_bytes_be(pk_raw + 48U, ya); |
1538 | 0 | } |
1539 | 0 | return b; |
1540 | 0 | } |
1541 | | |
1542 | | /** |
1543 | | Convert a public key from raw to its uncompressed form. |
1544 | | |
1545 | | The outparam `pk` points to 97 bytes of valid memory, i.e., uint8_t[97]. |
1546 | | The argument `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1547 | | |
1548 | | The function DOESN'T check whether (x, y) is a valid point. |
1549 | | */ |
1550 | | void |
1551 | | Hacl_P384_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk) |
1552 | 0 | { |
1553 | 0 | pk[0U] = 0x04U; |
1554 | 0 | memcpy(pk + 1U, pk_raw, 96U * sizeof(uint8_t)); |
1555 | 0 | } |
1556 | | |
1557 | | /** |
1558 | | Convert a public key from raw to its compressed form. |
1559 | | |
1560 | | The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. |
1561 | | The argument `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1562 | | |
1563 | | The function DOESN'T check whether (x, y) is a valid point. |
1564 | | */ |
1565 | | void |
1566 | | Hacl_P384_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk) |
1567 | 0 | { |
1568 | 0 | uint8_t *pk_x = pk_raw; |
1569 | 0 | uint8_t *pk_y = pk_raw + 48U; |
1570 | 0 | uint64_t bn_f[6U] = { 0U }; |
1571 | 0 | bn_from_bytes_be(bn_f, pk_y); |
1572 | 0 | uint64_t is_odd_f = bn_f[0U] & 1ULL; |
1573 | 0 | pk[0U] = (uint32_t)(uint8_t)is_odd_f + 0x02U; |
1574 | 0 | memcpy(pk + 1U, pk_x, 48U * sizeof(uint8_t)); |
1575 | 0 | } |
1576 | | |
1577 | | /******************/ |
1578 | | /* ECDH agreement */ |
1579 | | /******************/ |
1580 | | |
1581 | | /** |
1582 | | Compute the public key from the private key. |
1583 | | |
1584 | | The function returns `true` if a private key is valid and `false` otherwise. |
1585 | | |
1586 | | The outparam `public_key` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1587 | | The argument `private_key` points to 48 bytes of valid memory, i.e., uint8_t[48]. |
1588 | | |
1589 | | The private key is valid: |
1590 | | • 0 < `private_key` < the order of the curve. |
1591 | | */ |
1592 | | bool |
1593 | | Hacl_P384_dh_initiator(uint8_t *public_key, uint8_t *private_key) |
1594 | 116 | { |
1595 | 116 | uint64_t tmp[24U] = { 0U }; |
1596 | 116 | uint64_t *sk = tmp; |
1597 | 116 | uint64_t *pk = tmp + 6U; |
1598 | 116 | uint64_t is_sk_valid = load_qelem_conditional(sk, private_key); |
1599 | 116 | point_mul_g(pk, sk); |
1600 | 116 | uint64_t aff_p[12U] = { 0U }; |
1601 | 116 | uint64_t zinv[6U] = { 0U }; |
1602 | 116 | uint64_t *px = pk; |
1603 | 116 | uint64_t *py0 = pk + 6U; |
1604 | 116 | uint64_t *pz = pk + 12U; |
1605 | 116 | uint64_t *x = aff_p; |
1606 | 116 | uint64_t *y = aff_p + 6U; |
1607 | 116 | p384_finv(zinv, pz); |
1608 | 116 | fmul0(x, px, zinv); |
1609 | 116 | fmul0(y, py0, zinv); |
1610 | 116 | from_mont(x, x); |
1611 | 116 | from_mont(y, y); |
1612 | 116 | uint64_t *px0 = aff_p; |
1613 | 116 | uint64_t *py = aff_p + 6U; |
1614 | 116 | bn_to_bytes_be(public_key, px0); |
1615 | 116 | bn_to_bytes_be(public_key + 48U, py); |
1616 | 116 | return is_sk_valid == 0xFFFFFFFFFFFFFFFFULL; |
1617 | 116 | } |
1618 | | |
1619 | | /** |
1620 | | Execute the diffie-hellmann key exchange. |
1621 | | |
1622 | | The function returns `true` for successful creation of an ECDH shared secret and |
1623 | | `false` otherwise. |
1624 | | |
1625 | | The outparam `shared_secret` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1626 | | The argument `their_pubkey` points to 96 bytes of valid memory, i.e., uint8_t[96]. |
1627 | | The argument `private_key` points to 48 bytes of valid memory, i.e., uint8_t[48]. |
1628 | | |
1629 | | The function also checks whether `private_key` and `their_pubkey` are valid. |
1630 | | */ |
1631 | | bool |
1632 | | Hacl_P384_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key) |
1633 | 0 | { |
1634 | 0 | uint64_t tmp[192U] = { 0U }; |
1635 | 0 | uint64_t *sk = tmp; |
1636 | 0 | uint64_t *pk = tmp + 6U; |
1637 | 0 | uint64_t p_aff[12U] = { 0U }; |
1638 | 0 | uint8_t *p_x = their_pubkey; |
1639 | 0 | uint8_t *p_y = their_pubkey + 48U; |
1640 | 0 | uint64_t *bn_p_x = p_aff; |
1641 | 0 | uint64_t *bn_p_y = p_aff + 6U; |
1642 | 0 | bn_from_bytes_be(bn_p_x, p_x); |
1643 | 0 | bn_from_bytes_be(bn_p_y, p_y); |
1644 | 0 | uint64_t *px0 = p_aff; |
1645 | 0 | uint64_t *py0 = p_aff + 6U; |
1646 | 0 | uint64_t lessX = bn_is_lt_prime_mask(px0); |
1647 | 0 | uint64_t lessY = bn_is_lt_prime_mask(py0); |
1648 | 0 | uint64_t res0 = lessX & lessY; |
1649 | 0 | bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL; |
1650 | 0 | bool res; |
1651 | 0 | if (!is_xy_valid) { |
1652 | 0 | res = false; |
1653 | 0 | } else { |
1654 | 0 | uint64_t rp[6U] = { 0U }; |
1655 | 0 | uint64_t tx[6U] = { 0U }; |
1656 | 0 | uint64_t ty[6U] = { 0U }; |
1657 | 0 | uint64_t *px = p_aff; |
1658 | 0 | uint64_t *py = p_aff + 6U; |
1659 | 0 | to_mont(tx, px); |
1660 | 0 | to_mont(ty, py); |
1661 | 0 | uint64_t tmp1[6U] = { 0U }; |
1662 | 0 | fsqr0(rp, tx); |
1663 | 0 | fmul0(rp, rp, tx); |
1664 | 0 | p384_make_a_coeff(tmp1); |
1665 | 0 | fmul0(tmp1, tmp1, tx); |
1666 | 0 | fadd0(rp, tmp1, rp); |
1667 | 0 | p384_make_b_coeff(tmp1); |
1668 | 0 | fadd0(rp, tmp1, rp); |
1669 | 0 | fsqr0(ty, ty); |
1670 | 0 | uint64_t r = bn_is_eq_mask(ty, rp); |
1671 | 0 | uint64_t r0 = r; |
1672 | 0 | bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL; |
1673 | 0 | res = r1; |
1674 | 0 | } |
1675 | 0 | if (res) { |
1676 | 0 | uint64_t *px = p_aff; |
1677 | 0 | uint64_t *py = p_aff + 6U; |
1678 | 0 | uint64_t *rx = pk; |
1679 | 0 | uint64_t *ry = pk + 6U; |
1680 | 0 | uint64_t *rz = pk + 12U; |
1681 | 0 | to_mont(rx, px); |
1682 | 0 | to_mont(ry, py); |
1683 | 0 | p384_make_fone(rz); |
1684 | 0 | } |
1685 | 0 | bool is_pk_valid = res; |
1686 | 0 | uint64_t is_sk_valid = load_qelem_conditional(sk, private_key); |
1687 | 0 | uint64_t ss_proj[18U] = { 0U }; |
1688 | 0 | if (is_pk_valid) { |
1689 | 0 | point_mul(ss_proj, sk, pk); |
1690 | 0 | uint64_t aff_p[12U] = { 0U }; |
1691 | 0 | uint64_t zinv[6U] = { 0U }; |
1692 | 0 | uint64_t *px = ss_proj; |
1693 | 0 | uint64_t *py1 = ss_proj + 6U; |
1694 | 0 | uint64_t *pz = ss_proj + 12U; |
1695 | 0 | uint64_t *x = aff_p; |
1696 | 0 | uint64_t *y = aff_p + 6U; |
1697 | 0 | p384_finv(zinv, pz); |
1698 | 0 | fmul0(x, px, zinv); |
1699 | 0 | fmul0(y, py1, zinv); |
1700 | 0 | from_mont(x, x); |
1701 | 0 | from_mont(y, y); |
1702 | 0 | uint64_t *px1 = aff_p; |
1703 | 0 | uint64_t *py = aff_p + 6U; |
1704 | 0 | bn_to_bytes_be(shared_secret, px1); |
1705 | 0 | bn_to_bytes_be(shared_secret + 48U, py); |
1706 | 0 | } |
1707 | 0 | return is_sk_valid == 0xFFFFFFFFFFFFFFFFULL && is_pk_valid; |
1708 | 0 | } |