论文部分内容阅读
安全协议的安全性是网络安全的重要基础，运用形式化方法分析安全协议的安全性已成为目前研究的主要热点。本文主要研究运用形式化技术分析安全协议的理论与技术，对基于模型检测技术的运行模式分析法进行深入的研究，并把其应用到实用安全协议的分析与设计中去。主要的研究成果如下： (1) 对安全协议的背景及基本概念、安全协议的形式化分析方法的三种思路进行了系统的介绍； (2) 介绍两方安全协议的运行模式分析法，对只包括一个可信第三方服务器的协议的运行模式分析法进行归纳，提出多于一个可信第三方服务器协议的运行模式分析法； (3) 计算运行模式的数量上界，并给出有效的约束条件，构造与具体模型检测工具相独立的运行模式组合集，进一步提出了多方安全协议的运行模式分析法； (4) 使用运行模式分析法成功分析了实用的安全协议，如SSL3.0、TMN、Kerberos等协议，得到了较好的结论； (5) 根据协议的安全缺陷提出了安全协议的设计原则，并设计了一个安全的密钥建立协议； (6) 总结模型检测法，并与其他经典形式化分析方法进行了详细的比较。