Cryptology ePrint Archive: Report 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.

Category / Keywords: computational indistinguishability, equational proof system, SLR, type system, cryptographic proofs

Publication Info: A short version has been published at TLCA'2009

Date: received 8 Oct 2008, last revised 5 Feb 2010

Contact author: yu zhang at gmail com

Available format(s): PDF | BibTeX Citation

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

Version: 20100205:092033 (All versions of this report)

Short URL: ia.cr/2008/434

Discussion forum: Show discussion | Start new discussion