摘要
SMV是分析有限状态系统的一种工具,三方密码协议运行模式分析法是分析密码协议的有效方法之一。为了说明这种方法的可行性,使用三方密码协议运行模式分析法,并借助状态探测工具SMV分析了TMN密码协议,并成功地找到了对TMN协议的19种攻击。
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.
出处
《计算机工程》
EI
CAS
CSCD
北大核心
2005年第8期49-51,98,共4页
Computer Engineering
基金
国家自然科学基金资助项目(60102004
60273027
60025205)
关键词
运行模式分析法
TMN协议
SMV
Running-mode analysis
TMN protocol
Symbolic model verifier (SMV)
