Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage, C. Bansal, K. Bhargavan, A. Delignat-Lavaud & S. Maffeis

To protect sensitive user data against server-side attacks, a number of security-conscious web applications have turned to client-side encryption, where only encrypted user data is ever stored in the cloud. We formally investigate the security of a number of such applications, including password managers, cloud storage providers, an e-voting website and a conference management system. We show that their security relies on both their use of cryptography and the way it combines with common web security mechanisms as implemented in the browser. We model these applications using the WebSpi web security library for ProVerif, we discuss novel attacks found by automated formal analysis, and we propose robust countermeasures.

Discovered Attacks

* To more know about these attacks, please email us at [karthikeyan dot bhargavan at inria dot fr]

Scripts

Running the Scripts

You will need to have the latest version of ProVerif in order to be able to test the library and the models. ProVerif can be downloaded from here.
Then, you can use the following command to analyze the models:

proverif -lib model [file_name].pv