%0 Journal Article
%T Modular rewriting system based on method for intruder deduction<br>一种基于模重写系统的攻击者推理方法
%A LI Da-hai
%A HAN Ji-hong
%A WANG Ya-di
%A WANG Jing
%A <br>李大海
%A 韩继红
%A 王亚弟
%A 王静
%J 计算机应用研究
%D 2011
%I 
%X 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.
%K security protocol
%K equational theory
%K algebraic properties
%K modular rewriting system<br>安全协议
%K 等式理论
%K 代数特性
%K 模重写系统
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=BB4671B0871FE9EFB7606DE7C26C0567&yid=9377ED8094509821&vid=D3E34374A0D77D7F&iid=94C357A881DFC066&sid=7F4621C62254E923&eid=8827E7669C34610F&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=9