一种改进的基于认证测试的形式化分析方法

doi:10.3969/j.issn.1671-1122.2019.01.004

信息网络安全 ›› 2019, Vol. 19 ›› Issue (1): 27-33.doi: 10.3969/j.issn.1671-1122.2019.01.004

一种改进的基于认证测试的形式化分析方法

姚萌萌(), 朱正超, 刘明达

江南计算技术研究所,江苏无锡 214063

收稿日期:2018-09-19 出版日期:2019-01-20 发布日期:2020-05-11
作者简介:
作者简介：姚萌萌（1982—）,男,山东,博士研究生,主要研究方向为网络安全;朱正超（1974—）,男,湖南,高级工程师,硕士,主要研究方向为信息安全;刘明达（1991—）,男,山东,博士研究生,主要研究方向为区块链技术。
基金资助:
国家自然科学基金[91430214, 6732018];核高基重大专项[2017ZX01028101]

An Improved Formal Analysis Method Based on Authentication Tests

Mengmeng YAO(), Zhengchao ZHU, Mingda LIU

Jiangnan Institute of Computing Technology, Wuxi Jiangsu 214063, China

Received:2018-09-19 Online:2019-01-20 Published:2020-05-11

摘要/Abstract

摘要：

近年来,认证测试定理得到了改进,并应用于各种安全协议的分析。但是这些改进定理在应用范围和准确性方面存在一定的缺陷。针对这些缺陷,文章提出了一种改进的输入测试定理及加密测试定理,并给出了改进定理的证明。通过分析认证测试中常规节点的判定、证明过程中的错误、参数一致性证明过程中的不准确性和错误,指出了认证测试在使用过程中的缺陷。基于这些缺陷,文章提出了一种改进的基于认证测试的形式化分析方法——递归测试,并通过该方法证明了BAN-Yahalom协议。分析结果表明,该方法扩大了认证测试使用范围,且可以有效地、准确地分析安全协议。

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

Abstract:

In recent years, authentication tests has been improved and applied to the analysis of various security protocols. However, these improvement theorems also have certain defects in terms of application scope and accuracy. In response to these defects, in this paper, improved incoming test theorem and encryption test theorem are proposed, and proof of the improvement theorem is given. This paper points out the defects of the authentication test in use by analyzing the judgment of the normal nodes in the authentication test, the errors in the proof process, and the inaccuracies and errors in the process of parameter consistency verification. Based on these defects, an improved formal analysis method recursion test is proposed. This method is used to prove BAN-Yahalom protocol, the result proves this method has expanded the scope of the use of authentication tests, and can analyze the security protocol effectively, accurately.

Key words: strand space, authentication tests, formal analysis method, security protocol

中图分类号:

TP309

姚萌萌, 朱正超, 刘明达. 一种改进的基于认证测试的形式化分析方法[J]. 信息网络安全, 2019, 19(1): 27-33.

Mengmeng YAO, Zhengchao ZHU, Mingda LIU. An Improved Formal Analysis Method Based on Authentication Tests[J]. Netinfo Security, 2019, 19(1): 27-33.

图/表 7

表1

图1

图2

图3

图4

图5

图6

参考文献 18

[1]	DUAN Ran, XU Naiyang, HU Aiqun.Research on Authentication Protocol Security Based on Formal Verification Tool[J]. Netinfo Security, 2015, 15(7): 71-76.
	段然,徐乃阳,胡爱群. 基于形式化分析工具的认证协议安全性研究[J]. 信息网络安全,2015,15(7):71-76.
[2]	DOLEV D, YAO A.On the Security of Public Key Protocols[J]. Information Theory IEEE Transactions on, 1983, 29(2): 198-208.
[3]	FABREGA F J T, HERZOG J C, GUTTMAN J D. Strand Space: Proving Security Protocols Correct[J]. Journal of Computer Security, 1999, 7(2-3): 191-230.
[4]	GUTTMAN J D, THAYER F J.Authentication Tests and the Structure of Bundles[J]. Theoretical Computer Science, 2002, 283(2): 333-380.
[5]	PERRIG A, SONG D.Looking for Diamonds in the Desert-extending Automatic Protocol Generation to Three-party Authentication and Key Agreement[C]//IEEE. The 13th IEEE Computer Security Foundations Workshop, July 3-5, 2000, Cambridge, England. New Jersey: IEEE, 2000: 64-76.
[6]	LIU Jiafen, ZHOU Mingtian.Overcome Limitation on Authentication Test[J]. Journal of Software, 2009, 20(10): 2799-2809.
	刘家芬,周明天. 突破认证测试方法的局限性[J]. 软件学报,2009,20(10):2799-2809.
[7]	GUTTMAN J D.State and Progress in Strand Spaces: Proving Fair Exchange[J]. Journal of Automated Reasoning, 2012, 48(2): 159-195.
[8]	YU Lei, Wei Shimin.Aaylysis on Propertions for Principals Keys on Construction of Test Componment[J]. Computer Enginerring and Applications, 2013, 49(6): 114-117.
	余磊,魏仕民,卓泽朋. 协议主体密钥在测试组件和构造上的性质分析[J]. 计算机工程与应用,2013,49(6):114-117.
[9]	MUHAMMAD S.Applying Authentication Tests to Discover Man-in-the-middle Attack in Security Protocols[C]//IEEE. 8th International Conference on Digital Information Management, September 10-12, 2013, Islamabad, Pakistan. New Jersey: IEEE, 2013: 35-40.
[10]	XIONG Ling, PENG Daiyuan.An Improved Authentication Test for Security Protocol Analysis[J]. Communications Technology, 2014, 47(8): 951-954.
	熊玲,彭代渊. 一种改进的安全协议认证测试分析方法[J].通信技术,2014,47(8):951-954.
