Testing and proving security protocols

doi:10.3778/j.issn.1002-8331.2009.04.008

Computer Engineering and Applications ›› 2009, Vol. 45 ›› Issue (4): 26-29.DOI: 10.3778/j.issn.1002-8331.2009.04.008

• 博士论坛 • Previous Articles Next Articles

Testing and proving security protocols

QIAO Hai-yan

Zhongshan University，Guangzhou 510275，China

Received:2008-09-19 Revised:2008-11-10 Online:2009-02-01 Published:2009-02-01
Contact: QIAO Hai-yan

安全协议的测试与证明

乔海燕

中山大学，广州 510275

通讯作者: 乔海燕

Abstract

Abstract: It is shown how security protocols can be systematically tested，hence proved in Haskell.That is demonstrated by analyzing NS（Needham-Schroeder） and NSL（Needham-Schroeder-Lowe） protocols：runs of the protocols are formalized as event traces and properties on traces are tested.Complete runs of a protocol with a penetrator can be generated systematically，and properties of the protocol can be tested systematically.Lowe’s attack is easily revealed by testing NS protocol and authentication and secrecy are proved valid for NSL protocol by testing.

Key words: testing, Needham-Schroeder-Lowe（NSL） protocol, functional programming

摘要： 提出通过测试来证明安全协议的方法。以NS和NSL协议为例，首先将协议形式化为事件序列，协议的性质可以表示为序列上的性质。协议的完整运行可以系统地生成，因此，协议的性质可以系统地测试。形式化和测试在函数程序设计语言Haskell中完成。

关键词: 测试, Needham-Schroeder-Lowe协议, 函数程序设计

QIAO Hai-yan. Testing and proving security protocols[J]. Computer Engineering and Applications, 2009, 45(4): 26-29.

乔海燕. 安全协议的测试与证明[J]. 计算机工程与应用, 2009, 45(4): 26-29.

[1]	LI Duo, DONG Chaoqun, SI Pinchao, HE Man, LIU Qianchao. Survey of Research on Neural Network Verification and Testing Technology [J]. Computer Engineering and Applications, 2021, 57(22): 53-67.
[2]	WEI Danni, YANG Youlong, QIU Haiquan. Self-Training Algorithm Combining Density Peak and Cut Edge Weight [J]. Computer Engineering and Applications, 2021, 57(2): 70-76.
[3]	ZUO Kuo, LI Ning, TIAN Ying’ai, HOU Xia. Automatic Testing Method for Typesetting Effect of Reflowable Document [J]. Computer Engineering and Applications, 2021, 57(2): 273-278.
[4]	WU Xudong, TANG Qi, ZHANG Wei, ZHANG Jian, WEI Jibo, WANG Yijun. Research on SCA Compliance Testing Method Based on Extended Finite State Machine [J]. Computer Engineering and Applications, 2021, 57(16): 263-268.
[5]	TAN Lijuan, ZHENG Wei, LIU Youlin, FAN Xin, YANG Fengyu. Survey of Airborne Software Test and Verification Methods for Airworthiness Standards [J]. Computer Engineering and Applications, 2021, 57(15): 9-22.
[6]	LIU Youlin, ZHENG Wei, TAN Lijuan, FAN Xin, YANG Fengyu. Summary of Airborne Software Testing and Verification Tools for Airworthiness Standards [J]. Computer Engineering and Applications, 2021, 57(11): 1-10.
[7]	TANG Weijun, XU Kun, LIU Youquan, XIA Xuan. Method for Generating Three-Dimensional Point Cloud of Trees in Autonomous Vehicle Virtual Testing [J]. Computer Engineering and Applications, 2021, 57(11): 185-192.
[8]	MA Yuandong, LUO Zijiang, NI Zhaofeng, XU Bin, WU Fengjiao, SUN Shouyu, YANG Xiuzhang. Multi-target Detection Based on Improved SSD Algorithm [J]. Computer Engineering and Applications, 2020, 56(23): 23-30.
[9]	LIU Jialuo, YAO Yi, HUANG Song, HUI Zhanwei, CHEN Qiang, KOU Dalei, ZHANG Zhongwei. Metamorphic Testing Framework for Machine Learning Image Classification Program [J]. Computer Engineering and Applications, 2020, 56(17): 69-77.
[10]	WEI Qingjie1, LIU Shukun2. Method of Cross-Browser Compatibilities Testing for Web Application [J]. Computer Engineering and Applications, 2019, 55(5): 55-59.
[11]	MA Junyan, ZHANG Ying, LI Yi, WANG Jin, ZHANG Te. HA2：Hierarchical Anomaly Analysis Technology for IoT Sensing Device Firmware [J]. Computer Engineering and Applications, 2019, 55(22): 60-68.
[12]	YAO Yiwen, JIANG Shujuan, BO Lili. Survey of Mutation-Based Fault Location [J]. Computer Engineering and Applications, 2019, 55(20): 1-12.
[13]	LI Xiaowen, LI Yangyang, LEI Xiu. Research and Implementation of Authentication and Key Agreement Process in 5G Client [J]. Computer Engineering and Applications, 2019, 55(11): 35-39.
[14]	ZHU Shuqin, WANG Wenhong, LI Junqing. Designing a class of quadratic polynomial chaotic maps and their pseudo random number generator [J]. Computer Engineering and Applications, 2018, 54(9): 84-88.
[15]	ZHU Yi1，2, HUANG Zhiqiu1, ZHOU Hang1, LIU Linyuan1，3. Meta-modeling method for implementing template meta-programming of functional programming [J]. Computer Engineering and Applications, 2018, 54(7): 1-10.

Testing and proving security protocols

安全协议的测试与证明

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics