一种适用于嵌套加密协议分析的强认证测试方法

摘要

认证测试是一种新型的在串空间模型基础上提出来的用于分析协议认证属性的形式化方法,该方法因简单实用而受到学者的广泛关注,但其不能分析协议中认证测试组件嵌套加密的情况,这极大地限制了它的应用范围.而现存的针对该局限性的改进方案,由于没有从本质上对串空间模型中关于消息项结构关系方面的语义进行完善,很难彻底突破认证测试的局限性.为此,通过在串空间模型中引入等价类、类组件、安全加密元及安全包裹元等概念,提高了串空间刻画消息项之间及内部结构关系的能力,并结合实例来阐明引入这些概念的必要性.在此基础上,提出一种可以分析测试组件嵌套加密的通用的认证测试方法,并从形式化证明与实例分析两方面验证了新测试方法的正确性与有效性.