Paper 2026/2321
Mechanized Proofs of ORAM Correctness, Security, and Failure Bounds
, University of Porto (FCUP), INESC TEC, PQShield, Max Planck Institute for Security and Privacy, IMDEA Software Institute, PQShield, Inria Sophia-Antipolis, PQShield, Max Planck Institute for Security and PrivacyAbstract
ORAM is a fundamental cryptographic technique that permits outsourcing memory storage while probabilistically hiding memory access patterns of client programs. We use the EasyCrypt proof assistant to obtain fully mechanized proofs of correctness and security of Simple ORAM [Chung and Pass, 2013] and Path ORAM [Stefanov et al., CCS 2013]. To the best of our knowledge, these are the first machine-checked proofs that cover the correctness bound, i.e., the failure probability, of an ORAM construction. Our proofs refine, simplify, clarify and slightly improve the paper proofs, and many parts of our development can be reused to obtain similar results for other ORAM constructions. As a final contribution, we provide a general library that handles the recursive composition of ORAM constructions to reduce storage demands on the client, and apply this to Path ORAM to capture a practically-relevant instantiation.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Preprint.
- Keywords
- Formal MethodsOblivious RAM
- Contact author(s)
-
mbb @ fc up pt
gilles barthe @ mpi-sp org
gustavo delerue @ pqshield com
benjamin gregoire @ inria fr
pierre-yves strub @ pqshield com
xingyu xie @ mpi-sp org - History
- 2026-10-05: approved
- 2026-10-03: received
- See all versions
- Short URL
- https://ia.cr/2026/2321
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2026/2321,
author = {Manuel Barbosa and Gilles Barthe and Gustavo Delerue and Benjamin Gregoire and Pierre-Yves Strub and Xingyu Xie},
title = {Mechanized Proofs of {ORAM} Correctness, Security, and Failure Bounds},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/2321},
year = {2026},
url = {https://eprint.iacr.org/2026/2321}
}
