{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T02:40:41Z","timestamp":1747190441324,"version":"3.40.5"},"reference-count":27,"publisher":"Wiley","license":[{"start":{"date-parts":[[2021,8,20]],"date-time":"2021-08-20T00:00:00Z","timestamp":1629417600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Security and Communication Networks"],"published-print":{"date-parts":[[2021,8,20]]},"abstract":"<jats:p>As a newly proposed secure transport protocol, QUIC aims 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. An important safety goal of QUIC protocol is to provide effective data service for users. To aim this safety requirement, we propose a formal analysis method to analyze the safety of QUIC handshake protocol by using model checker SPIN and cryptographic protocol verifier ProVerif. Our analysis shows the counterexamples to safety properties, which reveal a design flaw in the current protocol specification. To this end, we also propose and verify a possible fix that is able to mitigate these flaws.<\/jats:p>","DOI":"10.1155\/2021\/1630223","type":"journal-article","created":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T00:05:41Z","timestamp":1629504341000},"page":"1-12","source":"Crossref","is-referenced-by-count":6,"title":["A Systematic Approach to Formal Analysis of QUIC Handshake Protocol Using Symbolic Model Checking"],"prefix":"10.1155","volume":"2021","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9075-7810","authenticated-orcid":true,"given":"Jingjing","family":"Zhang","sequence":"first","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, Institute of System Engineering, Chinese Academy of Military Science, Beijing 100039, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5797-818X","authenticated-orcid":true,"given":"Xianming","family":"Gao","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, Institute of System Engineering, Chinese Academy of Military Science, Beijing 100039, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6956-8177","authenticated-orcid":true,"given":"Lin","family":"Yang","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, Institute of System Engineering, Chinese Academy of Military Science, Beijing 100039, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7024-3003","authenticated-orcid":true,"given":"Tao","family":"Feng","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, Institute of System Engineering, Chinese Academy of Military Science, Beijing 100039, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0818-2526","authenticated-orcid":true,"given":"Dongyang","family":"Li","sequence":"additional","affiliation":[{"name":"College of Command and Control Engineering, Army Engineering University of China, Nanjing 210007, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5649-8694","authenticated-orcid":true,"given":"Qiang","family":"Wang","sequence":"additional","affiliation":[{"name":"National Key Laboratory of Science and Technology on Information System Security, Institute of System Engineering, Chinese Academy of Military Science, Beijing 100039, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"volume-title":"Security issues in the 5G standard and how formal methods come to the rescue","year":"2019","author":"L. Hirschi","key":"1"},{"key":"2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10575-8_22","volume-title":"Model Checking Security Protocols","author":"D. Basin","year":"2018"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363528"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.3233\/jcs-2006-14101"},{"first-page":"141","article-title":"Automated analysis of cryptographic protocols using mur\/spl phi","author":"J. C. Mitchell","key":"9"},{"first-page":"192","article-title":"Athena: a new efficient automatic checker for security protocol analysis","author":"D. X. Song","key":"10"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/access.2020.2969474"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61042-1_53"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/cyberc.2018.00019"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/pst47121.2019.8949057"},{"first-page":"1383","article-title":"A formal analysis of 5G authentication","author":"D. Basin","key":"15"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23394"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/dsc.2019.00082"},{"author":"S. R. Hussain","key":"19","article-title":"LTEinspector: a systematic approach for adversarial testing of 4G LTE"},{"first-page":"669","article-title":"A property-directed security and privacy analysis framework for 5G cellular network protocol","author":"S. R. Hussain","key":"20"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/tdsc.2020.3022797"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2016.2605087"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-76581-5_15"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/tit.1983.1056650"},{"key":"25","doi-asserted-by":"crossref","first-page":"14836","DOI":"10.1109\/ACCESS.2021.3052578","article-title":"Formal analysis of QUIC handshake protocol using symbolic model checking","volume":"9","author":"J. Zhang","year":"2021","journal-title":"IEEE Access"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/cscloud-edgecom49738.2020.00030"},{"author":"I. Jana","key":"27","article-title":"QUIC: A UDP-Based Multiplexed and Secure Transport"}],"container-title":["Security and Communication Networks"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/scn\/2021\/1630223.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/scn\/2021\/1630223.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/scn\/2021\/1630223.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T00:05:44Z","timestamp":1629504344000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/scn\/2021\/1630223\/"}},"subtitle":[],"editor":[{"given":"Ruhul","family":"Amin","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2021,8,20]]},"references-count":27,"alternative-id":["1630223","1630223"],"URL":"https:\/\/doi.org\/10.1155\/2021\/1630223","relation":{},"ISSN":["1939-0122","1939-0114"],"issn-type":[{"type":"electronic","value":"1939-0122"},{"type":"print","value":"1939-0114"}],"subject":[],"published":{"date-parts":[[2021,8,20]]}}}