Hacl_Curve25519_51.c (12175B)
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 "internal/Hacl_Curve25519_51.h" 26 27 #include "internal/Hacl_Krmllib.h" 28 #include "internal/Hacl_Bignum25519_51.h" 29 30 static const uint8_t g25519[32U] = { (uint8_t)9U }; 31 32 static void 33 point_add_and_double(uint64_t *q, uint64_t *p01_tmp1, FStar_UInt128_uint128 *tmp2) 34 { 35 uint64_t *nq = p01_tmp1; 36 uint64_t *nq_p1 = p01_tmp1 + (uint32_t)10U; 37 uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U; 38 uint64_t *x1 = q; 39 uint64_t *x2 = nq; 40 uint64_t *z2 = nq + (uint32_t)5U; 41 uint64_t *z3 = nq_p1 + (uint32_t)5U; 42 uint64_t *a = tmp1; 43 uint64_t *b = tmp1 + (uint32_t)5U; 44 uint64_t *ab = tmp1; 45 uint64_t *dc = tmp1 + (uint32_t)10U; 46 Hacl_Impl_Curve25519_Field51_fadd(a, x2, z2); 47 Hacl_Impl_Curve25519_Field51_fsub(b, x2, z2); 48 uint64_t *x3 = nq_p1; 49 uint64_t *z31 = nq_p1 + (uint32_t)5U; 50 uint64_t *d0 = dc; 51 uint64_t *c0 = dc + (uint32_t)5U; 52 Hacl_Impl_Curve25519_Field51_fadd(c0, x3, z31); 53 Hacl_Impl_Curve25519_Field51_fsub(d0, x3, z31); 54 Hacl_Impl_Curve25519_Field51_fmul2(dc, dc, ab, tmp2); 55 Hacl_Impl_Curve25519_Field51_fadd(x3, d0, c0); 56 Hacl_Impl_Curve25519_Field51_fsub(z31, d0, c0); 57 uint64_t *a1 = tmp1; 58 uint64_t *b1 = tmp1 + (uint32_t)5U; 59 uint64_t *d = tmp1 + (uint32_t)10U; 60 uint64_t *c = tmp1 + (uint32_t)15U; 61 uint64_t *ab1 = tmp1; 62 uint64_t *dc1 = tmp1 + (uint32_t)10U; 63 Hacl_Impl_Curve25519_Field51_fsqr2(dc1, ab1, tmp2); 64 Hacl_Impl_Curve25519_Field51_fsqr2(nq_p1, nq_p1, tmp2); 65 a1[0U] = c[0U]; 66 a1[1U] = c[1U]; 67 a1[2U] = c[2U]; 68 a1[3U] = c[3U]; 69 a1[4U] = c[4U]; 70 Hacl_Impl_Curve25519_Field51_fsub(c, d, c); 71 Hacl_Impl_Curve25519_Field51_fmul1(b1, c, (uint64_t)121665U); 72 Hacl_Impl_Curve25519_Field51_fadd(b1, b1, d); 73 Hacl_Impl_Curve25519_Field51_fmul2(nq, dc1, ab1, tmp2); 74 Hacl_Impl_Curve25519_Field51_fmul(z3, z3, x1, tmp2); 75 } 76 77 static void 78 point_double(uint64_t *nq, uint64_t *tmp1, FStar_UInt128_uint128 *tmp2) 79 { 80 uint64_t *x2 = nq; 81 uint64_t *z2 = nq + (uint32_t)5U; 82 uint64_t *a = tmp1; 83 uint64_t *b = tmp1 + (uint32_t)5U; 84 uint64_t *d = tmp1 + (uint32_t)10U; 85 uint64_t *c = tmp1 + (uint32_t)15U; 86 uint64_t *ab = tmp1; 87 uint64_t *dc = tmp1 + (uint32_t)10U; 88 Hacl_Impl_Curve25519_Field51_fadd(a, x2, z2); 89 Hacl_Impl_Curve25519_Field51_fsub(b, x2, z2); 90 Hacl_Impl_Curve25519_Field51_fsqr2(dc, ab, tmp2); 91 a[0U] = c[0U]; 92 a[1U] = c[1U]; 93 a[2U] = c[2U]; 94 a[3U] = c[3U]; 95 a[4U] = c[4U]; 96 Hacl_Impl_Curve25519_Field51_fsub(c, d, c); 97 Hacl_Impl_Curve25519_Field51_fmul1(b, c, (uint64_t)121665U); 98 Hacl_Impl_Curve25519_Field51_fadd(b, b, d); 99 Hacl_Impl_Curve25519_Field51_fmul2(nq, dc, ab, tmp2); 100 } 101 102 static void 103 montgomery_ladder(uint64_t *out, uint8_t *key, uint64_t *init) 104 { 105 FStar_UInt128_uint128 tmp2[10U]; 106 for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i) 107 tmp2[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 108 uint64_t p01_tmp1_swap[41U] = { 0U }; 109 uint64_t *p0 = p01_tmp1_swap; 110 uint64_t *p01 = p01_tmp1_swap; 111 uint64_t *p03 = p01; 112 uint64_t *p11 = p01 + (uint32_t)10U; 113 memcpy(p11, init, (uint32_t)10U * sizeof(uint64_t)); 114 uint64_t *x0 = p03; 115 uint64_t *z0 = p03 + (uint32_t)5U; 116 x0[0U] = (uint64_t)1U; 117 x0[1U] = (uint64_t)0U; 118 x0[2U] = (uint64_t)0U; 119 x0[3U] = (uint64_t)0U; 120 x0[4U] = (uint64_t)0U; 121 z0[0U] = (uint64_t)0U; 122 z0[1U] = (uint64_t)0U; 123 z0[2U] = (uint64_t)0U; 124 z0[3U] = (uint64_t)0U; 125 z0[4U] = (uint64_t)0U; 126 uint64_t *p01_tmp1 = p01_tmp1_swap; 127 uint64_t *p01_tmp11 = p01_tmp1_swap; 128 uint64_t *nq1 = p01_tmp1_swap; 129 uint64_t *nq_p11 = p01_tmp1_swap + (uint32_t)10U; 130 uint64_t *swap = p01_tmp1_swap + (uint32_t)40U; 131 Hacl_Impl_Curve25519_Field51_cswap2((uint64_t)1U, nq1, nq_p11); 132 point_add_and_double(init, p01_tmp11, tmp2); 133 swap[0U] = (uint64_t)1U; 134 for (uint32_t i = (uint32_t)0U; i < (uint32_t)251U; i++) { 135 uint64_t *p01_tmp12 = p01_tmp1_swap; 136 uint64_t *swap1 = p01_tmp1_swap + (uint32_t)40U; 137 uint64_t *nq2 = p01_tmp12; 138 uint64_t *nq_p12 = p01_tmp12 + (uint32_t)10U; 139 uint64_t 140 bit = 141 (uint64_t)(key[((uint32_t)253U - i) / (uint32_t)8U] >> ((uint32_t)253U - i) % (uint32_t)8U & (uint8_t)1U); 142 uint64_t sw = swap1[0U] ^ bit; 143 Hacl_Impl_Curve25519_Field51_cswap2(sw, nq2, nq_p12); 144 point_add_and_double(init, p01_tmp12, tmp2); 145 swap1[0U] = bit; 146 } 147 uint64_t sw = swap[0U]; 148 Hacl_Impl_Curve25519_Field51_cswap2(sw, nq1, nq_p11); 149 uint64_t *nq10 = p01_tmp1; 150 uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U; 151 point_double(nq10, tmp1, tmp2); 152 point_double(nq10, tmp1, tmp2); 153 point_double(nq10, tmp1, tmp2); 154 memcpy(out, p0, (uint32_t)10U * sizeof(uint64_t)); 155 } 156 157 void 158 Hacl_Curve25519_51_fsquare_times( 159 uint64_t *o, 160 uint64_t *inp, 161 FStar_UInt128_uint128 *tmp, 162 uint32_t n) 163 { 164 Hacl_Impl_Curve25519_Field51_fsqr(o, inp, tmp); 165 for (uint32_t i = (uint32_t)0U; i < n - (uint32_t)1U; i++) { 166 Hacl_Impl_Curve25519_Field51_fsqr(o, o, tmp); 167 } 168 } 169 170 void 171 Hacl_Curve25519_51_finv(uint64_t *o, uint64_t *i, FStar_UInt128_uint128 *tmp) 172 { 173 uint64_t t1[20U] = { 0U }; 174 uint64_t *a1 = t1; 175 uint64_t *b1 = t1 + (uint32_t)5U; 176 uint64_t *t010 = t1 + (uint32_t)15U; 177 FStar_UInt128_uint128 *tmp10 = tmp; 178 Hacl_Curve25519_51_fsquare_times(a1, i, tmp10, (uint32_t)1U); 179 Hacl_Curve25519_51_fsquare_times(t010, a1, tmp10, (uint32_t)2U); 180 Hacl_Impl_Curve25519_Field51_fmul(b1, t010, i, tmp); 181 Hacl_Impl_Curve25519_Field51_fmul(a1, b1, a1, tmp); 182 Hacl_Curve25519_51_fsquare_times(t010, a1, tmp10, (uint32_t)1U); 183 Hacl_Impl_Curve25519_Field51_fmul(b1, t010, b1, tmp); 184 Hacl_Curve25519_51_fsquare_times(t010, b1, tmp10, (uint32_t)5U); 185 Hacl_Impl_Curve25519_Field51_fmul(b1, t010, b1, tmp); 186 uint64_t *b10 = t1 + (uint32_t)5U; 187 uint64_t *c10 = t1 + (uint32_t)10U; 188 uint64_t *t011 = t1 + (uint32_t)15U; 189 FStar_UInt128_uint128 *tmp11 = tmp; 190 Hacl_Curve25519_51_fsquare_times(t011, b10, tmp11, (uint32_t)10U); 191 Hacl_Impl_Curve25519_Field51_fmul(c10, t011, b10, tmp); 192 Hacl_Curve25519_51_fsquare_times(t011, c10, tmp11, (uint32_t)20U); 193 Hacl_Impl_Curve25519_Field51_fmul(t011, t011, c10, tmp); 194 Hacl_Curve25519_51_fsquare_times(t011, t011, tmp11, (uint32_t)10U); 195 Hacl_Impl_Curve25519_Field51_fmul(b10, t011, b10, tmp); 196 Hacl_Curve25519_51_fsquare_times(t011, b10, tmp11, (uint32_t)50U); 197 Hacl_Impl_Curve25519_Field51_fmul(c10, t011, b10, tmp); 198 uint64_t *b11 = t1 + (uint32_t)5U; 199 uint64_t *c1 = t1 + (uint32_t)10U; 200 uint64_t *t01 = t1 + (uint32_t)15U; 201 FStar_UInt128_uint128 *tmp1 = tmp; 202 Hacl_Curve25519_51_fsquare_times(t01, c1, tmp1, (uint32_t)100U); 203 Hacl_Impl_Curve25519_Field51_fmul(t01, t01, c1, tmp); 204 Hacl_Curve25519_51_fsquare_times(t01, t01, tmp1, (uint32_t)50U); 205 Hacl_Impl_Curve25519_Field51_fmul(t01, t01, b11, tmp); 206 Hacl_Curve25519_51_fsquare_times(t01, t01, tmp1, (uint32_t)5U); 207 uint64_t *a = t1; 208 uint64_t *t0 = t1 + (uint32_t)15U; 209 Hacl_Impl_Curve25519_Field51_fmul(o, t0, a, tmp); 210 } 211 212 static void 213 encode_point(uint8_t *o, uint64_t *i) 214 { 215 uint64_t *x = i; 216 uint64_t *z = i + (uint32_t)5U; 217 uint64_t tmp[5U] = { 0U }; 218 uint64_t u64s[4U] = { 0U }; 219 FStar_UInt128_uint128 tmp_w[10U]; 220 for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i) 221 tmp_w[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 222 Hacl_Curve25519_51_finv(tmp, z, tmp_w); 223 Hacl_Impl_Curve25519_Field51_fmul(tmp, tmp, x, tmp_w); 224 Hacl_Impl_Curve25519_Field51_store_felem(u64s, tmp); 225 KRML_MAYBE_FOR4(i0, 226 (uint32_t)0U, 227 (uint32_t)4U, 228 (uint32_t)1U, 229 store64_le(o + i0 * (uint32_t)8U, u64s[i0]);); 230 } 231 232 /** 233 Compute the scalar multiple of a point. 234 235 @param out Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to. 236 @param priv Pointer to 32 bytes of memory where the secret/private key is read from. 237 @param pub Pointer to 32 bytes of memory where the public point is read from. 238 */ 239 void 240 Hacl_Curve25519_51_scalarmult(uint8_t *out, uint8_t *priv, uint8_t *pub) 241 { 242 uint64_t init[10U] = { 0U }; 243 uint64_t tmp[4U] = { 0U }; 244 KRML_MAYBE_FOR4(i, 245 (uint32_t)0U, 246 (uint32_t)4U, 247 (uint32_t)1U, 248 uint64_t *os = tmp; 249 uint8_t *bj = pub + i * (uint32_t)8U; 250 uint64_t u = load64_le(bj); 251 uint64_t r = u; 252 uint64_t x = r; 253 os[i] = x;); 254 uint64_t tmp3 = tmp[3U]; 255 tmp[3U] = tmp3 & (uint64_t)0x7fffffffffffffffU; 256 uint64_t *x = init; 257 uint64_t *z = init + (uint32_t)5U; 258 z[0U] = (uint64_t)1U; 259 z[1U] = (uint64_t)0U; 260 z[2U] = (uint64_t)0U; 261 z[3U] = (uint64_t)0U; 262 z[4U] = (uint64_t)0U; 263 uint64_t f0l = tmp[0U] & (uint64_t)0x7ffffffffffffU; 264 uint64_t f0h = tmp[0U] >> (uint32_t)51U; 265 uint64_t f1l = (tmp[1U] & (uint64_t)0x3fffffffffU) << (uint32_t)13U; 266 uint64_t f1h = tmp[1U] >> (uint32_t)38U; 267 uint64_t f2l = (tmp[2U] & (uint64_t)0x1ffffffU) << (uint32_t)26U; 268 uint64_t f2h = tmp[2U] >> (uint32_t)25U; 269 uint64_t f3l = (tmp[3U] & (uint64_t)0xfffU) << (uint32_t)39U; 270 uint64_t f3h = tmp[3U] >> (uint32_t)12U; 271 x[0U] = f0l; 272 x[1U] = f0h | f1l; 273 x[2U] = f1h | f2l; 274 x[3U] = f2h | f3l; 275 x[4U] = f3h; 276 montgomery_ladder(init, priv, init); 277 encode_point(out, init); 278 } 279 280 /** 281 Calculate a public point from a secret/private key. 282 283 This computes a scalar multiplication of the secret/private key with the curve's basepoint. 284 285 @param pub Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to. 286 @param priv Pointer to 32 bytes of memory where the secret/private key is read from. 287 */ 288 void 289 Hacl_Curve25519_51_secret_to_public(uint8_t *pub, uint8_t *priv) 290 { 291 uint8_t basepoint[32U] = { 0U }; 292 for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) { 293 uint8_t *os = basepoint; 294 uint8_t x = g25519[i]; 295 os[i] = x; 296 } 297 Hacl_Curve25519_51_scalarmult(pub, priv, basepoint); 298 } 299 300 /** 301 Execute the diffie-hellmann key exchange. 302 303 @param out Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to. 304 @param priv Pointer to 32 bytes of memory where **our** secret/private key is read from. 305 @param pub Pointer to 32 bytes of memory where **their** public point is read from. 306 */ 307 bool 308 Hacl_Curve25519_51_ecdh(uint8_t *out, uint8_t *priv, uint8_t *pub) 309 { 310 uint8_t zeros[32U] = { 0U }; 311 Hacl_Curve25519_51_scalarmult(out, priv, pub); 312 uint8_t res = (uint8_t)255U; 313 for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) { 314 uint8_t uu____0 = FStar_UInt8_eq_mask(out[i], zeros[i]); 315 res = uu____0 & res; 316 } 317 uint8_t z = res; 318 bool r = z == (uint8_t)255U; 319 return !r; 320 }