一种基于形式化验证的差分故障分析方法

摘要

本发明公开了一种基于形式化验证的差分故障分析方法，首先建立密码算法故障效应传播模型；然后进行故障效应传播模型仿真测试；接下来进行故障效应特征属性提取；之后进行故障注入攻击；最后基于形式化验证的攻击分析再基于属性约束利用形式化验证工具筛选满足属性的密钥信息，该信息即为加密密钥。本发明基于形式化验证方法，分析时利用少量故障信息即可筛选出符合属性约束的加密密钥，同时也可以分析出故障发生的准确位置，实现故障攻击分析自动化。