Formal Verification of Isogeny-Based Cryptography
Linfoot Number Theory Seminar
4th November 2020, 11:00 am – 12:00 pm
Virtual Seminar, https://zoom.us/j/93099723308
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.