On Separation Logic, Computational Independence, and Pseudorandomness (Extended Version)
Ugo Dal Lago, Davide Davoli, Bruce M. Kapron
TL;DR
The paper develops Cryptographic Probabilistic Separation Logic (CPSL), a computationally flavored version of probabilistic separation logic that encodes independence and pseudorandomness in a typed, distribution-centric setting. By restricting programs to be polytime and employing efficiently samplable distributions, CPSL derives a sound Hoare-style framework where separating conjunction captures computational independence. The approach yields concise cryptographic proofs, including the security of a pseudorandom generator-based OTP variant and pseudorandom key stretching, and provides a semantic characterization of computational independence aligned with cryptographic security notions. This work bridges separation-logic reasoning with cryptographic reasoning, enabling modular, compositional proofs of security without explicit reductions to adversaries. It also identifies fundamental limitations (no loops, restricted implications) and sketches directions to broaden applicability to more complex cryptographic constructions and proofs.
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.