论文摘要
近年来,大量的安全协议形式化分析方法和自动化验证工具涌现出来,但它们大多局限于单协议验证,没有考虑复合协议的验证问题。然而,现实生活中使用的许多协议都是由多个子协议复合而成,传统的安全协议形式化分析方法难以满足其验证需求,因此,研究提出一种能够验证复合协议的安全协议形式化分析方法是十分必要和有意义的。本文通过对协议复合性的研究,针对协议复合时需要解决的问题,提出了一种复合协议验证逻辑模型,并实现了对复合协议秘密性和认证性的自动化验证,主要工作包括以下几个方面:1.研究了国内外现有的能够验证复合协议的安全协议形式化分析方法,对它们进行了分类比较,并指出了每种方法的优缺点;根据多协议环境下协议交互的特点,研究分析了复合协议验证需要解决的可复合安全问题。2.通过对协议复合性的研究,针对协议复合时需要解决的可加性结合和非破坏性结合问题,研究提出了一种复合协议验证逻辑模型,给出了协议描述、逻辑语法、逻辑语义及相应的证明系统;基于提出的复合协议验证逻辑模型,给出了单协议环境下协议秘密性和认证性的形式化定义;根据协议运行顺序,将协议复合分为并行复合和顺序复合,并给出了相应的协议复合定理,不仅可以验证并行复合协议,还可以验证顺序复合协议,将对复合协议的验证转化为对各个子协议的验证,降低了协议验证的复杂度。这部分是本文工作的重点和难点。3.在深入分析IKEv2协议的基础上,用提出的复合协议验证逻辑模型对IKEv2协议进行了具体的建模分析,首先对它的各个子协议进行了秘密性和认证性分析,然后根据子协议之间的关系,利用协议复合定理和子协议验证结果,分析了各个子协议复合后能够实现的安全属性。分析发现,单独执行时IKEv2DS子协议不满足认证性,但IKEv2DS子协议与CREATE_CHILD_SA子协议顺序复合后的协议却能够满足认证性,实现了协议复合时的可加性结合。4.基于提出的复合协议验证逻辑模型以及秘密性和认证性的形式化定义,设计并实现了秘密性和认证性验证算法,对IKEv2协议进行了自动化验证,验证结果与手工推导一致。