Verifying Indistinguishability of Privacy-Preserving Protocols

Explore a groundbreaking approach to verifying privacy-preserving protocols in this 18-minute conference talk from OOPSLA2 2023. Delve into a novel verification framework called Waldo, implemented in F*, which offers a more precise alternative to symbolic models while remaining more accessible than computational models. Learn how the researchers formalize privacy as indistinguishability of possible network traces induced by a protocol, allowing for direct-style proofs of privacy. Discover how insights from distributed systems verification are leveraged to create sound synchronous models of concurrent protocols, easing automation. Examine two extensive case studies utilizing Waldo to verify indistinguishability in the Encrypted Client Hello (ECH) extension of the TLS protocol and a Private Information Retrieval (PIR) protocol. Uncover subtle flaws in the TLS ECH specification that were overlooked by other models, highlighting the importance of this innovative verification approach in detecting potential privacy vulnerabilities in internet protocols.