Systematic Synthesis of Elliptic Curve Cryptography Implementations

https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf [people.csail.mit.edu]

2016-11-30 20:49

We implemented a framework in the Coq proof assistant for generating efficient code for elliptic curve cryptography (ECC), with proofs of conformance to a whiteboard-level specification in number theory. While some past projects have verified this kind of code, ours is the first to synthesize it from security parameters.