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

摘要

The operation of super long integers is the basic component of the application of modern cryptosystem, and its correctness relates to the application value of the system. In order to verify the consistence between the requirement analysis and the design goal of these algorithms, the correctness of the algorithms are formally verified using PVS. This paper intro-duces the addition and subtraction algorithms for super long integers and analyses the design idea of these algorithms, presents the formal specification of super long integers and the algorithms. Then by describing the property of the algorithms as theorems, the consistency checking is converted to a problem of theorem proving. These property theorems are proved with the theorem prover of PVS, so the design requirements of these algorithms are satisfied.%超长整数的运算是现代密码系统的应用基础，运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性，利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后，给出了超长整数及其算法的形式规范，通过把算法需要满足的性质描述为定理，将算法的一致性验证问题转化为逻辑定理证明的问题，在PVS定理证明器上完成了相关定理的证明，从而表明这些算法是满足设计需求的。