Modular rewriting system based on method for intruder deduction
Jing Wang · Jisuanji yingyong yanjiu · 2011
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.