基于COQ的有限域GF(2n)的形式化研究

摘要：

有限域GF(2n)是多种安全关键性算法的基础,包括 AES加密算法、椭圆曲线加密和感染函数掩码等.相关资料表明,有限域上的运算因为自身的复杂性而容易出错,从而导致系统问题.基于测试和基于模型检测的验证方法只能在n固定的特定有限域上进行验证,而且计算量往往超出计算机的能力.基于交互式定理证明器的形式化验证为有限域性质的通用验证提供了可能性,但这方面的工作难度较大.已有研究主要针对有限域的抽象性质进行形式化验证,但计算机领域更关心的是有限域的构造性定义及相关性质的验证.针对这些问题,借助定理证明器COQ,建立了有限域GF (2 n )并给出了其基本运算的构造性定义,同时对一组与有限域有关的基本性质进行了形式化验证,包括有限域加法基本性质的验证、多项式乘法基本性质的验证等,其中多项式乘法是有限域乘法的基础.这项工作为有限域的完整的形式化及基于有限域的算法的形式化验证奠定了基础.

关键词：有限域、COQ、形式化验证、定理证明、多项式运算

所属期刊栏目：47

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

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

页数：共8页

页码：311-318