Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Analyzing and Fixing the QACCE Security of QUIC Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Security Analysis of the W3C Web Cryptography API

Authors : Kelsey Cairns, Harry Halpin, Graham Steel

Published in: Security Standardisation Research

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Due to the success of formal modeling of protocols such as TLS, there is a revival of interest in applying formal modeling to standardized APIs. We argue that formal modeling should happen as the standard is being developed (not afterwards) as it can detect complex or even simple attacks that the standardization group may not otherwise detect. As a case example of this, we discuss in detail the W3C Web Cryptography API. We demonstrate how a formal analysis of the API using the modeling language AVISPA with a SAT solver demonstrates that while the API has no errors in basic API operations and maintains its security properties for the most part, there are nonetheless attacks on secret key material due to how key wrapping and usages are implemented. Furthermore, there were a number of basic problems in terms of algorithm selection and a weakness that led to a padding attack. The results of this study led to the removal of algorithms before its completed standardization and the removal of the padding attack via normalization of error codes, although the key wrapping attack is still open. We expect this sort of formal methodology to be applied to new standardization efforts at the W3C such as the W3C Web Authentication API.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter NFC Payment Spy: A Privacy Attack on Contactless Payments
next chapter Algorithm Agility – Discussion on TPM 2.0 ECC Functionalities
Footnotes
5
See the results of the 2014 penetration testing report by Cure53.de available here: https://​cure53.​de/​pentest-report_​openpgpjs.​pdf.
 
6
The workshop was called ‘Identity in the Browser,’ archived at http://​www.​w3.​org/​2011/​identity-ws/​.
 
12
The formal semantics of AVISPA’s higher-level HLPSL that subsumes IF are out of scope but are given here: http://​www.​avispa-project.​org/​delivs/​2.​1/​d2-1.​pdf.
 
13
Throughout this paper we omit many AVISPA-specific constructs in order to focus on the underlying model. This includes statements that are necessary for modeling protocols but not APIs, but will nonetheless cause errors if omitted. The complete rules are available here: http://​www.​w3.​org/​2012/​webcrypto/​webcrypto_​if_​files.​tgz.
 
14
Note as of September 2016, the 2014 report is currently under revision.
 
19
Such as ARM TrustZone.
 
21
For details of the W3C Web Cryptography v.Next workshop that dealt with hardware tokens, FIDO, and trusted execution environments, see http://​www.​w3.​org/​2012/​webcrypto/​webcrypto-next-workshop/​.
 
