基于串空间理论的安全协议自动验证

doi:10.11772/j.issn.1001-9081.2015.07.1870

计算机应用 ›› 2015, Vol. 35 ›› Issue (7): 1870-1876.DOI: 10.11772/j.issn.1001-9081.2015.07.1870

基于串空间理论的安全协议自动验证

刘家芬^1,2

1. 西南财经大学经济信息工程学院, 成都 610054;
2. 西南财经大学四川省金融智能与金融工程重点实验室, 成都 610054

收稿日期:2015-01-30 修回日期:2015-03-26 出版日期:2015-07-10 发布日期:2015-07-17
通讯作者: 刘家芬(1980-),女,湖北荆州人,副教授,博士,CCF高级会员,主要研究方向:信息安全、智能信息处理,jfliu@swufe.edu.cn
基金资助:
国家自然科学基金重大项目(91218301);国家自然科学基金青年项目(60903201);中央高校基本科研业务费研究项目(JBK20505, JBK140129)。

Automatic verification of security protocols with strand space theory

LIU Jiafen^1,2

1. School of Economic Information Engineering, Southwestern University of Finance and Economics, Chengdu Sichuan 610054, China;
2. Key Laboratory of Financial Intelligence and Financial Engineering of Sichuan, Southwestern University of Finance and Economics, Chengdu Sichuan 610054, China

Received:2015-01-30 Revised:2015-03-26 Online:2015-07-10 Published:2015-07-17

摘要/Abstract

摘要：

针对目前串空间理论依赖分析人员主观判断、无法使用自动化工具进行验证的问题,提出了基于串空间理论的协议认证属性标准化验证过程。首先为协议消息项定义类型标签,对串空间及认证测试理论进行扩展;然后通过判断测试元素出现位置、检验测试元素参数一致性、确认变换进行边唯一存在性和检验目标串参数一致性,将基于串空间理论的协议验证过程标准化为可程序实现的步骤。该算法的时间复杂度为O(n²),避免了模型检测方法的状态空间爆炸问题,并在此基础上实现了安全协议认证属性的自动化验证工具。以BAN-Yahalom协议和TLS 1.0握手协议为例进行了标准化的分析验证,找到了对BAN-Yahalom协议的一种新攻击形式。该攻击无需限制服务器对随机数的检查,比Syverson发现的攻击更具普遍性。

关键词: 串空间, 认证测试, 安全协议, 自动化验证, 认证属性, BAN-Yahalom协议, 安全传输层握手协议

Abstract:

Strand space theory relies on individual judgments and subjective experiences much, and can hardly be automated. To solve this problem, a more formal and objective verification process based on strand space theory and authentication test was proposed. First, a set of type labels was defined for terms of protocol to expand strand space and authentication test theory. By listing all possible occurrences of test instances, checking agreement of arguments in test component, verifying uniqueness of transforming edge, examining agreement of arguments in goal strand, protocols verification process based on strand space could be formalized to a series of programmable procedures. Time complexity of the whole verification algorithm is O(n²), hence state space explosion problem common in state space search was avoided. On the basis of theoretical study, an automatic tool was implemented to verify authentication attributes of security protocols automatically. BAN-Yahalom protocol and TLS handshake protocol 1.0 were analyzed as examples, where a new attack to BAN-Yahalom was found. It is similar to Syverson's attack, but it has no restriction on server's verification of nonce, hence has more general application scenario than Syverson's.

Key words: strand space, authentication test, security protocol, automatic verification, authentication property, BAN-Yahalom protocol, Transport Layer Security (TLS) handshake protocol

中图分类号:

TP309.7

刘家芬. 基于串空间理论的安全协议自动验证[J]. 计算机应用, 2015, 35(7): 1870-1876.

LIU Jiafen. Automatic verification of security protocols with strand space theory[J]. Journal of Computer Applications, 2015, 35(7): 1870-1876.

参考文献

