[Resource Topic] 2008/434: The computational SLR: a logic for reasoning about computational indistinguishability

Welcome to the resource topic for 2008/434

Title:
The computational SLR: a logic for reasoning about computational indistinguishability

Authors: 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.

ePrint: https://eprint.iacr.org/2008/434

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .