目前安全协议的安全性仍是学术界关注的重点,但是安全协议的安全性分析仅仅停留在对安全协议抽象分析和验证方面,很难应用于日常研究中,而且在安全协议的代码实现中难免会出现一些人为漏洞,这可能会给安全协议引入更大的漏洞。安全协议代码的一般安全性(如数组下标越界、内存泄露、类型安全等),国内外学者已经做了很多有效的工作,但是关于安全协议实现代码的研究人们做的工作很少,故本文重点关注安全协议代码的密码学安全性。安全协议的最主要的安全性分析方法有两种,一种是构造攻击下的安全性分析,另外一种是模型形式化分析。本文基于安全协议的模型形式化分析方法,由代码级出发,进而研究安全协议的安全性,也就是对安全协议代码的安全性进行研究,以得到具有更强实用性的安全协议代码。针对这些问题,本文首先对概率标号迁移系统进行研究,探索提出安全协议代码的密码学安全性模型;其次探索应用概率进程演算:Blanchet演算建模安全协议抽象规范的方法,给出安全协议抽象规范建模的模版;以Blanchet演算建立的安全协议抽象规范模型为基础,研究代码转换的可行性,并建立与Java代码之间的映射关系。本文探索从安全协议抽象规范模型生成安全协议Java代码SP[Java]的方法。从进程、角色、目标多方面来建立Blanchet演算语言的映射模型,介绍转换软件的词法分析器、语法分析器、简化器、模板器的工作原理来阐述软件的开发过程。最后开发生成安全协议Java代码的自动化转换软件工具CV2JAVA。本文最后基于计算方法的自动化证明工具Crypto Verif证明SSHV2协议的抽象模型具有认证性,同时使用自动转换软件CV2JAVA对SSHV2建立的Blanchet演算模型语言进行转换,生成SSHV2的规范流程Java核心代码。SSHV2协议生成的核心代码嵌入Java环境进行验证分析,结果表明生成的安全协议代码具有SSHV2协议定义的身份认证性。