一种基于项重写的密码模块API安全性检测算法

doi:10.7523/j.issn.2095-6134.2013.05.020

中国科学院大学学报 ›› 2013, Vol. 30 ›› Issue (5): 699-705.DOI: 10.7523/j.issn.2095-6134.2013.05.020

一种基于项重写的密码模块API安全性检测算法

刘波^1,2, 陈华¹

1. 中国科学院软件研究所, 北京 100080;
2. 中国科学院大学, 北京 100049

收稿日期:2012-11-01 修回日期:2012-12-24 发布日期:2013-09-15
基金资助:
国家自然科学基金(91118006)资助 

A security analysis algorithm for cryptographic module API using term rewriting system

LIU Bo^1,2, CHEN Hua¹

1. Institute of Software, Chinese Academy of Sciences, Beijing 100080, China;
2. University of Chinese Academy of Sciences, Beijing 100049, China

Received:2012-11-01 Revised:2012-12-24 Published:2013-09-15
Contact: 刘波,E-mail:liubo@is.iscas.ac.cn

摘要/Abstract

摘要： 针对密码模块API的形式化验证,提出一种基于项重写形式化模型的检测算法. 该算法利用符号化及广度优先搜索方法,使用项重写规则对敌手的初始知识集不断进行匹配和扩展,直到找到攻击路径或者搜索完状态空间. 以密码模块API标准PKCS#11为例具体实现了该检测算法,通过5个实验完成了对PKCS#11对称密钥管理部分API的形式化验证. 实验结果表明,该方法能有效检测针对PKCS#11的攻击,并找到一个新的攻击序列.

关键词: PKCS#11, 模型检测, 项重写, 广度优先搜索

Abstract: For the formal verification of the cryptographic module API, a security analysis algorithm using term rewriting system was proposed. The term rewriting rules were used to extend the intruder's knowledge with breadth-first search and symbolic method. The search will stop until an attack path has been found or all the finite state space has been searched. The algorithm was applied to PKCS#11 which is an API standard for the cryptographic module, and five experiments were performed to complete the formal verification of the symmetric key management API commands of PKCS#11. The experimental results showed that the algorithm detected the attacks against PKCS#11 precisely and effectively, and also a new API attack sequence was discovered.

Key words: PKCS#11, model checking, term rewriting, breadth-first search

中图分类号:

TP309

刘波, 陈华. 一种基于项重写的密码模块API安全性检测算法[J]. 中国科学院大学学报, 2013, 30(5): 699-705.

LIU Bo, CHEN Hua. A security analysis algorithm for cryptographic module API using term rewriting system[J]. , 2013, 30(5): 699-705.

参考文献

[1] National Institute of Standards and Technology. Federal information processing standards publication 140-2: security requirements for cryptographic modules.
[2] Anderson R. The correctness of crypto transaction sets[C]//8th International Workshop on Security Protocols. Cambridge, UK: Springer, 2001:125-127.
[3] Bond M, Anderson R. API level attacks on embedded systems[J].IEEE Computer Magazine, 2001,34(10): 67-75.
[4] Bond M. Understanding security APIs[D].Cambridge,UK: University of Cambridge, 2004.
[5] Herzog J. Applying protocol analysis to security device interfaces[J]. IEEE Security & Privacy Magazine,2006,4(4):84-87.
[6] Delaune S, Kremer S, Steel G. Formal analysis of PKCS#11[C]//Proceedings of the 21st IEEE Computer Security Foundations Symposium. Pittsburgh,USA:IEEE Computer Society Press,2008:331-334.
[7] RSA Security Inc. PKCS#11: cryptographic token interface standard[S]. v2.20.
[8] Dolev D, Yao A.On the security of public key protocols[J].IEEE Transactions in Information Theory,1983,2(29):198-208.
[9] Durgin N, Lincon P, Mitchell J. Multiset rewriting and the complexity of bounded security protocols[J].Journal of Computer Security,2004,12(2):247-311.
[10] Holzmann G. The model checker SPIN[J].Transactions of Software Engineering,1997,23(5):279-295.
[11] Climatti A, Clarke E, Giunchiglia E, et al. NuSMV version 2: An open source tool for symbolic model checking[C]//Proceedings of International Conference on Computer-Aided Verification.Copenhagen,Denmark:Springer,2002:359-364.
[12] Basin D, Mödersheim S, Viganò L. OFMC: A symbolic model-checker for security protocols[J]. International Journal of Information Security, 2005, 4(3): 181-208.
[13] Armando A, Compagna L. SATMC: a SAT-based model checker for security protocols[C]//Proceedings of the 9th European Conference in Logics in Artificial Intelligence. Heidelberg, Germany:Springer, 2004: 730-733.
[14] Turuani M. The CL-atse protocol analyser[C]//Proceedings of Rewriting Techniques and Applications. Heidelberg, Germany: Springer, 2006: 277-286.
[15] Clulow J. On the security of PKCS#11[C]//Proceedings of the 5th International Workshop on Cryptographic Hardware and Embedded Systems. Cologne, Germany: Springer, 2003:411-425.

一种基于项重写的密码模块API安全性检测算法

A security analysis algorithm for cryptographic module API using term rewriting system

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

本文评价

访问统计

联系我们

[1]	谭屯子, 高随祥, 杨文国. 判断一个无向图是否连通图的方法[J]. 中国科学院大学学报, 2018, 35(5): 582-588.
[2]	高妍妍, 李曦, 周学海. L4进程间通信机制的模型检测方法[J]. 中国科学院大学学报, 2011, 28(6): 786-792.
[3]	刘秀英, 张玉清, 杨波, 邢戈. 三方密码协议运行模式分析法[J]. 中国科学院大学学报, 2004, 21(3): 380-385.
[4]	范红, 冯登国. 一种混合的安全协议形式化分析技术[J]. 中国科学院大学学报, 2002, 19(3): 240-245.