Abstract:
Cryptographers recognize that their field has reached a crisis of rigor where it is no longer viable to construct cryptographic proofs by hand, nor even verify them. Of all cryptographic proofs techniques, one known as the game-playing technique is particularly amenable to automated verification since it can be recasted in terms of transformation of probabilistic programs. We present our ongoing work on a language-based framework that supports the construction and automated verification of cryptographic proofs as sequences of games. Unsurprisingly, most of the game-rewriting transformations used by cryptographers happen to be common compiler optimizations that can be completely automated (e.g. dead-code elimination, constant propagation, code-motion) while the application of other domain pecific transformations can be greatly benefit from tool support.