Authentication Testing of Security Protocols-A Method for Testing Protocol Security Properties
HE Yun-hua1,2, YANG Chao1, ZHANG Jun-wei1, MA Jian-feng1
1. Key Laboratory of Computer Network and Information Security of Ministry of Education, Xidian University, Xi'an, Shaanxi 710071, China;
2. Department of Information Security, College of Computer Science, North China University of Technology, Beijing 100029, China
Authentication builds the trust relationship between communication parties,which is a magnitude guarantee for secure communications.However,existing protocol testing techniques focus on validating the protocol specification.Those techniques can not satisfy the requirements of testing protocol authentication as their lack of the method for describing security properties.Therefore,a protocol security property testing method is proposed for testing protocol authentication.This testing method uses a new formal model-Symbolic Parameterized Goal Extended Finite State Machine (SPG-EFSM) for describing protocols and their security properties.Then,a protocol attack algorithm is designed for testing protocol authentication based on different attack scenarios.Through test experiments on the well-known protocol Woo-lam and μ TESLA,it is found that the SPG-EFSM based attack algorithm can find several protocol security flaws and has better feasibility and high coverage.
[1] 周彦伟,杨波,张文政.异构无线网络可控匿名漫游认证协议[J].电子学报,2016,44(5):1117-1123. ZHOU Yan-wei,YANG Bo,ZHANG Wen-zheng.Controllable and anonymous roaming protocol for heterogeneous wireless network[J].Acta Electronica Sinica,2016,44(5):1117-1123.(in Chinese)
[2] Dalal Alrajeh,Jeff Kramer,Alessandra Russo,et al.Elaborating requirements using model checking and inductive learning[J].IEEE Transactions on Software Engineering,2013,39(3):361-383.
[3] 李顺东,杨坤伟,巩林明,等.标准模型下可公开验证的匿名IBE方案[J].电子学报,2016,44(3):673-678. LI Shun-dong,YANG Kun-wei,GONG Lin-ming,et al.A publicly verifiable anonymous IBE scheme in the standard model[J].Acta Electronica Sinica,2016,44(3):673-678.(in Chinese)
[4] Wen Tang,Sui Ai-Fen,Wolfgang Schmid.A model guided security vulnerability discovery approach for network protocol implementation[A].Proceedings of the 13th International Conference on Communication Technology[C].Beijing,China:IEEE,2011.675-680.
[5] Andrea Arcuri,Muhammad Zohaib Iqbal,Lionel Briand.Random testing:theoretical results and practical implications[J].IEEE Transactions on Software Engineering,2012,38(2):258-277.
[6] G Fraser,A Arcuri.Whole test suite generation[J].IEEE Transactions on Software Engineering,2013,39(2):276-291.
[7] Oulu University Secure Programming Group.PROTOS:Security Testing of Protocol Implementation[OL].http://www.ee.oulu.fi/research/ouspg/protos/index.html,2012-06-12.
[8] Tal O,Knight S,Dean T.Syntax-based vulnerability testing of frame-based network protocols[A]. Proceedings of the 21nd Conference on Privacy,Security and Trust[C].Fredericton:IEEE,2004.13-15.
[9] Jing C,Wang Z,Yin X,et al.Mutation testing of protocol messages based on extended TTCN-3[A].Proceedings of the 22nd International Conference on Advanced Information Networking and Applications[C].Okinawa:IEEE,2008.667-674.
[10] Fabian Yamaguchi,Nico Golde,Daniel Arp,et al.Modeling and discovering vulnerabilities with code property graphs[A].Proceedings of IEEE Symposium on Security and Privacy[C].San Jose:IEEE,2014.590-604.
[11] Gali Mashtizadeh,Andrea Bittau,Dan Boneh,et al.CCFI:cryptographically enforced control flow integrity[A].Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security[C].New York:ACM,2015.941-951.
[12] Shu G,Lee G.Formal methods and tools for testing communication protocol system security[D].Ohio,USA:Ohio State University,2008.
[13] Dolev D,Yao A.On the security of public-key protocols[J].IEEE Transaction on Information Theory,1983,29(2):198-208.
[14] Woo T,Lam S.Authentication for distributed systems[J].ACM Transactions on Computer Systems,1992,25(1):35-39.
[15] Perrig A,Szewczyk R,et al.SPINS:Security protocols for sensor networks[J].Wireless Networks,2002,8(5):521-534.
[16] Wenbo Mao.Modern Cryptography:Theory and Practice[M].New Jersey,USA:Prentice Hall,2004.
2016, Vol. 44 
