模型检测考虑的是协议的有限多种行为，检测它们满足一些正确条件，它更适合于去发现协议的攻击，而并非去证明协议的正确性。

模型检测有以下特点。

（1）关于协议操作行为的有限状态系统被刻画为有限状态迁移系统。这个系统的状态通过与环境的交互，满足一定条件就迁移到另一个状态。这些条件被标记到迁移的边上，这个系统称为标记迁移系统（Labelled Transitive System，LTS）。

（2）在每一个状态上，有某些性质被满足，这些性质描述为一个（古典逻辑或者时态等逻辑）公式。

（3）与定理证明一样，系统要满足的性质也被刻画为逻辑公式。(www.daowen.com)

（4）用自动机械的手段检测上述的性质是否在系统的每个轨迹上都被满足，这里的轨迹是指系统的一个可能迁移路径。

形式上说，假如一个系统为S，期望的系统性质表达为逻辑公式φ，那么模型检测就是验证S是否满足φ，通常在这个模型论中表示为S|=φ。

模型检测的方法完全是自动化的，这是这个方法的优点。但是，因为协议的行为是潜在无限的，而模型检测的方法只能够处理有限状态的系统，所以决定了这个方法的不完善性，即在实际应用过程中，一定要对检测的范围加以限制。同时，这个方法的另一个缺点在于，尽管人们已经探索了20余年，但是状态爆炸问题还是没有得到解决方法，因而对于复杂的系统，难以用模型检测的方法分析。更为实质性的一点是，常用的协议是不可判定的。这就决定了没有一个算法系统能够搜索协议所有可能的行为。

总之，这个方法注定是一个不完全的方法，其优点在于可以直观地发现协议的漏洞，然而如果没有发现协议存在漏洞，也不能保证协议就是正确的。