[1] THAYER FABREGA F J, HERZOG J C, GUTTMAN J D. Strand space: why is a security protocol correct [C]// Proceedings of the 1998 IEEE Symposium on Security and Privacy. Piscataway: IEEE, 1998: 160-171.
[2] THAYER FABREGA F J, HERZOG J C, GUTTMAN J D. Honest ideals on strand space [C]// Proceedings of the 11th IEEE Computer Security Foundations Workshop. Piscataway: IEEE, 1998: 66-77.
[3] THAYER FABREGA F J, 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 FABREGA F J. Key compromise, strand spaces and the authentication tests [J]. Electronic Notes in Theoretical Computer Science, 2001, 45: 1-21.
[5] GUTTMAN J D, THAYER FABREGA F J. Authentication tests and the structure of bundles [J]. Theoretical Computer Science, 2002, 283(2): 333-380.
[6] MUHAMMAD S. Applying authentication tests to discover Man-In-The-Middle attack in security protocols [C]// Proceedings of the 8th International Conference on Digital Information Management. Piscataway: IEEE, 2013: 35-40.
[7] ZHANG G, RONG M, FANG Y. One extension of authentication test based on strand space model [C]// Proceedings of the 5th International Conference on Wireless Communications, Networking and Mobile Computing. Piscataway: IEEE, 2009: 1-4.
[8] XIONG L, PENG D. An improved authentication test for security protocol analysis [J]. Communications Technology, 2014, 47(8): 951-954.(熊玲,彭代渊.一种改进的安全协议认证测试分析方法[J].通信技术,2014,47(8):951-954.)
[9] YAN L, PENG D, GAO Y. Analysis and improvement of sensor networks security protocol [J]. Journal on Communications, 2011, 32(5): 139-144.(闫丽丽,彭代渊,高悦翔.传感器网络安全协议的分析和改进[J].通信学报,2011,32(5):139-144.)
[10] GUTTMAN J D. Security protocol design via authentication tests [C]// Proceedings of the 2002 IEEE Computer Security Foundations Workshop. Washington, DC: IEEE Computer Society, 2002: 92-103.
[11] GUTTMAN J D. Cryptographic protocol composition via the authentication tests [C]// FOSSACS'09: Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software, LNCS 5504. Berlin: Springer, 2009: 303-317.
[12] LIU J, ZHOU M. Designing authentication protocols via authentication test [C]// Proceedings of the 2007 IEEE Symposium on Computers and Communications. Piscataway: IEEE, 2007: 475-480.
[13] LIU J, ZHOU M. Break through the limitation of authentication test [J]. Journal of Software, 2009, 20(10): 2799-2809.(刘家芬,周明天.突破认证测试的局限性[J].软件学报,2009,20(10):2799-2809.)
[14] SONG W. Limitations of authentication test in the analysis of multi-party security protocols [C]// Proceeding of the 2013 International Conference on Mechatronic Sciences, Electric Engineering and Computer. Piscataway: IEEE, 2013: 2243-2247.
[15] YU L, WEI S. Analysis on properties for principals' keys on construction of test components [J]. Computer Engineering and Applications, 2013, 49(6): 114-117.(余磊,魏仕民.协议主体密钥在测试组件构造上的性质分析[J].计算机工程与应用,2013,49(6):114-117.)
[16] DOGHMI S F, GUTTMAN J D, THAYER F. Completeness of the authentication test [C]// Proceedings of the 12th European Symposium on Research in Computer Security. Piscataway: IEEE, 2007: 106-121.
[17] FRÖSCHLE S. Adding branching to the strand space model [J]. Electronic Notes in Theoretical Computer Science, 2009, 242(1): 139-159.
[18] GUTTMAN J D. Security goals and protocol transformations [C]// TOSCA'11: Proceedings of the 2011 International Conference on Theory of Security and Applications, LNCS 6993. Berlin: Springer, 2011: 130-147.
[19] GUTTMAN J D. State and progress in strand spaces: proving fair exchange [J]. Journal of Automated Reasoning, 2012, 48(2): 159-195.
[20] BODEI C, DEGANO P, GAO H, et al. Detecting and preventing type flaws: a control flow analysis with tags [J]. Electronic Notes in Theoretical Computer Science, 2007, 194(1): 3-22.
[21] BURROWS M, ABADI M, NEEDHAM R. A logic of authentica-tion [J]. ACM Transactions on Computer Systems, 1989, 8(1): 18-36.
[22] SYVERSON P. A taxonomy of replay attacks [C]// Proceeding of the 7th IEEE Computer Security Foundations Workshop. Piscataway: IEEE, 1994: 187-191.
[23] DIERKS T, ALLEN C. The TLS Protocol Version 1.0, RFC 2246 [S/OL]. [2014-12-23]. http://www.ietf.org/rfc/rfc2246.txt.
[24] WANG D, WANG P, LEI M. Cryptanalysis and improvement of gateway-oriented password authenticated key exchange protocol based on RSA [J]. Acta Electronica Sinica, 2015, 43(1): 176-184.(汪定,王平,雷鸣.基于RSA的网关口令认证密钥交换协议安全性分析与改进[J].电子学报,2015,43(1):176-184.)

