基于Horn逻辑扩展模型的安全协议反例的自动构造

根据安全协议的Horn逻辑扩展模型和相应的安全协议验证方法,提出了自动构造不满足安全性质的安全协议反例的求解策略,并给出了重要定理的证明,设计了一系列自动构造协议攻击的构造算法,并在基于函数式编程语言Objective Caml开发的安全协议验证工具SPVT中实现了这些算法,给出了主要算法的优化方法,详细分析了主要算法的时间复杂度,从理论上证明了算法是线性时间算法.最后,用SPVT对一些典型的安全协议进行了验证,得到了不安全协议的反例,并对反例进行了分析.得到的反例非常方便于阅读,与Alice-Bob标记非常接近,从而使任何领域的专家都可以用这种形式化的方法检查安全协议是否存在真实的反例.

Automatically Constructing Counter-Examples of Security Protocols Based on the Extended Horn Logic Model

It is very important to construct counter-examples of security protocols automatically,but there are few methods to do this work.Based on the extended Horn logic model and the corresponding verification method of security protocols,the solution strategies are presented,which are used to construct automatically intuitionistic counter-examples in protocols which break the security properties.Some important theorems are proved to make sure the correctness of these solution strategies.Based on this model,a series of algorithms are designed to construct counter-examples of security protocols automatically,the optimal methods of some main algorithms are given,and their complexities are analyzed in detail.These algorithms are implemented in the verifier SPVT which is developed in the functional programming language Objective Caml.The time complexities of these algorithms are proved to be linear theoretically.Finally,some classical security protocols are verified by SPVT which presents counter-examples automatically.Those results are also discussed and some counter-examples are analyzed.The results of experiments also show that these algortithms are linear.As the form of counter-examples is very similar to Alice-Bob notations,it is very convenient to read.Therefore,this formal method can be used by experts in all fields to check if there is a real counter-example in security protocols.