Submitted by

Web traffic is exposed to potential eavesdroppers, and despite the use of encryption mechanisms, it has been shown vulnerable to side-channel attacks which reveal information about its contents. Although various countermeasures against such attacks have been proposed, the lack of mathematical foundations for reasoning about information leaks in web traffic has prevented the development of provably secure countermeasures. In this thesis, we develop a novel framework for reasoning about information leakage in web traffic. We propose flexible models of web applications, web browsing and web traffic, and develop two security models based on different notions of security: (1) an attacker’s knowledge about the possible secret values contained in the web traffic, and (2) the probability of an attacker to guess the secret values. In those models, we formalize countermeasures and network protocols, defining them as compositions of several basic building blocks. We use this framework to perform formal analysis of various aspects of informa-tion leakage in web traffic. We design principles for countermeasure composition which strengthens security, as well as investigate the utilization of structural prop-erties of web applications to design countermeasures which provide strong security guarantees. Additionally, we leverage and extend results from quantitative infor-mation flow to design algorithms for calculating security guarantees. Furthermore, we investigate the differences in the proposed security models, as well as the role of caching to the security of web applications. Finally, we perform two case studies empirically measuring the performance of countermeasures to a sample of web applications. We propose a methodology for dealing with computational challenges arising during practical analysis, and discuss the results of the case studies