Cryptol is a high-level domain-specific language we have developed at Galois for specifying and
compiling cryptographic algorithms. We've had a lot of success in automatically verifying the
functional correctness of hardware implementations of symmetric key algorithms such as DES and
AES by using SAT- and SMT-based equivalence checking.
We've recently started trying to equivalence check public key crypto algorithm primitives such
as modular multiplication, but here the story is much worse: public key primitives operate on
word sizes that are hundreds or thousands of bits long, yet our equivalence checker and every
SMT solver we've tried times out on just 20-bit words.
In this talk I'll lay out the problems we've hit, how we've had some initial success using the
Isabelle theorem prover, and how our lives would be much easier if SMT solvers directly
supported user-given rewrite rules.