Source code

Revision control

Copy as Markdown

Other Tools

/* 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_P521_H
#define __Hacl_P521_H
#if defined(__cplusplus)
extern "C" {
#endif
#include <string.h>
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "lib_intrinsics.h"
/*******************************************************************************
Verified C library for ECDSA and ECDH functions over the P-521 NIST curve.
This module implements signing and verification, key validation, conversions
between various point representations, and ECDH key agreement.
*******************************************************************************/
/*****************/
/* ECDSA signing */
/*****************/
/**
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 66 bytes (i.e. `msg_len >= 66`).
NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs
smaller than 66 bytes. These libraries left-pad the input with enough zeroes to
reach the minimum 66 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 132 bytes of valid memory, i.e., uint8_t[132].
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 66 bytes of valid memory, i.e., uint8_t[66].
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_P521_ecdsa_sign_p521_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 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 66 bytes (i.e. `msg_len >= 66`).
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 132 bytes of valid memory, i.e., uint8_t[132].
The arguments `signature_r` and `signature_s` point to 66 bytes of valid memory, i.e., uint8_t[66].
The function also checks whether `public_key` is valid
*/
bool
Hacl_P521_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 132 bytes of valid memory, i.e., uint8_t[132].
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.
*/
bool Hacl_P521_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 66 bytes of valid memory, i.e., uint8_t[66].
The private key is valid:
• 0 < `private_key` < the order of the curve
*/
bool Hacl_P521_validate_private_key(uint8_t *private_key);
/*******************************************************************************
Parsing and Serializing public keys.
A public key is a point (x, y) on the P-521 NIST curve.
The point can be represented in the following three ways.
• raw = [ x || y ], 132 bytes
• uncompressed = [ 0x04 || x || y ], 133 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 132 bytes of valid memory, i.e., uint8_t[132].
The argument `pk` points to 133 bytes of valid memory, i.e., uint8_t[133].
The function DOESN'T check whether (x, y) is a valid point.
*/
bool Hacl_P521_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 132 bytes of valid memory, i.e., uint8_t[132].
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_P521_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 133 bytes of valid memory, i.e., uint8_t[133].
The argument `pk_raw` points to 132 bytes of valid memory, i.e., uint8_t[132].
The function DOESN'T check whether (x, y) is a valid point.
*/
void Hacl_P521_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 132 bytes of valid memory, i.e., uint8_t[132].
The function DOESN'T check whether (x, y) is a valid point.
*/
void Hacl_P521_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 132 bytes of valid memory, i.e., uint8_t[132].
The argument `private_key` points to 66 bytes of valid memory, i.e., uint8_t[66].
The private key is valid:
• 0 < `private_key` < the order of the curve.
*/
bool Hacl_P521_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 132 bytes of valid memory, i.e., uint8_t[132].
The argument `their_pubkey` points to 132 bytes of valid memory, i.e., uint8_t[132].
The argument `private_key` points to 66 bytes of valid memory, i.e., uint8_t[66].
The function also checks whether `private_key` and `their_pubkey` are valid.
*/
bool
Hacl_P521_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key);
#if defined(__cplusplus)
}
#endif
#define __Hacl_P521_H_DEFINED
#endif