Formally Verified Elliptic Curve Cryptography Curve25519 in Dafny, Coq, or Lean

  by   Mukesh Tiwari






Departments Computer Science
DescriptionCurve25519 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
Preparation
Project Categories Security, Software Engineering
Project Keywords Algorithms, Cybersecurity, Logic


Level of Studies

Level 6 (Undergraduate Year 3) yes
Level 7 (Masters) yes
Level 8 (PhD) yes