论文部分内容阅读
描述了基于Objective Caml开发的一个安全协议验证工具SPVT（security protocol verifying tool）．在SPVT中，以扩展附加项的类被算作为安全协议描述语言，以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型，通过一组抽象规则将安全协议的类刀演算模型转换为逻辑程序模型，基于安全协议逻辑程序的不动点计算验证安全性质，从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例．以简化的Needham-Schroeder公钥认证