Module Hacl_star__Hacl.P256

ECDSA and ECDH functions using P-256

Point representation and conversions

Elliptic curve points have 2 32-byte coordinates (x, y) and can be represented in 3 ways:

  • "raw" form (64 bytes): the concatenation of the 2 coordinates
  • "compressed" form (33 bytes): the first byte is either \x02 or \x03, followed by y
  • "uncompressed" form (65 bytes): the first byte is always \04, followed by the "raw" form

These functions convert points between these representations:

val raw_to_compressed : bytes -> bytes

raw_to_compressed p converts a "raw" point p (64 bytes) to a "compressed" point (33 bytes)

val raw_to_uncompressed : bytes -> bytes

raw_to_uncompressed p converts a "raw" point p (64 bytes) to an "uncompressed" point (65 bytes)

val compressed_to_raw : bytes -> bytes option

compressed_to_raw p attempts to convert a "compressed" point p (33 bytes) to a "raw" point (64 bytes) and returns it if successful.

val uncompressed_to_raw : bytes -> bytes option

uncompressed_to_raw p attempts to convert an "uncompressed" point p (65 bytes) to a "raw" point (64 bytes) and returns it if successful.

Point validation

val valid_sk : sk:bytes -> bool

valid_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 0 < sk < the order of the curve.

val valid_pk : pk:bytes -> bool

valid_pk pk checks if the contents of pk is a valid public key, as specified in NIST SP 800-56A.

ECDH

ECDH key agreement protocol

val dh_initiator : sk:bytes -> bytes option

dh_initiator sk takes a 32-byte secret key sk and returns the corresponding 64-byte public key.

val dh_responder : sk:bytes -> pk:bytes -> bytes option

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

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.

val sign : sk:bytes -> msg:bytes -> k:bytes -> bytes option

sign sk msg k attempts to sign the message msg with secret key sk and signing secret k and returns the signature if successful.

val verify : pk:bytes -> msg:bytes -> signature:bytes -> bool

verify pk msg signature checks the signature of msg using public key pk and returns true if it is valid.

module Noalloc : sig ... end

Versions of these functions which write their output in a buffer passed in as an argument