Internet users rely on the protocols they use to protect their private
information including their identity and the websites they visit. Formal
verification of these protocols can detect subtle bugs that compromise these
protections at design time, but is a challenging task as it involves
probabilistic reasoning about random sampling, cryptographic primitives, and
concurrent execution. Existing approaches either reason about symbolic
models of the protocols that sacrifice precision for automation, or reason
about more precise computational models that are harder to automate and
require cryptographic expertise. In this paper we propose a novel approach
to verifying privacy-preserving protocols that is more precise than symbolic
models yet more accessible than computational models. Our approach permits
<i>direct-style</i> proofs of privacy, as opposed to indirect game-based
proofs in computational models, by formalizing privacy as
<i>indistinguishability</i> of possible network traces induced by a
protocol. We ease automation by leveraging insights from the distributed
systems verification community to create sound synchronous models of
concurrent protocols. Our verification framework is implemented in F* as a
library we call Waldo. We describe two large case studies of using Waldo
to verify indistinguishability; one on the <i>Encrypted Client Hello</i>
(ECH) extension of the TLS protocol and another on a <i>Private
Information Retrieval</i> (PIR) protocol. We uncover subtle flaws in the TLS
ECH specification that were missed by other models.