针对密码协议形式化分析中初始规则集过大且不易收敛的问题,给出一种基于先验知识集进行逻辑规则精简的方法。在初始规则迭代过程中,使用等价逻辑树理论进行规则集的蕴含和合一化处理,缩小初始规则集,并使形成的新的逻辑规则集具有与初始规则集等价的推导能力。
Aiming to solve the problem that the initial rule set in the formal analysis of cryptographic protocols is too large to converge,a new method is put forward to streamline the logical rules based on prior knowledge.Using equivalent logic tree theory,the rule set can be implicated and unified in initial rule iteration process,which makes the new logical rule set have the same capacity as the initial one that has not been deflated.