Paper 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).
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/
Metadata
- Available format(s)
-
PDF
PS
- Category
- Implementation
- Publication info
- Published elsewhere. Unknown where it was published
- Keywords
- Cryptographic ProofsAutomatic verification
- Contact author(s)
- shaih @ alum mit edu
- History
- 2005-06-15: received
- Short URL
- https://ia.cr/2005/181
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2005/181,
author = {Shai Halevi},
title = {A plausible approach to computer-aided cryptographic proofs},
howpublished = {Cryptology ePrint Archive, Paper 2005/181},
year = {2005},
note = {\url{https://eprint.iacr.org/2005/181}},
url = {https://eprint.iacr.org/2005/181}
}
