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

作者：周倜; 李梦君; 李舟军

来源：计算机学报, 2011, (07): 1275-1283.

• 安全协议
• 验证
• 不动点计算
• 不停机性
• 预测 security protocol
• verification
• fixpoint computation
• non-termination
• prediction

基于一般逻辑程序停机性刻画的动态方法,研究了解形式不动点不停机的一种动态刻画方法,给出了安全协议Horn逻辑扩展模型解形式不动点不停机性的一个充分条件.基于这个充分条件给出了一种不动点计算不终止的预测方法,该方法能够根据新产生的解形式逻辑规则,预测不动点计算的不终止性,同时定位模型中导致解形式不动点无穷计算的解形式逻辑规则.解形式不动点不停机性的预测结果将作为选择精确验证方法或者抽象验证方法验证安全协议的基本依据.相关实验结果表明文中给出的预测算法是高效的.

• 出版日期2011
• 单位北京航天飞行控制中心; 中国人民解放军国防科学技术大学; 北京航空航天大学