论文以链空间模型作为研究的起点.首先,该模型是一种代数方法,以极小元等理论为基础,可以给出可信度较高的证明;其次,该模型不是验证协议,而是试图证明协议的安全性.第三,该模型简单、易用,可以手工的方式完全证明,而且图形表示使其证明更加直观;第四,关于该模型有许多相关的研究工作,这为进一步工作打下了良好的基础.通过对原模型的扩充和完善,得到增强型链空间模型.与原模型相比,新模型具有更强的描述能力,可以证明更多的协议,发现更多的问题.关于机密性,论文首先描述了增强型链空间模型的代数基础,并给出了分析所依赖的消息代数的特征结构.新模型中增加了两个算子,一个表示散列操作,另一个表示密钥生成操作,用公理描述这两个操作与加密和连接操作的关系.接着,将入侵者的知识集看作是消息代数的子集,根据集合中数据之间的关系定义保护链,用保护链来描述数据项之间的保护关系.关于认证性,新模型中增加了对散列函数的描述,使得其可以分析包含散列操作的协议.最后,文章利用增强型链空间模型分析了目前较为流行的IKE(Internet Key Exchange)协议,并给出了较为详细、系统的结果.IKE是IPSes(Internet Protocol Security)的基础,而IPSes是实现VPN(Virtual Private Network)的重要技术之一,有着广泛的应用前景.论文根据文档的描述,经过一定抽象后给出了协议的形式化描述.以这些形式化抽象为基础,着重分析了IKE协议的机密性和认证性,并发现了一些问题.因为IKE协议本身由多个子协议组成,所以在分析时还考虑了子协议之间是否会相互影响的问题.