2018 IEEE Symposium on Security and Privacy (SP) (2018)
San Francisco, CA, US
May 21, 2018 to May 23, 2018
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SP.2018.00021
Karthikeyan Bhargavan , INRIA de Paris, France
Ioana Boureanu , Univ. of Surrey, SCCS, UK
Antoine Delignat-Lavaud , Microsoft Research, UK
Pierre-Alain Fouque , Univ. of Rennes 1, IRISA, France
Cristina Onete , Univ. of Limoges, XLIM, CNRS, France
Much of Internet traffic nowadays passes through active proxies, whose role is to inspect, filter, cache, or trans- form data exchanged between two endpoints. To perform their tasks, such proxies modify channel-securing protocols, like TLS, resulting in serious vulnerabilities. Such problems are exacerbated by the fact that middleboxes are often invisible to one or both endpoints, leading to a lack of accountability. A recent protocol, called mcTLS, pioneered accountability for proxies, which are authorized by the endpoints and given limited read/write permissions to application traffic. Unfortunately, we show that mcTLS is insecure: the protocol modifies the TLS protocol, exposing it to a new class of middlebox-confusion attacks. Such attacks went unnoticed mainly because mcTLS lacked a formal analysis and security proofs. Hence, our second contribution is to formalize the goal of accountable proxying over secure channels. Third, we propose a provably-secure alternative to soon-to-be-standardized mcTLS: a generic and modular protocol-design that care- fully composes generic secure channel-establishment protocols, which we prove secure. Finally, we present a proof-of-concept implementation of our design, instantiated with unmodified TLS 1.3, and evaluate its overheads.
K. Bhargavan, I. Boureanu, A. Delignat-Lavaud, P. Fouque and C. Onete, "A Formal Treatment of Accountable Proxying over TLS," 2018 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, US, , pp. 339-356.