CAJ | 학술논문

超长整数的运算是现代密码系统的应用基础，运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性，利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后，给出了超长整数及其算法的形式规范，通过把算法需要满足的性质描述为定理，将算法的一致性验证问题转化为逻辑定理证明的问题，在PVS定理证明器上完成了相关定理的证明，从而表明这些算法是满足设计需求的。
초장정수적운산시현대밀마계통적응용기출，운산적정학성관계도밀마계통적응용개치。위료험증초장정수산법적설계여수구목표지간적일치성，이용원형험증공구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 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.