超长整数运算的PVS规范与验证

摘要：

超长整数的运算是现代密码系统的应用基础，运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性，利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后，给出了超长整数及其算法的形式规范，通过把算法需要满足的性质描述为定理，将算法的一致性验证问题转化为逻辑定理证明的问题，在PVS定理证明器上完成了相关定理的证明，从而表明这些算法是满足设计需求的。

关键词：超长整数运算、原型验证系统(PVS)、一致性验证、形式规范、定理证明

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家重点基础研究发展规划973No.2007CB311100；国家高技术研究发展计划863No.2009AA01Z441。

在线出版日期：2015-02-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：93-97