一句话：提出概率分离逻辑 PSL，用分离建模概率独立，并验证密码构造的信息论安全性。
概率独立是描述随机采样结果、推理随机变量组的基本概念，但现有验证方法难以处理独立性质。本文提出概率分离逻辑 PSL，将分离逻辑中的分离连接词解释为概率独立。作者首先为 bunched implications（BI）逻辑给出新的概率模型，随后基于这些断言构建程序逻辑，并证明该证明系统的可靠性。在评估中，作者用该逻辑验证若干经典密码任务的信息论安全性，包括私有信息检索、不经意传输、安全多方加法和简单的 oblivious RAM。这些证明完全在高层次性质（如独立性与均匀性）上推理，而无需展开底层分布细节，展示了 PSL 在概率程序验证与密码协议分析中的表达力。
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 probabili stic 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.