CryptoDB
The computational SLR: a logic for reasoning about computational indistinguishability
| Authors: | |
|---|---|
| Download: | |
| Abstract: | Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal axiomatization system based on an extension of Hofmann's SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. We in particular define rules that justify directly the computational indistinguishability between programs and prove that these rules are sound with respect to the set-theoretic semantics, hence the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali's construction of pseudorandom generator, and the equivalence between next-bit unpredictability and pseudorandomness. |
BibTeX
@misc{eprint-2008-18176,
title={The computational SLR: a logic for reasoning about computational indistinguishability},
booktitle={IACR Eprint archive},
keywords={computational indistinguishability, equational proof system, formal verification},
url={http://eprint.iacr.org/2008/434},
note={ yu.zhang@gmail.com 14161 received 8 Oct 2008, last revised 8 Oct 2008},
author={Yu Zhang},
year=2008
}