Oblivious Algebraic Data Types
summary
Presents Lambda OADT, a dependently typed calculus that encodes recursive private data by tagging each type with a public view (e.g. max tree depth) and provides oblivious primitives (mux, leaky condition) so every instance has the same shape and control flow. Introduces tape semantics that treats decryption-like operations as values, pushes contexts into branches, and compiles them to oblivious muxes; proves non‑leakage in Coq and ships artifacts, but no concrete MPC implementation yet.
AI-written summary · about
chapters (14)
- 0:00Start
- 0:15A Mental Game
- 1:28Writing Secure Applications
- 2:02What's Missing?
- 2:18Oblivious Algebraic Data Types
- 5:33Running Example
- 5:48Defining Oblivious Data Type
- 7:45TREE WITHOUT PAYLOAD
- 8:14Oblivious Operations
- 13:33Get Stuck!
- 15:52Put Everything Together
- 17:37Formalization And Proofs
- 18:08Shameless Plug
- 18:19To Recap
related talks
56mToward Obfuscation from Affine Determinant Programs
26mA Core Calculus for Equational Proofs of Cryptographic Protocols
48mTales of Obfuscation in Bounded Arithmetic, Metacomplexity, and Differential Privacy
54mSnarky: Algebraic effects in the Coda cryptocurrency
35mOblivious RAM for MPC
57mIndistinguishability Obfuscation from Well-Founded Assumptions
01h 26mObfuscation 1
01h 03mLockable Obfuscation