TMN密码协议的SMV分析

作者：邢戈; 张玉清; 冯登国

来源：计算机工程, 2005, (08): 49-51+98.

• 运行模式分析法
• TMN协议
• SMV Running-mode analysis
• TMN protocol
• Symbolic model verifier (SMV)

SMV是分析有限状态系统的一种工具,三方密码协议运行模式分析法是分析密码协议的有效方法之一。为了说明这种方法的可行性,使用三方密码协议运行模式分析法,并借助状态探测工具SMV分析了TMN密码协议,并成功地找到了对TMN协议的19种攻击。

• 单位
  中国科学院研究生院; 信息安全国家重点实验室