Security analysis of TLS protocol implementations based on model checking

被引：0

作者：

Bi X. ^{[1
]}

Tang C. ^{[2
]}

机构：

[1] College of Advanced Interdisciplinary Studies, National University of Defense Technology, Changsha

[2] College of Electronic Science and Technology, National University of Defense Technology, Changsha

来源：

Xi Tong Gong Cheng Yu Dian Zi Ji Shu/Systems Engineering and Electronics | 2021年 / 43卷 / 03期

关键词：

Finite state machine; Model checking; Security protocol analysis; Transport layer security (TLS);

D O I：

10.12305/j.issn.1001-506X.2021.03.30

中图分类号：

学科分类号：

摘要：

In view of the problem that the traditional fuzzy testing method can find the memory vulnerability of the transport layer security (TLS) protocol implementation, but it can not find the logic loophole, based on the method of model detection, the state machine model of TLS protocol implementation is extracted, establishes the protocol security attribute model is establised, the possible abnormal behavior in the protocol implementation is looked, and the automation and system analysis of the protocol implementation is realized. The security attribute of the state machine for the protocol implementation generated by test cases is modeled, and the extracted model is checked by using the NuSMV tool. The experiment results show that the proposed method can effectively analyze the state machine model of TLS protocol implementation, and find the logic loopholes and the defects inconsistent with the specification. © 2021, Editorial Office of Systems Engineering and Electronics. All right reserved.

引用

页码：839 / 846

页数：7

共 27 条

[1]

RESCORLA E., The transport layer security (TLS) protocol version 1. 3

[2]

ALFARDAN N J, PATERSON K G., Lucky thirteen: breaking the TLS and DTLS record protocols, Proc. of the IEEE Symposium on Security and Privacy, pp. 526-540, (2013)

[3]

YAU A K L, PATERSON K G, MITCHELL C J., Padding oracle attacks on CBC-mode encryption with secret and random IVs, Proc. of the International Workshop on Fast Software Encryption, pp. 299-319, (2005)

[4]

MOLLER B, DUONG T, KOTOWICZ K., This POODLE bites: exploiting the SSL 3. 0 fallback

[5]

CIMATTI A, CLARKE E, GIUNCHIGLIA E, Et al., Nusmv 2: an opensource tool for symbolic model checking, Proc. of the International Conference on Computer Aided Verification, pp. 359-364, (2002)

[6]

BEURDOUCHE B, BHARGAVAN K, DELIGNAT-LAVAUD A, Et al., A messy state of the union: taming the composite state machines of TLS, Proc. of the IEEE Symposium on Security and Privacy, pp. 535-552, (2015)

[7]

BEURDOUCHE B, DELIGNAT-LAVAUD A, KOBEISSI N, Et al., FLEXTLS: a tool for testing TLS implementations, Proc. of the 9th USENIX Conference on Offensive Technologies, (2015)

[8]

SHEN Y Z, GU C X, CHEN X, Et al., Vulnerability analysis of OpenVPN system based on model learning, Journal of Software, 30, 12, pp. 3750-3764, (2019)

[9]

SHEN Y Z, GU C X, CHEN X., Network security protocol vulnerability analysis system based on model learning, Journal of Information Engineering University, 20, 1, pp. 111-115, (2019)

[10]

TSANKOV P, DASHTI M T, BASIN D., SECFUZZ: fuzz-testing security protocols, Proc. of the 7th International Workshop on Automation of Software Test, (2012)

← 1 2 3 →