论文部分内容阅读
本论文主要研究了密码协议的形式分析方法，作者所取得的主要研究结果如下：（1）研究了BAN逻辑在初始假设、理想化步骤、语义、探测对协议的攻击等方面所存在的缺陷；（2）首次采用模型检测工具SMV对密码协议进行分析，并给出了具体分析的方法，实践表明我们运用SMV对密码钥协议分析的方法是有效和成功的；（3）分析了Helsinki密码协议，并提出了一种更安全的Helsinki密码协议；（4）对TMN密码协议进行了有效的分析，并成功地找到了以往形式分析所没有发现过的新的一类攻击；（5）提出了一种针对两者密码协议的运行模式分析法，这是一种独立于任何模型检测工具的通用方法；（6）用运行模式分析法研究和分析了TW密码协议，分析结果表明运行模式分析法是有效和成功的；（7）建立了通用的两者密码协议的SMV分析程序框架。