在信息化高速发展的今天,人们越来越多的使用网络来获知信息,也越来越多的将个人信息提交到网络,社交聊天工具和一些网络应用的普及使得人们越来越多的关注信息安全。安全协议是信息安全的重要组成部分,由两个及以上的参与方在进行一系列消息交换后达到某种既定目的。目前对安全协议进行形式化分析,即用形式化建模方法分析验证安全协议的安全性,包括保密性和认证性等,人们做了大量工作。但是仅仅分析安全协议抽象规范的安全是不够的,因为在安全协议具体实施的过程中可能产生新的安全问题,因此安全协议实施安全成为安全协议研究的重要组成部分。本文对安全协议实施安全进行研究,完成以下工作:(1)根据应用PI演算与Java语言的操作语义关系,给出从应用PI演算到Java语言的语法结构的映射关系;(2)提出从安全协议应用PI演算实施生成安全协议Java实施的方法。首先对应用PI演算进行词法分析和语法分析,生成其语法树;接着根据转换映射,完成应用PI演算语法树到Java语法树的转换,最终将具有安全性的应用PI演算转成Java实施;(3)开发转换工具PV2JAVA,可将安全协议应用PI演算实施转为安全协议Java实施;(4)使用应用PI演算对SAML2.0、Oauth2.0、改进的Oauth2.0、SSHV2、TLS1.2五个安全协议进行形式化建模分析,应用ProVerif工具分析这些安全协议认证性,然后使用PV2JAVA对这些安全协议的应用PI演算实施转为Java实施,调整后放入eclipse运行,分析认证性,并与ProVerif得到的认证性结果进行对比,证明转换的正确性。