Wrenna Robson

Formal Verification of Isogeny-Based Cryptography

How can we know that the cryptographic implementations that we use are true implementations of the original specification on which they are based? How can we specify algorithms in a more precise manner? What are the challenges of doing so? Wrenna Robson, a PhD candidate at Royal Holloway, gives a talk on Cryptol, one tool for cryptographic specification, and her work using it to specify SIKE, a post-quantum scheme submitted to NIST based on the isogenies of elliptic curves.