Formal Analysis of QUIC Handshake Protocol Using Symbolic Model Checking

This work presents a security analysis of the QUIC handshake protocol based on symbolic model checking. As a newly proposed secure transport protocol, the purpose of QUIC is to improve the transport performance of HTTPS traffic and enable rapid deployment and evolution of transport mechanisms. QUIC is currently in the IETF standardization process and will potentially carry a significant portion of Internet traffic in the emerging future. For a better understanding of the essential security properties, we have developed a formal model of the QUIC handshake protocol and perform a comprehensive formal security analysis by using two state-of-the-art model checking tools for cryptographic protocols, i.e., ProVeirf and Verifpal. Our analysis shows that ProVerif is generally more powerful than Verifpal in terms of verifying authentication properties. Moreover, both tools produce a counterexample to some security properties, which reveal a design flaw in the current protocol specification. Last but not least, we analyze the root causes of this counterexample and suggest a possible fix.