针对密码模块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.