论文研究 一种基于模重写系统的攻击者推理方法.pdf

为了解决安全协议验证中攻击者模等式理论推理的可操作性问题，提出并设计了一种基于模重写系统的攻击者推理方法。该方法建立在一个反映两种密码原语代数特性的联合理论实例之上，由一组定向的重写规则和非定向的等式构成，前者进一步转换为项重写系统(term rewriting system，TRS)，而后者则转换为有限等价类理论，通过定义项间的模重写关系，使两者构成一个可以反映攻击者针对联合理论代数项操作能力的模重写系统。实例分析表明，该模型为攻击者模等式推理规则赋予了明确的操作语义，可以使攻击者达到对安全协议代数项规