Formalized analysis for authentication test model of TLS

doi:10.3778/j.issn.1002-8331.2009.23.028

Computer Engineering and Applications ›› 2009, Vol. 45 ›› Issue (23): 100-103.DOI: 10.3778/j.issn.1002-8331.2009.23.028

• 网络、通信、安全 • Previous Articles Next Articles

Formalized analysis for authentication test model of TLS

^{KONG Juan，CAO Li-pei}

Department of Computer Engineering，Anyang Institute Technology，Anyang，Henan 455000，China

Received:2009-03-23 Revised:2009-05-26 Online:2009-08-11 Published:2009-08-11
Contact: KONG Juan

TLS协议认证测试模型与形式化分析

^{孔娟，曹利培}

安阳工学院计算机科学与信息工程系，河南安阳 455000

通讯作者: 孔娟

Abstract

Abstract:

TLS protocol is an important transport layer security protocol，and is widely used.Based on strand space theory，this paper points out the DH parameter signature certification testing program，analyzes and proves the confidentiality and authentication of the agreement.The result shows that the TLS protocol meets their security statement.

Key words: Transport Layer Security（TLS） protocol, authentication test, strand space, formalized analysis

摘要：

TLS协议是一种重要的传输层安全协议，得到了广泛的应用。在结合串空间理论和方法的基础上，通过构造TLS握手协议的认证测试模型，提出了TLS协议的DH参数签名认证测试方案，分析和证明了协议的保密性和认证性等关键属性。结果表明TLS协议满足其安全性说明。

关键词: 传输层安全协议, 认证测试, 串空间, 形式化分析

CLC Number:

TP393

^{KONG Juan，CAO Li-pei}

Formalized analysis for authentication test model of TLS

[J]. Computer Engineering and Applications, 2009, 45(23): 100-103.

^{孔娟，曹利培}

TLS协议认证测试模型与形式化分析

[J]. 计算机工程与应用, 2009, 45(23): 100-103.

[1]	LI Qian1, WANG Zheng1, MA Jianfen1, LI Na2. Lightweight mobile payment protocol fairness analysis [J]. Computer Engineering and Applications, 2018, 54(19): 82-87.
[2]	YU Lei1, WEI Shimin1, ZHUO Zepeng2. Research on consistence of strand parameters for protocol principals in authentication test theory [J]. Computer Engineering and Applications, 2015, 51(13): 86-91.
[3]	YU Lei, WEI Shimin. Analysis on properties for principals’ keys on construction of test components [J]. Computer Engineering and Applications, 2013, 49(6): 114-117.
[4]	YU Lei, WEI Shimin. Security analysis of mutual-authentication cryptographic protocol in network management [J]. Computer Engineering and Applications, 2012, 48(4): 94-96.
[5]	CAO Lifeng1, CHEN Xingyuan1, DU Xuehui1, WANG Huaipeng2. Multi-level secure tunnel establishment protocol and its security analysis [J]. Computer Engineering and Applications, 2012, 48(20): 117-122.
[6]	DENG Fan，DENG Shaofeng，LI Yifa. Provable secure authenticated key exchange protocol under standard model [J]. Computer Engineering and Applications, 2011, 47(13): 106-109.
[7]	LI Ting-yuan1，2，QIN Zhi-guang1，LIU Xiao-dong2，ZHANG Xuan-fang2. Formal analysis of Needham-Schroeder protocol with authentication test methods [J]. Computer Engineering and Applications, 2010, 46(19): 100-102.
[8]	MA Yu-chi，ZHAO Yuan，DENG Yi-qun，LI Yi-fa. Trusted computing platform login authentication scheme based on CPK [J]. Computer Engineering and Applications, 2010, 46(1): 90-94.
[9]	ZHANG Yan，WANG Ze. Improved method of enhancing EAP-AKA protocol security [J]. Computer Engineering and Applications, 2009, 45(28): 96-98.
[10]	GUO Yu-yan¹,WEI Shi-min²,ZHUO Ze-peng³. Analyzing model of amended wireless authentication protocol SSM [J]. Computer Engineering and Applications, 2009, 45(1): 129-130.
[11]	DING Meng-wei,ZHOU Qing-lei,ZHAO Dong-ming. Strand space model of Yahalom-Paulson protocol and its analysis [J]. Computer Engineering and Applications, 2008, 44(22): 97-99.
[12]	ZHAO Hui，LI Ming-chu，WANG Zhi-hui. New formal verification method of grid security protocols based on virtual organization [J]. Computer Engineering and Applications, 2007, 43(24): 117-122.
[13]	WANG Peng，LI Xie-hua，LU Song-nian. Formal analysis of EAP-AKA protocol based on authentication tests [J]. Computer Engineering and Applications, 2007, 43(15): 157-159.
[14]	. Formal Specification and Verification of Andrew secure RPC protocol Based on Strand Spaces Model [J]. Computer Engineering and Applications, 2007, 43(13): 153-155.
[15]	JiaFen Liu,. Analysis of X.509 Authentication Protocol via Authentication Test [J]. Computer Engineering and Applications, 2006, 42(8期): 23-.

Formalized analysis for authentication test model of TLS

TLS协议认证测试模型与形式化分析

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics