Description | Curve25519 is a very popular elliptic curve for public key cryptography, especially when it was discovered that the NSA had potentially implemented a backdoor into the P-256 curve based Dual_EC_DRBG algorithm [1]. Our goal is to implement some of parts of Curve25519 cryptography and prove them correct. You can read more about how to implement it here [2].
This project requires basic understanding of logic and programming but you don't need to expert. Ultimately, we need to establish the it forms a group, but if you are not comfortable, we can find some middle ground, e.g,, Haskell implementation and property based testing to establish the correctness criteria.
[1] https://en.wikipedia.org/wiki/Curve25519
[2] https://www.cl.cam.ac.uk/teaching/2122/Crypto/curve25519.pdf |