论文部分内容阅读
安全协议是建立在密码体制基础上的网络通信协议。形式化的分析方法是当前安全协议领域研究的热点。BAN逻辑及类BAN逻辑方法是传统的形式化分析方法，在分析协议过程中有一定的特点，也是本文提出的形式化分析方法的基础之一。但是基于BAN逻辑及类BAN逻辑的分析方法也存在一些缺陷，其中最明显的一个缺陷就是状态空间爆炸问题。
最后本文针对目前一些形式化分析方法存在的一些问题，提出了一种改进的BAN逻辑与串空间理论相结合的安全协议形式化分析方法，此方法将两种方法的优点结合，可以有效地分析协议的安全性，用改进的BAN逻辑判断消息中随机数的新鲜性，避免了状态空间爆炸问题；用串空间来分析协议的认证性。并以Needham-Scheoeder公钥协议为例说明了该方法进行协议分析的过程。另外还基于此方法设计实现了安全协议的自动化分析工具。此工具应用方便，自动化分析程度很高。