libcrux-ecdh 0.0.4

Libcrux ECDH implementation
Documentation

Elliptic Curve Diffie-Hellman (ECDH)

This crate provides an API for performing elliptic curve Diffie-Hellman. Currently supported curves are Curve 25519 and NIST curve P256.

Verification

verified-hacl

This crate contains safe Rust that was compiled from verified C originating in the HACL* project.

The code for [these] algorithms is formally verified using the F* verification framework for memory safety, functional correctness, and secret independence (resistance to some types of timing side-channels). -- The HACL* repository

For more details on the compilation from C to Rust, please refer to "Compiling C to Safe Rust, Formalized" by Aymeric Fromherz and Jonathan Protzenko.