Paper 2005/181

A plausible approach to computer-aided cryptographic proofs

Shai Halevi


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).

Note: I plan to keep updated versions of this docuemnt (along with other update reports) on the web at

Available format(s)
Publication info
Published elsewhere. Unknown where it was published
Cryptographic ProofsAutomatic verification
Contact author(s)
shaih @ alum mit edu
2005-06-15: received
Short URL
Creative Commons Attribution


      author = {Shai Halevi},
      title = {A plausible approach to computer-aided cryptographic proofs},
      howpublished = {Cryptology ePrint Archive, Paper 2005/181},
      year = {2005},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.