/* MIT License * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors * * Permission is hereby granted, free of charge, to any person obtaining a copy * of this software and associated documentation files (the "Software"), to deal * in the Software without restriction, including without limitation the rights * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell * copies of the Software, and to permit persons to whom the Software is * furnished to do so, subject to the following conditions: * * The above copyright notice and this permission notice shall be included in all * copies or substantial portions of the Software. * * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE * SOFTWARE. */ #ifndef __Hacl_P256_H #define __Hacl_P256_H #if defined(__cplusplus) extern "C" { #endif #include #include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" #include "Hacl_Krmllib.h" #include "Hacl_Hash_SHA2.h" #include "lib_intrinsics.h" /******************************************************************************* Verified C library for ECDSA and ECDH functions over the P-256 NIST curve. This module implements signing and verification, key validation, conversions between various point representations, and ECDH key agreement. *******************************************************************************/ /*****************/ /* ECDSA signing */ /*****************/ /* As per the standard, a hash function *shall* be used. Therefore, we recommend using one of the three combined hash-and-sign variants. */ /** Create an ECDSA signature using SHA2-256. The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `private_key` and `nonce` are valid: • 0 < `private_key` < the order of the curve • 0 < `nonce` < the order of the curve */ bool Hacl_P256_ecdsa_sign_p256_sha2( uint8_t *signature, uint32_t msg_len, uint8_t *msg, uint8_t *private_key, uint8_t *nonce ); /** Create an ECDSA signature using SHA2-384. The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `private_key` and `nonce` are valid: • 0 < `private_key` < the order of the curve • 0 < `nonce` < the order of the curve */ bool Hacl_P256_ecdsa_sign_p256_sha384( uint8_t *signature, uint32_t msg_len, uint8_t *msg, uint8_t *private_key, uint8_t *nonce ); /** Create an ECDSA signature using SHA2-512. The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `private_key` and `nonce` are valid: • 0 < `private_key` < the order of the curve • 0 < `nonce` < the order of the curve */ bool Hacl_P256_ecdsa_sign_p256_sha512( uint8_t *signature, uint32_t msg_len, uint8_t *msg, uint8_t *private_key, uint8_t *nonce ); /** Create an ECDSA signature WITHOUT hashing first. This function is intended to receive a hash of the input. For convenience, we recommend using one of the hash-and-sign combined functions above. The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`). NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs smaller than 32 bytes. These libraries left-pad the input with enough zeroes to reach the minimum 32 byte size. Clients who need behavior identical to OpenSSL need to perform the left-padding themselves. The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `private_key` and `nonce` are valid values: • 0 < `private_key` < the order of the curve • 0 < `nonce` < the order of the curve */ bool Hacl_P256_ecdsa_sign_p256_without_hash( uint8_t *signature, uint32_t msg_len, uint8_t *msg, uint8_t *private_key, uint8_t *nonce ); /**********************/ /* ECDSA verification */ /**********************/ /** Verify an ECDSA signature using SHA2-256. The function returns `true` if the signature is valid and `false` otherwise. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64]. The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `public_key` is valid */ bool Hacl_P256_ecdsa_verif_p256_sha2( uint32_t msg_len, uint8_t *msg, uint8_t *public_key, uint8_t *signature_r, uint8_t *signature_s ); /** Verify an ECDSA signature using SHA2-384. The function returns `true` if the signature is valid and `false` otherwise. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64]. The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `public_key` is valid */ bool Hacl_P256_ecdsa_verif_p256_sha384( uint32_t msg_len, uint8_t *msg, uint8_t *public_key, uint8_t *signature_r, uint8_t *signature_s ); /** Verify an ECDSA signature using SHA2-512. The function returns `true` if the signature is valid and `false` otherwise. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64]. The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `public_key` is valid */ bool Hacl_P256_ecdsa_verif_p256_sha512( uint32_t msg_len, uint8_t *msg, uint8_t *public_key, uint8_t *signature_r, uint8_t *signature_s ); /** Verify an ECDSA signature WITHOUT hashing first. This function is intended to receive a hash of the input. For convenience, we recommend using one of the hash-and-verify combined functions above. The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`). The function returns `true` if the signature is valid and `false` otherwise. The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64]. The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `public_key` is valid */ bool Hacl_P256_ecdsa_verif_without_hash( uint32_t msg_len, uint8_t *msg, uint8_t *public_key, uint8_t *signature_r, uint8_t *signature_s ); /******************/ /* Key validation */ /******************/ /** Public key validation. The function returns `true` if a public key is valid and `false` otherwise. The argument `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64]. The public key (x || y) is valid (with respect to SP 800-56A): • the public key is not the “point at infinity”, represented as O. • the affine x and y coordinates of the point represented by the public key are in the range [0, p – 1] where p is the prime defining the finite field. • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation. The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/ */ bool Hacl_P256_validate_public_key(uint8_t *public_key); /** Private key validation. The function returns `true` if a private key is valid and `false` otherwise. The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. The private key is valid: • 0 < `private_key` < the order of the curve */ bool Hacl_P256_validate_private_key(uint8_t *private_key); /******************************************************************************* Parsing and Serializing public keys. A public key is a point (x, y) on the P-256 NIST curve. The point can be represented in the following three ways. • raw = [ x || y ], 64 bytes • uncompressed = [ 0x04 || x || y ], 65 bytes • compressed = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes *******************************************************************************/ /** Convert a public key from uncompressed to its raw form. The function returns `true` for successful conversion of a public key and `false` otherwise. The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `pk` points to 65 bytes of valid memory, i.e., uint8_t[65]. The function DOESN'T check whether (x, y) is a valid point. */ bool Hacl_P256_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw); /** Convert a public key from compressed to its raw form. The function returns `true` for successful conversion of a public key and `false` otherwise. The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. The function also checks whether (x, y) is a valid point. */ bool Hacl_P256_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw); /** Convert a public key from raw to its uncompressed form. The outparam `pk` points to 65 bytes of valid memory, i.e., uint8_t[65]. The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. The function DOESN'T check whether (x, y) is a valid point. */ void Hacl_P256_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk); /** Convert a public key from raw to its compressed form. The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. The function DOESN'T check whether (x, y) is a valid point. */ void Hacl_P256_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk); /******************/ /* ECDH agreement */ /******************/ /** Compute the public key from the private key. The function returns `true` if a private key is valid and `false` otherwise. The outparam `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. The private key is valid: • 0 < `private_key` < the order of the curve. */ bool Hacl_P256_dh_initiator(uint8_t *public_key, uint8_t *private_key); /** Execute the diffie-hellmann key exchange. The function returns `true` for successful creation of an ECDH shared secret and `false` otherwise. The outparam `shared_secret` points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `their_pubkey` points to 64 bytes of valid memory, i.e., uint8_t[64]. The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. The function also checks whether `private_key` and `their_pubkey` are valid. */ bool Hacl_P256_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key); #if defined(__cplusplus) } #endif #define __Hacl_P256_H_DEFINED #endif