CryptoDB
A plausible approach to computer-aided cryptographic proofs
| Authors: | |
|---|---|
| Download: | |
| 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). |
BibTeX
@misc{eprint-2005-12517,
title={A plausible approach to computer-aided cryptographic proofs},
booktitle={IACR Eprint archive},
keywords={implementation / Cryptographic Proofs, Automatic verification},
url={http://eprint.iacr.org/2005/181},
note={ shaih@alum.mit.edu 12949 received 15 Jun 2005},
author={Shai Halevi},
year=2005
}