Abstract
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 find 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.
Chapter PDF
Similar content being viewed by others
References
Browser security handbook, http://code.google.com/p/browsersec
How secure is Dropbox?, https://www.dropbox.com/help/27/en
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. SIGPLAN Not. 36, 104–115 (2001)
Adida, B.: Helios: Web-based open-audit voting. In: USENIX Security Symposium, pp. 335–348 (2008)
Adida, B., Barth, A., Jackson, C.: Rootkits for JavaScript environments. In: Workshop on Offensive Technologies, WOOT (2009)
Akhawe, D., Barth, A., Lam, P.E., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: CSF, pp. 290–304 (2010)
Arapinis, M., Bursuc, S., Ryan, M.: Privacy Supporting Cloud Computing: ConfiChair, a Case Study. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 89–108. Springer, Heidelberg (2012)
Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis. In: CSF, pp. 247–262 (2012)
Barth, A., Jackson, C., Mitchell, J.C.: Robust defenses for cross-site request forgery. In: CCS, pp. 75–88 (2008)
Belenko, A., Sklyarov, D.: “Secure Password Managers” and “Military-Grade Encryption” on Smartphones: Oh, Really? Technical report, Elcomsoft Ltd. (2012)
Bhargavan, K., Delignat-Lavaud, A.: Web-based attacks on host-proof encrypted storage. In: Workshop on Offensive Technologies, WOOT (2012)
Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security 17(4), 363–434 (2009)
Blanchet, B., Chaudhuri, A.: Automated formal analysis of a protocol for secure file sharing on untrusted storage. In: IEEE Symposium on Security & Privacy (2008)
Blanchet, B., Smyth, B.: ProVerif: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, http://www.proverif.inria.fr/manual.pdf
Bohannon, A., Pierce, B.C.: Featherweight Firefox: Formalizing the core of a web browser. In: WebApps (2010)
Groß, T.R., Pfitzmann, B., Sadeghi, A.-R.: Browser Model for Security Analysis of Browser-Based Protocols. In: De Capitani di Vimercati, S., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 489–508. Springer, Heidelberg (2005)
Hammer-Lahav, E., Recordon, D., Hardt, D.: The OAuth 2.0 Authorization Protocol. IETF Internet Draft (2011)
Jackson, D.: Alloy: A Logical Modelling Language. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, p. 1. Springer, Heidelberg (2003)
Kamara, S., Lauter, K.: Cryptographic Cloud Storage. In: Sion, R., Curtmola, R., Dietrich, S., Kiayias, A., Miret, J.M., Sako, K., Sebé, F. (eds.) FC 2010 Workshops. LNCS, vol. 6054, pp. 136–149. Springer, Heidelberg (2010)
Kelsey, J., Schneier, B., Hall, C., Wagner, D.: Secure Applications of Low-Entropy Keys. In: Okamoto, E., Davida, G., Mambo, M. (eds.) ISW 1997. LNCS, vol. 1396, pp. 121–134. Springer, Heidelberg (1998)
Rescorla, E.: HTTP over TLS. Request for Comments 2818, IETF (2000)
Rydstedt, G., Bursztein, E., Boneh, D., Jackson, C.: Busting frame busting: a study of clickjacking vulnerabilities at popular sites. In: Web 2.0 S&P (2010)
Stearne, B., Barth, A. (eds.): Content Security Policy 1.0. W3C Working Draft (2012)
Yoshihama, S., Tateishi, T., Tabuchi, N., Matsumoto, T.: Information-Flow-Based Access Control for Web Browsers. IEICE Transactions E92-D(5), 836–850 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bansal, C., Bhargavan, K., Delignat-Lavaud, A., Maffeis, S. (2013). Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage. In: Basin, D., Mitchell, J.C. (eds) Principles of Security and Trust. POST 2013. Lecture Notes in Computer Science, vol 7796. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36830-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-36830-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36829-5
Online ISBN: 978-3-642-36830-1
eBook Packages: Computer ScienceComputer Science (R0)