1 /* MIT License
2  *
3  * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
4  *
5  * Permission is hereby granted, free of charge, to any person obtaining a copy
6  * of this software and associated documentation files (the "Software"), to deal
7  * in the Software without restriction, including without limitation the rights
8  * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9  * copies of the Software, and to permit persons to whom the Software is
10  * furnished to do so, subject to the following conditions:
11  *
12  * The above copyright notice and this permission notice shall be included in all
13  * copies or substantial portions of the Software.
14  *
15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20  * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21  * SOFTWARE.
22  */
23 
24 #include "Hacl_Curve25519_51.h"
25 
26 static const uint8_t g25519[32U] = { (uint8_t)9U };
27 
28 static void
point_add_and_double(uint64_t * q,uint64_t * p01_tmp1,FStar_UInt128_uint128 * tmp2)29 point_add_and_double(uint64_t *q, uint64_t *p01_tmp1, FStar_UInt128_uint128 *tmp2)
30 {
31     uint64_t *nq = p01_tmp1;
32     uint64_t *nq_p1 = p01_tmp1 + (uint32_t)10U;
33     uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U;
34     uint64_t *x1 = q;
35     uint64_t *x2 = nq;
36     uint64_t *z2 = nq + (uint32_t)5U;
37     uint64_t *z3 = nq_p1 + (uint32_t)5U;
38     uint64_t *a = tmp1;
39     uint64_t *b = tmp1 + (uint32_t)5U;
40     uint64_t *ab = tmp1;
41     uint64_t *dc = tmp1 + (uint32_t)10U;
42     Hacl_Impl_Curve25519_Field51_fadd(a, x2, z2);
43     Hacl_Impl_Curve25519_Field51_fsub(b, x2, z2);
44     uint64_t *x3 = nq_p1;
45     uint64_t *z31 = nq_p1 + (uint32_t)5U;
46     uint64_t *d0 = dc;
47     uint64_t *c0 = dc + (uint32_t)5U;
48     Hacl_Impl_Curve25519_Field51_fadd(c0, x3, z31);
49     Hacl_Impl_Curve25519_Field51_fsub(d0, x3, z31);
50     Hacl_Impl_Curve25519_Field51_fmul2(dc, dc, ab, tmp2);
51     Hacl_Impl_Curve25519_Field51_fadd(x3, d0, c0);
52     Hacl_Impl_Curve25519_Field51_fsub(z31, d0, c0);
53     uint64_t *a1 = tmp1;
54     uint64_t *b1 = tmp1 + (uint32_t)5U;
55     uint64_t *d = tmp1 + (uint32_t)10U;
56     uint64_t *c = tmp1 + (uint32_t)15U;
57     uint64_t *ab1 = tmp1;
58     uint64_t *dc1 = tmp1 + (uint32_t)10U;
59     Hacl_Impl_Curve25519_Field51_fsqr2(dc1, ab1, tmp2);
60     Hacl_Impl_Curve25519_Field51_fsqr2(nq_p1, nq_p1, tmp2);
61     a1[0U] = c[0U];
62     a1[1U] = c[1U];
63     a1[2U] = c[2U];
64     a1[3U] = c[3U];
65     a1[4U] = c[4U];
66     Hacl_Impl_Curve25519_Field51_fsub(c, d, c);
67     Hacl_Impl_Curve25519_Field51_fmul1(b1, c, (uint64_t)121665U);
68     Hacl_Impl_Curve25519_Field51_fadd(b1, b1, d);
69     Hacl_Impl_Curve25519_Field51_fmul2(nq, dc1, ab1, tmp2);
70     Hacl_Impl_Curve25519_Field51_fmul(z3, z3, x1, tmp2);
71 }
72 
73 static void
point_double(uint64_t * nq,uint64_t * tmp1,FStar_UInt128_uint128 * tmp2)74 point_double(uint64_t *nq, uint64_t *tmp1, FStar_UInt128_uint128 *tmp2)
75 {
76     uint64_t *x2 = nq;
77     uint64_t *z2 = nq + (uint32_t)5U;
78     uint64_t *a = tmp1;
79     uint64_t *b = tmp1 + (uint32_t)5U;
80     uint64_t *d = tmp1 + (uint32_t)10U;
81     uint64_t *c = tmp1 + (uint32_t)15U;
82     uint64_t *ab = tmp1;
83     uint64_t *dc = tmp1 + (uint32_t)10U;
84     Hacl_Impl_Curve25519_Field51_fadd(a, x2, z2);
85     Hacl_Impl_Curve25519_Field51_fsub(b, x2, z2);
86     Hacl_Impl_Curve25519_Field51_fsqr2(dc, ab, tmp2);
87     a[0U] = c[0U];
88     a[1U] = c[1U];
89     a[2U] = c[2U];
90     a[3U] = c[3U];
91     a[4U] = c[4U];
92     Hacl_Impl_Curve25519_Field51_fsub(c, d, c);
93     Hacl_Impl_Curve25519_Field51_fmul1(b, c, (uint64_t)121665U);
94     Hacl_Impl_Curve25519_Field51_fadd(b, b, d);
95     Hacl_Impl_Curve25519_Field51_fmul2(nq, dc, ab, tmp2);
96 }
97 
98 static void
montgomery_ladder(uint64_t * out,uint8_t * key,uint64_t * init)99 montgomery_ladder(uint64_t *out, uint8_t *key, uint64_t *init)
100 {
101     FStar_UInt128_uint128 tmp2[10U];
102     for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
103         tmp2[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
104     uint64_t p01_tmp1_swap[41U] = { 0U };
105     uint64_t *p0 = p01_tmp1_swap;
106     uint64_t *p01 = p01_tmp1_swap;
107     uint64_t *p03 = p01;
108     uint64_t *p11 = p01 + (uint32_t)10U;
109     memcpy(p11, init, (uint32_t)10U * sizeof(uint64_t));
110     uint64_t *x0 = p03;
111     uint64_t *z0 = p03 + (uint32_t)5U;
112     x0[0U] = (uint64_t)1U;
113     x0[1U] = (uint64_t)0U;
114     x0[2U] = (uint64_t)0U;
115     x0[3U] = (uint64_t)0U;
116     x0[4U] = (uint64_t)0U;
117     z0[0U] = (uint64_t)0U;
118     z0[1U] = (uint64_t)0U;
119     z0[2U] = (uint64_t)0U;
120     z0[3U] = (uint64_t)0U;
121     z0[4U] = (uint64_t)0U;
122     uint64_t *p01_tmp1 = p01_tmp1_swap;
123     uint64_t *p01_tmp11 = p01_tmp1_swap;
124     uint64_t *nq1 = p01_tmp1_swap;
125     uint64_t *nq_p11 = p01_tmp1_swap + (uint32_t)10U;
126     uint64_t *swap = p01_tmp1_swap + (uint32_t)40U;
127     Hacl_Impl_Curve25519_Field51_cswap2((uint64_t)1U, nq1, nq_p11);
128     point_add_and_double(init, p01_tmp11, tmp2);
129     swap[0U] = (uint64_t)1U;
130     for (uint32_t i = (uint32_t)0U; i < (uint32_t)251U; i++) {
131         uint64_t *p01_tmp12 = p01_tmp1_swap;
132         uint64_t *swap1 = p01_tmp1_swap + (uint32_t)40U;
133         uint64_t *nq2 = p01_tmp12;
134         uint64_t *nq_p12 = p01_tmp12 + (uint32_t)10U;
135         uint64_t
136             bit =
137                 (uint64_t)(key[((uint32_t)253U - i) / (uint32_t)8U] >> ((uint32_t)253U - i) % (uint32_t)8U & (uint8_t)1U);
138         uint64_t sw = swap1[0U] ^ bit;
139         Hacl_Impl_Curve25519_Field51_cswap2(sw, nq2, nq_p12);
140         point_add_and_double(init, p01_tmp12, tmp2);
141         swap1[0U] = bit;
142     }
143     uint64_t sw = swap[0U];
144     Hacl_Impl_Curve25519_Field51_cswap2(sw, nq1, nq_p11);
145     uint64_t *nq10 = p01_tmp1;
146     uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U;
147     point_double(nq10, tmp1, tmp2);
148     point_double(nq10, tmp1, tmp2);
149     point_double(nq10, tmp1, tmp2);
150     memcpy(out, p0, (uint32_t)10U * sizeof(uint64_t));
151 }
152 
153 static void
fsquare_times(uint64_t * o,uint64_t * inp,FStar_UInt128_uint128 * tmp,uint32_t n)154 fsquare_times(uint64_t *o, uint64_t *inp, FStar_UInt128_uint128 *tmp, uint32_t n)
155 {
156     Hacl_Impl_Curve25519_Field51_fsqr(o, inp, tmp);
157     for (uint32_t i = (uint32_t)0U; i < n - (uint32_t)1U; i++) {
158         Hacl_Impl_Curve25519_Field51_fsqr(o, o, tmp);
159     }
160 }
161 
162 static void
finv(uint64_t * o,uint64_t * i,FStar_UInt128_uint128 * tmp)163 finv(uint64_t *o, uint64_t *i, FStar_UInt128_uint128 *tmp)
164 {
165     uint64_t t1[20U] = { 0U };
166     uint64_t *a1 = t1;
167     uint64_t *b1 = t1 + (uint32_t)5U;
168     uint64_t *t010 = t1 + (uint32_t)15U;
169     FStar_UInt128_uint128 *tmp10 = tmp;
170     fsquare_times(a1, i, tmp10, (uint32_t)1U);
171     fsquare_times(t010, a1, tmp10, (uint32_t)2U);
172     Hacl_Impl_Curve25519_Field51_fmul(b1, t010, i, tmp);
173     Hacl_Impl_Curve25519_Field51_fmul(a1, b1, a1, tmp);
174     fsquare_times(t010, a1, tmp10, (uint32_t)1U);
175     Hacl_Impl_Curve25519_Field51_fmul(b1, t010, b1, tmp);
176     fsquare_times(t010, b1, tmp10, (uint32_t)5U);
177     Hacl_Impl_Curve25519_Field51_fmul(b1, t010, b1, tmp);
178     uint64_t *b10 = t1 + (uint32_t)5U;
179     uint64_t *c10 = t1 + (uint32_t)10U;
180     uint64_t *t011 = t1 + (uint32_t)15U;
181     FStar_UInt128_uint128 *tmp11 = tmp;
182     fsquare_times(t011, b10, tmp11, (uint32_t)10U);
183     Hacl_Impl_Curve25519_Field51_fmul(c10, t011, b10, tmp);
184     fsquare_times(t011, c10, tmp11, (uint32_t)20U);
185     Hacl_Impl_Curve25519_Field51_fmul(t011, t011, c10, tmp);
186     fsquare_times(t011, t011, tmp11, (uint32_t)10U);
187     Hacl_Impl_Curve25519_Field51_fmul(b10, t011, b10, tmp);
188     fsquare_times(t011, b10, tmp11, (uint32_t)50U);
189     Hacl_Impl_Curve25519_Field51_fmul(c10, t011, b10, tmp);
190     uint64_t *b11 = t1 + (uint32_t)5U;
191     uint64_t *c1 = t1 + (uint32_t)10U;
192     uint64_t *t01 = t1 + (uint32_t)15U;
193     FStar_UInt128_uint128 *tmp1 = tmp;
194     fsquare_times(t01, c1, tmp1, (uint32_t)100U);
195     Hacl_Impl_Curve25519_Field51_fmul(t01, t01, c1, tmp);
196     fsquare_times(t01, t01, tmp1, (uint32_t)50U);
197     Hacl_Impl_Curve25519_Field51_fmul(t01, t01, b11, tmp);
198     fsquare_times(t01, t01, tmp1, (uint32_t)5U);
199     uint64_t *a = t1;
200     uint64_t *t0 = t1 + (uint32_t)15U;
201     Hacl_Impl_Curve25519_Field51_fmul(o, t0, a, tmp);
202 }
203 
204 static void
encode_point(uint8_t * o,uint64_t * i)205 encode_point(uint8_t *o, uint64_t *i)
206 {
207     uint64_t *x = i;
208     uint64_t *z = i + (uint32_t)5U;
209     uint64_t tmp[5U] = { 0U };
210     uint64_t u64s[4U] = { 0U };
211     FStar_UInt128_uint128 tmp_w[10U];
212     for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
213         tmp_w[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
214     finv(tmp, z, tmp_w);
215     Hacl_Impl_Curve25519_Field51_fmul(tmp, tmp, x, tmp_w);
216     Hacl_Impl_Curve25519_Field51_store_felem(u64s, tmp);
217     for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) {
218         store64_le(o + i0 * (uint32_t)8U, u64s[i0]);
219     }
220 }
221 
222 void
Hacl_Curve25519_51_scalarmult(uint8_t * out,uint8_t * priv,uint8_t * pub)223 Hacl_Curve25519_51_scalarmult(uint8_t *out, uint8_t *priv, uint8_t *pub)
224 {
225     uint64_t init[10U] = { 0U };
226     uint64_t tmp[4U] = { 0U };
227     for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i++) {
228         uint64_t *os = tmp;
229         uint8_t *bj = pub + i * (uint32_t)8U;
230         uint64_t u = load64_le(bj);
231         uint64_t r = u;
232         uint64_t x = r;
233         os[i] = x;
234     }
235     uint64_t tmp3 = tmp[3U];
236     tmp[3U] = tmp3 & (uint64_t)0x7fffffffffffffffU;
237     uint64_t *x = init;
238     uint64_t *z = init + (uint32_t)5U;
239     z[0U] = (uint64_t)1U;
240     z[1U] = (uint64_t)0U;
241     z[2U] = (uint64_t)0U;
242     z[3U] = (uint64_t)0U;
243     z[4U] = (uint64_t)0U;
244     uint64_t f0l = tmp[0U] & (uint64_t)0x7ffffffffffffU;
245     uint64_t f0h = tmp[0U] >> (uint32_t)51U;
246     uint64_t f1l = (tmp[1U] & (uint64_t)0x3fffffffffU) << (uint32_t)13U;
247     uint64_t f1h = tmp[1U] >> (uint32_t)38U;
248     uint64_t f2l = (tmp[2U] & (uint64_t)0x1ffffffU) << (uint32_t)26U;
249     uint64_t f2h = tmp[2U] >> (uint32_t)25U;
250     uint64_t f3l = (tmp[3U] & (uint64_t)0xfffU) << (uint32_t)39U;
251     uint64_t f3h = tmp[3U] >> (uint32_t)12U;
252     x[0U] = f0l;
253     x[1U] = f0h | f1l;
254     x[2U] = f1h | f2l;
255     x[3U] = f2h | f3l;
256     x[4U] = f3h;
257     montgomery_ladder(init, priv, init);
258     encode_point(out, init);
259 }
260 
261 void
Hacl_Curve25519_51_secret_to_public(uint8_t * pub,uint8_t * priv)262 Hacl_Curve25519_51_secret_to_public(uint8_t *pub, uint8_t *priv)
263 {
264     uint8_t basepoint[32U] = { 0U };
265     for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
266         uint8_t *os = basepoint;
267         uint8_t x = g25519[i];
268         os[i] = x;
269     }
270     Hacl_Curve25519_51_scalarmult(pub, priv, basepoint);
271 }
272 
273 bool
Hacl_Curve25519_51_ecdh(uint8_t * out,uint8_t * priv,uint8_t * pub)274 Hacl_Curve25519_51_ecdh(uint8_t *out, uint8_t *priv, uint8_t *pub)
275 {
276     uint8_t zeros[32U] = { 0U };
277     Hacl_Curve25519_51_scalarmult(out, priv, pub);
278     uint8_t res = (uint8_t)255U;
279     for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
280         uint8_t uu____0 = FStar_UInt8_eq_mask(out[i], zeros[i]);
281         res = uu____0 & res;
282     }
283     uint8_t z = res;
284     bool r = z == (uint8_t)255U;
285     return !r;
286 }
287