Analyzing and fixing the QACCE security of QUIC

Citations of this article
Mendeley users who have this article in their library.
Get full text


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.




Sakurada, H., Yoneyama, K., Hanatani, Y., & Yoshida, M. (2016). Analyzing and fixing the QACCE security of QUIC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10074 LNCS, pp. 1–31). Springer Verlag.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free