微信服务号

微信订阅号

2025-5-15- 18
Home > Archive>Volume 32, Issue 9, 2021 >2849-2866. DOI:10.13328/j.cnki.jos.005973
PDF HTML XML Export Cite reminder
Formal Analysis and Optimization of TLS1.3 Protocol in Strong Security Model
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

National Natural Science Foundation of China (61472414, 61772514, 61602061)

  • Article
    • | |
  • Metrics
    • |
  • Reference [36]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    TLS protocol works between the transport layer and application layer in TCP/IP system. The safety of transport layer is effectively protected by providing a series of security services such as confidentiality, integrity, authentication server required, as well as optional client authentication. In order to reduce network latency, TLS1.3 protocol adds the support for 0-RTT data, through caching long-term public key of server by client, and the long-term public key is directly used to generate a session key to send part of application layer data in the first message. For three kinds of 0-RTT mode, this study uses Scyther tools for formal analysis to obtain two attack paths of the 0-RTT data in CK security model, and an optimized protocol is proposed based on the 1-RTT semi-static mode. Through security proof and formal analysis, it is proved that the protocol is resistant to KCI attacks and replay attack against 0-RTT data in CK security model.

    Reference
    [1] Freier A, Karlton P, Kocher P. The secure sockets layer (SSL) protocol version 3.0. IETF RFC-6101, 2011.
    [2] Dierks T, Allen C. The TLS protocol version 1.0. IETF RFC-2246, 1999.
    [3] Dierks T, Rescorla E. The transport layer security (TLS) protocol version 1.2. IETF RFC-5246, 2008.
    [4] Alfardan N, Bernstein D, Paterson K, et al. On the security of RC4 in TLS. In:Proc. of the Usenix Conf. on Security. USENIX Association, 2013. 305-320.
    [5] Fardan N, Paterson K. Lucky thirteen:Breaking the TLS and DTLS record protocols. In:Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2013. 526-540.
    [6] Möller B, Duong T, Kotowicz K. This POODLE bites:Exploiting the SSL 3.0 fallback. Security Advisory, 2014.
    [7] Adrian D, Bhargavan K, Durumeric Z, et al. Imperfect forward secrecy:How diffie-hellman fails in practice. In:Proc. of the ACM Sigsac Conf. on Computer and Communications Security. ACM, 2015. 5-17.
    [8] Bhargavan K, Lavaud A, Fournet C, et al. Triple handshakes and cookie cutters:Breaking and fixing authentication over TLS. In:Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2014. 98-113.
    [9] Gujrathi S. Heartbleed bug:An OpenSSL heartbeat vulnerability. Int'l Journal of Computer Sciences and Engineering, 2014,2(5):61-64.
    [10] Beurdouche B, Bhargavan K, Delignat-Lavaud A, et al. A messy state of the union:taming the composite state machines of TLS. In:Proc. of the IEEE Symp. on Security & Privacy, 2015. 535-552.
    [11] Rescorla E. The transport layer security (TLS) protocol version 1.3. IETF draft-ietf-tls-tls13-20, 2017.
    [12] Bhargavan K, Leurent G. Transcript collision attacks:breaking authentication in TLS, IKE and SSH. British Journal of Psychiatry the Journal of Mental Science, 2016,41(7):8-13.
    [13] Jager T, Schwenk J, Somorovsky J. On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 encryption. In:Proc. of the ACM Sigsac Conf. on Computer and Communications Security. ACM, 2015. 1185-1196.
    [14] Paar C, Adrian D, Kasper E, et al. DROWN:Breaking TLS using SSLv2. In:Proc. of the Usenix Security Symp. USENIX Association, 2016. 689-706.
    [15] Cremers C, Horvat M, Hoyland J, et al. A comprehensive symbolic analysis of TLS 1.3. In:Proc. of the 2017 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2017. 1773-1788.
    [16] Bhargavan K, Blanchet B, Kobeissi N. Verified models and reference implementations for the TLS 1.3 standard candidate. In:Proc. of the 2017 IEEE Symp. on Security and Privacy (SP). IEEE, 2017. 483-502.
    [17] Krawczyk H, Wee H. The OPTLS protocol and TLS1.3. In:Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2016. 81-96.
    [18] Somorovsky J. Systematic fuzzing and testing of TLS libraries. In:Proc. of the ACM Sigsac Conf. on Computer and Communications Security. ACM, 2016. 1492-1504.
    [19] Xue R, Feng DG. The approaches and technologies for formal verification of security protocols. Chinese Journal of Computers, 2006,29(1):1-20(in Chinese with English abstract).
    [20] Cremers C. Scyther:Semantics and verification of security protocols. Netherlands:Eindhoven University of Technology, 2006.
    [21] Cremers C. Key exchange in IPsec revisited:Formal analysis of IKEv1 and IKEv2. In:Proc. of the European Symp. on Research in Computer Security (ESORICS 2011). Berlin:Springer-Verlag, 2011. 315-334.
    [22] Basin D, Cremers C, Meier S. Provably repairing the ISO/IEC 9798 standard for entity authentication. Journal of Computer Security, 2013,21(6):817-846.
    [23] Yang H, Prinz A, Oleshchuk V. Formal analysis and model checking of a group authentication protocol by Scyther. In:Proc. of the Euromicro Int'l Conf. on Parallel, Distributed, and Network-based Processing. IEEE Computer Society, 2016. 553-557.
    [24] Yang H, Oleshchuk V, Prinz A. Verifying group authentication protocols by scyther. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), 2016,7(2):3-19.
    [25] Ray B, Chowdhury M, Abawajy J. Secure object tracking protocol for the Internet of things. IEEE Internet of Things Journal, 2016, 3(4):1-10.
    [26] Meier S, Cremers C, Basin D. Strong invariants for the efficient construction of machine-checked protocol security proofs. In:Proc. of the IEEE Computer Security Foundations Symp. IEEE Computer Society, 2010. 231-245.
    [27] Meier S, Schmidt B, Cremers C, et al. The TAMARIN prover for the symbolic analysis of security protocols. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2013. 696-701.
    [28] Canetti R, Krawczyk H. Analysis of key-exchange protocols and their use for building secure channels. In:Proc. of the Advances in Cryptology (EUROCRYPT 2001). Berlin:Springer-Verlag, 2001. 453-474.
    [29] Günther C. An identity-based key-exchange protocol. In:Proc. of the Workshop on the Theory and Application of of Cryptographic Techniques. Berlin:Springer-Verlag, 1989. 29-37.
    [30] Cha J, Cheon J. An identity-based signature from gap diffie-hellman groups. In:Proc. of the Int'l Workshop on Theory and Practice in Public Key Cryptography:Public Key Cryptography. Berlin:Springer-Verlag, 2002. 18-30.
    [31] Fischlin M, Günther F. Multi-stage key exchange and the case of Google's QUIC protocol. In:Proc. of the 2014 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2014. 1193-1204.
    [32] Cremers C. Formally and practically relating the CK, CK-HMQV, and eCK security models for authenticated key exchange. Cryptology Eprint Archive, 2009.
    [33] Cremers C. Examining indistinguishability-based security models for key exchange protocols:The case of CK, CK-HMQV, and eCK. In:Proc. of the ACM Symp. on Information, Computer and Communications Security. ACM, 2011. 80-91.
    [34] Gorantla M, Boyd C, Nieto J. Modeling key compromise impersonation attacks on group key exchange protocols. ACM Trans. on Information & System Security, 2009,14(4):1-24.
    附中文参考文献:
    [19] 薛锐,冯登国.安全协议的形式化分析技术与方法.计算机学报,2006,29(1):1-20.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

陆思奇,周思渊,毛颖.强安全模型下TLS1.3协议的形式化分析与优化.软件学报,2021,32(9):2849-2866

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 15,2018
  • Revised:August 30,2018
  • Online: September 15,2021
  • Published: September 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044692Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063