基于UPPAAL的NS密码协议模型检测分析

形式化分析方法是目前密码协议分析的主流方法。然而，典型的密码协议形式化验证方法没有考虑时间因素，这个选择使得分析简单化。本文提出了运用基于时间自动机的模型检测工具UPPAAL分析密码协议的方法，并对著名的Needham-Schroeder协议（简称NS协议）的简单版本进行了分析。在对NS协议进行建模时，考虑消息实际传输需花费时间，引入消息的时间信息，从而构建NS协议的时间自动机模型。该方法利用UPPAAL的检查引擎所用的先进技术使其克服了一般时间自动机应用存在的状态空间爆炸问题。实验结果UPPAAL给出了NS协议认证失败的一种可能之一。分析结果表明，入侵者可以轻松地对NS公钥协议进行有效攻击。从而证明UPPAAL工具可以成功检测出NS协议的缺陷。