{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:19Z","timestamp":1790927599399,"version":"4.1.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100007015","name":"University of Wisconsin--Madison","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007015","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ONR","award":["N00014-12-1-0914,N00014-15-1-2750,N00014-19-1-2292"],"award-info":[{"award-number":["N00014-12-1-0914,N00014-15-1-2750,N00014-19-1-2292"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Facebook"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"Probabilistic independence is a useful concept for describing the result of random sampling\u2014a basic operation in all probabilistic languages\u2014and 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.<\/jats:p>","DOI":"10.1145\/3371123","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["A probabilistic separation logic"],"prefix":"10.1145","volume":"4","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI for Security and Privacy, Germany \/ IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kevin","family":"Liao","sequence":"additional","affiliation":[{"name":"MPI for Security and Privacy, Germany \/ University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"key-10.1145\/3371123-1","unstructured":"Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, and Jason M. Rute. 2019. On the computability of graphons. In IEEE Symposium on Logic in Computer Science (LICS), Vancouver, British Columbia."},{"key":"key-10.1145\/3371123-2","unstructured":"Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub. 2015. Verified Proofs of Higher-Order Masking. In IACR International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT), Sofia, Bulgaria (Lecture Notes in Computer Science) , Vol. 9056. Springer-Verlag, 457–485."},{"key":"key-10.1145\/3371123-3","unstructured":"Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. An AssertionBased Program Logic for Probabilistic Programs. In European Symposium on Programming (ESOP), Thessaloniki, Greece. arXiv: cs.LO\/1803.05535 https:\/\/arxiv.org\/abs\/1803.05535"},{"key":"key-10.1145\/3371123-4","unstructured":"Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017. Proving uniformity and independence by self-composition and coupling. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Maun, Botswana (EPiC Series in Computing) , Vol. 46. 385–403. http:\/\/www.easychair.org\/ publications\/paper\/340344"},{"key":"key-10.1145\/3371123-5","unstructured":"Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy (Leibniz International Proceedings in Informatics) , Vol. 55. Schloss Dagstuhl–Leibniz Center for Informatics, 107:1–107:15."},{"key":"key-10.1145\/3371123-6","unstructured":"Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Savannah, Georgia. 90–101."},{"key":"key-10.1145\/3371123-7","doi-asserted-by":"crossref","unstructured":"Gilles Barthe, Justin Hsu, and Kevin Liao. 2020. A Probabilistic Separation Logic. Proceedings of the ACM on Programming Languages 4, POPL (Jan. 2020). arXiv: cs.PL\/1907.10708 https:\/\/arxiv.org\/abs\/1907.10708","DOI":"10.1145\/3371123"},{"key":"key-10.1145\/3371123-8","unstructured":"Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proceedings of the ACM on Programming Languages 3, POPL (2019), 34:1–34:29."},{"key":"key-10.1145\/3371123-9","unstructured":"Stephen Brookes. 2007. A semantics for concurrent separation logic. Theoretical Computer Science 375, 1–3 (2007), 227–270."},{"key":"key-10.1145\/3371123-10","unstructured":"T.-H. Hubert Chan, Jonathan Katz, Kartik Nayak, Antigoni Polychroniadou, and Elaine Shi. 2018. More is Less: Perfectly Secure Oblivious Algorithms in the Multi-server Setting. In International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT), Brisbane, Australia (Lecture Notes in Computer Science) , Thomas Peyrin and Steven D. Galbraith (Eds.), Vol. 11274. Springer-Verlag, 158–188."},{"key":"key-10.1145\/3371123-11","unstructured":"Benny Chor, Oded Goldreich, Eyal Kushilevitz, and Madhu Sudan. 1995. Private information retrieval. In IEEE Symposium on Foundations of Computer Science (FOCS), Milwaukee, Wisconsin . 41–50."},{"key":"key-10.1145\/3371123-12","unstructured":"Kai-Min Chung and Rafael Pass. 2013. A Simple ORAM. IACR Cryptology ePrint Archive 2013 (2013), 243. http:\/\/eprint.iacr. org\/2013\/243"},{"key":"key-10.1145\/3371123-13","doi-asserted-by":"crossref","unstructured":"Ronald Cramer, Ivan Bjerre Damgård, and Jesper Buus Nielsen. 2015. Secure Multiparty Computation. Cambridge University Press.","DOI":"10.1017\/CBO9781107337756"},{"key":"key-10.1145\/3371123-14","doi-asserted-by":"crossref","unstructured":"David Darais, Chang Liu, Ian Sweet, and Michael Hicks. 2020. A Language for Probabilistically Oblivious Computation. Proceedings of the ACM on Programming Languages 4, POPL (Jan. 2020). http:\/\/arxiv.org\/abs\/1711.09305","DOI":"10.1145\/3371118"},{"key":"key-10.1145\/3371123-15","unstructured":"Simon Docherty. 2019. Bunched Logics: A Uniform Approach. Ph.D. Dissertation. University College London."},{"key":"key-10.1145\/3371123-16","unstructured":"Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2018. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proceedings of the ACM on Programming Languages 2, POPL (2018), 59:1–59:28."},{"key":"key-10.1145\/3371123-17","unstructured":"Didier Galmiche, Daniel Méry, and David J. Pym. 2005. The semantics of BI and resource tableaux. Mathematical Structures in Computer Science 15, 6 (2005), 1033–1088."},{"key":"key-10.1145\/3371123-18","unstructured":"Craig Gentry, Kenny A. Goldman, Shai Halevi, Charanjit S. Jutla, Mariana Raykova, and Daniel Wichs. 2013. Optimizing ORAM and Using It Efficiently for Secure Computation. In International Symposium on Privacy Enhancing Technologies (PETS), Bloomington, Indiana (Lecture Notes in Computer Science) , Vol. 7981. Springer-Verlag, 1–18."},{"key":"key-10.1145\/3371123-19","unstructured":"Michèle Giry. 1982. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis. Springer Berlin Heidelberg, Berlin, Heidelberg, 68–85."},{"key":"key-10.1145\/3371123-20","unstructured":"Oded Goldreich. 1987. Towards a Theory of Software Protection and Simulation by Oblivious RAMs. In ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York , Alfred V. Aho (Ed.). 182–194."},{"key":"key-10.1145\/3371123-21","unstructured":"Oded Goldreich, Silvio Micali, and Avi Wigderson. 1987. How to play any mental game. In ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York . 218–229."},{"key":"key-10.1145\/3371123-22","unstructured":"Oded Goldreich and Rafail Ostrovsky. 1996. Software Protection and Simulation on Oblivious RAMs. Journal of the ACM 43, 3 (1996), 431–473."},{"key":"key-10.1145\/3371123-23","unstructured":"Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff. 2015. Automated Analysis and Synthesis of Authenticated Encryption Schemes. IACR Cryptology ePrint Archive 2015 (2015), 624. http:\/\/eprint.iacr.org\/2015\/624"},{"key":"key-10.1145\/3371123-24","unstructured":"Russell Impagliazzo and Steven Rudich. 1988. Limits on the Provable Consequences of One-way Permutations. In IACR International Cryptology Conference (CRYPTO), Santa Barbara, California (Lecture Notes in Computer Science) , Vol. 403. Springer, 8–26."},{"key":"key-10.1145\/3371123-25","unstructured":"Samin S. Ishtiaq and Peter W. O’Hearn. 2001. BI as an assertion language for mutable data structures. In ACM SIGPLAN– SIGACT Symposium on Principles of Programming Languages (POPL), London, England . 14–26. https:\/\/dl.acm.org\/citation. cfm?id=375719"},{"key":"key-10.1145\/3371123-26","doi-asserted-by":"crossref","unstructured":"Jonathan Katz and Yehuda Lindell. 2014. Introduction to Modern Cryptography. Chapman and Hall\/CRC.","DOI":"10.1201\/b17668"},{"key":"key-10.1145\/3371123-27","unstructured":"Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. System Sci. 22, 3 (1981), 328–350."},{"key":"key-10.1145\/3371123-28","doi-asserted-by":"crossref","unstructured":"Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. System Sci. 30, 2 (1985).","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"key-10.1145\/3371123-29","unstructured":"Yehuda Lindell. 2017. How to simulate it–a tutorial on the simulation proof technique. In Tutorials on the Foundations of Cryptography . Springer-Verlag, 277–346."},{"key":"key-10.1145\/3371123-30","unstructured":"Daniele Micciancio. 1997. Oblivious Data Structures: Applications to Cryptography. In ACM SIGACT Symposium on Theory of Computing (STOC), El Paso, Texas . 456–464."},{"key":"key-10.1145\/3371123-31","unstructured":"Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Transactions on Programming Languages and Systems 18, 3 (1996), 325–353."},{"key":"key-10.1145\/3371123-32","unstructured":"Moni Naor and Vanessa Teague. 2001. Anti-presistence: history independent data structures. In Proceedings on 33rd Annual ACM Symposium on Theory of Computing, July 6-8, 2001, Heraklion, Crete, Greece . ACM, 492–501."},{"key":"key-10.1145\/3371123-33","unstructured":"Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical Computer Science 375, 1–3 (2007), 271–307."},{"key":"key-10.1145\/3371123-34","doi-asserted-by":"crossref","unstructured":"Peter W. O’Hearn and David J. Pym. 1999. The logic of bunched implications. Bulletin of Symbolic Logic 5, 2 (1999), 215–244. http:\/\/www.math.ucla.edu\/%7Easl\/bsl\/0502\/0502-003.ps","DOI":"10.2307\/421090"},{"key":"key-10.1145\/3371123-35","unstructured":"Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In International Workshop on Computer Science Logic (CSL), Paris, France (Lecture Notes in Computer Science), Vol. 2142. Springer-Verlag, 1–19."},{"key":"key-10.1145\/3371123-36","unstructured":"David J. Pym. 1999. On Bunched Predicate Logic. In IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy. 183–192."},{"key":"key-10.1145\/3371123-37","doi-asserted-by":"crossref","unstructured":"D. J. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, Vol. 26. Kluwer Academic Publishers. Errata and Remarks maintained at: http:\/\/www.cantab.net\/users\/david.pym\/BI-monographerrata.pdf .","DOI":"10.1007\/978-94-017-0091-7"},{"key":"key-10.1145\/3371123-38","unstructured":"David J. Pym, Peter W. O’Hearn, and Hongseok Yang. 2004. Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315, 1 (2004), 257–305."},{"key":"key-10.1145\/3371123-39","unstructured":"Michael O. Rabin. 2005. How To Exchange Secrets with Oblivious Transfer. IACR Cryptology ePrint Archive 2005 (2005), 187."},{"key":"key-10.1145\/3371123-40","unstructured":"John C. Reynolds. 2008. An Introduction to Separation Logic (Preliminary Draft). Technical Report. ITU University, Copenhagen. https:\/\/www.cs.cmu.edu\/~jcr\/copenhagen08.pdf"},{"key":"key-10.1145\/3371123-41","unstructured":"Ronald Rivest. 1999. Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initializer. (1999)."},{"key":"key-10.1145\/3371123-42","unstructured":"N. Saheb-Djahromi. 1980. CPO’s of Measures for Nondeterminism. Theoretical Computer Science 12 (1980), 19–37."},{"key":"key-10.1145\/3371123-43","unstructured":"Elaine Shi, T.-H. Hubert Chan, Emil Stefanov, and Mingfei Li. 2011. Oblivious RAM with 𝑂 ( (log 𝑁 ) 3 ) Worst-Case Cost. In International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT), Seoul, South Korea (Lecture Notes in Computer Science) , Vol. 7073. Springer, 197–214."},{"key":"key-10.1145\/3371123-44","unstructured":"Alex Simpson. 2018. Category-theoretic Structure for Independence and Conditional Independence. Electronic Notes in Theoretical Computer Science 336 (2018), 281–297."},{"key":"key-10.1145\/3371123-45","unstructured":"Geoffrey Smith. 2003. Probabilistic Noninterference through Weak Probabilistic Bisimulation. In IEEE Computer Security Foundations Workshop (CSFW), Pacific Grove, California . 3–13."},{"key":"key-10.1145\/3371123-46","unstructured":"Sam Staton, Dario Stein, Hongseok Yang, Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. 2018. The BetaBernoulli process and algebraic effects. In International Colloquium on Automata, Languages and Programming (ICALP), Prague, Czech Republic (Leibniz International Proceedings in Informatics) , Vol. 107. Schloss Dagstuhl–Leibniz Center for Informatics, 141:1–141:15."},{"key":"key-10.1145\/3371123-47","unstructured":"Emil Stefanov, Marten van Dijk, Elaine Shi, Christopher W. Fletcher, Ling Ren, Xiangyao Yu, and Srinivas Devadas. 2013. Path ORAM: an extremely simple oblivious RAM protocol. In ACM SIGSAC Conference on Computer and Communications Security (CCS), Berlin, Germany . 299–310."},{"key":"key-10.1145\/3371123-48","unstructured":"Joseph Tassarotti and Robert Harper. 2019. A separation logic for concurrent randomized programs. Proceedings of the ACM on Programming Languages 3, POPL (2019), 64:1–64:30."},{"key":"key-10.1145\/3371123-49","unstructured":"Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3, POPL (2019), 36:1–36:29. https:\/\/dl.acm.org\/citation.cfm?id=3290349"},{"key":"key-10.1145\/3371123-50","unstructured":"Xiao Shaun Wang, Kartik Nayak, Chang Liu, T.-H. Hubert Chan, Elaine Shi, Emil Stefanov, and Yan Huang. 2014. Oblivious Data Structures. In ACM SIGSAC Conference on Computer and Communications Security (CCS), Scottsdale, Arizona. 215–226."},{"key":"key-10.1145\/3371123-51","unstructured":"Hongseok Yang. 2001. Local Reasoning for Stateful Programs. Ph.D. Dissertation. Champaign, IL, USA. AAI3023240."},{"key":"key-10.1145\/3371123-52","unstructured":"Andrew Chi-Chih Yao. 1986. How to generate and exchange secrets. In IEEE Symposium on Foundations of Computer Science (FOCS), Toronto, Ontario . 162–167."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371123","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371123","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":52,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371123"],"URL":"https:\/\/doi.org\/10.1145\/3371123","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}