一种基于模重写系统的攻击者推理方法

摘要

To solve the operability of intruder deduction modulo equational theories in formal verification of cryptographic protocols, this paper presented a modular rewriting system based method for intruder deduction.The method established over an instance of combined theories was composed of a set of directional rewriting rules, which could be used as a TRS and a set of nondirectional equations that could be used as an modular theories.By the definition of modulo rewriting relation induced by the instance of combined theories, transformed the two part into a modular rewriting system, which provided the intruder with the ability to operate algebraic terms.The analysis of the example shows that the model endues the intruder deduction modulo equational theories with clear operability to term specification and deduction.%为了解决安全协议验证中攻击者模等式理论推理的可操作性问题,提出并设计了一种基于模重写系统的攻击者推理方法.该方法建立在一个反映两种密码原语代数特性的联合理论实例之上,由一组定向的重写规则和非定向的等式构成,前者进一步转换为项重写系统(term rewriting system,TRS),而后者则转换为有限等价类理论,通过定义项间的模重写关系,使两者构成一个可以反映攻击者针对联合理论代数项操作能力的模重写系统.实例分析表明,该模型为攻击者模等式推理规则赋予了明确的操作语义,可以使攻击者达到对安全协议代数项规约、推理的目的.