Hacl.P256ECDSA and ECDH functions using P-256
Buffers have the following size constraints:
pk: 64 bytes, corresponding to the "raw" representation of an elliptic curve point (see Point representation and conversions)sk, k: 32 bytessignature: 64 bytesmsg: depends on which hash function is being used (see ECDSA)Elliptic curve points have two 32-byte coordinates (x, y) and can be represented in 3 ways:
x || y0x02 + (y % 2), followed by x0x04, followed by the "raw" formThese functions convert points between these representations:
raw_to_compressed p converts a "raw" point p (64 bytes) to a "compressed" point (33 bytes).
raw_to_uncompressed p converts a "raw" point p (64 bytes) to an "uncompressed" point (65 bytes).
compressed_to_raw p attempts to convert a "compressed" point p (33 bytes) to a "raw" point (64 bytes) and returns it if successful.
uncompressed_to_raw p attempts to convert an "uncompressed" point p (65 bytes) to a "raw" point (64 bytes) and returns it if successful.
val valid_sk : sk:bytes -> boolvalid_sk sk checks if the contents of sk can be used as a secret key or as a signing secret. This is the case if:
sk is 32 bytes longsk < the order of the curve.val valid_pk : pk:bytes -> boolvalid_pk pk checks if the contents of pk is a valid public key, as specified in NIST SP 800-56A.
ECDH key agreement protocol
dh_initiator sk takes a 32-byte secret key sk and returns the corresponding 64-byte public key.
dh_responder sk pk takes a 32-byte secret key sk and another party's 64-byte public key and returns the 64-byte ECDH shared key.
ECDSA signing and signature verification functions
For the sign and verify functions included in this module msg is the digest of the message to be signed, requiring users to use a cryptographic hash function of their choosing before calling them. In this case, msg needs to be at least 32 bytes long.
sign sk msg k attempts to sign the message msg with secret key sk and signing secret k and returns the signature if successful.
verify pk msg signature checks the signature of msg using public key pk and returns true if it is valid.
The functions in the other submodules take the unhashed message msg and first hash it using their corresponding version of the SHA-2 hash function. In this case, there is no minimum size requirement for msg.
module SHA2_256 : SharedDefs.ECDSABuffers have the following size constraints:
module SHA2_384 : SharedDefs.ECDSABuffers have the following size constraints:
module SHA2_512 : SharedDefs.ECDSABuffers have the following size constraints:
module Noalloc : sig ... endVersions of these functions which write their output in a buffer passed in as an argument