基于串空间理论的安全协议自动验证

Automatic verification of security protocols with strand space theory

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	肖跃雷, 邓小凡. 基于证书的有线局域网安全关联方案改进与分析[J]. 计算机应用, 2021, 41(7): 1970-1976.
[2]	肖跃雷, 武君胜, 朱志祥. 基于预共享密钥的LAN安全关联方案改进与分析[J]. 计算机应用, 2018, 38(11): 3246-3251.
[3]	董海韬, 田静, 杨军, 叶晓舟, 宋磊. 适用于网络内容审计的SSL/TLS保密数据高效明文采集方法[J]. 计算机应用, 2015, 35(10): 2891-2895.
[4]	林瑞钟诚华蓓. 隐私保护的一站多表跨多表频繁项集挖掘[J]. 计算机应用, 2013, 33(12): 3437-3440.
[5]	周星刘军董春冻张玉静. 对辅助定位按需路由协议的安全性改进[J]. 计算机应用, 2013, 33(06): 1619-1629.
[6]	曹夕许力陈兰香. 云存储系统中数据完整性验证协议[J]. 计算机应用, 2012, 32(01): 8-12.
[7]	胡韬魏国珩. 基于低成本标签的RFID匿名双向认证协议[J]. 计算机应用, 2012, 32(01): 111-114.
[8]	杨建书吴尽昭周瑾. 基于CSP的OWL-S语义分析与建模[J]. 计算机应用, 2010, 30(8): 2173-2176.
[9]	邓帆邓少锋李益发. 应用组合方法设计安全协议[J]. 计算机应用, 2010, 30(4): 1033-1037.
[10]	田树华陈立佳李建茹. 基于Offline-TTP的电子支付协议公平性分析[J]. 计算机应用, 2009, 29(07): 1839-1843.
[11]	黎兴华雷新锋刘军. 一种时间相关安全协议的自动验证工具[J]. 计算机应用, 2009, 29(06): 1654-1658.
[12]	王新锋刘建国蒋旭刘胜利. 移动型RFID安全协议及其GNY逻辑分析[J]. 计算机应用, 2008, 28(9): 2239-2241.
[13]	杨帆吕庆聪曹奇英. 普适环境中一种安全协议的设计及分析[J]. 计算机应用, 2008, 28(7): 1802-1806.
[14]	吴开贵徐成廖振岚. IEEE 802.11i 协议的形式化分析[J]. 计算机应用, 2008, 28(5): 1125-1127.
[15]	方燕萍章晓芳张广泉. 串空间模型及其认证测试方法的一种扩展与应用[J]. 计算机应用, 2008, 28(12): 3205-3207.