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

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

作　　者：刘波[1,2] 陈华[1] 

机构地区：[1]中国科学院软件研究所,北京100080 [2]中国科学院大学,北京100049

出　　处：《中国科学院大学学报（中英文）》2013年第5期699-705,共7页Journal of University of Chinese Academy of Sciences

基　　金：国家自然科学基金(91118006)资助

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

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]