[11]	RAMSDELL J D, DOUGHERTY D J, GUTTMAN J D, et al.A Hybrid Analysis for Security Protocols with State[C]//Springer. 2014 International Conference on Integrated Formal Methods, September 9-11, 2014, Bertinoro, Italy. Heidelberg: Springer, 2014: 272-278.
[12]	SONG Weitao, HU Bin.One Strong Authentication Test Suitable for Analysis of Nested Encryption Protocols[J]. Computer Science, 2015, 42(1): 149-169.
	宋巍涛,胡斌. 一种适用于嵌套加密协议分析的强认证测试方法[J]. 计算机科学,2015,42(1):149-169.
[13]	FENG Wei, FENG Dengguo.Analyzing Trusted Computing Protocol Based on the Strand Spaces Model[J]. Chinese Journal of Computers, 2015, 38(4): 701-716.
	冯伟,冯登国. 基于串空间的可信计算协议分析[J]. 计算机学报,2015,38(4):701-716.
[14]	LIU Jiafen.Automatic Verification of Security Protolcols with Strand Space Theory[J]. Journal of Computers Applications, 2015, 35(7): 1870-1876.
	刘家芬. 基于串空间理论的安全协议自动验证[J]. 计算机应用,2015,35(7):1870-1876.
[15]	YU Lei, WEI Shimin, JIANG Mingming.Formal Analysis Method of Security Protocol Based on Correlation Degree of Principals[J]. Netinfo Security, 2018, 19(6): 45-51.
	余磊,魏仕民,江明明. 基于主体关联度的安全协议形式化分析方法[J]. 信息网络安全,2018,19(6):45-51.
[16]	YUAN Boao, LIU Jun, ZHOU Haigang.Study and Development on Cryptographic Protocol[J]. Journal of Military Communications Technology, 2017, 38(1): 90-94.
	苑博奥,刘军,周海刚. 密码协义研究与发展[J]. 军事通信技术,2017,38(1):90-94.
[17]	ZHANG Huanguo, WU Fusheng, WANG Houzhen, et al.A Survey: Security Verification Analysis of Cryptographic Protocols Implementations on Real Code[J]. Chinese Journal of Computers, 2017, 40(2): 288-308.
	张焕国,吴福生,王后珍,等. 密码协议代码执行的安全验证分析综述[J]. 计算机学报,2017,40(2):288-308.
[18]	YI Huifan, WAN Liang, HUANG Nana, et al.Research on Attacker Modeling Method of Security Protocol Based on SPIN[J]. Netinfo Security, 2018, 19(2): 61-70.
	易辉凡,万良,黄娜娜,等. 基于SPIN的安全协议的攻击者建模方法研究[J]. 信息网络安全,2018,19(2):61-70.

符号	意义
A, B	主体
A, B	主体A与主体B的身份信息
KA	主体A的公钥
KA^-1	主体A的私钥
Kab	主体A与主体B之间的共享密钥
Kas	主体A与主体S之间的共享密钥
Kbs	主体B与主体S之间的共享密钥
N_a, N_b	主体A与主体B产生的随机数
K_sym	对称密钥集合
{M}_K	使用密钥K对消息M加密形成的消息
I(A)	攻击者假冒主体A
Data	组件类型为数据
Identity	组件类型为身份标识
Nonce	组件类型为随机数
P	攻击者所有可能获知的消息集合
?_c	丛c上的偏序关系
n⇒⁺n′	点n到n′的边,n, n′不一定相邻

一种改进的基于认证测试的形式化分析方法

An Improved Formal Analysis Method Based on Authentication Tests

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 7

参考文献 18

相关文章 10

编辑推荐

Metrics

本文评价

[1]	姚萌萌, 唐黎, 凌永兴, 肖卫东. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.
[2]	韦永霜, 陈建华, 韦永美. 基于椭圆曲线密码的RFID/NFC安全认证协议[J]. 信息网络安全, 2019, 19(12): 64-71.
[3]	余磊, 魏仕民, 江明明. 基于主体关联度的安全协议形式化分析方法[J]. 信息网络安全, 2018, 18(6): 45-51.
[4]	易辉凡, 万良, 黄娜娜, 王鹍鹏. 基于SPIN的安全协议的攻击者建模方法研究[J]. 信息网络安全, 2018, 18(2): 61-70.
[5]	杨元原, 陆臻, 顾健. RFID安全协议追踪攻击的形式化分析[J]. 信息网络安全, 2015, 15(9): 25-28.
[6]	张蕾，郑飞. 无线局域网安全协议的分析和研究[J]. 信息网络安全, 2014, 14(9): 132-137.
[7]	刘宇靓;任伟. 基于通用可组合理论的协议安全性证明方法讨论[J]. , 2012, 12(6): 0-0.
[8]	铁玲;易勇;何迪. 多跳快速切换代理移动IPv6预认证协议的安全分析[J]. , 2012, 12(6): 0-0.
[9]	刘磊;周庆;井蔚;刘冰. 基于多核处理器的网络安全协议并行处理研究[J]. , 2011, 11(9): 0-0.
[10]	刘明华;任志考;董洪灿. 基于Web安全的电子商务安全模型研究[J]. , 2009, 9(4): 0-0.