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