Cryptology ePrint Archive: Report 2005/181

A plausible approach to computer-aided cryptographic proofs

Shai Halevi

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

Category / Keywords: implementation / Cryptographic Proofs, Automatic verification

Date: received 15 Jun 2005

Contact author: shaih at alum mit edu

Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Note: I plan to keep updated versions of this docuemnt (along with other update reports) on the web at http://www.research.ibm.com/people/s/shaih/CAV/

Version: 20050615:215332 (All versions of this report)

Short URL: ia.cr/2005/181

Discussion forum: Show discussion | Start new discussion