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

doi:10.3969/j.issn.1001-2400.2012.04.022

J4 ›› 2012, Vol. 39 ›› Issue (4): 120-125+183.doi: 10.3969/j.issn.1001-2400.2012.04.022

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

杨元原^1,2;马文平¹;刘维博¹;俞优²;顾健²

(1. 西安电子科技大学综合业务网理论及关键技术国家重点实验室，陕西西安 710071；
2. 公安部第3研究所, 上海 200031)

收稿日期:2011-04-29 出版日期:2012-08-20 发布日期:2012-10-08
通讯作者: 杨元原
作者简介:杨元原(1981-)，男，西安电子科技大学博士研究生，E-mail: yangyy@mail.xidian.edu.cn．
基金资助:
国家自然科学基金资助项目(61072140);高等学校创新引智计划资助项目(B08038);高等学校博士学科点专项科研基金资助项目(20100203110003);陕西省教育厅科研计划资助项目(2010JK825)

Automatic detection of security protocols with XOR

YANG Yuanyuan^1,2;MA Wenping¹;LIU Weibo¹;YU You²;GU Jian²

(1. State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071， China;
2. The Third Research Inst. of Ministry of Public Security, Shanghai 200031， China)

Received:2011-04-29 Online:2012-08-20 Published:2012-10-08
Contact: YANG Yuanyuan

摘要/Abstract

摘要：

针对当前模型检测工具普遍不能检测带有异或运算安全协议的问题，提出了一个新的模型检测器SAT＃．该模型检测器通过引入抽象异或项的概念及其运算规则，大大降低了攻击者生成的异或消息数量，解决了由于引入传统异或运算导致的状态空间爆炸问题．在此基础上，通过在SAT模型中增加基于抽象异或项的重写规则，扩展了攻击者的异或运算能力，实现了对带有异或运算安全协议的自动化检测．通过对BULL协议的检测，证明了抽象异或项的实用性，同时也证明了SAT＃模型检测器的可靠性．

关键词: 安全协议, 形式化分析, 模型检测, 代数性质

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

中图分类号:

TP 393.08

杨元原;马文平;刘维博;俞优;顾健. 带有异或运算安全协议的自动化检测[J]. J4, 2012, 39(4): 120-125+183.

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.

参考文献

［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]	沈利香,慕德俊,曹国,谢光前,束方勇. 针对硬件木马的形式化验证模型构造方法[J]. 西安电子科技大学学报, 2021, 48(3): 146-153.
[2]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[3]	陈矗. RFCcertDT:SSL/TLS中证书验证的测试工具[J]. 西安电子科技大学学报, 2019, 46(3): 20-25.
[4]	丁明,张书玲,张琛,张军. 一种航空电子系统安全性需求验证方法[J]. 西安电子科技大学学报, 2019, 46(3): 66-73.
[5]	段钊, 刘锟龙. 采用CPAChecker的动态程序验证[J]. 西安电子科技大学学报, 2019, 46(1): 33-38.
[6]	刘佼;孙聪;马建峰;焦政达. 采用可信平台度量的车辆远程诊断授权协议[J]. 西安电子科技大学学报, 2017, 44(3): 49-54+119.
[7]	毛立强;黄影. MANET安全路由协议自动化分析[J]. 西安电子科技大学学报, 2016, 43(6): 56-61.
[8]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.
[9]	杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.
[10]	张志勇1;2;裴庆祺1;杨林3;马建峰1. 支持验证代理方的远程证明模型及其安全协议 [J]. J4, 2009, 36(1): 58-63.
[11]	毛立强1;马建峰1;2. 可证明安全的MANET按需距离矢量路由协议分析 [J]. J4, 2008, 35(6): 1063-1068.
[12]	铁满霞1;2;李建东1;2;王育民1. WAPI证书鉴别协议的改进及性能分析 [J]. J4, 2007, 34(7): 1-4.
[13]	田海博(1);丁勇(2);王育民(1). 形式化攻击者能力描述的计算可靠性研究 [J]. J4, 2006, 33(5): 800-803.
[14]	慕建君. 一种形式化分析安全协议的新模型[J]. J4, 2006, 33(3): 381-385.
[15]	刘秀英1;2;张玉清2;杨波1;邢戈2. TMN协议的形式化分析[J]. J4, 2004, 31(5): 785-790.

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

Automatic detection of security protocols with XOR

PDF (PC)

赞

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 10