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

Formal specification and verification of operation of super long integers using PVS

作　　者：孙国栋[1] 牛晋刚[1] 

机构地区：[1]北京工业大学计算机学院,北京100124

出　　处：《计算机工程与应用》2015年第3期93-97,共5页Computer Engineering and Applications

基　　金：国家重点基础研究发展规划(973)(No.2007CB311100);国家高技术研究发展计划(863)(No.2009AA01Z441)

摘　　要：超长整数的运算是现代密码系统的应用基础,运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性,利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后,给出了超长整数及其算法的形式规范,通过把算法需要满足的性质描述为定理,将算法的一致性验证问题转化为逻辑定理证明的问题,在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 introduces 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) 一致性验证 形式规范 定理证明 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]