基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析

发布时间：2021-03-29 16:02

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

【文章来源】：华东交通大学江西省

【文章页数】：57 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
符号说明
第一章 绪论
    1.1 研究背景及意义
    1.2 发展历史及研究现状
    1.3 本文主要内容
    1.4 论文结构安排
第二章 无线Mesh网络协议及形式化方法概述
    2.1 无线Mesh网络
        2.1.1 无线Mesh网络概述
        2.1.2 无线Mesh网络的安全威胁
        2.1.3 无线Mesh网络认证协议的安全需求
    2.2 无线Mesh网络客户端协议分析
        2.2.1 WMN客户端与LTCA间认证协议
        2.2.2 WMN客户端间认证协议
    2.3 形式化方法概述
        2.3.1 模型检测
        2.3.2 定理证明
第三章 事件逻辑理论
    3.1 事件逻辑理论
        3.1.1 基本定义
        3.1.2 加密系统建模
    3.2 事件逻辑理论公理、推论及性质
        3.2.1 事件逻辑理论公理
        3.2.2 事件逻辑理论推论及性质
    3.3 形式化方法描述协议
        3.3.1 线程和基本序列
        3.3.2 匹配会话及协议动作
        3.3.3 事件逻辑方法描述协议
    3.4 安全协议证明过程
        3.4.1 事件逻辑理论方法证明流程详述
        3.4.2 事件逻辑理论方法证明流程
    3.5 本章小结
第四章 无线Mesh网协议形式化分析
    4.1 WMN客户端与LTCA间双向认证协议证明
        4.1.1 协议的形式化分析
        4.1.2 协议证明过程
    4.2 WMN客户端间双向协议认证性证明
        4.2.1 协议的形式化分析
        4.2.2 协议证明过程
    4.3 本章小结
第五章 形式化方法对比分析
    5.1 事件逻辑理论与模态逻辑比较
    5.2 事件逻辑理论与PCL比较
    5.3 事件逻辑理论通用性
第六章 总结与展望
    6.1 总结
    6.2 展望
参考文献
个人简历在读期间发表的学术论文
致谢



本文编号：3107803