REESSE1+公钥密码体制为公钥密码研究开辟了新的方向,可能成为量子计算机时代的备选加密方案之一。本文介绍了REESSE1+(2008年3月9日2.0版本)的相关内容,在此基础上研究了密码体制中密钥生成、加密和解密算法的形式化规范和验证以及根据数字签名算法敌手不可伪造签名。　　 形式化方法是基于数学的方法来描述目标软件系统属性的一种技术,它可以用来检测软件的可靠性和正确性。许多计算机科学家都认为,采用形式化方法对系统进行形式化验证和分析是构造可靠安全的软件的一个重要途径,而原型验证系统PVS(Prototype Verification System)就是著名的模型检测和自动化验证工具之一。　　 PVS为开发形式化规范和分析验证提供了一个集成化环境,它既有强有力的机器推理支持,规约语言,又有足够丰富的表达手段。本文对原型验证系统PVS做了非常全面的说明,使用PVS自动化验证工具对密码体制中密钥生成、加密和解密算法进行形式化建模和分析验证,成功证明了密码系统中的基本性质,形成了较为系统化的算法的形式化建模方法。　　 随机预言机(Random Oracle)是一个确定性的公共可访问的随机函数,分叉引理是随机预言机模型下的一种可证明安全的规约方法。本文采用分叉引理证明了根据REESSE1+数字签名算法敌手不能伪造签名。首先,文章形式地定义了数字签名的安全性,把数字签名方案的安全性归结为至少等价于离散对数的难题y≡Wδ(％M)。然后,为敌手提供一个与实际环境不可区分的模拟环境,回答敌手的oracle询问,最后,利用敌手的攻击结果解决y≡Wδ(％M)。