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.