Abstract: This paper discusses the advantages and disadvantages of model checking technology and theory generation technology, and gives a specification of the new mixed technology of the two technologies which can provide a more complete formal analysis of security protocols. The technology is more efficient than former technology and can be easily realized in practices.

Key words: Security protocols, Formal analysis, Model check

摘要： 分析了模型检测技术和逻辑推证技术的优点与不足，介绍了两种形式化分析方法相结合的混合分析方法，并给出实例，证明混合分析技术在检测协议漏洞方面是更为完全的。该技术的效率大大高于一些起初的模型，且易于实现。

关键词: 安全协议, 形式化分析, 模型检测