随着信息时代的发展，人们越来越关注隐私数据的保护，信息安全问题变得越来越突出。安全协议作为网络通信中保证数据安全传输的基石，其安全性与有效性成为大众关注的热点，也是安全协议研究者的研究重点。形式化方法是分析与验证安全协议的重要技术，主要包括：形式化安全协议，建立安全协议抽象模型，应用自动化分析工具验证协议的安全属性。安全协议形式化分析取得了丰硕成果，已提出了多个安全模型及发布了多种自动化分析工具。尽管安全协议的形式化分析技术能够证明安全协议的安全属性，但分析主要是建立在协议的抽象模型上，实用性差。实践表明，已被正确证明的安全协议在编码实现时会引入新的安全问题，因此分析安全协议代码的密码学安全属性不可避免。目前对安全协议代码的研究较少，模型抽取和代码生成是其中的主要技术。本文基于模型抽取技术，对安全协议的Java源码进行分析，抽取出其安全模型，并形式化为Blanchet演算代码。使用基于计算方法的自动化证明工具CryptoVerif证明该源码的认证性。主要工作如下：(1)描述了安全协议的形式化技术和安全协议代码形式化技术。重点介绍计算方法的相关理论和模型抽取技术。(2)分析安全协议的Java实现和Java的语法规范，建立安全协议实现的Java语法子集SubJ。介绍了基于计算方法的形式化语言Blanchet演算，定义SubJ与Blanchet演算间的语法映射关系。(3)基于模型抽取技术，开发模型抽取工具SubJ2CV。该工具主要对协议的ubJ代码首先进行词法分析、语法分析和生成抽象语法树，之后化简抽象语法树，抽取出安全模型。将其转换为Blanchet演算的抽象语法树，最后生成Blanchet演算代码。(4)使用SubJ2CV抽取一个认证协议Java实现代码的安全模型，将其转换为Blanchet演算代码，应用自动化分析工具CryptoVerif分析安全属性，证明协议代码的认证性。