论文研究-超长整数运算的PVS规范与验证.pdf
需积分: 9 96 浏览量
2019-09-10
15:52:07
上传
评论
收藏 489KB PDF 举报
2015，51（3）
1 引言
为了抵御攻击者计算能力的不断提高，公钥密码体
制
[1]
往往通过增加模数的长度来增大攻击者攻击的难
度，从而保障密码体制在实际应用中的安全性。例如，
为了保证足够的安全性，RSA 公钥密码体制
[2]
模数的长
度已经增加到至少 1 024 比特，REESSE1+公钥密码体
制
[3]
的模长至少是 696 比特，ECC 体制
[4]
的模长最少为
160 比特。这些大整数的长度远远超出了现有程序语言
及其编译器的处理能力，因此，设计超长整数运算的算
法，是这些公钥密码体制应用的基础。
在设计 REESSE1+公钥密码系统的过程中，针对超
长整数的运算设计了相关的算法
[5]
。这些算法是否实现
了需求分析的目标需要验证，同时，设计的算法正确与
否直接影响到后面程序实现的正确性。传统的验证方
法是在程序中输入数据进行测试，这样只能保证算法对
某些输入数据是正确的，运用形式化方法
[6]
对这些算法
的设计和需求目标之间的一致性进行验证，从而保证算
法设计的正确性，同时，也能保障 REESSE1+公钥密码
系统的应用价值。
本文利用原型验证系统 PVS
[7]
对超长整数及其加减
法进行了形式规范，并且完成了加法和减法算法的一致
性验证。
超长整数运算的 PVS 规范与验证
孙国栋，牛晋刚
SUN Guod ong, NIU Jingang
北京工业大学 计算机学院，北京 100124
College of Computer Science, Beijing University of Technology, Beijing 10 0124, China
SUN Guodong, NI U Jingang. Formal specification and verificati on of operation of super long integers using PVS.
Computer Engineering and Applications, 2015, 51（3）：93-97.
Abstract：The operation of super long integers is the basic component of the application of moder n cryptosystem, and its
correctness re lates to the application value of the system. In order to verify the consistence between the r equirement 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 d esign idea o f these algo rithms, presents
the formal specification of s uper long integers and the algorithms. Then by descr ibing the property of the algorithms as
theorems, the consistency c hecking is converted to a problem of theorem proving. These property theore ms are p roved
with the theorem prover of PVS, so the desi gn requirements of these algorithms are sati sfied .
Key words：operation of super long i ntegers; Prototype Verification System（PVS）; consistency verification; formal spec-
ification; theorem proving
摘 要：超长整数的运算是现代密码系统的应用基础，运算的正确性关系到密码系统的应用价值。为了验证超长整
数算法的设计与需求目标之间的一致性，利用原型验证工具 PVS 对算法的正确性进行了证明。在介绍了超长整数
的加法和减法算法并分析了其设计思想之后，给出了超长整数及其算法的形式规范，通过把算法需要满足的性质描
述为定理，将算法的一致性验证问题转化为逻辑定理证明的问题，在 PVS 定理证明器上完成了相关定理的证明，从
而表明这些算法是满足设计需求的。
关键词：超长整数运算；原型验证系统（PVS）；一致性验证；形式规范；定理证明
文献标志码：A 中图分类号：TP311.5 doi：10.3778/j. issn.1002-8331.1402-0408
基金项目：国家重点基础研究发展规划（973）（No.2007CB311100）；国家高技术研究发展计划（863）（No.2009AA01Z441）。
作者简 介：孙国 栋（1985—），男，博 士研 究生，CC F 学生会 员，主要研 究领域 为信息 安全、公钥密 码学和 形式化 方法；牛晋刚
（1984—），男，硕士，主要研究领域为公钥密码学和形式化方法。E-mail：sgd-150@163.com
收稿日期：2014-0 3-03 修回日期：2014-0 6-10 文章编号：1002-8 331（2015）03-00 93-05
CNKI 网络优先出版：2014-07-11，http://www.cnki.net/kcms/doi/10.3778/j.issn.1002-8331.1402-0408.html
C omputer Engineering and Applications 计算机工程与应用
93
资源评论
weixin_38744270
- 粉丝: 327
- 资源: 2万+
