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

关键词: 运行模式分析法, TMN协议, SMV

Abstract: This paper proposes a method to analyze cryptographic protocols using running-mode analysis of the three-party cryptographic protocols and SMV (a tool for checking finite state systems). To prove its feasibility, an example to analyze the TMN protocol using the proposed method is also demonstrated and 19 attacks are successfully discovered.

中图分类号: 

• TN918.1