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...

Full description

Saved in:
Bibliographic Details
Published in:IEEE access 2021, Vol.9, p.14836-14848
Main Authors: Zhang, Jingjing, Yang, Lin, Gao, Xianming, Tang, Gaigai, Zhang, Jiyong, Wang, Qiang
Format: Article
Language:English
Subjects:
Analytical models
applied pi calculus
Calculus
cryptographic protocol
Cryptographic protocols
Cryptography
formal verification
Handshaking protocols
Model checking
Properties (attributes)
Protocol (computers)
Protocols
ProVerif
QUIC
Security
Servers
Standardization
Verifpal
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2169-3536
2169-3536
DOI:10.1109/ACCESS.2021.3052578