International Association
for Cryptologic Research

Censorship circumvention tools enable clients to access endpoints in a network despite the presence of a censor. Censors use a variety of techniques to identify content they wish to block, including patterns that are characteristic of proxy or circumvention protocols. In response to this class of blocking behavior, circumvention practitioners have developed a family of "fully encrypted" protocols (FEPs), intended to have traffic that appears indistinguishable from random. For such protocols to be effective it is crucial that one can establish shared keys and protocol agreement without revealing to observers that an obfuscated protocol is in use. Despite their social significance to millions of users, there is no formal description of security for this handshake phase. This talk recounts the development of the obfs4 handshake, a highly-adopted FEP used to enable access to the Tor network in censored regions, which has incurred an iterative design process in response to censor behavior. We then present concrete results from our work formalizing obfuscated key exchange, capturing the goals of these protocols concretely and analyzing the obfs4 design. We demonstrate how to extend the obfs4 design to defend against stronger censorship attacks and to make it quantum-safe. With our analysis in mind, we point to challenges that remain in modeling and improving upon obfuscated protocols for future work.