计算机科学 ›› 2020, Vol. 47 ›› Issue (12): 311-318.doi: 10.11896/jsjkx.190900197
范永乾, 陈钢, 崔敏
FAN Yong-qian, CHEN Gang, CUI Min
摘要： 有限域GF(2n)是多种安全关键性算法的基础包括AES加密算法、椭圆曲线加密和感染函数掩码等.相关资料表明有限域上的运算因为自身的复杂性而容易出错从而导致系统问题.基于测试和基于模型检测的验证方法只能在n固定的特定有限域上进行验证而且计算量往往超出计算机的能力.基于交互式定理证明器的形式化验证为有限域性质的通用验证提供了可能性但这方面的工作难度较大.已有研究主要针对有限域的抽象性质进行形式化验证但计算机领域更关心的是有限域的构造性定义及相关性质的验证.针对这些问题借助定理证明器COQ建立了有限域GF(2n)并给出了其基本运算的构造性定义同时对一组与有限域有关的基本性质进行了形式化验证包括有限域加法基本性质的验证、多项式乘法基本性质的验证等其中多项式乘法是有限域乘法的基础.这项工作为有限域的完整的形式化及基于有限域的算法的形式化验证奠定了基础.
中图分类号:
| [1] MCELIECE R J.Finite fields for computer scientists and engineers[M].Springer Science &Business Media,2012. [2] DAEMEN J,RIJMEN V.The design of Rijndael:AES-the advanced encryption standard[M].Springer Science &Business Media,2013. [3] HANKERSON D,MENEZES A J,VANSTONE S.Guide to elliptic curve cryptography[M].Springer Science &Business Media,2006. [4] OSHIDA H,UENO R,HOMMA N,et al.On Masked Galois-Field Multiplication for Authenticated Encryption Resistant to Side Channel Analysis[C]//International Workshop on Constructive Side-Channel Analysis and Secure Design.Cham:Springer,2018:44-57. [5] PHILIPOOM J.Correct-by-construction finite field arithmetic in Coq[D].Cambridge:Massachusetts Institute of Technology ,2018. [6] INRIA.Coq Ring Theory[DB/OL].[2019-09-02].https://coq.inria.fr/distrib/current/stdlib/Coq.setoid_ring.Ring_theory.html. [7] INRIA.Coq Field Theory[DB/OL].[2019-09-02].https://coq.inria.fr/distrib/current/stdlib/Coq.setoid_ring.Field_theory.html. [8] GONTHIER G,MAHBOUBI A,RIDEAU L,et al.A modular formalisation of finite group theory[C]//International Confe-rence on Theorem Proving in Higher Order Logics.Berlin:Springer,2007:86-101. [9] YU C,CIESIELSKI M.Formal Analysis of Galois Field Arithmetic Circuits-Parallel Verification and Reverse Engineering[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2018,38(2):354-365. [10] YU C,CIESIELSKI M.Efficient parallel verification of galois field multipliers[C]//2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC).IEEE,2017:238-243. [11] PAAR C,FLEISCHMANN P,ROELSE P.Efficient multiplier architectures for Galois fields GF (2/sup 4n/)[J].IEEE Transactions on Computers,1998,47(2):162-170. [12] LV J,KALLA P,ENESCU F.Verification of composite Galois field multipliers over GF ((2m)n) using computer algebra techniques[C]//2011 IEEE International High Level Design Validation and Test Workshop.IEEE,2011:136-143. [13] TEAM T C D.The Coq Proof Assistant Reference Manual-Version V8.7.1[C]//INRIA.2016. [14] BERTOT Y,CASTÉRAN P.Interactive theorem proving and program development:Coq'Art:the calculus of inductive constructions[M].Springer Science &Business Media,2013. [15] ANDRONICK J,CHETALI B,LY O.Using coq to verify java card tm applet isolation properties[C]//International Conference on Theorem Proving in Higher Order Logics.Berlin:Springer,2003:335-351. [16] GONTHIER G.Formal proof-the four-color theorem[J].Notices of the AMS,2008,55(11):1382-1393. [17] BLANQUI F,COUPET-GRIMAL S,DELOBEL W,et al.CoLoR:a Coq Library on Rewriting and termination[C]//Eighth International Workshop on Termination (WST2006).Seattle,United States,2006. [18] OKAZAKI H,ARAI K,SHIDAMA Y.Formal Verification of AES Using the Mizar Proof Checker[C]//Proceedings of the 2012 International Conference on Foundations of Computer Science (FCS'12).2012:78-84. [19] ARAI K,OKAZAKI H.Formalization of the Advanced Encryption Standard.Part I[J].Formalized Mathematics,2013,21(3):171-184. [20] LIDL R,NIEDERREITER H.Finite fields[M].Cambridge:Cambridge University Press,1997. [21] COLLINS G E.Computing multiplicative inverses in GF(p)[J].Mathematics of Computation,1969,23(105):197-200. [22] ILIEV A,KYURKCHIEV N,RAHNEV A.A Note on Adaptation of the Knuth's Extended Euclidean Algorithm for Computing Multiplicative Inverse[J].International Journal of Pure and Applied Mathematics,2018,118(2):281-290. [23] WIKIPEDIA.Rijndael MixColumns[DB/OL].[2019-04-17].https://en.wikipedia.org/wiki/Rijndael_MixColumns. |
| [1] | 蹇奇芮, 陈泽茂, 武晓康. 面向无人机通信的认证和密钥协商协议 Authentication and Key Agreement Protocol for UAV Communication 计算机科学, 2022, 49(8): 306-313. https://doi.org/10.11896/jsjkx.220200098 |
| [2] | 孙小祥, 陈哲. 基于定理证明的内存安全性动态检测算法的正确性研究 Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving 计算机科学, 2021, 48(1): 268-272. https://doi.org/10.11896/jsjkx.200100097 |
| [3] | 杨萍, 王生原. CompCert编译器目标代码生成机制分析 Analysis of Target Code Generation Mechanism of CompCert Compiler 计算机科学, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018 |
| [4] | 李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design 计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173 |
| [5] | 马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022 |
| [6] | 陈昊,罗蕾,李允,陈丽蓉. 安全虚拟机监视器的形式化验证研究 Study on Formal Verification of Secure Virtual Machine Monitor 计算机科学, 2019, 46(3): 170-179. https://doi.org/10.11896/j.issn.1002-137X.2019.03.026 |
| [7] | 魏万银,杜小妮,李芝霞,万韫琦. 周期为pq的四元广义分圆序列的线性复杂度 Linear Complexity of Quaternary Generalized Cyclotomic Sequences with Period pq 计算机科学, 2017, 44(6): 174-176. https://doi.org/10.11896/j.issn.1002-137X.2017.06.029 |
| [8] | 魏晴,孙光洪. 一类有限域上的置换多项式 Class of Permutation Polynomials over Finite Fields 计算机科学, 2017, 44(5): 170-171. https://doi.org/10.11896/j.issn.1002-137X.2017.05.030 |
| [9] | 祝现威,朱智强,孙磊. Xen混合多策略模型的设计与形式化验证 Design and Formal Verification of Xen Hybrid Multi-police Model 计算机科学, 2017, 44(10): 134-141. https://doi.org/10.11896/j.issn.1002-137X.2017.10.026 |
| [10] | 李姗姗,赵春娜,关永,施智平,王瑞,李晓娟,叶世伟. 分数阶微积分定义的一致性在HOL4中的验证 Formalization of Consistency of Fractional Calculus in HOL4 计算机科学, 2016, 43(3): 23-26. https://doi.org/10.11896/j.issn.1002-137X.2016.03.004 |
| [11] | 李艳春,李晓娟,关永,王瑞,张杰,魏洪兴. 基于xMAS模型的SpaceWire信誉逻辑的形式化验证 xMAS-based Formal Verification of SpaceWire Credit Logic 计算机科学, 2016, 43(2): 113-117. https://doi.org/10.11896/j.issn.1002-137X.2016.02.026 |
| [12] | 杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰. 函数矩阵及其微积分的高阶逻辑形式化 Higher-order Logic Formalization of Function Matrix and its Calculus 计算机科学, 2016, 43(11): 24-29. https://doi.org/10.11896/j.issn.1002-137X.2016.11.005 |
| [13] | 陈丽蓉,李允,罗蕾. 嵌入式操作系统的形式化验证研究 Research on Formal Verification of Embedded Operating System 计算机科学, 2015, 42(8): 203-214. |
| [14] | 吕兴利,施智平,李晓娟,关 永,叶世伟,张 杰. 连续傅里叶变换基础理论的高阶逻辑形式化 Higher-order Logic Formalization of Basic Theory of Continuous Fourier Transform 计算机科学, 2015, 42(4): 31-36. https://doi.org/10.11896/j.issn.1002-137X.2015.04.004 |
| [15] | 欧阳显斌,邵利平. 一种基于GF(23)的(K,N)有意义无扩张图像分存方案 Meaningful (K,N) Free Expansion Image Sharing Scheme Based on GF(23) 计算机科学, 2015, 42(12): 251-256. |
|
||
首页