论文深入分析了TCP/IP、SPLCE/AS、IPSec等协议，分析了IKE协议的组成、IKE协商的过程、IKE消息的格式、协议安全性等。通过形式化的描述来分析协议的安全性。
通过本文对IPSec、IKE的介绍与分析，使我们对VPN的理解和实现能够达到一个更深的层次，并为进一步完善VPN提供了可能。
实践证明,安全协议形式化分析方法是一种非常有效的检验协议安全性的手段,但也有其局限性。首先对安全协议的分析或推证往往是基于某些假设,只有当假设成立时,证明才成立;而一旦某种假设不成立,一切证明也就无从谈起。另一方面,对一些关键性的假设,只要攻击者违反了它们,仍可成功入侵系统。而且,即使明确给出假设的详尽说明,但总不可避免地会遗漏一些情况,这在客观上就错漏了一些攻击的可能。其次安全性是由数据完整性、秘密性、实体识别、消息认证和可追究性等诸多特性组成,根据用户要达成的不同协议目的,一些安全特性要比另一些安全特性更重要。一个特性可能会与另一个特性发生冲突,或者满足了一个特性却使另一个特性无法满足。如在实现中,电子商务中的匿名性和可追究性就是发生冲突的两个特性。因此,没有一个安全协议是百分之百安全的,任何安全性都是有条件的, 或是基于某种假设之上的,谁也不可能对某一协议的安全性给出百分之百的证明。那种期望运用形式化分析工具,可以找出所有协议漏洞的想法是不切实际的。
就形式化分析技术自身而言,仍需从以下几方面加以提升。
1)扩展现有形式化分析工具的能力,使之不仅能分析证明一个安全协议的不安全性,还能证明协议的安全性,以及分析和评测系统的安全性;
2)为现有形式语言构造完善的数学描述,并进行严谨的理论证明,为各种协议形式化分析方法形成一个统一的形式语言表述,以描述可利用的必要信息,并使之能应用于一些新的应用协议的分析中;
3)将形式化方法应用于协议说明与协议设计阶段,使之不仅仅用于分析具体的某个安全协议的安全性,而且可以极小的代价尽可能早地发现错误;
4)Strandspace模型是一种有着广阔应用前景的方法,有待于进一步研究。其研究 方向包括:在 Strandspace理论基础上,提出一种支持自动推理或模型检测的、具有丰富表达能力的,并且可以自然容纳群协议的形式模型;研究改进的模型的形式推理或检测的相关技术;发展改进的模型的形式推理或检测的自动工具;研究改进的模型在具体协议中的应用,特别是在大型实用协议中的分析研究。此外,如何把分析小系统协议的思想与方法扩充到大系统协议;如何扩充已较成熟的理论或方法,去研究更多的安全性质,使同一系统中安全性质在统一的框架下进行验证,而不是同一系统中不同安全性质采用不同系统进行验证。这些都是值得进一步研究的问题。
