Paper 2008/434

The computational SLR: a logic for reasoning about computational indistinguishability

Yu Zhang

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

Note: A more general definition of computational indistinguishability is given to allow reasoning about distributions of higher-order objects.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. A short version has been published at TLCA'2009
Keywords
computational indistinguishabilityequational proof systemSLRtype systemcryptographic proofs
Contact author(s)
yu zhang @ gmail com
History
2010-02-05: last of 4 revisions
2008-10-08: received
See all versions
Short URL
https://ia.cr/2008/434
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2008/434,
      author = {Yu Zhang},
      title = {The computational SLR: a logic for reasoning about computational indistinguishability},
      howpublished = {Cryptology ePrint Archive, Paper 2008/434},
      year = {2008},
      note = {\url{https://eprint.iacr.org/2008/434}},
      url = {https://eprint.iacr.org/2008/434}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.