Tracking issue for supporting ECDH and EdDSA #199
Description
We'd like orion to support this by utilizing https://github.com/mit-plv/fiat-crypto. fiat-crypto is able to generate formally verified code which, in other words, means the field arithmetic from fiat-crypto has had its correctness proven by the Coq theorem prover.
Using fiat-crypto means:
- Greater confidence in the implementations offered by orion
- Less work required to maintain the implementations
- Less work required to audit the implementations
(the same motivation for #198)
Based on popularity and usage in for example TLS 1.3, the curve that will be supported is Curve25519. Additionally, this will also mean X25519 in terms of ECDH and Ed25519 in terms of EdDSA. Both these are also used in TLS 1.3. Using X25519 also allows us to build a higher-level key-exchange API that is compatible with libsodium's.
Initial work for X25519 and integration of fiat's Curve25519 arithmetic has been started in #197.
This will serve more as a tracking issue, since this will require a substantial amount of work.
TODO:
- Finish X25519 implementation in X25519 using fiat-crypto Curve25519 field arithmetic #197
- Implement Ed25519
- Add fuzzing targets for both (hazardous + high-level) in https://github.com/orion-rs/orion-fuzz
- X25519 and Ed25519 additions in the wiki, README (security section needs updates perhaps), crate meta-data, etc
- High-level key-exchange API
- High-level digital signatures API
- Extensive documentation for hazardous and high-level additions
- We could also add orion in the fiat-crypto usage tracker Tracking uses of fiat-crypto mit-plv/fiat-crypto#902 once implementations exist