基于模型抽取的安全协议Web实施安全性分析

发布时间：2023-10-02 05:35

　　安全协议Web实施是网络空间安全的重要组成部分。目前,人们在抽象模型层面验证了安全的安全协议,在实际开发时,程序员根据抽象模型规范开发安全协议实施过程中可能会引入不易被检测到的逻辑错误和编码错误,导致安全协议的实施与其验证了安全性的抽象模型规范相差甚远。为解决该问题,必须对安全协议Web实施安全性进行分析,发现安全协议实施中是否存在安全问题。本论文利用模型抽取技术,从安全协议客户端JavaScript语言实施和Web服务器安全协议Python语言实施中抽取安全协议Applied PI演算实施,然后利用ProVerif分析其安全性。主要工作如下:(1)结合国内外关于安全协议实施安全性分析的研究情况和发展趋势讨论进行安全协议实施安全性分析的手段和方法。(2)分析安全协议JavaScript语言实施和安全协议Python语言实施的核心语句,定义JavaScript语言子集SubJavaScript和Python语言子集SubPython并分别给出SubJavaScript,SubPython和Applied PI演算的BNF表示形式BNF[SubJavaScript],BNF[SubPyth...

【文章页数】：71 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景与意义
    1.2 国内外研究现状
    1.3 论文研究内容与目的
第二章 相关技术
    2.1 模型抽取方法
    2.2 JavaCC
    2.3 本章小结
第三章 SubJavaScript与 SubPython及 Applied PI演算
    3.1 SubPython及其BNF
    3.2 SubJavaScript及其BNF
    3.3 Applied PI演算及其BNF
    3.4 本章小结
第四章 安全协议Web实施到安全协议Applied PI演算的映射模型
    4.1 SubPython到 Applied PI演算的映射模型
        4.1.1 SubPython到 Applied PI演算的语句映射
        4.1.2 SubPython到 Applied PI演算的类型映射
    4.2 SubJavaScript到 Applied PI演算的映射模型
        4.2.1 SubJavaScript到 Applied PI演算的语句映射
        4.2.2 SubJavaScript到 Applied PI演算的类型映射
    4.3 本章小结
第五章 开发SubJavaScript2PV与 SubPython2PV
    5.1 开发SubJavaScript2PV
        5.1.1 SubJavaScript词法分析器
        5.1.2 SubJavaScript语法分析器
        5.1.3 SubJavaScript语法树分析结构图
        5.1.4 遍历SubJavaScript抽象语法树
        5.1.5 生成Applied PI演算
        5.1.6 SubJavaScript2PV界面设计与功能介绍
    5.2 开发SubPython2PV
        5.2.1 SubPython词法分析器
        5.2.2 SubPython语法分析器
        5.2.3 SubPython语法树分析结构图
        5.2.4 遍历SubPython抽象语法树
        5.2.5 生成AppliedPI演算
        5.2.6 SubPython2PV界面设计与功能介绍
    5.3 本章小结
第六章 应用案例
    6.1 51Talk项目中用户登录协议实施安全性分析
    6.2 商城管理系统中数据传输协议实施安全性分析
    6.3 其他典型安全协议实施安全性分析
    6.4 本章小结
第七章 总结与展望
    7.1 总结与讨论
    7.2 未来工作展望
参考文献
致谢
附录A 攻读学位期间成果目录



本文编号：3850198