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:
Cover of the book

2016 | OriginalPaper | Chapter

Analyzing and Fixing the QACCE Security of QUIC

Authors : Hideki Sakurada, Kazuki Yoneyama, Yoshikazu Hanatani, Maki Yoshida

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

QUIC is a secure transport protocol developed by Google. Lychev et al. proposed a security model (QACCE model) to capture the security of QUIC. However, the QACCE model is very complicated, and it is not clear if security requirements for QUIC are appropriately defined. In this paper, we show the first formal analysis result of QUIC using automated security verification tool ProVerif. Our symbolic model formalizes the QACCE model and the specification of QUIC. As the result of the verification, we find three attacks against QUIC in the QACCE model. It means that the Lychev et al.’s security proofs are not correct. We discuss why such attacks occur, and clarify there are unnecessarily strong points in the QACCE model. Finally, we give a way to improve the QACCE model to exactly address the appropriate security requirements.

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
next chapter Cross-Tool Semantics for Protocol Security Goals
Appendix
Available only for authorised users
Footnotes
1
In the original model, this query returns the encryption of \(m_{b^{q}_{p,j}}\). However, since p in \(m_{b^{q}_{p,j}}\) is equal to p in \(\pi ^{r}_{p,j}\), \(m_{b^{q}_{p,j}}\) must be changed to \(m_{b^{r}_{p,j}}\).
 
2
In the original model, \(\mathsf {encrypt}\) query for \(\pi ^{r}_{p,j}\) is prohibited. However, \(\mathsf {encrypt}( \pi ^{r}_{p,j}, *, *, *, \mathsf {init})\) returns the ciphertext generated by p, and it is not reasonable. In this definition, the ciphertext of generated by \(p'\) should be prohibited. Thus, \(\pi ^{r}_{p,j}\) must be changed to \(\pi ^{q}_{p',i}\).
 
Literature
1.
Dierks, T., Allen, C.: The TLS protocol version 1.0. In: RFC 2246 (Proposed Standard), Internet Engineering Task Force (1999)
2.
Ford, B.: Structured streams: a new transport abstraction. In: SIGCOMM 2007, pp. 361–372 (2007)
3.
Stewart, R.: Stream control transmission protocol. In: RFC 4960 (Proposed Standard), Internet Engineering Task Force (2007)
4.
Erman, J., Gopalakrishnan, V., Jana, R., Ramakrishnan, K.K.: Towards a SPDY’ier mobile web? In: CoNEXT 2013, pp. 303–314 (2013)
5.
6.
7.
Fischlin, M., Günther, F.: Multi-stage key exchange and the case of Google’s QUIC protocol. In: ACM Conference on Computer and Communications Security 2014, pp. 1193–1204 (2014)
8.
9.
Lychev, R., Jero, S., Boldyreva, A., Nita-Rotaru, C.: How secure and quick is QUIC? Provable security and performance analyses. In: 2015 IEEE Symposium on Security and Privacy, pp. 214–231 (2015)
10.
Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.3. Internet-Draft draft-ietf-tls-tls13-13 (2016)
11.
12.
Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363–434 (2009)CrossRef
13.
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Logic Algebraic Program. 75(1), 3–51 (2008). Algebraic Process Calculi. The First Twenty Five Years and Beyond. IIIMathSciNetCrossRefMATH
14.
Metadata
Title
Analyzing and Fixing the QACCE Security of QUIC
Authors
Hideki Sakurada
Kazuki Yoneyama
Yoshikazu Hanatani
Maki Yoshida
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_1

Premium Partner

    Image Credits