形式化攻击者能力描述的计算可靠性研究

研究在安全协议仅使用数据完整性算法时，形式化分析方法中形式化攻击者能力描述的计算可靠性，首先假设计算性攻击者的能力超过形式化攻击者的能力，然后构造攻击实验，进而论证攻击实验中计算攻击者的输出与签名算法或密钥杂凑函数的安全定义相矛盾。因此得出计算性攻击者所能生成的消息均属于形式化攻击者所能生成的消息闭集这一结论，基于该结论，可以构建或者改进形式化分析系统，使其具有计算可靠性。