模型检测分析（model detection analysis），理学-计算机科学技术-信息安全-密码学-密码协议-密码协议分析，利用模型检测技术分析密码协议安全性的方法。模型检测是通过一定的手段检测系统是否满足性质，即是否满足。密码协议模型检测分析是考虑协议的有限多种行为，检测协议是否满足一些正确条件。它更适合于发现协议的攻击，而并非去证明协议的正确性。模型检测分析具有以下特点：①密码协议操作行为的有限状态系统，被刻画为有限状态迁移系统。这个系统的状态通过与环境的交互，满足一定条件就迁移到另一个状态，这些条件被标记到迁移的边上，这个系统成为标记迁移系统（LTS）。②在每个状态上，有某些性质被满足，这些性质描述为一个公式。③与定理证明一样，系统要满足的性质也被刻画为逻辑公式。④用自动机械检测上述性质是否在系统每个轨迹上都被满足，这里的轨迹是指系统的一个可能迁移路径。模型检测分析系统主要包括：符号互模拟系统CCS、FDR自动验证系统和其他系统，如演算、NRL系统、项重写系统等。基于模型检测工具多达数十款，主流工具包括：ProVerif、AVISPA、Maude-NPA、Scyther等。