libcrux - the formally verified crypto library

Please refer to the [Architecture] document for a detailed overview of the libcrux architecture and properties.

Algorithms

Note The available algorithms is still work in progress and will grow in future.

| Algorithm | Platforms | spec equivalence | security proof | | ---------------- | ------------ | ---------------- | -------------- | | AES | x64 (AES-NI) | Coq | | | AES-GCM | x64 (AES-NI) | | | | Chacha20 | x64, arm64 | F* (EC) | | | Poly1305 | x64, arm64 | F* (EC) | | | Chacha20Poly1305 | x64, arm64 | (F* or hacspec) | | | Curve25519 | x64, arm64 | (F*) | | | EdDSA 25519 | x64, arm64 | (F*) | | | EcDSA P256 | x64, arm64 | | | | Sha2 | x64, arm64 | (F*) | | | Sha3 | x64, arm64 | (F*) (EC) | (EC) | | Blake2 | x64, arm64 | | | | HMAC | x64, arm64 | | | | HKDF | x64, arm64 | | | | Bls12-381 | x64, arm64 | Coq | | | HPKE | x64, arm64 | hacspec | |

ToDos

Everything in parenthesis still needs to be done

• [ ] Add references to all spec equivalence entries
• [ ] Bls hash to curve?

Equivalence proofs

• [ ] Chacha20 EC
• [ ] Poly EC
• [ ] Chacha20Poly1305 F* or hacspec
• [ ] Curve25519 F*
• [ ] Ed25519 F*
• [ ] Sha2 F*
• [ ] Sha3 F*
• [ ] Sha3 EC

Benchmarks

| Algorithm | Platforms | Performance | Performance "RustCrypto" | Performance "Ring" | Performance "OpenSSL" | | ----------------- | --------------------- | --------------------- | ------------------------ | --------------------- | --------------------- | | Chacha20Poly1305 | x64 (avx2) | | | | | | (encrypt/decrypt) | arm64 (Apple silicon) | 758.89 / 761.19 MiB/s | 249.33 / 230.08 MiB/s | 973.04 / 773.60 MiB/s | 1.6296 / 1.4670 GiB/s | | Curve25519 | x64 (avx2) | | | | | | | arm64 (Apple silicon) | 30.320 µs | 35.465 µs | 30.363 µs | 32.272 µs | | Sha2 224 | x64 (avx2) | | | - | | | | arm64 (Apple silicon) | 306.41 MiB/s | 318.87 MiB/s | - | 2.2335 GiB/s | | Sha2 256 | x64 (avx2) | | | | | | | arm64 (Apple silicon) | 311.76 MiB/s | 319.10 MiB/s | 2.2491 GiB/s | 2.2455 GiB/s | | Sha2 384 | x64 (avx2) | | | | | | | arm64 (Apple silicon) | 496.62 MiB/s | 513.94 MiB/s | 592.38 MiB/s | 1.3251 GiB/s | | Sha2 512 | x64 (avx2) | | | | | | | arm64 (Apple silicon) | 489.83 MiB/s | 513.53 MiB/s | 590.17 MiB/s | 1.3307 GiB/s | | Sha3 224 | x64 (avx2) | 422.04 MiB/s | 246.88 MiB/s | - | 281.23 MiB/s | | | arm64 (Apple silicon) | 611.62 MiB/s | 609.51 MiB/s | - | 660.30 MiB/s | | Sha3 256 | x64 (avx2) | 371.56 MiB/s | 233.28 MiB/s | - | 309.27 MiB/s | | | arm64 (Apple silicon) | 574.39 MiB/s | 573.89 MiB/s | - | 625.37 MiB/s | | Sha3 384 | x64 (avx2) | 304.05 MiB/s | 189.76 MiB/s | - | 236.08 MiB/s | | | arm64 (Apple silicon) | 440.18 MiB/s | 442.02 MiB/s | - | 480.97 MiB/s | | Sha3 512 | x64 (avx2) | 207.69 MiB/s | 129.79 MiB/s | - | 162.59 MiB/s | | | arm64 (Apple silicon) | 306.78 MiB/s | 307.47 MiB/s | - | 335.92 MiB/s |

HPKE

Ciphersuite: x25519, Sha256, Chacha20Poly1305

| | libcrux | HPKE | | -------------- | ------- | ------------------------------------- | | Setup Sender | 79.9 μs | 68 μs | | Setup Receiver | 76 μs | 54.4 μs |

"-": The library does not support this algorithm and/or platform.

Hardware support

The build enables all available hardware features for the target architecture. Further, the library always performs runtime checks to ensure that the required CPU features are available.

libcrux uses the following configurations for its hardware abstractions

• simd128 assumes 128 bit SIMD instructions on the platform. This implies SSE3 and SSE4.1 on x64 CPUs and NEON on arm CPUs.
• simd256 assumes 256 bit SIMD instructions on the platform This implies AVX and AVX2 on x64 CPUs.

Randomness

libcrux provides a DRBG implementation that can be used standalone (drbg::Drbg) or through the Rng traits.