# A Probabilistic Separation Logic

## TL;DR

This paper introduces PSL, a probabilistic separation logic that models independence, enabling high-level reasoning about probabilistic programs and verifying cryptographic security properties.

## Contribution

It presents a new probabilistic model of BI and develops a sound program logic for reasoning about independence in probabilistic programs.

## Key findings

- Verified cryptographic protocols using PSL
- Reasoned about independence and uniformity in proofs
- Demonstrated applicability to security properties

## Abstract

Probabilistic independence is a useful concept for describing the result of random sampling---a basic operation in all probabilistic languages---and for reasoning about groups of random variables. Nevertheless, existing verification methods handle independence poorly, if at all. We propose a probabilistic separation logic PSL, where separation models probabilistic independence. We first give a new, probabilistic model of the logic of bunched implications (BI). We then build a program logic based on these assertions, and prove soundness of the proof system. We demonstrate our logic by verifying information-theoretic security of cryptographic constructions for several well-known tasks, including private information retrieval, oblivious transfer, secure multi-party addition, and simple oblivious RAM. Our proofs reason purely in terms of high-level properties, like independence and uniformity.

---
Source: https://tomesphere.com/paper/1907.10708