安全协议Web实施是网络空间安全的重要组成部分。目前,人们在抽象模型层面验证了安全的安全协议,在实际开发时,程序员根据抽象模型规范开发安全协议实施过程中可能会引入不易被检测到的逻辑错误和编码错误,导致安全协议的实施与其验证了安全性的抽象模型规范相差甚远。为解决该问题,必须对安全协议Web实施安全性进行分析,发现安全协议实施中是否存在安全问题。本论文利用模型抽取技术,从安全协议客户端JavaScript语言实施和Web服务器安全协议Python语言实施中抽取安全协议Applied PI演算实施,然后利用ProVerif分析其安全性。主要工作如下:(1)结合国内外关于安全协议实施安全性分析的研究情况和发展趋势讨论进行安全协议实施安全性分析的手段和方法。(2)分析安全协议JavaScript语言实施和安全协议Python语言实施的核心语句,定义JavaScript语言子集SubJavaScript和Python语言子集SubPython并分别给出SubJavaScript,SubPython和Applied PI演算的BNF表示形式BNF[SubJavaScript],BNF[SubPython]和BNF[Applied PI]。(3)根据BNF[SubJavaScript],BNF[Python]和BNF[Applied PI],分别建立SubJavaScript和SubPython到Applied PI演算的映射模型,该模型包含语句映射和类型映射模型。(4)依据SubJavaScript和SubPython到Applied PI演算的映射模型,利用JavaCC开发Applied PI演算的模型抽取工具SubJavaScript2PV和SubPython2PV,并分别从词法分析器、语法分析器、抽象语法树结构分析、遍历抽象语法树和生成Applied PI演算、模型抽取工具界面设计与功能介绍六个方面进行了详细描述。(5)利用SubJavaScript2PV和SubPython2PV分别对51 Talk、商城管理系统、盈透证券、米酷多元化互融平台、GETWELL临床科研管理项目的安全协议实施进行了安全性分析与结果讨论。结果表明51 Talk的用户登录协议中password、商城管理系统的数据传输协议中pukey-c和DESkey、盈透证券的登录协议中pwAndPhone、米酷多元化互融平台的注册协议中pwandAgainPw和GETWELL临床科研管理项目的登录协议中pw均具有机密性且安全协议实施服务器端对客户端均不具有认证性。