论文部分内容阅读
安全协议保障信息资源在交互过程中的机密性、完整性及可用性。形式化方法规范密码协议的安全特性,拥有较完善的理论体系及模型。定理证明是形式化方法的一种,基于严格数学理论知识和逻辑推导,确定协议是否在合理假设下满足要验证的安全属性。事件逻辑理论是一种描述并发与分布式系统中状态迁移和算法的定理证明方法,可用于证明网络协议的安全性。本文运用事件逻辑理论分析无线Mesh网络客户端认证协议安全性,降低协议分析过程中的冗余度及复杂度,提高协议分析效率。论文主要工作如下:(1)基于事件逻辑理论,结合事件结构、事件类、公理簇以及随机数引理等,提出置换规则保证协议交互用户在置换中性质的等价转换,推导出多组合信息交互、不叠加、事件匹配、去重复、去未来等性质,扩展事件逻辑理论在协议分析中的应用。(2)通过事件逻辑描述客户端与LTCA间交互协议的基本序列,对协议交互动作形式化描述。证明协议强认证性质,得出无线Mesh网络客户端与LTCA间认证协议在合理假设下是安全的。表明事件逻辑理论可以对安全协议不同身份主体间的认证性进行证明。(3)在客户端用户已得到LCA颁发的认证证书条件下,通过事件逻辑理论证明无线Mesh网络客户端间认证协议安全性,得出无线Mesh网络客户端间认证协议在合理假设下是安全的。表明事件逻辑理论不仅可以证明有线网络协议安全属性,对无线网络协议的安全属性也可以论证,从而保证安全协议在信息交互过程的可靠性。(4)详述事件逻辑理论证明协议安全属性过程,通过流程图简化协议形式化证明步骤,体现事件逻辑理论的指导实用性。比较分析事件逻辑理论与其它逻辑推理方法,表明事件逻辑理论具有通用性。