带有异或运算安全协议的自动化检测

doi:10.3969/j.issn.1001-2400.2012.04.022

Abstract

Abstract:

Since most of the current model checking tools can not detect security protocols with XOR, a new model checker named SAT＃ is proposed. By defining the concept of abstract XOR term and its reduction rules, the new model greatly reduces the number of XOR messages produced by the intruder, and resolves the state space explosion problem resulting from the introduction of XOR operations, on the basis of which by adding the rewrite rules of XOR based on the abstract XOR term, the new model endows the intruder with the XOR operations, and thus is able to automatically detect the security protocols with XOR. The detection results of the BULL protocol show not only the practicality of the abstract XOR term but also the reliability of the SAT＃.

Key words: security protocols, formal analyses, model checking, algebraic properties

CLC Number:

TP 393.08

YANG Yuanyuan;MA Wenping;LIU Weibo;YU You;GU Jian. Automatic detection of security protocols with XOR[J].J4, 2012, 39(4): 120-125+183.

References

［1］ Veronique C, Steve K, Bogdan W. A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems［J］. Journal of Automated Reasoning, 2011, 46(3-4): 225-259.
［2］ Vincent C, Hubert C, Stephanie D. Automating Security Analysis: Symbolic Equivalence of Constraint Systems［C］//The 5th International Joint Conference on Automated Reasoning. Wroclaw: Springer, 2010: 412-426.
［3］ Stephanie D, Steve K, Mark D R. Symbolic Bisimulation for the Applied pi Calculus［J］. Journal of Computer Security, 2010, 18(2): 317-377.
［4］ Chevalier Y, Küsters R, Rusinowitch M, et al. An NP Decision Procedure for Protocol Insecurity with XOR［J］. Theoretical Computer Science, 2005, 338(1-3): 247-274.
［5］ Ralf K, Tomasz T. On the Automatic Analysis of Recursive Security Protocols with XOR［C］//24th Annual Symposium on Theoretical Aspects of Computer Science. Aachen: Springer, 2007: 646-657.
［6］ Veronique C, Gavin K, Graham S. Automatic Analysis of the Security of XOR-Based Key Management Schemes［C］//13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Braga: Springer, 2007: 538-552.
［7］ Ralf K, Tomasz T. Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach［C］//15th ACM Conference on Computer and Communications Security. Alexandria: ACM, 2008: 129-138.
［8］ Alessandro A, Luca C. SAT-based Model-checking for Security Protocols Analysis［J］. International Journal of Information Security, 2008, 7(1): 3-32.
［9］ Marques-Silva J P, Sakallah K A. GRASP—a Search Algorithm for Propositional Satisfiability［J］. IEEE Trans on Computers, 1999, 48(5): 506-521.
［10］杜志强, 沈玉龙, 马建峰, 等. 一种实用的传感器网络广播认证协议［J］. 西安电子科技大学学报, 2010, 37(2): 305-310.
Du Zhiqiang, Shen Yulong, Ma Jianfeng, et al. Practical Broadcast Authentication Protocol for Sensor Networks［J］. Journal of Xidian University, 2010, 37(2): 305-310.

[1]	SHEN Lixiang,MU Dejun,CAO Guo,XIE Guangqian,SHU Fangyong. Constructing formal verification models for hardware Trojans [J]. Journal of Xidian University, 2021, 48(3): 146-153.
[2]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[3]	DING Ming,ZHANG Shuling,ZHANG Chen,Zhang Jun. Method for the verification of safety requirements of avionics systems [J]. Journal of Xidian University, 2019, 46(3): 66-73.
[4]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[5]	PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic [J]. J4, 2014, 41(2): 79-84.
[6]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[7]	ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic [J]. J4, 2009, 36(2): 338-342.
[8]	ZHANG Hai-bin;DUANG Zhen-hua. Model checking multirate hybrid systems [J]. J4, 2008, 35(1): 60-648.
[9]	GUO Jian1;JIN Nai-yong2. Vacuity detection in computation temperal logic [J]. J4, 2007, 34(5): 794-799.
[10]	ZHANG Hai-bin;DUAN Zhen-hua. Decidability of the dense timed interval temporal logic [J]. J4, 2007, 34(3): 463-467.
[11]	TIAN Hai-bo(1);DING Yong(2);WANG Yu-min(1). Research on computational soundness of formal attacker ability description [J]. J4, 2006, 33(5): 800-803.
[12]	LIU Xiu-ying1;2;ZHANG Yu-qing2;YANG Bo1;XING Ge2. An approach to the formal analysis of the TMN protocol [J]. J4, 2004, 31(5): 785-790.

Automatic detection of security protocols with XOR

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 12

Metrics

Comments

Recommended 10