A Proof-producing Compiler for Secure Public-Key Infrastructure

by
Guodong Li and Jianjun Duan

Advised by
Konrad Slind

The project is to produce highly secure Public-Key Infrastructure via a novel proof-producing compiler, which is targeted at cryptographic applications. The compiler can produce either hardware circuits or software (ARM assembly language). The main example will be a verified implementation of Elliptic Curve Cryptography.