Modular rewriting system based on method for intruder deduction
一种基于模重写系统的攻击者推理方法

To solve the operability of intruder deduction modulo equational theories in formal verification of cryptographic protocols, a modular rewriting system based method for intruder deduction is presented. The method establish over an instance of combined theories is composed of a set of directional rewriting rules, which can be used as a TRS and a set of nondirectional equations that can be used as an modular theories. By the definition of modulo rewriting relation induced by the instance of combined theories, the two part are transformed into a modular rewriting system, which provide 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.