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

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

Previous Articles Next Articles

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 Online:2013-09-15
Contact: 刘波,E-mail:liubo@is.iscas.ac.cn

Abstract

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

CLC Number:

TP309

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

References

[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.

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

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 5

Recommended Articles

Metrics

Comments

[1]	TAN Tunzi, GAO Suixiang, YANG Wenguo. Determining the connectedness of an undirected graph [J]. , 2018, 35(5): 582-588.
[2]	GAO Yan-Yan, LI Xi, ZHOU Xue-Hai. Verification of the L4 IPC implementation [J]. , 2011, 28(6): 786-792.
[3]	LIU XiuYing, ZHANG YuQing, YANG Bo, XING Ge. Running-Mode Analysis of the Three-Party Cryptographic Protocol [J]. , 2004, 21(3): 380-385.
[4]	LIU Yi-Wen, LI Wei-Qin. Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces [J]. , 2002, 19(3): 288-294.
[5]	FAN Hong, FENG Deng-Guo. A Mixed Formal Analysis Technology of Security Protocols [J]. , 2002, 19(3): 240-245.