基于Prolog的安全协议在线自动化分析

作者：陈铁明; 张杰; 蔡家楣

来源：计算机应用研究, 2008, (08): 2447-2449.

• 形式化
• 串空间
• 参数串
• 约束消减
• Prolog formal method
• strand space
• parametric strand
• constraint elimination
• Prolog

基于串空间理论和约束消减方法,提出安全协议可达性分析模型;采用Prolog实现模型自动推理,利用XSB的Java接口实现基于Web的自动分析工具。

• 单位
  浙江工业大学; 软件开发环境国家重点实验室; 北京航空航天大学