On Separation Logic, Computational Independence, and Pseudorandomness (Extended Version)

TL;DR

This paper explores the adaptation of separation logic to account for computational independence in cryptography, enabling simpler proofs of cryptographic results and linking independence with pseudorandomness.

Contribution

It introduces a semantics for separation logic that incorporates computationally bounded adversaries, facilitating cryptographic proofs and connecting independence with pseudorandomness.

Findings

Semantics of separation logic can be adapted for complexity-bounded adversaries.

The logical system simplifies cryptographic proofs involving hidden adversaries.

Establishes a connection between independence notions and pseudorandomness in cryptography.

Abstract

Separation logic is a substructural logic which has proved to have numerous and fruitful applications to the verification of programs working on dynamic data structures. Recently, Barthe, Hsu and Liao have proposed a new way of giving semantics to separation logic formulas in which separating conjunction is interpreted in terms of probabilistic independence. The latter is taken in its exact form, i.e., two events are independent if and only if the joint probability is the product of the probabilities of the two events. There is indeed a literature on weaker notions of independence which are computational in nature, i.e. independence holds only against efficient adversaries and modulo a negligible probability of success. The aim of this work is to explore the nature of computational independence in a cryptographic scenario, in view of the aforementioned advances in separation logic. We show on the one hand that the semantics of separation logic can be adapted so as to account for complexity bounded adversaries, and on the other hand that the obtained logical system is useful for writing simple and compact proofs of standard cryptographic results in which the adversary remains hidden. Remarkably, this allows for a fruitful interplay between independence and pseudorandomness, itself a crucial notion in cryptography.