模型检测是通过一定的手段检测系统是否满足性质，即是否满足。密码协议模型检测分析是考虑协议的有限多种行为，检测协议是否满足一些正确条件。它更适合于发现协议的攻击，而并非去证明协议的正确性。

模型检测分析具有以下特点：

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

②在每个状态上，有某些性质被满足，这些性质描述为一个公式。

③与定理证明一样，系统要满足的性质也被刻画为逻辑公式。

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

模型检测分析系统主要包括：符号互模拟系统CCS、FDR自动验证系统和其他系统，如演算、NRL系统、项重写系统等。基于模型检测工具多达数十款，主流工具包括：ProVerif、AVISPA、Maude-NPA、Scyther等。2001年法国国家信息与自动化研究所的B.布兰切提出ProVerif。该工具基于逻辑编程语言Prolog规则和一种高效算法，可以基于一些规则推断事件是否会发生，用以实现协议机密性的验证，利用模型检测和逻辑分析相结合解决状态爆炸问题。2005年由A.Armando等人提出的AVISPA提供了模块化的形式化语言并整合了4种后台验证器：OFMC、CL-AtSe、SATMC和TA4SP。这不仅可以发现协议攻击和漏洞，还可以对协议安全性进行验证。Maude-NPA是2009年Catherine Meadows团队开发的NRL工具升级版，该工具支持多种代数性质：异或运算、加解密运算、运算结合律以及Diffie-Hellman幂运算。利用模型检测和定理证明相结合，不仅可以实现攻击和漏洞搜索，还可以实现安全性证明。Scyther是瑞士苏黎世大学Cas Cremers开发的协议形式化分析工具。该工具对于无限会话以及无限状态集合的协议可以给出明确的终止，并且支持多协议的并行分析。Scyther工具支持强安全模型，对状态集合轨迹有着明确的描述，对攻击搜索、角色的执行以及安全性证明有着巨大的帮助。

模型检测分析可以直观地发现协议漏洞，并可实现密码协议分析自动化，但由于协议的行为是潜在无限的，而模型检测的方法只能处理有限状态的系统，故而决定了该方法的不完善性，即在实际分析过程中，需要对检测的协议状态加以限制，否则会出现状态爆炸。上述工具均通过合理假设对协议状态进行合理化限制，避免了状态爆炸问题，可明确给出协议分析结果。当前模型检测分析技术发展较快，工具数量较多，算法和工具的应用、分析以及设计研究是研究者关注的焦点。