A plausible approach to computer-aided cryptographic proofs.
Shai Halevi · 2005
This paper tries to sell a potential approach to making the process of writing and verifying our cryptographic proofs less prone to errors. Specifically, I advocate creating an automated tool to help us with the mundane parts of writing and checking common arguments in our proofs. On a high level, this tool should help us verify that two pieces of code induce the same probability distribution on some of their common variables. In this paper I explain why I think that such a tool would be useful, by considering two very different proofs of security from the literature and showing the places in those proofs where having this tool would have been useful. I also explain how I believe that this tool can be built. Perhaps surprisingly, it seems to me that the functionality of such tool can be implemented using only “static code analysis” (i.e., things that compilers do). I plan to keep updated versions of this docuemnt along with other update reports on the web at