安全协议逻辑程序不停机性快速预测的动态方法  

A Dynamic Approach on Quickly Predicting Non-Termination of Logic Program of Security Protocol

作　　者：周倜[1,2] 李梦君[1] 李舟军[3] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073 [2]北京航天飞行控制中心软件室,北京100094 [3]北京航空航天大学计算机学院,北京100083

出　　处：《计算机学报》2011年第7期1275-1283,共9页Chinese Journal of Computers

基　　金：国家自然科学基金(60973105,90604007,90104026,90718017,60703075)资助~~

摘　　要：基于一般逻辑程序停机性刻画的动态方法,研究了解形式不动点不停机的一种动态刻画方法,给出了安全协议Horn逻辑扩展模型解形式不动点不停机性的一个充分条件.基于这个充分条件给出了一种不动点计算不终止的预测方法,该方法能够根据新产生的解形式逻辑规则,预测不动点计算的不终止性,同时定位模型中导致解形式不动点无穷计算的解形式逻辑规则.解形式不动点不停机性的预测结果将作为选择精确验证方法或者抽象验证方法验证安全协议的基本依据.相关实验结果表明文中给出的预测算法是高效的.Based on the dynamic approach to characterizing termination of generic logic program,a dynamic approach to characterizing termination of solved-form fixpoint is researched in this paper,and a sufficient condition of non-termination of solved-form fixpoint of the extended Horn logic model of security protocol is presented.Based on this condition,an approach is represented to predict non-termination of computation of solved-form fixpoint.This approach can predict the non-termination of computing fixpoint by checking new generated rules,and localize the solved-form rules in the extended Horn logic model which cause infinite computations of solved-form fixpoint.The non-termination prediction results will provide the criteria for choosing different verification methods of security protocols,such as accurate methods and abstract methods.The experiment results show the effectiveness of the prediction algorithms.

关 键 词：安全协议 验证 不动点计算 不停机性 预测 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]