Verifying Indistinguishability of Privacy-Preserving Protocols
summary
Library Waldo implements a middle ground between symbolic and computational models in F by modeling messages as bitstrings, using a tape to factor out randomness, and applying a synchronization rewrite to eliminate concurrency. The framework proves indistinguishability via proof by coupling, verifies an ECH (Encrypted Client Hello) deployment and a PIR scheme, and uncovers subtle TLS ECH specification leaks requiring explicit length- and field-padding assumptions to restore privacy.
AI-written summary · about
chapters (7)
- 0:00Verifying privacy protocols
- 1:47Formal verification necessity
- 3:14Computational vs symbolic models
- 6:28Precision versus automation
- 7:53Non-determinism in verification
- 12:06Case study: TLS Encrypted Client Hello
- 14:55Conclusion and future work
related talks
16mLost and Found in the Fog of Trust
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
38mDemystifying Privacy Preserving Computing
29mPrivacy-preserving methods: Building secure projects
29mVerifying Pufferfish Privacy in Hidden Markov Models
39mPrivacy-preserving Approaches to Transparency Logs
28mPaying for Privacy Preserving Messaging
26mA Framework for Adversarial Streaming via Differential Privacy and Difference Estimators