Transport layer data leaks metadata unintentionally$\unicode{x2013}$such as who communicates with whom. While tools for strong transport layer privacy exist, they have adoption obstacles, including performance overheads incompatible with mobile devices. We posit that by changing the objective of metadata privacy for $\textit{all traffic}$, we can open up a new design space for pragmatic approaches to transport layer privacy. As a first step in this direction, we propose the $\textit{hybrid model}$, a system model that allows one to practically combine, and formally reason about network traffic with different privacy guarantees ($\textit{regular}$ and $\textit{deniable}$) in one joint system. Using techniques from information flow control we present a principled approach to construct a formal model and prove that deniable traffic achieves transport layer privacy against strong adversaries$\unicode{x2013}$this constitutes the first bridging of information flow control and anonymous communication to our knowledge. Additionally, we show that existing state-of-the-art protocols can be extended to support transport layer privacy, by designing a novel protocol for $\textit{deniable instant messaging}$ (DenIM), which is a variant of the Signal protocol. As an instantiation of the hybrid model, we implement and evaluate a proof-of-concept instant messaging system running both DenIM and regular Signal. We empirically show that the hybrid model can maintain low-latency for regular Signal traffic without breaking existing features, while at the same time supporting deniable Signal traffic.
翻译:传输层数据无意中泄露元数据$\unicode{x2013}$如谁与谁通信。尽管存在实现强传输层隐私的工具,但它们在采用上面临障碍,包括与移动设备不兼容的性能开销。我们认为,通过改变$\textit{所有流量}$的元数据隐私目标,可以为传输层隐私的务实方法开辟新的设计空间。作为这一方向的第一步,我们提出$\textit{混合模型}$,这是一种系统模型,允许在单一联合系统中实际结合并形式化推理具有不同隐私保证($\textit{常规}$和$\textit{可否认}$)的网络流量。利用信息流控制技术,我们提出了一种原则性方法来构建形式化模型,并证明可否认流量能针对强敌手实现传输层隐私$\unicode{x2013}$据我们所知,这首次将信息流控制与匿名通信联系起来。此外,我们展示了现有最先进协议可扩展以支持传输层隐私,通过设计一种新颖的$\textit{可否认即时通讯}$(DenIM)协议,它是Signal协议的变体。作为混合模型的实例化,我们实现并评估了一个运行DenIM和常规Signal的概念验证即时通讯系统。实验表明,混合模型能在不破坏现有功能的情况下保持常规Signal流量的低延迟,同时支持可否认的Signal流量。