Literature
1.
Adrian, D., Bhargavan, K., Durumeric, Z., Gaudry, P., Green, M., Halderman, J.A., Heninger, N., Springall, D., Thomé, E., Valenta, L., et al.: Imperfect forward secrecy: how Diffie-Hellman fails in practice. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pp. 5–17. ACM (2015)
2.
Akhawe, D., Barth, A., Lam, P.E., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pp. 290–304. IEEE Computer Society, Washington, DC, USA (2010)
3.
4.
Bansal, C., Bhargavan, K., Delignat-Lavaud, A., Maffeis, S.: Keys to the cloud: formal analysis and concrete attacks on encrypted web storage. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 126–146. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-36830-1_​7 CrossRef
5.
Bardou, R., Focardi, R., Kawamoto, Y., Simionato, L., Steel, G., Tsay, J.-K.: Efficient padding oracle attacks on cryptographic hardware. In: Safavi-Naini, R., Canetti, R. (eds.) CRYPTO 2012. LNCS, vol. 7417, pp. 608–625. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-32009-5_​36 CrossRef
6.
7.
Bellare, M.: New proofs for NMAC and HMAC: security without collision-resistance. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 602–619. Springer, Heidelberg (2006). doi:10.​1007/​11818175_​36 CrossRef
8.
Bellare, M., Rogaway, P.: The exact security of digital signatures-how to sign with RSA and Rabin. In: Maurer, U. (ed.) EUROCRYPT 1996. LNCS, vol. 1070, pp. 399–416. Springer, Heidelberg (1996). doi:10.​1007/​3-540-68339-9_​34
9.
Beurdouche, B., Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y., Zinzindohoue, J.K.: A messy state of the union: taming the composite state machines of TLS. In: 2015 IEEE Symposium on Security and Privacy (SP), pp. 535–552. IEEE (2015)
10.
Bhargavan, K., Lavaud, A.D., Fournet, C., Pironti, A., Strub, P.-Y.: Triple handshakes and cookie cutters: breaking and fixing authentication over TLS. In: 2014 IEEE Symposium on Security and Privacy (SP), pp. 98–113. IEEE (2014)
11.
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE Workshop on Computer Security Foundations, CSFW 2001, pp. 82–96. IEEE Computer Society, Washington, DC, USA (2001)
12.
Bleichenbacher, D.: Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS #1. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 1–12. Springer, Heidelberg (1998). doi:10.​1007/​BFb0055716 CrossRef
13.
Bond, M., Anderson, R.: API-level attacks on embedded systems. Computer 34(10), 67–75 (2001)CrossRef
14.
Boneh, D., Shparlinski, I.E.: On the unpredictability of bits of the elliptic curve Diffie-Hellman scheme. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 201–212. Springer, Heidelberg (2001). doi:10.​1007/​3-540-44647-8_​12 CrossRef
15.
16.
Cremers, C.J.F.: The Scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-70545-1_​38 CrossRef
17.
Delaune, S., Kremer, S., Steel, G.: Formal security analysis of PKCS#11 and proprietary extensions. J. Comput. Secur. 18(6), 1211–1245 (2010)CrossRef
18.
Dennis, G., Chang, F.S.-H., Jackson, D.: Modular verification of code with SAT. In: Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, 17–20 July 2006, Portland, Maine, USA, pp. 109–120 (2006)
19.
20.
Georgiev, M., Iyengar, S., Jana, S., Anubhai, R., Boneh, D., Shmatikov, V.: The most dangerous code in the world: validating SSL certificates in non-browser software. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS 2012, pp. 38–49. ACM, New York (2012)
21.
Halpin, H.: The W3C web cryptography API: motivation and overview. In: Proceedings of the Companion Publication of the 23rd International Conference on World Wide Web Companion, WWW Companion 2014, pp. 959–964, Republic and Canton of Geneva, Switzerland. International World Wide Web Conferences Steering Committee (2014)
22.
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRef
23.
Jager, T., Schinzel, S., Somorovsky, J.: Bleichenbacher’s attack strikes again: breaking PKCS#1 v1.5 in XML encryption. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 752–769. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33167-1_​43 CrossRef
24.
25.
Kaminsky, A., Kurdziel, M., Radziszowski, S.: An overview of cryptanalysis research for the advanced encryption standard. In: 2010 Military Communications Conference - MILCOM 2010 (2010)
26.
27.
Künnemann, R., Steel, G.: YubiSecure? Formal security analysis results for the Yubikey and YubiHSM. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol. 7783, pp. 257–272. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38004-4_​17 CrossRef
28.
29.
Mitchell, C.J.: Error Oracle attacks on CBC mode: is there a future for CBC mode encryption? In: Zhou, J., Lopez, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 244–258. Springer, Heidelberg (2005). doi:10.​1007/​11556992_​18 CrossRef
30.
Near, J.P., Jackson, D.: Derailer: interactive security analysis for web applications. In: Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 587–598. IEEE/ACM (2014)
31.
32.
33.
Rizzo, J.: Duong., T.: Practical padding Oracle attacks. In: Proceedings of the 4th USENIX Conference on Offensive Technologies, WOOT 2010, pp. 1–8. USENIX Association, Berkeley, CA, USA (2010)
34.
Rogaway, P., Shrimpton, T.: A provable-security treatment of the key-wrap problem. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 373–390. Springer, Heidelberg (2006). doi:10.​1007/​11761679_​23 CrossRef
35.
Rogaway, P.: Evaluation of some blockcipher modes of operation. Technical report, University of California, Davis, Evaluation carried out for the Cryptography Research and Evaluation Committees (CRYPTREC) for the Government of Japan, February 2011
36.
Schmidt, B., Sasse, R., Cremers, C., Basin, D.: Automated verification of group key agreement protocols. In: 2014 IEEE Symposium on Security and Privacy (SP), pp. 179–194. IEEE (2014)
37.
Smart, N.P., Rijmen, V., Warinschi, B., Watson, G., Patterson, K., Stam, M.: Algorithms, key sizes and parameters report: 2014 recommendations. Technical report, November 2014. ENISA Report. Version 1.0
38.
Stark, E., Hamburg, M., Boneh, D.: Symmetric cryptography in Javascript. In: Proceedings of the 2009 Annual Computer Security Applications Conference, ACSAC 2009, pp. 373–381. IEEE Computer Society, Washington, DC, USA (2009)
39.
Taly, A., Erlingsson, Ú., Mitchell, J.C., Miller, M.S., Nagra, J.: Automated analysis of security-critical Javascript APIs. In: Proceedings of the 2011 IEEE Symposium on Security and Privacy, SP 2011, pp. 363–378. IEEE Computer Society, Washington, DC, USA (2011)
40.
Torlak, E., Taghdiri, M., Dennis, G., Near, J.P.: Applications and extensions of alloy: past, present and future. Math. Struct. Comput. Sci. 23(4), 915–933 (2013)MathSciNetCrossRef
41.
Vaudenay, S.: Security flaws induced by CBC padding — applications to SSL, IPSEC, WTLS. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 534–545. Springer, Heidelberg (2002). doi:10.​1007/​3-540-46035-7_​35 CrossRef
42.
Wen, C.C., Dawson, E., González Nieto, J.M., Simpson, L.: A framework for security analysis of key derivation functions. In: Ryan, M.D., Smyth, B., Wang, G. (eds.) ISPEC 2012. LNCS, vol. 7232, pp. 199–216. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-29101-2_​14 CrossRef
43.
Metadata
Title
Security Analysis of the W3C Web Cryptography API
Authors
Kelsey Cairns
Harry Halpin
Graham Steel
Copyright Year
2016
Book
Security Standardisation Research

Print ISBN: 978-3-319-49099-1

Electronic ISBN: 978-3-319-49100-4

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-49100-4_5

Premium Partner

    Image Credits